Actual slot solves on a common torus

The source is evaluated on the lifted copy path. Only periodicity on the coarsest torus is used; finer native periodicity is not an input.

noncomputable def NavierStokes.CommonCoverSolve.coverEquiv : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane

Cover equiv, given by TorusAverages.slotChart (3, 1) (1, 5) (by norm_num).

Equations

• NavierStokes.CommonCoverSolve.coverEquiv = NavierStokes.TorusAverages.slotChart (3, 1) (1, 5) NavierStokes.CommonCoverSolve.coverEquiv._proof_1

theorem NavierStokes.CommonCoverSolve.coverEquiv_apply (Y : TorusInverse.Plane) : coverEquiv Y = SlotGeometry.cover Y

noncomputable def NavierStokes.CommonCoverSolve.coverPower : ℕ → TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane

Cover power as an element of ℕ → Plane ≃L[ℝ] Plane | 0 => ContinuousLinearEquiv.refl ℝ Plane | d + 1 => (coverPower d).trans coverEquiv.

Equations

• NavierStokes.CommonCoverSolve.coverPower 0 = ContinuousLinearEquiv.refl ℝ NavierStokes.TorusInverse.Plane
• NavierStokes.CommonCoverSolve.coverPower d.succ = (NavierStokes.CommonCoverSolve.coverPower d).trans NavierStokes.CommonCoverSolve.coverEquiv

theorem NavierStokes.CommonCoverSolve.coverPower_apply (d : ℕ) (Y : TorusInverse.Plane) : (coverPower d) Y = (SlotGeometry.cover ^ d) Y

noncomputable def NavierStokes.CommonCoverSolve.indexMap (k : TorusInverse.Frequency) : TorusInverse.Frequency

Index map, given by (3 * k.1 + k.2, k.1 + 5 * k.2).

Equations

• NavierStokes.CommonCoverSolve.indexMap k = (3 * k.1 + k.2, k.1 + 5 * k.2)

noncomputable def NavierStokes.CommonCoverSolve.coverIndex (d : ℕ) (k : TorusInverse.Frequency) : TorusInverse.Frequency

Cover index, given by indexMap^[d] k.

Equations

• NavierStokes.CommonCoverSolve.coverIndex d k = NavierStokes.CommonCoverSolve.indexMap^[d] k

theorem NavierStokes.CommonCoverSolve.coverEquiv_lattice (k : TorusInverse.Frequency) : coverEquiv (TorusAverages.latticePoint k) = TorusAverages.latticePoint (indexMap k)

theorem NavierStokes.CommonCoverSolve.coverPower_lattice (d : ℕ) (k : TorusInverse.Frequency) : (coverPower d) (TorusAverages.latticePoint k) = TorusAverages.latticePoint (coverIndex d k)

theorem NavierStokes.CommonCoverSolve.norm_coverPower_le (d : ℕ) (Y : TorusInverse.Plane) : ‖(coverPower d) Y‖ ≤ 6 ^ d * ‖Y‖

theorem NavierStokes.CommonCoverSolve.norm_coverPower_le_of_gap_le {d D : ℕ} (hd : d ≤ D) (Y : TorusInverse.Plane) : ‖(coverPower d) Y‖ ≤ 6 ^ D * ‖Y‖

structure NavierStokes.CommonCoverSolve.Geometry : Type

Fixed geometry for a level whose gap above the common coarsest level is gap. The columns of basis are the native radial and transverse vectors.

• gap : ℕ

  Gap of Geometry, of type ℕ.

• basis : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane

  Basis of Geometry, of type Plane ≃L[ℝ] Plane.

• center : TorusInverse.Plane

  Center of Geometry, of type Plane.

noncomputable def NavierStokes.CommonCoverSolve.Geometry.coordinates (g : Geometry) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) : TorusInverse.Plane

Coordinates, given by g.basis.symm (coverPower g.gap Y - g.center - TorusAverages.latticePoint k).

Equations

• g.coordinates k Y = g.basis.symm ((NavierStokes.CommonCoverSolve.coverPower g.gap) Y - g.center - NavierStokes.TorusAverages.latticePoint k)

noncomputable def NavierStokes.CommonCoverSolve.Geometry.point (g : Geometry) (k : TorusInverse.Frequency) (z : TorusInverse.Plane) : TorusInverse.Plane

Point, given by (coverPower g.gap).symm (g.center + TorusAverages.latticePoint k + g.basis z).

Equations

• g.point k z = (NavierStokes.CommonCoverSolve.coverPower g.gap).symm (g.center + NavierStokes.TorusAverages.latticePoint k + g.basis z)

theorem NavierStokes.CommonCoverSolve.Geometry.coordinates_point (g : Geometry) (k : TorusInverse.Frequency) (z : TorusInverse.Plane) : g.coordinates k (g.point k z) = z

theorem NavierStokes.CommonCoverSolve.Geometry.point_coordinates (g : Geometry) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) : g.point k (g.coordinates k Y) = Y

theorem NavierStokes.CommonCoverSolve.Geometry.point_add (g : Geometry) (k : TorusInverse.Frequency) (z h : TorusInverse.Plane) : g.point k (z + h) = g.point k z + (coverPower g.gap).symm (g.basis h)

noncomputable def NavierStokes.CommonCoverSolve.Geometry.path (g : Geometry) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) (eta : ℝ) : TorusInverse.Plane

Path, given by g.point k ((g.coordinates k Y).1, eta).

Equations

• g.path k Y eta = g.point k ((g.coordinates k Y).1, eta)

theorem NavierStokes.CommonCoverSolve.Geometry.coordinates_path (g : Geometry) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) (eta : ℝ) : g.coordinates k (g.path k Y eta) = ((g.coordinates k Y).1, eta)

theorem NavierStokes.CommonCoverSolve.Geometry.path_current (g : Geometry) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) : g.path k Y (g.coordinates k Y).2 = Y

theorem NavierStokes.CommonCoverSolve.Geometry.path_path (g : Geometry) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) (eta eta' : ℝ) : g.path k (g.path k Y eta) eta' = g.path k Y eta'

theorem NavierStokes.CommonCoverSolve.Geometry.path_eq_shift (g : Geometry) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) (eta : ℝ) : g.path k Y eta = Y + (coverPower g.gap).symm ((eta - (g.coordinates k Y).2) • g.basis (0, 1))

