Upgrade to mathlib 4.30 and fix Navier-Stokes target

Problems/BirchSwinnertonDyer/Millennium.lean

@@ -133,7 +133,7 @@ theorem localEulerFactor_aeval_eq_clay
   have hΔ' : (W.baseChange (ZMod (p : ℕ))).Δ ≠ 0 := by
     simpa [WeierstrassCurve.baseChange, WeierstrassCurve.map_Δ] using hΔmod
   have hIsUnit : IsUnit (W.baseChange (ZMod (p : ℕ))).Δ := by
-    simpa [isUnit_iff_ne_zero, hΔ']
+    simp [isUnit_iff_ne_zero, hΔ']
   letI : (W.baseChange (ZMod (p : ℕ))).IsElliptic := ⟨hIsUnit⟩
   have hEll : (W.baseChange (ZMod (p : ℕ))).IsElliptic := by infer_instance
   have hap :

Problems/Hodge/Millennium.lean

@@ -4,7 +4,7 @@ namespace MillenniumHodge
 
 open AlgebraicGeometry Scheme Complex Algebra VarietyDefinition
 
-universe u u₁ u₂ u₃
+universe u₁ u₂ u₃
 
 /-!
 # The Hodge Conjecture
@@ -67,7 +67,7 @@ The Hodge Conjecture: for a smooth complex projective variety,
 every Hodge class is a rational linear combination of cycle classes.
 -/
 def HodgeConjecture : Prop :=
-  ∀ (X : SmoothProjectiveVariety.{0, u} ℂ) (p : ℕ) (data : HodgeData.{u₁, u₂, u₃, u} X),
+  ∀ (X : SmoothProjectiveVariety ℂ) (p : ℕ) (data : HodgeData.{u₁, u₂, u₃} X),
     data.hodgeClass p ≤ data.algebraicCohomology p
 
 end MillenniumHodge

Problems/Hodge/Variety.lean

@@ -127,7 +127,7 @@ theorem hodgeSubspace_le_hodgeFiltration (data : HodgeData X) (n p a : ℕ) (ha
 The `ℚ`-subspace of Hodge classes in degree `2p` (Clay PDF, Section 1):
 rational classes whose complexification lies in `H^{p,p}(X)`.
 -/
-def hodgeClass (data : HodgeData X) (p : ℕ) : Submodule ℚ (data.cohomologyQ (2 * p)) :=
+noncomputable def hodgeClass (data : HodgeData X) (p : ℕ) : Submodule ℚ (data.cohomologyQ (2 * p)) :=
   Submodule.comap (data.extensionOfScalarsQC (2 * p))
     ((data.hodgeSubspace (2 * p) p p).restrictScalars ℚ)
 
@@ -144,7 +144,7 @@ The Clay PDF notes that, for projective non-singular varieties,
 In this repository we define `hodgeClass` using the `(p,p)`-summand, and also provide this
 filtration-based variant.
 -/
-def hodgeClassFiltration (data : HodgeData X) (p : ℕ) : Submodule ℚ (data.cohomologyQ (2 * p)) :=
+noncomputable def hodgeClassFiltration (data : HodgeData X) (p : ℕ) : Submodule ℚ (data.cohomologyQ (2 * p)) :=
   Submodule.comap (data.extensionOfScalarsQC (2 * p))
     ((data.hodgeFiltration (2 * p) p).restrictScalars ℚ)
 

Problems/NavierStokes/AdjointSpace.lean

@@ -160,7 +160,7 @@ theorem inner_self_nonpos {x : E} : re ⟪x, x⟫ ≤ 0 ↔ x = 0 := by
   constructor
   · have ⟨c,d,hc,_,h⟩ := inner_top_equiv_norm (𝕜:=𝕜) (E:=E)
     have ⟨h,_⟩ := h x
-    intro h'; simp[h'] at h
+    intro h'; simp at h
     have : ‖x‖^2 ≤ 0 := by nlinarith
     have : ‖x‖ ≤ 0 := by nlinarith
     simp_all only [gt_iff_lt, smul_eq_mul, norm_le_zero_iff]
@@ -297,10 +297,10 @@ instance : AdjointSpace 𝕜 𝕜 where
   conj_symm := by simp[mul_comm]
   add_left := by
     intro x y z
-    simp [mul_add, add_mul, mul_assoc]
+    simp [mul_add]
   smul_left := by
     intro x y r
-    simp [mul_assoc, mul_left_comm, mul_comm]
+    simp [mul_left_comm, mul_comm]
 
 /-- The unit type carries the trivial inner product. -/
 instance : Inner 𝕜 Unit where
@@ -349,7 +349,7 @@ instance : AdjointSpace 𝕜 (X×Y) where
       -- Split on which component attains the max norm on the product.
       by_cases hxy : ‖x‖ ≤ ‖y‖
       · have hnorm : ‖(x, y)‖ = ‖y‖ := by
-          simpa [Prod.norm_mk, max_eq_right hxy]
+          simp [Prod.norm_mk, max_eq_right hxy]
         have hmin_le : min cx cy ≤ cy := min_le_right _ _
         have hmul : (min cx cy) * ‖(x, y)‖ ^ 2 ≤ cy * ‖y‖ ^ 2 := by
           have hy_sq : 0 ≤ (‖y‖ ^ 2 : ℝ) := by
@@ -361,7 +361,7 @@ instance : AdjointSpace 𝕜 (X×Y) where
         simpa [inner, map_add, hnorm] using hle'
       · have hyx : ‖y‖ ≤ ‖x‖ := le_of_not_ge hxy
         have hnorm : ‖(x, y)‖ = ‖x‖ := by
-          simpa [Prod.norm_mk, max_eq_left hyx]
+          simp [Prod.norm_mk, max_eq_left hyx]
         have hmin_le : min cx cy ≤ cx := min_le_left _ _
         have hmul : (min cx cy) * ‖(x, y)‖ ^ 2 ≤ cx * ‖x‖ ^ 2 := by
           have hx_sq : 0 ≤ (‖x‖ ^ 2 : ℝ) := by
@@ -373,9 +373,9 @@ instance : AdjointSpace 𝕜 (X×Y) where
         simpa [inner, map_add, hnorm] using hle'
     · -- upper bound
       have hnorm_x : ‖x‖ ≤ ‖(x, y)‖ := by
-        simpa [Prod.norm_mk] using le_max_left ‖x‖ ‖y‖
+        simp [Prod.norm_mk]
       have hnorm_y : ‖y‖ ≤ ‖(x, y)‖ := by
-        simpa [Prod.norm_mk] using le_max_right ‖x‖ ‖y‖
+        simp [Prod.norm_mk]
       have hx_sq : ‖x‖ ^ 2 ≤ ‖(x, y)‖ ^ 2 := by
         simpa [pow_two] using
           mul_le_mul hnorm_x hnorm_x (norm_nonneg x) (norm_nonneg (x, y))
@@ -491,7 +491,7 @@ instance : AdjointSpace 𝕜 ((i : ι) → E i) where
           -- Rewrite `re (inner x x)` as a sum of real parts.
           have hre :
               re (∑ i : ι, ⟪x i, x i⟫_𝕜) = ∑ i : ι, re ⟪x i, x i⟫_𝕜 := by
-            simpa using (map_sum (RCLike.re : 𝕜 →+ ℝ) (fun i : ι => ⟪x i, x i⟫_𝕜) Finset.univ)
+            simp
           simpa [inner, smul_eq_mul, hre] using hmain
         · -- upper bound
           -- Bound each coordinate by `‖x‖` and sum.
@@ -517,7 +517,7 @@ instance : AdjointSpace 𝕜 ((i : ι) → E i) where
             simpa [Finset.sum_mul] using this
           have hre :
               re (∑ i : ι, ⟪x i, x i⟫_𝕜) = ∑ i : ι, re ⟪x i, x i⟫_𝕜 := by
-            simpa using (map_sum (RCLike.re : 𝕜 →+ ℝ) (fun i : ι => ⟪x i, x i⟫_𝕜) Finset.univ)
+            simp
           simpa [inner, smul_eq_mul, d0, hre] using hsum
     · -- Empty index set: everything is zero, so any positive constants work.
       refine ⟨1, 1, by positivity, by positivity, ?_⟩
@@ -532,8 +532,8 @@ instance : AdjointSpace 𝕜 ((i : ι) → E i) where
         exact hne this
       have hnorm : ‖x‖ = 0 := by
         -- For an empty index set, the `L^∞` norm is `0`.
-        simpa [Pi.norm_def, huniv]
-      constructor <;> simp [inner, smul_eq_mul, huniv, hnorm]
+        simp [Pi.norm_def, huniv]
+      constructor <;> simp [smul_eq_mul, huniv, hnorm]
   conj_symm := by simp
   add_left := by simp[inner_add_left,Finset.sum_add_distrib]
   smul_left := by simp[inner_smul_left,Finset.mul_sum]

Problems/NavierStokes/Definitions.lean

@@ -35,14 +35,14 @@ noncomputable def standardBasis (i : Fin n) : Euc ℝ n :=
 
 @[simp] theorem standardBasis_apply (i j : Fin n) :
     (standardBasis (n := n) i) j = if j = i then 1 else 0 := by
-  simp [standardBasis, EuclideanSpace.single_apply, eq_comm]
+  simp [standardBasis, eq_comm]
 
 @[simp] theorem standardBasis_self (i : Fin n) : (standardBasis (n := n) i) i = 1 := by
-  simp [standardBasis, EuclideanSpace.single_apply]
+  simp [standardBasis]
 
 @[simp] theorem standardBasis_neq (i j : Fin n) (h : i ≠ j) :
     (standardBasis (n := n) i) j = 0 := by
-  simp [standardBasis, EuclideanSpace.single_apply, Ne.symm h]
+  simp [standardBasis, Ne.symm h]
 
 /-- Partial derivative `∂ᵢ f(x)` for `f : ℝⁿ → ℝ`, defined via `fderiv`. -/
 noncomputable def partialDeriv (i : Fin n) (f : Euc ℝ n → ℝ) (x : Euc ℝ n) : ℝ :=

Problems/NavierStokes/Imports.lean

@@ -7,7 +7,7 @@ import Mathlib.Data.Matrix.Basic
 import Mathlib.LinearAlgebra.Basis.Defs
 import Mathlib.Data.Real.Basic
 import Mathlib.Analysis.InnerProductSpace.PiL2
-import Mathlib.Analysis.Distribution.SchwartzSpace
+import Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
 import Mathlib.Analysis.InnerProductSpace.Basic
 import Mathlib.MeasureTheory.Integral.Lebesgue.Basic
 import Mathlib.Analysis.Calculus.FDeriv.Basic

Problems/NavierStokes/Millennium.lean

@@ -13,16 +13,30 @@ setting and (B,D) in the periodic setting. In this repository they are formalize
 - `MillenniumNS_BoundedDomain.FeffermanB` and `MillenniumNS_BoundedDomain.FeffermanD`
   (`Problems/NavierStokes/MillenniumBoundedDomain.lean`)
 
-The Clay Millennium problem asks for a proof of one of these four statements; the combined
-statement is `MillenniumNS_BoundedDomain.FeffermanMillenniumProblem`, which we also re-export as
-`MillenniumNavierStokes.NavierStokesMillenniumProblem` below.
+The Clay Millennium problem asks for a proof of one of these four statements. We expose the four
+formal targets separately below, rather than as a single disjunction.
 -/
 
 namespace MillenniumNavierStokes
 
-/-- Fefferman's Clay Millennium problem statement (A)–(D), as a single disjunction. -/
-abbrev NavierStokesMillenniumProblem : Prop :=
+/-- Fefferman's Clay Millennium problem statements (A)–(D), kept as separate targets. -/
+abbrev NavierStokesMillenniumProblem : MillenniumNS_BoundedDomain.FeffermanMillenniumProblems :=
   MillenniumNS_BoundedDomain.FeffermanMillenniumProblem
 
-end MillenniumNavierStokes
+/-- Fefferman's statement (A), existence and smoothness on `ℝ³` with zero force. -/
+abbrev FeffermanA : Prop :=
+  MillenniumNS_BoundedDomain.FeffermanMillenniumProblem.A
+
+/-- Fefferman's statement (B), existence and smoothness in the periodic setting with zero force. -/
+abbrev FeffermanB : Prop :=
+  MillenniumNS_BoundedDomain.FeffermanMillenniumProblem.B
+
+/-- Fefferman's statement (C), breakdown on `ℝ³` with forcing allowed. -/
+abbrev FeffermanC : Prop :=
+  MillenniumNS_BoundedDomain.FeffermanMillenniumProblem.C
 
+/-- Fefferman's statement (D), breakdown in the periodic setting with forcing allowed. -/
+abbrev FeffermanD : Prop :=
+  MillenniumNS_BoundedDomain.FeffermanMillenniumProblem.D
+
+end MillenniumNavierStokes

Problems/NavierStokes/MillenniumBoundedDomain.lean

@@ -97,11 +97,23 @@ def FeffermanD : Prop :=
               FeffermanCond10 sol.u sol.p)
 
 /--
-The Clay Millennium problem asks for a proof of one of Fefferman's four statements (A)–(D).
+The four Fefferman alternatives appearing in Clay's Navier--Stokes problem statement.
 
-Here we assemble them as a single disjunction.
+We keep these as separate targets. Assembling the `ℝ³` alternatives into a single proposition
+`FeffermanA ∨ FeffermanC` is classically too weak in this formalization: if (A) fails, the
+zero-force counterexample already satisfies the forcing hypotheses in (C).
 -/
-def FeffermanMillenniumProblem : Prop :=
-  MillenniumNSRDomain.FeffermanA ∨ FeffermanB ∨ MillenniumNSRDomain.FeffermanC ∨ FeffermanD
+structure FeffermanMillenniumProblems where
+  /-- Fefferman's statement (A), existence and smoothness on `ℝ³` with zero force. -/
+  A : Prop := MillenniumNSRDomain.FeffermanA
+  /-- Fefferman's statement (B), existence and smoothness in the periodic setting with zero force. -/
+  B : Prop := FeffermanB
+  /-- Fefferman's statement (C), breakdown on `ℝ³` with forcing allowed. -/
+  C : Prop := MillenniumNSRDomain.FeffermanC
+  /-- Fefferman's statement (D), breakdown in the periodic setting with forcing allowed. -/
+  D : Prop := FeffermanD
+
+/-- The separated Navier--Stokes Millennium problem targets. -/
+def FeffermanMillenniumProblem : FeffermanMillenniumProblems := {}
 
 end MillenniumNS_BoundedDomain