Whole-lift bounds from the actual native copies

The copy meeting a point is allowed to depend on both the band and the point. Closed, locally finite support cells give a genuine zero germ on their complement, including all derivatives. Constants in the native estimates are chosen before the band, copy, and evaluation point.

The Gaussian error is assembled as the sum of cutoff-derivative terms plus one uncovered-source term. In particular, the source is never summed once for every inactive copy.

structure NavierStokes.PeriodizedWaveBounds.Cells (D : Type u_4) [TopologicalSpace D] (I : Type u_5) : Type (max u_4 u_5)

Closed support cells, with a unique cell at a point. Neither a finite index set nor one cell covering the whole strip is required.

• carrier : ℕ → I → Set D

  Carrier of Cells, of type ℕ → I → Set D.

• closed (n : ℕ) (i : I) : IsClosed (self.carrier n i)
• locallyFinite (n : ℕ) : LocallyFinite (self.carrier n)
• unique (n : ℕ) (i j : I) (x : D) : x ∈ self.carrier n i → x ∈ self.carrier n j → i = j

structure NavierStokes.PeriodizedWaveBounds.LocalJets {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {I : Type u_3} (s : WeightedClasses.StripData D) (w : ℕ → D → ℝ) (α : ℝ) (K : ℕ → I → Set D) (f : ℕ → I → D → E) : Prop

Native estimates on the actual functions. Smoothness is local at the closed support cell; no continuation of the uncut function around the torus is imposed. The weight is evaluated at the actual global point.

• smooth (n : ℕ) (i : I) (x : D) : x ∈ s.domain → x ∈ K n i → ContDiffAt ℝ (↑⊤) (f n i) x
• bounds (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (f n i) x‖ ≤ WeightedClasses.majorant s w α C p n x

theorem NavierStokes.PeriodizedWaveBounds.jets_eq_of_germ {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : D → E} {x : D} (h : f =ᶠ[nhds x] g) (m : ℕ) : iteratedFDeriv ℝ m f x = iteratedFDeriv ℝ m g x

theorem NavierStokes.PeriodizedWaveBounds.memClass_of_local_germs {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {I : Type u_3} {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {K : ℕ → I → Set D} {f : ℕ → I → D → E} {F : ℕ → D → E} (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) (hlocal : LocalJets s w α K f) (hcover : ∀ (n : ℕ), ∀ x ∈ s.domain, (∃ (i : I), x ∈ K n i ∧ F n =ᶠ[nhds x] f n i) ∨ F n =ᶠ[nhds x] fun (x : D) => 0) : WeightedClasses.MemClass s w α F

Gluing uses equality on neighborhoods, rather than equality of values or pointwise derivative limits.

noncomputable def NavierStokes.PeriodizedWaveBounds.copySum {D : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {I : Type u_3} (f : I → D → E) (x : D) : E

The actual locally finite copy sum. Local finiteness is proved from support cells below; it is not encoded by replacing the sum with a selector.

Equations

• NavierStokes.PeriodizedWaveBounds.copySum f x = ∑' (i : I), f i x

theorem NavierStokes.PeriodizedWaveBounds.zero_germ_of_support {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedAddCommGroup E] {K : Set D} (hK : IsClosed K) {f : D → E} (hf : Function.support f ⊆ K) {x : D} (hx : x ∉ K) : f =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.PeriodizedWaveBounds.copySum_germ {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedAddCommGroup E] {I : Type u_3} (K : Cells D I) (n : ℕ) (f : I → D → E) (hs : ∀ (i : I), Function.support (f i) ⊆ K.carrier n i) {i : I} {x : D} (hx : x ∈ K.carrier n i) : copySum f =ᶠ[nhds x] f i

theorem NavierStokes.PeriodizedWaveBounds.copySum_zero_germ {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedAddCommGroup E] {I : Type u_3} (K : Cells D I) (n : ℕ) (f : I → D → E) (hs : ∀ (i : I), Function.support (f i) ⊆ K.carrier n i) {x : D} (hx : ∀ (i : I), x ∉ K.carrier n i) : copySum f =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.PeriodizedWaveBounds.copySum_germ_cover {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedAddCommGroup E] {I : Type u_3} (K : Cells D I) (n : ℕ) (f : I → D → E) (hs : ∀ (i : I), Function.support (f i) ⊆ K.carrier n i) (x : D) : (∃ (i : I), x ∈ K.carrier n i ∧ copySum f =ᶠ[nhds x] f i) ∨ copySum f =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.PeriodizedWaveBounds.copySum_memClass {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {I : Type u_3} {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} (K : Cells D I) {f : ℕ → I → D → E} (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) (hs : ∀ (n : ℕ) (i : I), Function.support (f n i) ⊆ K.carrier n i) (hj : LocalJets s w α K.carrier f) : WeightedClasses.MemClass s w α fun (n : ℕ) => copySum (f n)

theorem NavierStokes.PeriodizedWaveBounds.copySum_jet_bound {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {I : Type u_3} (K : Cells D I) {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α C : ℝ} {p m : ℕ} (hC : 0 ≤ C) (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) {f : ℕ → I → D → E} (hs : ∀ (n : ℕ) (i : I), Function.support (f n i) ⊆ K.carrier n i) (hb : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K.carrier n i → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (f n i) x‖ ≤ WeightedClasses.majorant s w α C p n x) (n : ℕ) {x : D} (hx : x ∈ s.domain) (j : ℕ) (hj : j ≤ m) : ‖iteratedFDeriv ℝ j (copySum (f n)) x‖ ≤ WeightedClasses.majorant s w α C p n x

The proof also gives the very same prefix constants globally.

theorem NavierStokes.PeriodizedWaveBounds.copySum_support {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedAddCommGroup E] {I : Type u_3} (K : Cells D I) (n : ℕ) (f : I → D → E) (hs : ∀ (i : I), Function.support (f i) ⊆ K.carrier n i) : Function.support (copySum f) ⊆ ⋃ (i : I), K.carrier n i

theorem NavierStokes.PeriodizedWaveBounds.copySum_eventually_finite {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedAddCommGroup E] {I : Type u_3} (K : Cells D I) (n : ℕ) (f : I → D → E) (hs : ∀ (i : I), Function.support (f i) ⊆ K.carrier n i) (x : D) : ∃ (J : Finset I), copySum f =ᶠ[nhds x] fun (y : D) => ∑ i ∈ J, f i y

theorem NavierStokes.PeriodizedWaveBounds.copySum_tsupport {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedAddCommGroup E] {I : Type u_3} (K : Cells D I) (n : ℕ) (f : I → D → E) (hs : ∀ (i : I), Function.support (f i) ⊆ K.carrier n i) : tsupport (copySum f) ⊆ ⋃ (i : I), K.carrier n i

theorem NavierStokes.PeriodizedWaveBounds.copySum_translate {D : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {I : Type u_3} (f : I → D → E) (T : D → D) (e : I ≃ I) (h : ∀ (i : I) (x : D), f (e i) (T x) = f i x) (x : D) : copySum f (T x) = copySum f x

structure NavierStokes.PeriodizedWaveBounds.ComplementJets {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {I : Type u_3} (s : WeightedClasses.StripData D) (w : ℕ → D → ℝ) (α : ℝ) (K : ℕ → I → Set D) (f : ℕ → D → E) : Prop

Only the primitive source is estimated on the uncovered set. This is useful when coverage gives a small tail instead of an identically zero one.

• smooth (n : ℕ) (x : D) : x ∈ s.domain → (∀ (i : I), x ∉ K n i) → ContDiffAt ℝ (↑⊤) (f n) x
• bounds (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ), ∀ x ∈ s.domain, (∀ (i : I), x ∉ K n i) → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (f n) x‖ ≤ WeightedClasses.majorant s w α C p n x

theorem NavierStokes.PeriodizedWaveBounds.majorant_mono_constant {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (w : ℕ → D → ℝ) (α : ℝ) {C B : ℝ} (hCB : C ≤ B) (p n : ℕ) (x : D) (hw : 0 ≤ w n x) : WeightedClasses.majorant s w α C p n x ≤ WeightedClasses.majorant s w α B p n x

theorem NavierStokes.PeriodizedWaveBounds.memClass_of_local_and_complement_germs {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {I : Type u_3} {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {K : ℕ → I → Set D} {f : ℕ → I → D → E} {f₀ F : ℕ → D → E} (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) (hlocal : LocalJets s w α K f) (houtside : ComplementJets s w α K f₀) (hactive : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → F n =ᶠ[nhds x] f n i) (hinactive : ∀ (n : ℕ), ∀ x ∈ s.domain, (∀ (i : I), x ∉ K n i) → F n =ᶠ[nhds x] f₀ n) : WeightedClasses.MemClass s w α F

theorem NavierStokes.PeriodizedWaveBounds.source_zero_germ {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedAddCommGroup E] {I : Type u_3} (K : Cells D I) {f : ℕ → D → E} (hs : ∀ (n : ℕ), Function.support (f n) ⊆ ⋃ (i : I), K.carrier n i) {n : ℕ} {x : D} (hx : ∀ (i : I), x ∉ K.carrier n i) : f n =ᶠ[nhds x] fun (x : D) => 0

structure NavierStokes.PeriodizedWaveBounds.UniformLocalJets {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Type u_2} {I : Type u_3} (s : WeightedClasses.StripData D) (w : L → ℕ → D → ℝ) (α : ℝ) (K : L → ℕ → I → Set D) (f : L → ℕ → I → D → E) : Prop

Native bounds uniform also in an external spatial label. The lattice copy remains a separate index, so overlap among different labels is not mistaken for disjointness of copies of one label.

• smooth (l : L) (n : ℕ) (i : I) (x : D) : x ∈ s.domain → x ∈ K l n i → ContDiffAt ℝ (↑⊤) (f l n i) x
• bounds (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ), ∀ (l : L) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K l n i → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (f l n i) x‖ ≤ WeightedClasses.majorant s (w l) α C p n x

theorem NavierStokes.PeriodizedWaveBounds.UniformLocalJets.each {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Type u_2} {I : Type u_3} {s : WeightedClasses.StripData D} {w : L → ℕ → D → ℝ} {α : ℝ} {K : L → ℕ → I → Set D} {f : L → ℕ → I → D → E} (hf : UniformLocalJets s w α K f) (l : L) : LocalJets s (w l) α (K l) (f l)

theorem NavierStokes.PeriodizedWaveBounds.uniformClass_of_local_germs {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Type u_2} {I : Type u_3} {s : WeightedClasses.StripData D} {w : L → ℕ → D → ℝ} {α : ℝ} {K : L → ℕ → I → Set D} {f : L → ℕ → I → D → E} {F : L → ℕ → D → E} (hw : ∀ (l : L) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w l n x) (hj : UniformLocalJets s w α K f) (hcover : ∀ (l : L) (n : ℕ), ∀ x ∈ s.domain, (∃ (i : I), x ∈ K l n i ∧ F l n =ᶠ[nhds x] f l n i) ∨ F l n =ᶠ[nhds x] fun (x : D) => 0) : LabelSumBounds.UniformClass s w α F

theorem NavierStokes.PeriodizedWaveBounds.copySum_uniformClass {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Type u_2} {I : Type u_3} {s : WeightedClasses.StripData D} {w : L → ℕ → D → ℝ} {α : ℝ} (K : L → Cells D I) {f : L → ℕ → I → D → E} (hw : ∀ (l : L) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w l n x) (hs : ∀ (l : L) (n : ℕ) (i : I), Function.support (f l n i) ⊆ (K l).carrier n i) (hj : UniformLocalJets s w α (fun (l : L) => (K l).carrier) f) : LabelSumBounds.UniformClass s w α fun (l : L) (n : ℕ) => copySum (f l n)

noncomputable def NavierStokes.PeriodizedWaveBounds.nativeCell {P : Type} (g : CommonCoverSolve.Geometry) (K : Set TorusInverse.Plane) (k : TorusInverse.Frequency) : Set (P × TorusInverse.Plane)

Native cell, given by {z | g.coordinates k z.2 ∈ K}.

Equations

• NavierStokes.PeriodizedWaveBounds.nativeCell g K k = {z : P × NavierStokes.TorusInverse.Plane | g.coordinates k z.2 ∈ K}

theorem NavierStokes.PeriodizedWaveBounds.nativeCell_closed {P : Type} [NormedAddCommGroup P] (g : CommonCoverSolve.Geometry) {K : Set TorusInverse.Plane} (hK : IsClosed K) (k : TorusInverse.Frequency) : IsClosed (nativeCell g K k)

theorem NavierStokes.PeriodizedWaveBounds.nativeCell_locallyFinite {P : Type} [NormedAddCommGroup P] (g : CommonCoverSolve.Geometry) {K : Set TorusInverse.Plane} (hK : IsCompact K) : LocallyFinite (nativeCell g K)

Compact native cells have a locally finite family of all lattice copies. This applies to a rectangle as well as the actual closed cutoff support.

noncomputable def NavierStokes.PeriodizedWaveBounds.nativeCells {P : Type} [NormedAddCommGroup P] (g : ℕ → CommonCoverSolve.Geometry) (K : ℕ → Set TorusInverse.Plane) (hK : ∀ (n : ℕ), IsCompact (K n)) (hinj : ∀ (n : ℕ), Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (g n).center + (g n).basis z) '' K n)) : Cells (P × TorusInverse.Plane) TorusInverse.Frequency

Native cells, bundling carrier, closed, locallyFinite, unique.

Equations

• NavierStokes.PeriodizedWaveBounds.nativeCells g K hK hinj = { carrier := fun (n : ℕ) => NavierStokes.PeriodizedWaveBounds.nativeCell (g n) (K n), closed := ⋯, locallyFinite := ⋯, unique := ⋯ }

theorem NavierStokes.PeriodizedWaveBounds.native_cutoff_support {P : Type} (g : CommonCoverSolve.Geometry) {K : Set TorusInverse.Plane} {κ : TorusInverse.Plane → ℝ} (hκ : Function.support κ ⊆ K) (k : TorusInverse.Frequency) : (Function.support fun (z : P × TorusInverse.Plane) => κ (g.coordinates k z.2)) ⊆ nativeCell g K k

theorem NavierStokes.PeriodizedWaveBounds.native_localized_support {P E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : CommonCoverSolve.Geometry) {K : Set TorusInverse.Plane} {κ : TorusInverse.Plane → ℝ} (hκ : Function.support κ ⊆ K) (f : TorusInverse.Frequency → P × TorusInverse.Plane → E) (k : TorusInverse.Frequency) : (Function.support fun (z : P × TorusInverse.Plane) => κ (g.coordinates k z.2) • f k z) ⊆ nativeCell g K k

theorem NavierStokes.PeriodizedWaveBounds.periodizedCopies_memClass {P E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData (P × TorusInverse.Plane)} {w : ℕ → P × TorusInverse.Plane → ℝ} {α : ℝ} (g : ℕ → CommonCoverSolve.Geometry) (K : ℕ → Set TorusInverse.Plane) (hK : ∀ (n : ℕ), IsCompact (K n)) (hinj : ∀ (n : ℕ), Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (g n).center + (g n).basis z) '' K n)) (κ : ℕ → TorusInverse.Plane → ℝ) (hκ : ∀ (n : ℕ), Function.support (κ n) ⊆ K n) (f : ℕ → TorusInverse.Frequency → P × TorusInverse.Plane → E) (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) (hj : LocalJets s w α (fun (n : ℕ) => nativeCell (g n) (K n)) fun (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) => κ n ((g n).coordinates k x.2) • f n k x) : WeightedClasses.MemClass s w α fun (n : ℕ) => ParticularWaveBounds.periodizedCopies (g n) (κ n) (f n)

Whole-lift weighted bounds for the literal common-copy sum. The native smoothness and all-jet estimates are needed only on their own support cell.

theorem NavierStokes.PeriodizedWaveBounds.LocalJets.of_memClass {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {I : Type u_5} {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {K : ℕ → I → Set D} {f₀ : ℕ → D → E} (hf : WeightedClasses.MemClass s w α f₀) : LocalJets s w α K fun (n : ℕ) (x : I) => f₀ n

theorem NavierStokes.PeriodizedWaveBounds.LocalJets.map {D : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {I : Type u_5} {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {K : ℕ → I → Set D} {f : ℕ → I → D → E} (hf : LocalJets s w α K f) (L : E →L[ℝ] F) : LocalJets s w α K fun (n : ℕ) (i : I) (x : D) => L (f n i x)

theorem NavierStokes.PeriodizedWaveBounds.LocalJets.add {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {I : Type u_5} {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {K : ℕ → I → Set D} {f g : ℕ → I → D → E} (hf : LocalJets s w α K f) (hg : LocalJets s w α K g) (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) : LocalJets s w α K fun (n : ℕ) (i : I) (x : D) => f n i x + g n i x

theorem NavierStokes.PeriodizedWaveBounds.LocalJets.fderiv {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {I : Type u_5} {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {K : ℕ → I → Set D} {f : ℕ → I → D → E} (hf : LocalJets s w α K f) : LocalJets s w α K fun (n : ℕ) (i : I) => _root_.fderiv ℝ (f n i)

theorem NavierStokes.PeriodizedWaveBounds.LocalJets.bilinear {D : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {I : Type u_5} {s : WeightedClasses.StripData D} {w v : ℕ → D → ℝ} {α β : ℝ} {K : ℕ → I → Set D} {f : ℕ → I → D → E} {u : ℕ → I → D → F} (hf : LocalJets s w α K f) (hu : LocalJets s v β K u) (L : E →L[ℝ] F →L[ℝ] G) (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) (hv : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ v n x) : LocalJets s (fun (n : ℕ) (x : D) => w n x * v n x) (α + β) K fun (n : ℕ) (i : I) (x : D) => (L (f n i x)) (u n i x)

theorem NavierStokes.PeriodizedWaveBounds.LocalJets.smul {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {I : Type u_5} {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {K : ℕ → I → Set D} {f : ℕ → I → D → E} {r : ℕ → I → D → ℝ} (hr : LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K r) (hf : LocalJets s w α K f) (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) : LocalJets s w α K fun (n : ℕ) (i : I) (x : D) => r n i x • f n i x

theorem NavierStokes.PeriodizedWaveBounds.LocalJets.band_smul {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {I : Type u_5} {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {K : ℕ → I → Set D} {f : ℕ → I → D → E} {r : ℕ → ℝ} (hf : LocalJets s w α K f) (hr : WeightedClasses.BandBound s 0 r) (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) : LocalJets s w α K fun (n : ℕ) (i : I) (x : D) => r n • f n i x

theorem NavierStokes.PeriodizedWaveBounds.local_gaussian_tail_bound {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {I : Type u_3} {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {W : ℕ → D → ℝ} {α c : ℝ} {f : ℕ → I → D → E} (hf : LocalJets s (fun (n : ℕ) (x : D) => √(s.zeta x) * W n x) α K f) (edges : GaussianTailFlat.FlatEdges s) (scales : GaussianTailFlat.BandScaleControl s) (θ : ℕ → I → D → ℝ) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 0 < L n) (ell : ℝ) (hell : 0 < ell) (hLell : ∀ (n : ℕ), ell * ChartScales.S n ≤ L n) (hc : 0 < c) (hW : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → W n x ≤ Real.exp (-c * (θ n i x - 1 / 2) ^ 2 * L n)) (hzero : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → |θ n i x - 1 / 2| < 1 / 5 → f n i =ᶠ[nhds x] fun (x : D) => 0) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (f n i) x‖ ≤ C * (1 + ChartScales.S n) ^ p * Real.exp (-(c * ell / 50) * ChartScales.S n)

The Gaussian absorption argument is uniform in the native copy. Its only local field estimate is the weighted jet bound before absorption.

theorem NavierStokes.PeriodizedWaveBounds.local_gaussian_all_gains {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {I : Type u_3} {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {W : ℕ → D → ℝ} {α c : ℝ} {f : ℕ → I → D → E} (hf : LocalJets s (fun (n : ℕ) (x : D) => √(s.zeta x) * W n x) α K f) (edges : GaussianTailFlat.FlatEdges s) (scales : GaussianTailFlat.BandScaleControl s) (θ : ℕ → I → D → ℝ) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 0 < L n) (ell : ℝ) (hell : 0 < ell) (hLell : ∀ (n : ℕ), ell * ChartScales.S n ≤ L n) (hc : 0 < c) (hW : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → W n x ≤ Real.exp (-c * (θ n i x - 1 / 2) ^ 2 * L n)) (hzero : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → |θ n i x - 1 / 2| < 1 / 5 → f n i =ᶠ[nhds x] fun (x : D) => 0) (β : ℝ) : LocalJets s (fun (x : ℕ) (x_1 : D) => 1) β K f

theorem NavierStokes.PeriodizedWaveBounds.principal_germ {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {a b : D → HarmonicCalculus.ComplexVector} {p q : D → ℂ} {x : D} (ha : a =ᶠ[nhds x] b) (hp : p =ᶠ[nhds x] q) (ε K : ℝ) (R F G Φ : D → ℝ) (Vr Vθ Vz Vf : D → D) : LinearWaveResidual.principal ε K R F G Vr Vθ Vz Vf Φ a p =ᶠ[nhds x] LinearWaveResidual.principal ε K R F G Vr Vθ Vz Vf Φ b q

theorem NavierStokes.PeriodizedWaveBounds.remainder_germ {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {a b : D → HarmonicCalculus.ComplexVector} {p q : D → ℂ} {x : D} (ha : a =ᶠ[nhds x] b) (hp : p =ᶠ[nhds x] q) (ε K : ℝ) (R B F G Φ : D → ℝ) (Vr Vθ Vz Vf Vs : D → D) : LinearWaveResidual.remainder ε K R B F G Vr Vθ Vz Vf Vs Φ a p =ᶠ[nhds x] LinearWaveResidual.remainder ε K R B F G Vr Vθ Vz Vf Vs Φ b q

theorem NavierStokes.PeriodizedWaveBounds.curlCorrection_germ {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {a b : D → HarmonicCalculus.ComplexVector} {x : D} (ha : a =ᶠ[nhds x] b) (K : ℝ) (R Φ : D → ℝ) (Vr Vθ Vz : D → D) : CurlClassBounds.curlRemainder K R Vr Vθ Vz (CurlClassBounds.coefficient R Vr Vθ Vz Φ a) =ᶠ[nhds x] CurlClassBounds.curlRemainder K R Vr Vθ Vz (CurlClassBounds.coefficient R Vr Vθ Vz Φ b)

theorem NavierStokes.PeriodizedWaveBounds.potential_germ {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {a b : D → HarmonicCalculus.ComplexVector} {x : D} (ha : a =ᶠ[nhds x] b) (K : ℝ) (R Φ : D → ℝ) (Vr Vθ Vz : D → D) : CurlClassBounds.vectorPotential K R Vr Vθ Vz Φ a =ᶠ[nhds x] CurlClassBounds.vectorPotential K R Vr Vθ Vz Φ b

theorem NavierStokes.PeriodizedWaveBounds.divergence_germ {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {a b : D → HarmonicCalculus.ComplexVector} {x : D} (ha : a =ᶠ[nhds x] b) (R : D → ℝ) (Vr Vθ Vz : D → D) : HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz a =ᶠ[nhds x] HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz b

@[simp]

theorem NavierStokes.PeriodizedWaveBounds.normalCoefficient_zero (N : CurlClassBounds.RealVector) : CurlClassBounds.normalCoefficient N 0 = 0

@[simp]

theorem NavierStokes.PeriodizedWaveBounds.coefficient_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R Φ : D → ℝ) (Vr Vθ Vz : D → D) : (CurlClassBounds.coefficient R Vr Vθ Vz Φ fun (x : D) => 0) = fun (x : D) => 0

@[simp]

theorem NavierStokes.PeriodizedWaveBounds.cylindricalCurl_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vθ Vz : D → D) : (CurlClassBounds.cylindricalCurl R Vr Vθ Vz fun (x : D) => 0) = fun (x : D) => 0

@[simp]

theorem NavierStokes.PeriodizedWaveBounds.curlRemainder_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (K : ℝ) (R : D → ℝ) (Vr Vθ Vz : D → D) : (CurlClassBounds.curlRemainder K R Vr Vθ Vz fun (x : D) => 0) = fun (x : D) => 0

@[simp]

theorem NavierStokes.PeriodizedWaveBounds.realizedCoefficient_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (K : ℝ) (R Φ : D → ℝ) (Vr Vθ Vz : D → D) : (CurlClassBounds.realizedCoefficient K R Vr Vθ Vz Φ fun (x : D) => 0) = fun (x : D) => 0

@[simp]

theorem NavierStokes.PeriodizedWaveBounds.vectorPotential_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (K : ℝ) (R Φ : D → ℝ) (Vr Vθ Vz : D → D) : (CurlClassBounds.vectorPotential K R Vr Vθ Vz Φ fun (x : D) => 0) = fun (x : D) => 0

@[simp]

theorem NavierStokes.PeriodizedWaveBounds.principal_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (ε K : ℝ) (R F G Φ : D → ℝ) (Vr Vθ Vz Vf : D → D) : (LinearWaveResidual.principal ε K R F G Vr Vθ Vz Vf Φ (fun (x : D) => 0) fun (x : D) => 0) = fun (x : D) => 0

@[simp]

theorem NavierStokes.PeriodizedWaveBounds.along_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (V : D → D) : (HarmonicCalculus.along V fun (x : D) => 0) = fun (x : D) => 0

@[simp]

theorem NavierStokes.PeriodizedWaveBounds.remainder_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (ε K : ℝ) (R B F G Φ : D → ℝ) (Vr Vθ Vz Vf Vs : D → D) : (LinearWaveResidual.remainder ε K R B F G Vr Vθ Vz Vf Vs Φ (fun (x : D) => 0) fun (x : D) => 0) = fun (x : D) => 0

@[simp]

theorem NavierStokes.PeriodizedWaveBounds.linearResidual_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (ε : ℝ) (R : D → ℝ) (Vr Vθ Vz Vt : D → D) (B : D → HarmonicCalculus.ComplexVector) : (LinearWaveResidual.linearResidual ε R Vr Vθ Vz Vt B (fun (x : D) => 0) fun (x : D) => 0) = fun (x : D) => 0

@[simp]

theorem NavierStokes.PeriodizedWaveBounds.cylindricalDivergence_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vθ Vz : D → D) : (HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz fun (x : D) => 0) = fun (x : D) => 0

structure NavierStokes.PeriodizedWaveBounds.CopyData (D I : Type) : Type

Local raw copies share one physical carrier and background. Their amplitudes and pressures may differ in every copy and need not be periodic.

• background : LinearWaveBounds.WaveCoefficients D

  Background of CopyData, of type WaveCoefficients D.

• amplitude : ℕ → I → D → HarmonicCalculus.ComplexVector

  Amplitude of CopyData, of type ℕ → I → D → ComplexVector.

• pressure : ℕ → I → D → ℂ

  Pressure field of CopyData, of type ℕ → I → D → ℂ.

• cutoff : ℕ → I → D → ℝ

  Cutoff of CopyData, of type ℕ → I → D → ℝ.

• source : ℕ → D → HarmonicCalculus.ComplexVector

  Source of CopyData, of type ℕ → D → ComplexVector.

noncomputable def NavierStokes.PeriodizedWaveBounds.CopyData.raw {D I : Type} (a : CopyData D I) (i : I) : LinearWaveBounds.WaveCoefficients D

Raw, given by { a.background with amplitude := fun n => a.amplitude n i pressure := fun n => a.pressure n i }.

Equations

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

noncomputable def NavierStokes.PeriodizedWaveBounds.CopyData.localized {D I : Type} (a : CopyData D I) (i : I) : LinearWaveBounds.WaveCoefficients D

Localized, given by (a.raw i).withCutoff (fun n => a.cutoff n i).

Equations

• a.localized i = (a.raw i).withCutoff fun (n : ℕ) => a.cutoff n i

noncomputable def NavierStokes.PeriodizedWaveBounds.CopyData.corrected {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (i : I) : LinearWaveBounds.WaveCoefficients D

Corrected, given by (a.raw i).corrected s d (fun n => a.cutoff n i).

Equations

• a.corrected s d i = (a.raw i).corrected s d fun (n : ℕ) => a.cutoff n i

noncomputable def NavierStokes.PeriodizedWaveBounds.CopyData.localGood {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) (i : I) : D → HarmonicCalculus.ComplexVector

Local good, given by (a.raw i).constructedGood s d (fun n => a.cutoff n i) n.

Equations

• a.localGood s d n i = (a.raw i).constructedGood s d (fun (n : ℕ) => a.cutoff n i) n

noncomputable def NavierStokes.PeriodizedWaveBounds.CopyData.localTail {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) (i : I) (x : D) : HarmonicCalculus.ComplexVector

Local tail, given by d.Dfast (fun n => a.cutoff n i) n x • a.amplitude n i x.

Equations

• a.localTail d n i x = d.Dfast (fun (n : ℕ) => a.cutoff n i) n x • a.amplitude n i x

noncomputable def NavierStokes.PeriodizedWaveBounds.CopyData.localGaussian {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) (i : I) : D → HarmonicCalculus.ComplexVector

Local gaussian, given by excludedSlotError d (fun n => a.cutoff n i) (fun n => a.amplitude n i) a.source n.

Equations

• a.localGaussian d n i = NavierStokes.LinearWaveBounds.excludedSlotError d (fun (n : ℕ) => a.cutoff n i) (fun (n : ℕ) => a.amplitude n i) a.source n

noncomputable def NavierStokes.PeriodizedWaveBounds.CopyData.common {D I : Type} (a : CopyData D I) : LinearWaveBounds.WaveCoefficients D

The single native cutoff is applied before periodization and curl.

Equations

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

noncomputable def NavierStokes.PeriodizedWaveBounds.CopyData.commonCorrected {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) : LinearWaveBounds.WaveCoefficients D

Common corrected, given by a.common.addAmplitude (a.common.curlCorrection s d).

Equations

• a.commonCorrected s d = a.common.addAmplitude (a.common.curlCorrection s d)

noncomputable def NavierStokes.PeriodizedWaveBounds.CopyData.globalGood {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) : D → HarmonicCalculus.ComplexVector

An actual global good coefficient, assembled from the cutoff-and-curl formula on each native copy.

Equations

• a.globalGood s d n = NavierStokes.PeriodizedWaveBounds.copySum (a.localGood s d n)

noncomputable def NavierStokes.PeriodizedWaveBounds.CopyData.cutoffSum {D I : Type} (a : CopyData D I) (n : ℕ) : D → ℝ

Cutoff sum, given by copySum (a.cutoff n).

Equations

• a.cutoffSum n = NavierStokes.PeriodizedWaveBounds.copySum (a.cutoff n)

noncomputable def NavierStokes.PeriodizedWaveBounds.CopyData.globalTail {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) : D → HarmonicCalculus.ComplexVector

Global tail, given by copySum (a.localTail d n).

Equations

• a.globalTail d n = NavierStokes.PeriodizedWaveBounds.copySum (a.localTail d n)

noncomputable def NavierStokes.PeriodizedWaveBounds.CopyData.globalGaussian {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) (x : D) : HarmonicCalculus.ComplexVector

The shared source occurs once. This definition also makes sense off every native patch and preserves the uncovered-source term there.

Equations

• a.globalGaussian d n x = a.globalTail d n x + (1 - a.cutoffSum n x) • a.source n x

theorem NavierStokes.PeriodizedWaveBounds.CopyData.localGaussian_eq {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) (i : I) (x : D) : a.localGaussian d n i x = a.localTail d n i x + (1 - a.cutoff n i x) • a.source n x

theorem NavierStokes.PeriodizedWaveBounds.CopyData.common_amplitude_germ {D I : Type} [NormedAddCommGroup D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (n : ℕ) {i : I} {x : D} (hx : x ∈ K.carrier n i) : a.common.amplitude n =ᶠ[nhds x] (a.localized i).amplitude n

theorem NavierStokes.PeriodizedWaveBounds.CopyData.common_pressure_germ {D I : Type} [NormedAddCommGroup D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (n : ℕ) {i : I} {x : D} (hx : x ∈ K.carrier n i) : a.common.pressure n =ᶠ[nhds x] (a.localized i).pressure n

theorem NavierStokes.PeriodizedWaveBounds.CopyData.commonCorrected_amplitude_germ {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) {i : I} {x : D} (hx : x ∈ K.carrier n i) : (a.commonCorrected s d).amplitude n =ᶠ[nhds x] (a.corrected s d i).amplitude n

theorem NavierStokes.PeriodizedWaveBounds.CopyData.commonCorrected_residual_germ {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) {i : I} {x : D} (hx : x ∈ K.carrier n i) : (a.commonCorrected s d).harmonicResidual s d n =ᶠ[nhds x] (a.corrected s d i).harmonicResidual s d n

theorem NavierStokes.PeriodizedWaveBounds.CopyData.localized_amplitude_support {D I : Type} [NormedAddCommGroup D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (n : ℕ) (i : I) : Function.support ((a.localized i).amplitude n) ⊆ K.carrier n i

theorem NavierStokes.PeriodizedWaveBounds.CopyData.localized_pressure_support {D I : Type} [NormedAddCommGroup D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (n : ℕ) (i : I) : Function.support ((a.localized i).pressure n) ⊆ K.carrier n i

theorem NavierStokes.PeriodizedWaveBounds.CopyData.localized_zero_germs {D I : Type} [NormedAddCommGroup D] (a : CopyData D I) {n : ℕ} {i : I} {x : D} (hψ : a.cutoff n i =ᶠ[nhds x] fun (x : D) => 0) : ((a.localized i).amplitude n =ᶠ[nhds x] fun (x : D) => 0) ∧ (a.localized i).pressure n =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.PeriodizedWaveBounds.CopyData.localized_correction_zero_germ {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) {n : ℕ} {i : I} {x : D} (hψ : a.cutoff n i =ᶠ[nhds x] fun (x : D) => 0) : (a.localized i).curlCorrection s d n =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.PeriodizedWaveBounds.CopyData.corrected_zero_germ {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) {n : ℕ} {i : I} {x : D} (hψ : a.cutoff n i =ᶠ[nhds x] fun (x : D) => 0) : (a.corrected s d i).amplitude n =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.PeriodizedWaveBounds.CopyData.localGood_zero_germ {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) {n : ℕ} {i : I} {x : D} (hψ : a.cutoff n i =ᶠ[nhds x] fun (x : D) => 0) : a.localGood s d n i =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.PeriodizedWaveBounds.CopyData.localTail_zero_germ {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (d : LinearWaveBounds.GraphDirections D) {n : ℕ} {i : I} {x : D} (hψ : a.cutoff n i =ᶠ[nhds x] fun (x : D) => 0) : a.localTail d n i =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.PeriodizedWaveBounds.CopyData.localGood_support {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) (i : I) : Function.support (a.localGood s d n i) ⊆ K.carrier n i

theorem NavierStokes.PeriodizedWaveBounds.CopyData.localTail_support {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) (i : I) : Function.support (a.localTail d n i) ⊆ K.carrier n i

theorem NavierStokes.PeriodizedWaveBounds.CopyData.corrected_support {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) (i : I) : Function.support ((a.corrected s d i).amplitude n) ⊆ K.carrier n i

theorem NavierStokes.PeriodizedWaveBounds.CopyData.common_zero_germs {D I : Type} [NormedAddCommGroup D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) {n : ℕ} {x : D} (hx : ∀ (i : I), x ∉ K.carrier n i) : (a.common.amplitude n =ᶠ[nhds x] fun (x : D) => 0) ∧ a.common.pressure n =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.PeriodizedWaveBounds.CopyData.commonCorrected_zero_germ {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) {n : ℕ} {x : D} (hx : ∀ (i : I), x ∉ K.carrier n i) : (a.commonCorrected s d).amplitude n =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.PeriodizedWaveBounds.CopyData.commonResidual_zero_germ {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) {n : ℕ} {x : D} (hx : ∀ (i : I), x ∉ K.carrier n i) : (a.commonCorrected s d).harmonicResidual s d n =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.PeriodizedWaveBounds.CopyData.globalGood_germ {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) {i : I} {x : D} (hx : x ∈ K.carrier n i) : a.globalGood s d n =ᶠ[nhds x] a.localGood s d n i

theorem NavierStokes.PeriodizedWaveBounds.CopyData.globalGood_zero_germ {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) {n : ℕ} {x : D} (hx : ∀ (i : I), x ∉ K.carrier n i) : a.globalGood s d n =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.PeriodizedWaveBounds.CopyData.globalGaussian_germ {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) {i : I} {x : D} (hx : x ∈ K.carrier n i) : a.globalGaussian d n =ᶠ[nhds x] a.localGaussian d n i

The global Gaussian field has the full native error as its germ, with both terms and all cutoff derivatives unchanged.

theorem NavierStokes.PeriodizedWaveBounds.CopyData.globalGaussian_uncovered_germ {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (d : LinearWaveBounds.GraphDirections D) {n : ℕ} {x : D} (hx : ∀ (i : I), x ∉ K.carrier n i) : a.globalGaussian d n =ᶠ[nhds x] a.source n

The exact uncovered-source term persists outside the cutoff cells.

theorem NavierStokes.PeriodizedWaveBounds.CopyData.common_cancellation {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (hlocal : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K.carrier n i → ((a.corrected s d i).harmonicResidual s d n x + fun (j : Fin 3) => a.source n x j * HarmonicCalculus.carrier (a.background.frequency n) (a.background.phase n) x) = fun (j : Fin 3) => (a.localGood s d n i x j + a.localGaussian d n i x j) * HarmonicCalculus.carrier (a.background.frequency n) (a.background.phase n) x) (n : ℕ) {x : D} (hx : x ∈ s.domain) : ((a.commonCorrected s d).harmonicResidual s d n x + fun (j : Fin 3) => a.source n x j * HarmonicCalculus.carrier (a.background.frequency n) (a.background.phase n) x) = fun (j : Fin 3) => (a.globalGood s d n x j + a.globalGaussian d n x j) * HarmonicCalculus.carrier (a.background.frequency n) (a.background.phase n) x

Local native cancellation implies cancellation everywhere on the whole lift. The source need not vanish on the uncovered complement.

theorem NavierStokes.PeriodizedWaveBounds.CopyData.common_classes {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α β : ℝ} (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) (ha : LocalJets s w α K.carrier fun (n : ℕ) (i : I) => (a.localized i).amplitude n) (hp : LocalJets s w β K.carrier fun (n : ℕ) (i : I) => (a.localized i).pressure n) : WeightedClasses.MemClass s w α a.common.amplitude ∧ WeightedClasses.MemClass s w β a.common.pressure

Global classes for the actually localized common velocity and pressure. The input fields need be smooth only at their own native support cells.

theorem NavierStokes.PeriodizedWaveBounds.CopyData.commonCorrected_class_of_native {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) {s : WeightedClasses.StripData D} (d : LinearWaveBounds.GraphDirections D) {w : ℕ → D → ℝ} {α : ℝ} (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) (ha : LocalJets s w α K.carrier fun (n : ℕ) (i : I) => (a.corrected s d i).amplitude n) : WeightedClasses.MemClass s w α (a.commonCorrected s d).amplitude

theorem NavierStokes.PeriodizedWaveBounds.CopyData.globalGood_class_of_native {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) {s : WeightedClasses.StripData D} (d : LinearWaveBounds.GraphDirections D) {w : ℕ → D → ℝ} {α : ℝ} (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) (hg : LocalJets s w α K.carrier (a.localGood s d)) : WeightedClasses.MemClass s w α (a.globalGood s d)

theorem NavierStokes.PeriodizedWaveBounds.CopyData.globalGaussian_class_of_covered_source {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (hsource : ∀ (n : ℕ), Function.support (a.source n) ⊆ ⋃ (i : I), K.carrier n i) {s : WeightedClasses.StripData D} (d : LinearWaveBounds.GraphDirections D) {w : ℕ → D → ℝ} {α : ℝ} (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) (hg : LocalJets s w α K.carrier (a.localGaussian d)) : WeightedClasses.MemClass s w α (a.globalGaussian d)

If the literal incoming source is supported in the union of native cores, the global Gaussian error is flat whenever the native error jets are uniformly flat. No global error class is assumed.

theorem NavierStokes.PeriodizedWaveBounds.CopyData.globalGaussian_class_with_complement {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) {s : WeightedClasses.StripData D} (d : LinearWaveBounds.GraphDirections D) {w : ℕ → D → ℝ} {α : ℝ} (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) (hg : LocalJets s w α K.carrier (a.localGaussian d)) (hf : ComplementJets s w α K.carrier a.source) : WeightedClasses.MemClass s w α (a.globalGaussian d)

A nonzero uncovered source is retained and estimated from its own primitive jets on that complement.

theorem NavierStokes.PeriodizedWaveBounds.CopyData.globalGaussian_of_source_zero {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (d : LinearWaveBounds.GraphDirections D) (hf : a.source = fun (x : ℕ) (x_1 : D) => 0) : a.globalGaussian d = a.globalTail d

The homogeneous construction has only the periodized derivative tail.

theorem NavierStokes.PeriodizedWaveBounds.CopyData.globalGood_support {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) : Function.support (a.globalGood s d n) ⊆ ⋃ (i : I), K.carrier n i

theorem NavierStokes.PeriodizedWaveBounds.CopyData.globalGaussian_support {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (hsource : ∀ (n : ℕ), Function.support (a.source n) ⊆ ⋃ (i : I), K.carrier n i) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) : Function.support (a.globalGaussian d n) ⊆ ⋃ (i : I), K.carrier n i

noncomputable def NavierStokes.PeriodizedWaveBounds.CopyData.differentialGood {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) (x : D) : HarmonicCalculus.ComplexVector

The global differential formula corresponding to the sum of native good terms. Its equality with that sum is proved from actual germs.

Equations

• a.differentialGood s d n x = a.common.principalVelocity s d (a.common.curlCorrection s d) n x + (a.commonCorrected s d).remainder s d n x

theorem NavierStokes.PeriodizedWaveBounds.CopyData.differentialGood_germ {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) {i : I} {x : D} (hx : x ∈ K.carrier n i) : a.differentialGood s d n =ᶠ[nhds x] a.localGood s d n i

theorem NavierStokes.PeriodizedWaveBounds.CopyData.differentialGood_zero_germ {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) {n : ℕ} {x : D} (hx : ∀ (i : I), x ∉ K.carrier n i) : a.differentialGood s d n =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.PeriodizedWaveBounds.CopyData.globalGood_eq_differentialGood {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) : a.globalGood s d = a.differentialGood s d

noncomputable def NavierStokes.PeriodizedWaveBounds.CopyData.backgroundOnly {D I : Type} (a : CopyData D I) : LinearWaveBounds.WaveCoefficients D

Only the carrier, geometry, and base fields of this coefficient are used in the background estimates.

Equations

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

theorem NavierStokes.PeriodizedWaveBounds.CopyData.common_inputBounds {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) {s : WeightedClasses.StripData D} {d : LinearWaveBounds.GraphDirections D} {W : ℕ → D → ℝ} {α κ : ℝ} (hb : LinearWaveBounds.InputBounds s W α κ d a.backgroundOnly) (ha : LocalJets s (fun (n : ℕ) (x : D) => √(s.zeta x) * W n x) α K.carrier fun (n : ℕ) (i : I) => (a.localized i).amplitude n) (hp : LocalJets s (fun (n : ℕ) (x : D) => √(s.zeta x) * W n x) (α + 1 / 2) K.carrier fun (n : ℕ) (i : I) => (a.localized i).pressure n) : LinearWaveBounds.InputBounds s W α κ d a.common

theorem NavierStokes.PeriodizedWaveBounds.CopyData.common_bounds_from_native {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) {s : WeightedClasses.StripData D} {d : LinearWaveBounds.GraphDirections D} {W : ℕ → D → ℝ} {α κ : ℝ} (hb : LinearWaveBounds.InputBounds s W α κ d a.backgroundOnly) (ha : LocalJets s (fun (n : ℕ) (x : D) => √(s.zeta x) * W n x) α K.carrier fun (n : ℕ) (i : I) => (a.localized i).amplitude n) (hp : LocalJets s (fun (n : ℕ) (x : D) => √(s.zeta x) * W n x) (α + 1 / 2) K.carrier fun (n : ℕ) (i : I) => (a.localized i).pressure n) (hκ : κ ≤ 1 / 2) {R : D → ℝ} (hR : a.background.radius = fun (x : ℕ) => R) (hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) (a.background.normal s d)) {b M : ℝ} (hpos : 0 < b) (hlower : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖a.background.normal s d n x‖) (hupper : ∀ (n : ℕ), ∀ x ∈ s.domain, ‖a.background.normal s d n x‖ ≤ M) (hK : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / a.background.frequency n) : WeightedClasses.WaveClass s W α a.common.amplitude ∧ WeightedClasses.WaveClass s W α (a.commonCorrected s d).amplitude ∧ WeightedClasses.WaveClass s W (α + 1 / 2) a.common.pressure ∧ WeightedClasses.WaveClass s W (α + 1 / 2 - κ) (a.common.curlCorrection s d) ∧ WeightedClasses.WaveClass s W (α + 1 / 2 - 3 * κ) (a.globalGood s d)

Primitive background estimates and native localized velocity/pressure jets imply the actual global curl correction and good-remainder classes. Neither a local nor a global remainder-class hypothesis is used.

theorem NavierStokes.PeriodizedWaveBounds.CopyData.localGaussian_wave_jets {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) {s : WeightedClasses.StripData D} (d : LinearWaveBounds.GraphDirections D) {K : ℕ → I → Set D} {w : ℕ → D → ℝ} {α : ℝ} (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) (hψ : LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K a.cutoff) (hfast : WeightedClasses.BandBound s 0 d.fastScale) (hu : LocalJets s w α K a.amplitude) (hf : LocalJets s w α K fun (n : ℕ) (x : I) => a.source n) : LocalJets s w α K (a.localGaussian d)

theorem NavierStokes.PeriodizedWaveBounds.CopyData.localGaussian_zero_of_cutoff_one {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (d : LinearWaveBounds.GraphDirections D) {n : ℕ} {i : I} {x : D} (hψ : a.cutoff n i =ᶠ[nhds x] fun (x : D) => 1) : a.localGaussian d n i =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.PeriodizedWaveBounds.CopyData.localGaussian_zero_of_fields {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (d : LinearWaveBounds.GraphDirections D) {n : ℕ} {i : I} {x : D} (hu : a.amplitude n i =ᶠ[nhds x] fun (x : D) => 0) (hf : a.source n =ᶠ[nhds x] fun (x : D) => 0) : a.localGaussian d n i =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.PeriodizedWaveBounds.CopyData.localGaussian_all_gains_from_native {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) {s : WeightedClasses.StripData D} (d : LinearWaveBounds.GraphDirections D) {K : ℕ → I → Set D} {W : ℕ → D → ℝ} {α c : ℝ} (hWnonneg : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W n x) (hψ : LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K a.cutoff) (hfast : WeightedClasses.BandBound s 0 d.fastScale) (hu : LocalJets s (fun (n : ℕ) (x : D) => √(s.zeta x) * W n x) α K a.amplitude) (hf : LocalJets s (fun (n : ℕ) (x : D) => √(s.zeta x) * W n x) α K fun (n : ℕ) (x : I) => a.source n) (edges : GaussianTailFlat.FlatEdges s) (scales : GaussianTailFlat.BandScaleControl s) (θ : ℕ → I → D → ℝ) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 0 < L n) (ell : ℝ) (hell : 0 < ell) (hLell : ∀ (n : ℕ), ell * ChartScales.S n ≤ L n) (hc : 0 < c) (hW : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → W n x ≤ Real.exp (-c * (θ n i x - 1 / 2) ^ 2 * L n)) (hcentral : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → |θ n i x - 1 / 2| < 1 / 5 → (a.cutoff n i =ᶠ[nhds x] fun (x : D) => 1) ∨ (a.amplitude n i =ᶠ[nhds x] fun (x : D) => 0) ∧ a.source n =ᶠ[nhds x] fun (x : D) => 0) (β : ℝ) : LocalJets s (fun (x : ℕ) (x_1 : D) => 1) β K (a.localGaussian d)

Primitive native amplitude/source/cutoff jets and a Gaussian envelope prove flatness of the actual two cutoff products, uniformly over every copy. The central alternative allows transverse regions where both fields vanish.

theorem NavierStokes.PeriodizedWaveBounds.CopyData.globalGaussian_all_gains_from_native {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (hsource : ∀ (n : ℕ), Function.support (a.source n) ⊆ ⋃ (i : I), K.carrier n i) {s : WeightedClasses.StripData D} (d : LinearWaveBounds.GraphDirections D) {W : ℕ → D → ℝ} {α c : ℝ} (hWnonneg : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W n x) (hψ : LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K.carrier a.cutoff) (hfast : WeightedClasses.BandBound s 0 d.fastScale) (hu : LocalJets s (fun (n : ℕ) (x : D) => √(s.zeta x) * W n x) α K.carrier a.amplitude) (hf : LocalJets s (fun (n : ℕ) (x : D) => √(s.zeta x) * W n x) α K.carrier fun (n : ℕ) (x : I) => a.source n) (edges : GaussianTailFlat.FlatEdges s) (scales : GaussianTailFlat.BandScaleControl s) (θ : ℕ → I → D → ℝ) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 0 < L n) (ell : ℝ) (hell : 0 < ell) (hLell : ∀ (n : ℕ), ell * ChartScales.S n ≤ L n) (hc : 0 < c) (hW : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K.carrier n i → W n x ≤ Real.exp (-c * (θ n i x - 1 / 2) ^ 2 * L n)) (hcentral : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K.carrier n i → |θ n i x - 1 / 2| < 1 / 5 → (a.cutoff n i =ᶠ[nhds x] fun (x : D) => 1) ∨ (a.amplitude n i =ᶠ[nhds x] fun (x : D) => 0) ∧ a.source n =ᶠ[nhds x] fun (x : D) => 0) (β : ℝ) : WeightedClasses.UnweightedClass s β (a.globalGaussian d)

The whole-lift Gaussian estimate derives every native output jet from primitive data, then glues using the actual periodized fields and source coverage. No Gaussian error class is an input.

theorem NavierStokes.PeriodizedWaveBounds.CopyData.common_potential_germ {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) {i : I} {x : D} (hx : x ∈ K.carrier n i) : a.common.curlPotential s d n =ᶠ[nhds x] (a.localized i).curlPotential s d n

theorem NavierStokes.PeriodizedWaveBounds.CopyData.common_potential_zero_germ {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) {n : ℕ} {x : D} (hx : ∀ (i : I), x ∉ K.carrier n i) : a.common.curlPotential s d n =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.PeriodizedWaveBounds.CopyData.common_realizes_curl {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (hnative : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K.carrier n i → CurlClassBounds.cylindricalCurl (a.background.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n) ((a.localized i).curlPotential s d n) x = HarmonicCalculus.vectorMode (a.background.frequency n) (a.background.phase n) ((a.corrected s d i).amplitude n) x) (n : ℕ) {x : D} (hx : x ∈ s.domain) : CurlClassBounds.cylindricalCurl (a.background.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n) (a.common.curlPotential s d n) x = HarmonicCalculus.vectorMode (a.background.frequency n) (a.background.phase n) ((a.commonCorrected s d).amplitude n) x

The globally assembled velocity is the actual curl of the globally assembled potential whenever the native construction has that identity.

theorem NavierStokes.PeriodizedWaveBounds.CopyData.common_divergence_zero {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (K : Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (hnative : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K.carrier n i → HarmonicCalculus.cylindricalDivergence (a.background.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n) (HarmonicCalculus.vectorMode (a.background.frequency n) (a.background.phase n) ((a.corrected s d i).amplitude n)) x = 0) (n : ℕ) {x : D} (hx : x ∈ s.domain) : HarmonicCalculus.cylindricalDivergence (a.background.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n) (HarmonicCalculus.vectorMode (a.background.frequency n) (a.background.phase n) ((a.commonCorrected s d).amplitude n)) x = 0

A local differential identity is transported through full neighborhood germs, so the support boundary contributes no extra divergence.

theorem NavierStokes.PeriodizedWaveBounds.CopyData.common_amplitude_invariant {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (v : D) (hψ : ∀ (n : ℕ) (i : I), CopyAngularInvariance.Invariant v (a.cutoff n i)) (hu : ∀ (n : ℕ) (i : I), CopyAngularInvariance.Invariant v (a.amplitude n i)) (n : ℕ) : CopyAngularInvariance.Invariant v (a.common.amplitude n)

theorem NavierStokes.PeriodizedWaveBounds.CopyData.common_pressure_invariant {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (v : D) (hψ : ∀ (n : ℕ) (i : I), CopyAngularInvariance.Invariant v (a.cutoff n i)) (hp : ∀ (n : ℕ) (i : I), CopyAngularInvariance.Invariant v (a.pressure n i)) (n : ℕ) : CopyAngularInvariance.Invariant v (a.common.pressure n)

theorem NavierStokes.PeriodizedWaveBounds.CopyData.commonCorrected_invariant {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (v : D) (hψ : ∀ (n : ℕ) (i : I), CopyAngularInvariance.Invariant v (a.cutoff n i)) (hu : ∀ (n : ℕ) (i : I), CopyAngularInvariance.Invariant v (a.amplitude n i)) (hR : ∀ (n : ℕ), CopyAngularInvariance.Invariant v (a.background.radius n)) (hr : ∀ (n : ℕ), CopyAngularInvariance.Invariant v (d.radialField n)) (hz : ∀ (n : ℕ), CopyAngularInvariance.Invariant v (d.axialField s n)) (hΦ : ∀ (n : ℕ), ∃ (m : ℝ), CopyAngularInvariance.AffinePhase v m (a.background.phase n)) (n : ℕ) : CopyAngularInvariance.Invariant v ((a.commonCorrected s d).amplitude n)

theorem NavierStokes.PeriodizedWaveBounds.CopyData.globalGaussian_invariant {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (d : LinearWaveBounds.GraphDirections D) (v : D) (hψ : ∀ (n : ℕ) (i : I), CopyAngularInvariance.Invariant v (a.cutoff n i)) (hu : ∀ (n : ℕ) (i : I), CopyAngularInvariance.Invariant v (a.amplitude n i)) (hf : ∀ (n : ℕ), CopyAngularInvariance.Invariant v (a.source n)) (n : ℕ) : CopyAngularInvariance.Invariant v (a.globalGaussian d n)

theorem NavierStokes.PeriodizedWaveBounds.CopyData.globalGood_invariant {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (hψ : ∀ (n : ℕ) (i : I), CopyAngularInvariance.Invariant d.angular (a.cutoff n i)) (hu : ∀ (n : ℕ) (i : I), CopyAngularInvariance.Invariant d.angular (a.amplitude n i)) (hp : ∀ (n : ℕ) (i : I), CopyAngularInvariance.Invariant d.angular (a.pressure n i)) (hR : ∀ (n : ℕ), CopyAngularInvariance.Invariant d.angular (a.background.radius n)) (hb : ∀ (n : ℕ), CopyAngularInvariance.Invariant d.angular (a.background.radialBase n)) (hF : ∀ (n : ℕ), CopyAngularInvariance.Invariant d.angular (a.background.frequencyBase n)) (hG : ∀ (n : ℕ), CopyAngularInvariance.Invariant d.angular (a.background.axialBase n)) (hr : ∀ (n : ℕ), CopyAngularInvariance.Invariant d.angular (d.radialField n)) (hz : ∀ (n : ℕ), CopyAngularInvariance.Invariant d.angular (d.axialField s n)) (hΦ : ∀ (n : ℕ), ∃ (m : ℝ), CopyAngularInvariance.AffinePhase d.angular m (a.background.phase n)) (n : ℕ) : CopyAngularInvariance.Invariant d.angular (a.globalGood s d n)

theorem NavierStokes.PeriodizedWaveBounds.CopyData.common_translate {D I : Type} (a : CopyData D I) (n : ℕ) (T : D → D) (e : I ≃ I) (hψ : ∀ (i : I) (x : D), a.cutoff n (e i) (T x) = a.cutoff n i x) (hu : ∀ (i : I) (x : D), a.amplitude n (e i) (T x) = a.amplitude n i x) (hp : ∀ (i : I) (x : D), a.pressure n (e i) (T x) = a.pressure n i x) (x : D) : a.common.amplitude n (T x) = a.common.amplitude n x ∧ a.common.pressure n (T x) = a.common.pressure n x

Deck reindexing is sufficient for common-field periodicity; individual uncut copies need not be periodic.

theorem NavierStokes.PeriodizedWaveBounds.CopyData.globalGaussian_translate {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : CopyData D I) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) (z : D) (e : I ≃ I) (hψ : ∀ (i : I) (x : D), a.cutoff n (e i) (x + z) = a.cutoff n i x) (hu : ∀ (i : I) (x : D), a.amplitude n (e i) (x + z) = a.amplitude n i x) (hf : ∀ (x : D), a.source n (x + z) = a.source n x) (x : D) : a.globalGaussian d n (x + z) = a.globalGaussian d n x

noncomputable def NavierStokes.PeriodizedWaveBounds.complexCopyData {P : Type} (base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space) (source : ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : ℕ → CommonCoverSolve.Geometry) (entry exit : ℕ → ℝ) (hab : ∀ (n : ℕ), entry n ≤ exit n) (κ : ℕ → TorusInverse.Plane → ℝ) : CopyData (P × TorusInverse.Plane) TorusInverse.Frequency

Actual complex copy solves with arbitrary band-dependent entry/exit times. In particular, a transported clock may use exit = length / clock. The tangent coefficients, source, geometry, and frequency are the actual inputs of complexCopyVelocity and its projected pressure.

Equations

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

theorem NavierStokes.PeriodizedWaveBounds.complexCopyData_common {P : Type} (base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space) (source : ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : ℕ → CommonCoverSolve.Geometry) (entry exit : ℕ → ℝ) (hab : ∀ (n : ℕ), entry n ≤ exit n) (κ : ℕ → TorusInverse.Plane → ℝ) : (complexCopyData base t source g entry exit hab κ).common = { radius := base.radius, radialBase := base.radialBase, frequencyBase := base.frequencyBase, axialBase := base.axialBase, phase := base.phase, amplitude := fun (n : ℕ) => ParticularWaveBounds.commonVelocity (t n) (source n) (g n) ⋯ (κ n), pressure := fun (n : ℕ) => ParticularWaveBounds.commonPressure (t n) (source n) (g n) ⋯ (κ n) (base.frequency n), frequency := base.frequency }

theorem NavierStokes.PeriodizedWaveBounds.complexCopyData_common_periodic {P : Type} (base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space) (source : ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : ℕ → CommonCoverSolve.Geometry) (entry exit : ℕ → ℝ) (hab : ∀ (n : ℕ), entry n ≤ exit n) (κ : ℕ → TorusInverse.Plane → ℝ) (n : ℕ) (p : P) (hp : CommonCoverSolve.PeriodicAt (source n) p) : CommonCoverSolve.PeriodicAt ((complexCopyData base t source g entry exit hab κ).common.amplitude n) p ∧ CommonCoverSolve.PeriodicAt ((complexCopyData base t source g entry exit hab κ).common.pressure n) p

theorem NavierStokes.PeriodizedWaveBounds.complexCopyData_cutoff_support {P : Type} (base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space) (source : ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : ℕ → CommonCoverSolve.Geometry) (entry exit : ℕ → ℝ) (hab : ∀ (n : ℕ), entry n ≤ exit n) (κ : ℕ → TorusInverse.Plane → ℝ) (K : ℕ → Set TorusInverse.Plane) (hκ : ∀ (n : ℕ), Function.support (κ n) ⊆ K n) (n : ℕ) (k : TorusInverse.Frequency) : Function.support ((complexCopyData base t source g entry exit hab κ).cutoff n k) ⊆ nativeCell (g n) (K n) k

noncomputable def NavierStokes.PeriodizedWaveBounds.particularData {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : ParticularWaveAssembly.Reference P) (charts : ParticularWaveAssembly.BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) : CopyData ((P × ℝ) × TorusInverse.Plane) TorusInverse.Frequency

The data-only binding to the actual fixed-reference particular solve. The source is the literal coefficient of the incoming harmonic residual; no inverse, output field, or residual witness is supplied separately.

Equations

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

theorem NavierStokes.PeriodizedWaveBounds.particularData_eq_complexCopyData {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : ParticularWaveAssembly.Reference P) (charts : ParticularWaveAssembly.BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) : particularData r charts c u b G A j base = complexCopyData (ParticularWaveAssembly.actualCarrier base b j) (fun (n : ℕ) => ParticularWaveAssembly.angleTangent (ParticularWaveAssembly.bandTangent r charts j n)) (fun (n : ℕ) => ParticularWaveAssembly.angleLift (ParticularWaveAssembly.residualSource c u b G A j n)) (ParticularWaveAssembly.bandGeometry r charts) (fun (x : ℕ) => 0) (fun (x : ℕ) => r.length) ⋯ fun (x : ℕ) => r.cutoff

theorem NavierStokes.PeriodizedWaveBounds.particularData_raw {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : ParticularWaveAssembly.Reference P) (charts : ParticularWaveAssembly.BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (k : TorusInverse.Frequency) : (particularData r charts c u b G A j base).raw k = ParticularWaveAssembly.actualCopyCoefficients r charts c u b G A j base fun (x : ℕ) => k

theorem NavierStokes.PeriodizedWaveBounds.particularData_source {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : ParticularWaveAssembly.Reference P) (charts : ParticularWaveAssembly.BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (n : ℕ) (z : (P × ℝ) × TorusInverse.Plane) (i : Fin 3) : (particularData r charts c u b G A j base).source n z i = ((HarmonicResidual.residualBlock c u b G A).velocity n i).coeff j (z.1.1, z.2)

theorem NavierStokes.PeriodizedWaveBounds.particularData_frequency {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : ParticularWaveAssembly.Reference P) (charts : ParticularWaveAssembly.BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (n : ℕ) : (particularData r charts c u b G A j base).background.frequency n = ↑j * b.frequency n

theorem NavierStokes.PeriodizedWaveBounds.particularData_phase {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : ParticularWaveAssembly.Reference P) (charts : ParticularWaveAssembly.BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (n : ℕ) (z : (P × ℝ) × TorusInverse.Plane) : (particularData r charts c u b G A j base).background.phase n z = b.phase n (z.1.1, z.2) + ↑(b.angularFrequency n) / b.frequency n * z.1.2

theorem NavierStokes.PeriodizedWaveBounds.particularData_cutoff_support {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : ParticularWaveAssembly.Reference P) (charts : ParticularWaveAssembly.BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (K : ℕ → Set TorusInverse.Plane) (hK : ∀ (n : ℕ), Function.support r.cutoff ⊆ K n) (n : ℕ) (k : TorusInverse.Frequency) : Function.support ((particularData r charts c u b G A j base).cutoff n k) ⊆ nativeCell (ParticularWaveAssembly.bandGeometry r charts n) (K n) k

theorem NavierStokes.PeriodizedWaveBounds.particularData_common {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : ParticularWaveAssembly.Reference P) (charts : ParticularWaveAssembly.BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) {j : ℤ} (hj : j ≠ 0) (hfrequency : ∀ (n : ℕ), b.frequency n ≠ 0) (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) : (particularData r charts c u b G A j base).common = ParticularWaveAssembly.actualCommonCoefficients r charts c u b G A j base

This is the same actual periodization as ParticularWaveAssembly, with its single physical reference and original source.

theorem NavierStokes.PeriodizedWaveBounds.particularData_commonCorrected {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : ParticularWaveAssembly.Reference P) (charts : ParticularWaveAssembly.BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) {j : ℤ} (hj : j ≠ 0) (hfrequency : ∀ (n : ℕ), b.frequency n ≠ 0) (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)) (d : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)) : (particularData r charts c u b G A j base).commonCorrected s d = ParticularWaveAssembly.actualCorrectedCommon r charts c u b G A j base s d