The manuscript's copy-path formula, in the common coarsest coordinates. The final native basis vector is v_t.

theorem NavierStokes.CommonCoverSolve.Geometry.point_deck (g : Geometry) (k n : TorusInverse.Frequency) (z : TorusInverse.Plane) : g.point (k + coverIndex g.gap n) z = g.point k z + TorusAverages.latticePoint n

theorem NavierStokes.CommonCoverSolve.Geometry.coordinates_deck (g : Geometry) (k n : TorusInverse.Frequency) (Y : TorusInverse.Plane) : g.coordinates (k + coverIndex g.gap n) (Y + TorusAverages.latticePoint n) = g.coordinates k Y

theorem NavierStokes.CommonCoverSolve.Geometry.path_deck (g : Geometry) (k n : TorusInverse.Frequency) (Y : TorusInverse.Plane) (eta : ℝ) : g.path (k + coverIndex g.gap n) (Y + TorusAverages.latticePoint n) eta = g.path k Y eta + TorusAverages.latticePoint n

theorem NavierStokes.CommonCoverSolve.Geometry.coordinates_contDiff (g : Geometry) (k : TorusInverse.Frequency) : ContDiff ℝ (↑⊤) (g.coordinates k)

theorem NavierStokes.CommonCoverSolve.Geometry.point_contDiff (g : Geometry) (k : TorusInverse.Frequency) : ContDiff ℝ (↑⊤) (g.point k)

theorem NavierStokes.CommonCoverSolve.Geometry.path_contDiff (g : Geometry) (k : TorusInverse.Frequency) : ContDiff ℝ ↑⊤ fun (z : TorusInverse.Plane × ℝ) => g.path k z.1 z.2

Actual forced linear equations on the copy paths

structure NavierStokes.CommonCoverSolve.LinearData (P V E : Type) [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] : Type

Native coefficients and a native linear conversion of an ambient source. The source itself is a function on the common coarsest coordinates. This allows the tangent-frame projection to depend on the native slot.

• coefficient : P × TorusInverse.Plane → E →L[ℝ] E

  Coefficient of LinearData, of type P × Plane → E →L[ℝ] E.

• forcingMap : P × TorusInverse.Plane → V →L[ℝ] E

  Forcing map of LinearData, of type P × Plane → V →L[ℝ] E.

• source : P × TorusInverse.Plane → V

  Source of LinearData, of type P × Plane → V.

def NavierStokes.CommonCoverSolve.PeriodicAt {P V : Type} (f : P × TorusInverse.Plane → V) (p : P) : Prop

Periodic at, given by ∀ Y : Plane, ∀ n : Frequency, f (p, Y + TorusAverages.latticePoint n) = f (p, Y).

Equations

• NavierStokes.CommonCoverSolve.PeriodicAt f p = ∀ (Y : NavierStokes.TorusInverse.Plane) (n : NavierStokes.TorusInverse.Frequency), f (p, Y + NavierStokes.TorusAverages.latticePoint n) = f (p, Y)

noncomputable def NavierStokes.CommonCoverSolve.LinearData.coefficientAlong {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : LinearData P V E) (g : Geometry) (k : TorusInverse.Frequency) (w : (P × TorusInverse.Plane) × ℝ) : E →L[ℝ] E

Coefficient along, given by d.coefficient (w.1.1, ((g.coordinates k w.1.2).1, w.2)).

Equations

• d.coefficientAlong g k w = d.coefficient (w.1.1, (g.coordinates k w.1.2).1, w.2)

noncomputable def NavierStokes.CommonCoverSolve.LinearData.forcingAlong {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : LinearData P V E) (g : Geometry) (k : TorusInverse.Frequency) (w : (P × TorusInverse.Plane) × ℝ) : E

Forcing along, given by d.forcingMap (w.1.1, ((g.coordinates k w.1.2).1, w.2)) (d.source (w.1.1, g.path k w.1.2 w.2)).

Equations

• d.forcingAlong g k w = (d.forcingMap (w.1.1, (g.coordinates k w.1.2).1, w.2)) (d.source (w.1.1, g.path k w.1.2 w.2))

theorem NavierStokes.CommonCoverSolve.LinearData.coefficientAlong_deck {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : LinearData P V E) (g : Geometry) (k n : TorusInverse.Frequency) (p : P) (Y : TorusInverse.Plane) (s : ℝ) : d.coefficientAlong g (k + coverIndex g.gap n) ((p, Y + TorusAverages.latticePoint n), s) = d.coefficientAlong g k ((p, Y), s)

theorem NavierStokes.CommonCoverSolve.LinearData.forcingAlong_deck {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : LinearData P V E) (g : Geometry) (k n : TorusInverse.Frequency) (p : P) (hp : PeriodicAt d.source p) (Y : TorusInverse.Plane) (s : ℝ) : d.forcingAlong g (k + coverIndex g.gap n) ((p, Y + TorusAverages.latticePoint n), s) = d.forcingAlong g k ((p, Y), s)

theorem NavierStokes.CommonCoverSolve.LinearData.coefficientAlong_reanchor {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : LinearData P V E) (g : Geometry) (k : TorusInverse.Frequency) (p : P) (Y : TorusInverse.Plane) (eta s : ℝ) : d.coefficientAlong g k ((p, g.path k Y eta), s) = d.coefficientAlong g k ((p, Y), s)

theorem NavierStokes.CommonCoverSolve.LinearData.forcingAlong_reanchor {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : LinearData P V E) (g : Geometry) (k : TorusInverse.Frequency) (p : P) (Y : TorusInverse.Plane) (eta s : ℝ) : d.forcingAlong g k ((p, g.path k Y eta), s) = d.forcingAlong g k ((p, Y), s)

theorem NavierStokes.CommonCoverSolve.pathFamily_congr_slice {Q W : Type} [NormedAddCommGroup W] {a b : ℝ} (F G : Q × ℝ → W) (p q : Q) (h : ∀ (t : ↑(Set.Icc a b)), F (p, ↑t) = G (q, ↑t)) : SmoothPathFamily.pathFamily F p = SmoothPathFamily.pathFamily G q

noncomputable def NavierStokes.CommonCoverSolve.LinearData.coefficientPath {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (k : TorusInverse.Frequency) (p : P × TorusInverse.Plane) : ParametricODE.Coefficient a b E

Coefficient path, given by SmoothPathFamily.pathFamily (d.coefficientAlong g k) p.

Equations

• d.coefficientPath g k p = NavierStokes.SmoothPathFamily.pathFamily (d.coefficientAlong g k) p

noncomputable def NavierStokes.CommonCoverSolve.LinearData.forcingPath {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (k : TorusInverse.Frequency) (p : P × TorusInverse.Plane) : ParametricODE.Curve a b E

Forcing path, given by SmoothPathFamily.pathFamily (d.forcingAlong g k) p.

Equations

• d.forcingPath g k p = NavierStokes.SmoothPathFamily.pathFamily (d.forcingAlong g k) p

noncomputable def NavierStokes.CommonCoverSolve.LinearData.anchoredSolve {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) (k : TorusInverse.Frequency) (p : P × TorusInverse.Plane) (s : ℝ) : E

The genuine Volterra solution, with zero entry data, evaluated along the copy path anchored at the current common coordinate.

Equations

• d.anchoredSolve g hab k p s = NavierStokes.ParametricODE.solutionExtension hab (d.coefficientPath g k p) 0 (d.forcingPath g k p) s

noncomputable def NavierStokes.CommonCoverSolve.LinearData.copySolve {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) (k : TorusInverse.Frequency) (p : P × TorusInverse.Plane) : E

Value of the constructed solution at the current native slot coordinate.

Equations

• d.copySolve g hab k p = d.anchoredSolve g hab k p (g.coordinates k p.2).2

theorem NavierStokes.CommonCoverSolve.LinearData.coefficientPath_deck {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (k n : TorusInverse.Frequency) (p : P) (Y : TorusInverse.Plane) : d.coefficientPath g (k + coverIndex g.gap n) (p, Y + TorusAverages.latticePoint n) = d.coefficientPath g k (p, Y)

theorem NavierStokes.CommonCoverSolve.LinearData.forcingPath_deck {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (k n : TorusInverse.Frequency) (p : P) (hp : PeriodicAt d.source p) (Y : TorusInverse.Plane) : d.forcingPath g (k + coverIndex g.gap n) (p, Y + TorusAverages.latticePoint n) = d.forcingPath g k (p, Y)

theorem NavierStokes.CommonCoverSolve.LinearData.anchoredSolve_deck {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) (k n : TorusInverse.Frequency) (p : P) (hp : PeriodicAt d.source p) (Y : TorusInverse.Plane) (s : ℝ) : d.anchoredSolve g hab (k + coverIndex g.gap n) (p, Y + TorusAverages.latticePoint n) s = d.anchoredSolve g hab k (p, Y) s

theorem NavierStokes.CommonCoverSolve.LinearData.copySolve_deck {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) (k n : TorusInverse.Frequency) (p : P) (hp : PeriodicAt d.source p) (Y : TorusInverse.Plane) : d.copySolve g hab (k + coverIndex g.gap n) (p, Y + TorusAverages.latticePoint n) = d.copySolve g hab k (p, Y)

theorem NavierStokes.CommonCoverSolve.LinearData.anchoredSolve_reanchor {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) (k : TorusInverse.Frequency) (p : P) (Y : TorusInverse.Plane) (eta s : ℝ) : d.anchoredSolve g hab k (p, g.path k Y eta) s = d.anchoredSolve g hab k (p, Y) s

theorem NavierStokes.CommonCoverSolve.LinearData.copySolve_path {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) (k : TorusInverse.Frequency) (p : P) (Y : TorusInverse.Plane) (s : ℝ) : d.copySolve g hab k (p, g.path k Y s) = d.anchoredSolve g hab k (p, Y) s

theorem NavierStokes.CommonCoverSolve.LinearData.anchoredSolve_initial {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) (k : TorusInverse.Frequency) (p : P × TorusInverse.Plane) : d.anchoredSolve g hab k p a = 0

theorem NavierStokes.CommonCoverSolve.LinearData.copySolve_at_entry {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) (k : TorusInverse.Frequency) (p : P) (xi : ℝ) : d.copySolve g hab k (p, g.point k (xi, a)) = 0

theorem NavierStokes.CommonCoverSolve.solutionExtension_zero {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (hab : a ≤ b) (A : ParametricODE.Coefficient a b E) [CompleteSpace E] (s : ℝ) : ParametricODE.solutionExtension hab A 0 0 s = 0

theorem NavierStokes.CommonCoverSolve.LinearData.forcingPath_zero_of_source_zero {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (k : TorusInverse.Frequency) (p : P) (Y : TorusInverse.Plane) (hf : ∀ s ∈ Set.Icc a b, d.source (p, g.path k Y s) = 0) : d.forcingPath g k (p, Y) = 0

theorem NavierStokes.CommonCoverSolve.LinearData.anchoredSolve_zero_of_source_zero {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) (k : TorusInverse.Frequency) (p : P) (Y : TorusInverse.Plane) (hf : ∀ s ∈ Set.Icc a b, d.source (p, g.path k Y s) = 0) (eta : ℝ) : d.anchoredSolve g hab k (p, Y) eta = 0

Vanishing along the entire source path forces the constructed zero-entry solution to vanish. No vanishing assumption on the output is used.

theorem NavierStokes.CommonCoverSolve.LinearData.copySolve_zero_of_source_zero {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) (k : TorusInverse.Frequency) (p : P) (Y : TorusInverse.Plane) (hf : ∀ s ∈ Set.Icc a b, d.source (p, g.path k Y s) = 0) : d.copySolve g hab k (p, Y) = 0

theorem NavierStokes.CommonCoverSolve.LinearData.copySolve_preserves_slow_support {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) {U : Set P} (hf : ∀ p ∉ U, ∀ (Y : TorusInverse.Plane), d.source (p, Y) = 0) (k : TorusInverse.Frequency) {p : P} (hp : p ∉ U) (Y : TorusInverse.Plane) : d.copySolve g hab k (p, Y) = 0

theorem NavierStokes.CommonCoverSolve.LinearData.copySolve_preserves_transverse_support {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) (k : TorusInverse.Frequency) {S : Set ℝ} (p : P) (hf : ∀ xi ∉ S, ∀ eta ∈ Set.Icc a b, d.source (p, g.point k (xi, eta)) = 0) (Y : TorusInverse.Plane) (hY : (g.coordinates k Y).1 ∉ S) : d.copySolve g hab k (p, Y) = 0

theorem NavierStokes.CommonCoverSolve.Geometry.nativeArgument_contDiff {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : Geometry) (k : TorusInverse.Frequency) : ContDiff ℝ ↑⊤ fun (w : (P × TorusInverse.Plane) × ℝ) => (w.1.1, (g.coordinates k w.1.2).1, w.2)

theorem NavierStokes.CommonCoverSolve.Geometry.pathArgument_contDiff {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : Geometry) (k : TorusInverse.Frequency) : ContDiff ℝ ↑⊤ fun (w : (P × TorusInverse.Plane) × ℝ) => (w.1.1, g.path k w.1.2 w.2)

theorem NavierStokes.CommonCoverSolve.LinearData.coefficientAlong_continuousOn {P V E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : LinearData P V E) (g : Geometry) {U : Set P} (k : TorusInverse.Frequency) (hA : ContinuousOn d.coefficient (U ×ˢ Set.univ)) : ContinuousOn (d.coefficientAlong g k) ((U ×ˢ Set.univ) ×ˢ Set.univ)

theorem NavierStokes.CommonCoverSolve.LinearData.forcingAlong_continuousOn {P V E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : LinearData P V E) (g : Geometry) {U : Set P} (k : TorusInverse.Frequency) (hB : ContinuousOn d.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn d.source (U ×ˢ Set.univ)) : ContinuousOn (d.forcingAlong g k) ((U ×ˢ Set.univ) ×ˢ Set.univ)

theorem NavierStokes.CommonCoverSolve.LinearData.coefficientAlong_contDiffOn {P V E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : LinearData P V E) (g : Geometry) {U : Set P} (k : TorusInverse.Frequency) (hA : ContDiffOn ℝ (↑⊤) d.coefficient (U ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (d.coefficientAlong g k) ((U ×ˢ Set.univ) ×ˢ Set.univ)

theorem NavierStokes.CommonCoverSolve.LinearData.forcingAlong_contDiffOn {P V E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : LinearData P V E) (g : Geometry) {U : Set P} (k : TorusInverse.Frequency) (hB : ContDiffOn ℝ (↑⊤) d.forcingMap (U ×ˢ Set.univ)) (hf : ContDiffOn ℝ (↑⊤) d.source (U ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (d.forcingAlong g k) ((U ×ˢ Set.univ) ×ˢ Set.univ)

theorem NavierStokes.CommonCoverSolve.LinearData.anchoredSolve_hasDerivAt {P V E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : LinearData P V E) (g : Geometry) {U : Set P} [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (k : TorusInverse.Frequency) (hA : ContinuousOn d.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn d.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn d.source (U ×ˢ Set.univ)) {p : P} (hp : p ∈ U) (Y : TorusInverse.Plane) (s : ↑(Set.Icc a b)) : HasDerivAt (d.anchoredSolve g hab k (p, Y)) ((d.coefficientAlong g k ((p, Y), ↑s)) (d.anchoredSolve g hab k (p, Y) ↑s) + d.forcingAlong g k ((p, Y), ↑s)) ↑s

The constructed extension satisfies the original forced equation on the copy path, including both endpoints as a differentiable extension.

theorem NavierStokes.CommonCoverSolve.LinearData.copySolve_alongPath_hasDerivAt {P V E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : LinearData P V E) (g : Geometry) {U : Set P} [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (k : TorusInverse.Frequency) (hA : ContinuousOn d.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn d.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn d.source (U ×ˢ Set.univ)) {p : P} (hp : p ∈ U) (Y : TorusInverse.Plane) (s : ↑(Set.Icc a b)) : HasDerivAt (fun (t : ℝ) => d.copySolve g hab k (p, g.path k Y t)) ((d.coefficientAlong g k ((p, Y), ↑s)) (d.copySolve g hab k (p, g.path k Y ↑s)) + d.forcingAlong g k ((p, Y), ↑s)) ↑s

theorem NavierStokes.CommonCoverSolve.LinearData.anchoredSolve_unique {P V E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : LinearData P V E) (g : Geometry) {U : Set P} [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (k : TorusInverse.Frequency) (hA : ContinuousOn d.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn d.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn d.source (U ×ˢ Set.univ)) {p : P} (hp : p ∈ U) (Y : TorusInverse.Plane) {u : ℝ → E} (hu0 : u a = 0) (hu : ∀ s ∈ Set.Icc a b, HasDerivAt u ((d.coefficientAlong g k ((p, Y), s)) (u s) + d.forcingAlong g k ((p, Y), s)) s) : Set.EqOn u (d.anchoredSolve g hab k (p, Y)) (Set.Icc a b)

Localization and the actual common-torus field

theorem NavierStokes.CommonCoverSolve.Geometry.cutoff_as_translate (g : Geometry) (κ : TorusInverse.Plane → ℝ) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) : κ (g.coordinates k Y) = TorusAverages.nativeField g.basis g.center κ (TorusAverages.latticePoint (-k) + (coverPower g.gap) Y)

theorem NavierStokes.CommonCoverSolve.Geometry.finite_copy_cutoffs (g : Geometry) {κ : TorusInverse.Plane → ℝ} (hκ : HasCompactSupport κ) (R : ℝ) : ∃ (s : Finset TorusInverse.Frequency), ∀ (Y : TorusInverse.Plane), ‖Y‖ ≤ R → ∀ k ∉ s, κ (g.coordinates k Y) = 0

noncomputable def NavierStokes.CommonCoverSolve.LinearData.localizedCopy {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (k : TorusInverse.Frequency) (p : P × TorusInverse.Plane) : E

Localized copy, given by κ (g.coordinates k p.2) • d.copySolve g hab k p.

Equations

• d.localizedCopy g hab κ k p = κ (g.coordinates k p.2) • d.copySolve g hab k p

noncomputable def NavierStokes.CommonCoverSolve.LinearData.commonSolve {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (p : P × TorusInverse.Plane) : E

The actual sum of localized copy solves. Sources in different native copies are evaluated at their own absolute-lift points.

Equations

• d.commonSolve g hab κ p = ∑' (k : NavierStokes.TorusInverse.Frequency), d.localizedCopy g hab κ k p

theorem NavierStokes.CommonCoverSolve.LinearData.localizedCopy_deck {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (k n : TorusInverse.Frequency) (p : P) (hp : PeriodicAt d.source p) (Y : TorusInverse.Plane) : d.localizedCopy g hab κ (k + coverIndex g.gap n) (p, Y + TorusAverages.latticePoint n) = d.localizedCopy g hab κ k (p, Y)

theorem NavierStokes.CommonCoverSolve.LinearData.commonSolve_periodic {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (p : P) (hp : PeriodicAt d.source p) (Y : TorusInverse.Plane) (n : TorusInverse.Frequency) : d.commonSolve g hab κ (p, Y + TorusAverages.latticePoint n) = d.commonSolve g hab κ (p, Y)

Common-torus periodicity follows by reindexing the actual copy sum. The source is required to be periodic only in the common variable.

theorem NavierStokes.CommonCoverSolve.LinearData.commonSolve_preserves_slow_support {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) {U : Set P} (hf : ∀ p ∉ U, ∀ (Y : TorusInverse.Plane), d.source (p, Y) = 0) {p : P} (hp : p ∉ U) (Y : TorusInverse.Plane) : d.commonSolve g hab κ (p, Y) = 0

theorem NavierStokes.CommonCoverSolve.LinearData.localizedCopy_preserves_transverse_support {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (k : TorusInverse.Frequency) {S : Set ℝ} (p : P) (hf : ∀ xi ∉ S, ∀ eta ∈ Set.Icc a b, d.source (p, g.point k (xi, eta)) = 0) (Y : TorusInverse.Plane) (hY : (g.coordinates k Y).1 ∉ S) : d.localizedCopy g hab κ k (p, Y) = 0

theorem NavierStokes.CommonCoverSolve.LinearData.commonSolve_eventually_eq_sum {P V E : Type} [NormedAddCommGroup P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) {κ : TorusInverse.Plane → ℝ} (hκ : HasCompactSupport κ) (p : P × TorusInverse.Plane) : ∃ (s : Finset TorusInverse.Frequency), d.commonSolve g hab κ =ᶠ[nhds p] fun (q : P × TorusInverse.Plane) => ∑ k ∈ s, d.localizedCopy g hab κ k q

theorem NavierStokes.CommonCoverSolve.LinearData.commonSolve_contDiffOn_of_copies {P V E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) {U : Set P} (hU : IsOpen U) {κ : TorusInverse.Plane → ℝ} (hκ : HasCompactSupport κ) (hc : ∀ (k : TorusInverse.Frequency), ContDiffOn ℝ (↑⊤) (d.localizedCopy g hab κ k) (U ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (d.commonSolve g hab κ) (U ×ˢ Set.univ)

A function on the quotient torus, not merely a periodic lift

def NavierStokes.CommonCoverSolve.LatticePeriodic {W : Type} (f : TorusInverse.Plane → W) : Prop

Lattice periodic, given by ∀ Y : Plane, ∀ k : Frequency, f (Y + TorusAverages.latticePoint k) = f Y.

Equations

• NavierStokes.CommonCoverSolve.LatticePeriodic f = ∀ (Y : NavierStokes.TorusInverse.Plane) (k : NavierStokes.TorusInverse.Frequency), f (Y + NavierStokes.TorusAverages.latticePoint k) = f Y

theorem NavierStokes.CommonCoverSolve.latticePeriodic_first {W : Type} {f : TorusInverse.Plane → W} (hf : LatticePeriodic f) (y : ℝ) : Function.Periodic (fun (x : ℝ) => f (x, y)) 1

theorem NavierStokes.CommonCoverSolve.latticePeriodic_second {W : Type} {f : TorusInverse.Plane → W} (hf : LatticePeriodic f) (x : ℝ) : Function.Periodic (fun (y : ℝ) => f (x, y)) 1

noncomputable def NavierStokes.CommonCoverSolve.firstDescent {W : Type} (f : TorusInverse.Plane → W) (hf : LatticePeriodic f) (z : UnitAddCircle) (y : ℝ) : W

First descent, given by (latticePeriodic_first hf y).lift z.

Equations

• NavierStokes.CommonCoverSolve.firstDescent f hf z y = ⋯.lift z

theorem NavierStokes.CommonCoverSolve.firstDescent_periodic {W : Type} (f : TorusInverse.Plane → W) (hf : LatticePeriodic f) (z : UnitAddCircle) : Function.Periodic (firstDescent f hf z) 1

noncomputable def NavierStokes.CommonCoverSolve.torusDescent {W : Type} (f : TorusInverse.Plane → W) (hf : LatticePeriodic f) (z : TorusInverse.Torus) : W

Torus descent, given by (firstDescent_periodic f hf z.1).lift z.2.

Equations

• NavierStokes.CommonCoverSolve.torusDescent f hf z = ⋯.lift z.2

theorem NavierStokes.CommonCoverSolve.torusDescent_coe {W : Type} (f : TorusInverse.Plane → W) (hf : LatticePeriodic f) (Y : TorusInverse.Plane) : torusDescent f hf (TorusAverages.quotientPoint Y) = f Y

theorem NavierStokes.CommonCoverSolve.torusDescent_continuous {W : Type} [TopologicalSpace W] {f : TorusInverse.Plane → W} (hf : LatticePeriodic f) (hc : Continuous f) : Continuous (torusDescent f hf)

noncomputable def NavierStokes.CommonCoverSolve.LinearData.commonOnTorus {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (p : P) (hp : PeriodicAt d.source p) : TorusInverse.Torus → E

The constructed common-torus solution is obtained by a genuine quotient lift of the reindexed copy sum.

Equations

• d.commonOnTorus g hab κ p hp = NavierStokes.CommonCoverSolve.torusDescent (fun (Y : NavierStokes.TorusInverse.Plane) => d.commonSolve g hab κ (p, Y)) ⋯

theorem NavierStokes.CommonCoverSolve.LinearData.commonOnTorus_coe {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (p : P) (hp : PeriodicAt d.source p) (Y : TorusInverse.Plane) : d.commonOnTorus g hab κ p hp (TorusAverages.quotientPoint Y) = d.commonSolve g hab κ (p, Y)

Joint regularity is derived from the actual ODE construction.

theorem NavierStokes.CommonCoverSolve.LinearData.anchoredSolve_contDiffOn {P V E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) {U : Set P} (hU : IsOpen U) (k : TorusInverse.Frequency) (hA : ContDiffOn ℝ (↑⊤) d.coefficient (U ×ˢ Set.univ)) (hB : ContDiffOn ℝ (↑⊤) d.forcingMap (U ×ˢ Set.univ)) (hf : ContDiffOn ℝ (↑⊤) d.source (U ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (fun (z : (P × TorusInverse.Plane) × ℝ) => d.anchoredSolve g hab k z.1 z.2) ((U ×ˢ Set.univ) ×ˢ Set.Ioo a b)

theorem NavierStokes.CommonCoverSolve.LinearData.copySolve_contDiffAt {P V E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) {U : Set P} (hU : IsOpen U) (k : TorusInverse.Frequency) (hA : ContDiffOn ℝ (↑⊤) d.coefficient (U ×ˢ Set.univ)) (hB : ContDiffOn ℝ (↑⊤) d.forcingMap (U ×ˢ Set.univ)) (hf : ContDiffOn ℝ (↑⊤) d.source (U ×ˢ Set.univ)) {p : P × TorusInverse.Plane} (hp : p.1 ∈ U) (heta : (g.coordinates k p.2).2 ∈ Set.Ioo a b) : ContDiffAt ℝ (↑⊤) (d.copySolve g hab k) p

theorem NavierStokes.CommonCoverSolve.LinearData.localizedCopy_contDiffOn {P V E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) {U : Set P} (hU : IsOpen U) (k : TorusInverse.Frequency) (hA : ContDiffOn ℝ (↑⊤) d.coefficient (U ×ˢ Set.univ)) (hB : ContDiffOn ℝ (↑⊤) d.forcingMap (U ×ˢ Set.univ)) (hf : ContDiffOn ℝ (↑⊤) d.source (U ×ˢ Set.univ)) {κ : TorusInverse.Plane → ℝ} (hκ : ContDiff ℝ (↑⊤) κ) (hsupp : tsupport κ ⊆ Set.univ ×ˢ Set.Ioo a b) : ContDiffOn ℝ (↑⊤) (d.localizedCopy g hab κ k) (U ×ˢ Set.univ)

The localization cutoff is supported strictly inside the slot interval. The clamped extension outside the interval is never claimed to be smooth.

theorem NavierStokes.CommonCoverSolve.LinearData.commonSolve_contDiffOn {P V E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) {U : Set P} (hU : IsOpen U) (hA : ContDiffOn ℝ (↑⊤) d.coefficient (U ×ˢ Set.univ)) (hB : ContDiffOn ℝ (↑⊤) d.forcingMap (U ×ˢ Set.univ)) (hf : ContDiffOn ℝ (↑⊤) d.source (U ×ˢ Set.univ)) {κ : TorusInverse.Plane → ℝ} (hκ : ContDiff ℝ (↑⊤) κ) (hcκ : HasCompactSupport κ) (hsupp : tsupport κ ⊆ Set.univ ×ˢ Set.Ioo a b) : ContDiffOn ℝ (↑⊤) (d.commonSolve g hab κ) (U ×ˢ Set.univ)

The actual sum of native copy solves is jointly smooth in slow and common torus coordinates. Local finiteness was proved from compact support.

theorem NavierStokes.CommonCoverSolve.LinearData.commonOnTorus_continuous {P V E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) {U : Set P} (hU : IsOpen U) (hA : ContDiffOn ℝ (↑⊤) d.coefficient (U ×ˢ Set.univ)) (hB : ContDiffOn ℝ (↑⊤) d.forcingMap (U ×ˢ Set.univ)) (hf : ContDiffOn ℝ (↑⊤) d.source (U ×ˢ Set.univ)) {κ : TorusInverse.Plane → ℝ} (hκ : ContDiff ℝ (↑⊤) κ) (hcκ : HasCompactSupport κ) (hsupp : tsupport κ ⊆ Set.univ ×ˢ Set.Ioo a b) (p : P) (hp : p ∈ U) (hper : PeriodicAt d.source p) : Continuous (d.commonOnTorus g hab κ p hper)

Bounded covering gaps and actual derivative costs

noncomputable def NavierStokes.CommonCoverSolve.coveringBound (D : ℕ) : ℝ

Covering bound, given by 1 + ∑ d ∈ Finset.range (D + 1), (‖(coverPower d : Plane →L[ℝ] Plane)‖ + ‖((coverPower d).symm : Plane →L[ℝ] Plane)‖).

Equations

• NavierStokes.CommonCoverSolve.coveringBound D = 1 + ∑ d ∈ Finset.range (D + 1), (‖↑(NavierStokes.CommonCoverSolve.coverPower d)‖ + ‖↑(NavierStokes.CommonCoverSolve.coverPower d).symm‖)

theorem NavierStokes.CommonCoverSolve.coveringBound_pos (D : ℕ) : 0 < coveringBound D

theorem NavierStokes.CommonCoverSolve.coveringNorm_le_bound {d D : ℕ} (hd : d ≤ D) : ‖↑(coverPower d)‖ ≤ coveringBound D

theorem NavierStokes.CommonCoverSolve.inverseCoveringNorm_le_bound {d D : ℕ} (hd : d ≤ D) : ‖↑(coverPower d).symm‖ ≤ coveringBound D

noncomputable def NavierStokes.CommonCoverSolve.Geometry.coordinateLinear (g : Geometry) : TorusInverse.Plane →L[ℝ] TorusInverse.Plane

Coordinate linear, given by (g.basis.symm : Plane →L[ℝ] Plane).comp (coverPower g.gap : Plane →L[ℝ] Plane).

Equations

• g.coordinateLinear = ↑g.basis.symm ∘SL ↑(NavierStokes.CommonCoverSolve.coverPower g.gap)

noncomputable def NavierStokes.CommonCoverSolve.Geometry.pointLinear (g : Geometry) : TorusInverse.Plane →L[ℝ] TorusInverse.Plane

Point linear, given by ((coverPower g.gap).symm : Plane →L[ℝ] Plane).comp (g.basis : Plane →L[ℝ] Plane).

Equations

• g.pointLinear = ↑(NavierStokes.CommonCoverSolve.coverPower g.gap).symm ∘SL ↑g.basis

noncomputable def NavierStokes.CommonCoverSolve.Geometry.horizontal : TorusInverse.Plane →L[ℝ] TorusInverse.Plane

Horizontal, given by (ContinuousLinearMap.fst ℝ ℝ ℝ).prod 0.

Equations

• NavierStokes.CommonCoverSolve.Geometry.horizontal = (ContinuousLinearMap.fst ℝ ℝ ℝ).prod 0

noncomputable def NavierStokes.CommonCoverSolve.Geometry.pathLinear (g : Geometry) : TorusInverse.Plane →L[ℝ] TorusInverse.Plane

Path linear, given by g.pointLinear.comp (horizontal.comp g.coordinateLinear).

Equations

• g.pathLinear = g.pointLinear ∘SL NavierStokes.CommonCoverSolve.Geometry.horizontal ∘SL g.coordinateLinear

theorem NavierStokes.CommonCoverSolve.Geometry.coordinates_eq_affine (g : Geometry) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) : g.coordinates k Y = g.coordinates k 0 + g.coordinateLinear Y

theorem NavierStokes.CommonCoverSolve.Geometry.point_eq_affine (g : Geometry) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) : g.point k Y = g.point k 0 + g.pointLinear Y

theorem NavierStokes.CommonCoverSolve.Geometry.path_eq_affine (g : Geometry) (k : TorusInverse.Frequency) (eta : ℝ) (Y : TorusInverse.Plane) : g.path k Y eta = g.path k 0 eta + g.pathLinear Y

theorem NavierStokes.CommonCoverSolve.Geometry.norm_coordinateLinear_le (g : Geometry) {D : ℕ} (hd : g.gap ≤ D) : ‖g.coordinateLinear‖ ≤ ‖↑g.basis.symm‖ * coveringBound D

theorem NavierStokes.CommonCoverSolve.Geometry.norm_pointLinear_le (g : Geometry) {D : ℕ} (hd : g.gap ≤ D) : ‖g.pointLinear‖ ≤ coveringBound D * ‖↑g.basis‖

theorem NavierStokes.CommonCoverSolve.Geometry.norm_horizontal_le : ‖horizontal‖ ≤ 1

noncomputable def NavierStokes.CommonCoverSolve.Geometry.pathBound (g : Geometry) (D : ℕ) : ℝ

Path bound, given by (coveringBound D * ‖(g.basis : Plane →L[ℝ] Plane)‖) * (‖(g.basis.symm : Plane →L[ℝ] Plane)‖ * coveringBound D).

Equations

• g.pathBound D = NavierStokes.CommonCoverSolve.coveringBound D * ‖↑g.basis‖ * (‖↑g.basis.symm‖ * NavierStokes.CommonCoverSolve.coveringBound D)

theorem NavierStokes.CommonCoverSolve.Geometry.pathBound_nonneg (g : Geometry) (D : ℕ) : 0 ≤ g.pathBound D

theorem NavierStokes.CommonCoverSolve.Geometry.norm_pathLinear_le (g : Geometry) {D : ℕ} (hd : g.gap ≤ D) : ‖g.pathLinear‖ ≤ g.pathBound D

theorem NavierStokes.CommonCoverSolve.Geometry.path_displacement_le (g : Geometry) {D : ℕ} (hd : g.gap ≤ D) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) (eta : ℝ) : ‖g.path k Y eta - Y‖ ≤ coveringBound D * (|eta - (g.coordinates k Y).2| * ‖g.basis (0, 1)‖)

The common-variable path shifts have a bound depending only on the finite index gap and the fixed native basis, never on the copy index.

theorem NavierStokes.CommonCoverSolve.norm_iteratedFDeriv_affine_le {X Y W : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [NormedAddCommGroup W] [NormedSpace ℝ W] {f : Y → W} (hf : ContDiff ℝ (↑⊤) f) (L : X →L[ℝ] Y) (c : Y) (x : X) (n : ℕ) : ‖iteratedFDeriv ℝ n (fun (z : X) => f (c + L z)) x‖ ≤ ‖iteratedFDeriv ℝ n f (c + L x)‖ * ‖L‖ ^ n

All actual derivative orders of an affine pullback have the expected operator-norm cost. No independent jet family is supplied.

theorem NavierStokes.CommonCoverSolve.Geometry.norm_path_pullback_jet_le {W : Type} [NormedAddCommGroup W] [NormedSpace ℝ W] (g : Geometry) {D : ℕ} (hd : g.gap ≤ D) {f : TorusInverse.Plane → W} (hf : ContDiff ℝ (↑⊤) f) (k : TorusInverse.Frequency) (eta : ℝ) (Y : TorusInverse.Plane) (n : ℕ) : ‖iteratedFDeriv ℝ n (fun (Z : TorusInverse.Plane) => f (g.path k Z eta)) Y‖ ≤ ‖iteratedFDeriv ℝ n f (g.path k Y eta)‖ * g.pathBound D ^ n

theorem NavierStokes.CommonCoverSolve.LinearData.anchoredSolve_jets_le_polynomial {P V E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : LinearData P V E) (g : Geometry) (hab : a ≤ b) {U : Set P} (hU : IsOpen U) (k : TorusInverse.Frequency) (hA : ContDiffOn ℝ (↑⊤) d.coefficient (U ×ˢ Set.univ)) (hB : ContDiffOn ℝ (↑⊤) d.forcingMap (U ×ˢ Set.univ)) (hf : ContDiffOn ℝ (↑⊤) d.source (U ×ˢ Set.univ)) {p : P × TorusInverse.Plane} (hp : p.1 ∈ U) (rate W : ℝ → ℝ) {μ S K w : ℝ} (hμ : 0 ≤ μ) (hW : ∀ (t : ℝ), 0 < W t) (hdW : ∀ (t : ℝ), HasDerivAt W (rate t * W t) t) (henergy : ∀ (t : ↑(Set.Icc a b)) (x : E), inner ℝ x ((d.coefficientAlong g k (p, ↑t)) x) ≤ (rate ↑t + μ) * ‖x‖ ^ 2) (hC : Real.exp (μ * (b - a)) ≤ K) (hS : 1 ≤ S) (hK : 1 ≤ K) (hw : 0 ≤ w) (hslot : b - a ≤ K * S) (m N : ℕ) (hAj : ∀ j ≤ N, ∀ (t : ↑(Set.Icc a b)), ‖iteratedFDeriv ℝ j (fun (q : P × TorusInverse.Plane) => d.coefficientAlong g k (q, ↑t)) p‖ ≤ K * S ^ m) (hfj : ∀ j ≤ N, ∀ (t : ↑(Set.Icc a b)), ‖iteratedFDeriv ℝ j (fun (q : P × TorusInverse.Plane) => d.forcingAlong g k (q, ↑t)) p‖ ≤ w * K * S ^ m * W ↑t) (n : ℕ) (hn : n ≤ N) (t : ↑(Set.Icc a b)) : ‖iteratedFDeriv ℝ n (fun (q : P × TorusInverse.Plane) => d.anchoredSolve g hab k q ↑t) p‖ ≤ w * (2 ^ (N + 1) * K ^ 3) ^ (n + 1) * S ^ ((m + 1) * (n + 1)) * W ↑t

The verified weighted ODE estimate applies to this exact path solve. All hypotheses are bounds on the actual pulled-back input coefficients and source, rather than bounds or equations assumed for an output family.

Concrete projected tangent equation

noncomputable def NavierStokes.CommonCoverSolve.negativeTangentProjection {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (n : H) : H →L[ℝ] H

Negative tangent projection, given by -(ContinuousLinearMap.id ℝ H - (innerSL ℝ n).smulRight ((⟪n, n⟫_ℝ)⁻¹ • n)).

Equations

• NavierStokes.CommonCoverSolve.negativeTangentProjection n = -(ContinuousLinearMap.id ℝ H - ((innerSL ℝ) n).smulRight ((inner ℝ n n)⁻¹ • n))

theorem NavierStokes.CommonCoverSolve.negativeTangentProjection_apply {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (n x : H) : (negativeTangentProjection n) x = -TangentProjection.tangentProj n x

structure NavierStokes.CommonCoverSolve.TangentData (P H : Type) [NormedAddCommGroup H] [InnerProductSpace ℝ H] : Type

All quantities in the actual projected tangent equation, before solving. The native normal and its slot derivative are explicit input fields.

• normal : P × TorusInverse.Plane → H

  Normal of TangentData, of type P × Plane → H.

• normalDot : P × TorusInverse.Plane → H

  Normal dot of TangentData, of type P × Plane → H.

• action : P × TorusInverse.Plane → H →L[ℝ] H

  Action of TangentData, of type P × Plane → H →L[ℝ] H.

• damping : P × TorusInverse.Plane → ℝ

  Damping of TangentData, of type P × Plane → ℝ.

• source : P × TorusInverse.Plane → H

  Source of TangentData, of type P × Plane → H.

noncomputable def NavierStokes.CommonCoverSolve.TangentData.linearData {P H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (t : TangentData P H) : LinearData P H H

Linear data, bundling coefficient, forcingMap, source.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.CommonCoverSolve.TangentData.anchoredSolve_projected_equation {P H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (t : TangentData P H) (g : Geometry) {a b : ℝ} (hab : a ≤ b) {U : Set P} (k : TorusInverse.Frequency) (hA : ContinuousOn t.linearData.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn t.linearData.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn t.source (U ×ˢ Set.univ)) {p : P} (hp : p ∈ U) (Y : TorusInverse.Plane) (s : ↑(Set.Icc a b)) : have z := (p, (g.coordinates k Y).1, ↑s); HasDerivAt (t.linearData.anchoredSolve g hab k (p, Y)) (TangentProjection.projectedRhs (t.normal z) (t.normalDot z) (t.linearData.anchoredSolve g hab k (p, Y) ↑s) ((t.action z) (t.linearData.anchoredSolve g hab k (p, Y) ↑s)) (t.source (p, g.path k Y ↑s)) (t.damping z)) ↑s

The concrete copy solve satisfies equation (27) with the source evaluated at the actual lifted earlier point, including the normal-motion term.

theorem NavierStokes.CommonCoverSolve.TangentData.copySolve_tangent {P H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (t : TangentData P H) (g : Geometry) {a b : ℝ} (hab : a ≤ b) {U : Set P} (k : TorusInverse.Frequency) (hA : ContinuousOn t.linearData.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn t.linearData.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn t.source (U ×ˢ Set.univ)) (hδ : ContinuousOn t.damping (U ×ˢ Set.univ)) {p : P} (hp : p ∈ U) (Y : TorusInverse.Plane) (hn0 : ∀ s ∈ Set.Icc a b, t.normal (p, (g.coordinates k Y).1, s) ≠ 0) (hn : ∀ s ∈ Set.Icc a b, HasDerivAt (fun (v : ℝ) => t.normal (p, (g.coordinates k Y).1, v)) (t.normalDot (p, (g.coordinates k Y).1, s)) s) (heta : (g.coordinates k Y).2 ∈ Set.Icc a b) : inner ℝ (t.normal (p, g.coordinates k Y)) (t.linearData.copySolve g hab k (p, Y)) = 0

Tangency of this constructed solution follows from the moving-normal defect equation and zero initial data.