Wave bounds from primitive jets on native support cells

The background phase and its material defect are controlled only where the native coefficient can be nonzero. No extension of these controls to the whole fast lift is required.

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

A local all-jet class. The extra index can contain both the spatial label and the lattice copy, and the envelope may depend on that index. Every constant precedes the band, label, copy, and evaluation point.

• weight_nonneg (n : ℕ) (i : I) (x : D) : x ∈ s.domain → 0 ≤ w n i x
• 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 (fun (n : ℕ) (x : D) => w n i x) α C p n x

@[reducible, inline]

abbrev NavierStokes.LocalizedWaveBounds.LocalWave {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (s : WeightedClasses.StripData D) (K : ℕ → I → Set D) (P : ℕ → I → D → ℝ) (α : ℝ) (f : ℕ → I → D → E) : Prop

Local wave: an abbreviation for LocalClass s K (fun n i x => Real.sqrt (s.zeta x) * P n i x) α f.

Equations

• NavierStokes.LocalizedWaveBounds.LocalWave s K P α f = NavierStokes.LocalizedWaveBounds.LocalClass s K (fun (n : ℕ) (i : I) (x : D) => √(s.zeta x) * P n i x) α f

@[reducible, inline]

abbrev NavierStokes.LocalizedWaveBounds.LocalUnweighted {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (s : WeightedClasses.StripData D) (K : ℕ → I → Set D) (α : ℝ) (f : ℕ → I → D → E) : Prop

Local unweighted: an abbreviation for LocalClass s K (fun _ _ _ => 1) α f.

Equations

• NavierStokes.LocalizedWaveBounds.LocalUnweighted s K α f = NavierStokes.LocalizedWaveBounds.LocalClass s K (fun (x : ℕ) (x_1 : I) (x_2 : D) => 1) α f

theorem NavierStokes.LocalizedWaveBounds.LocalClass.of_global {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {α : ℝ} {w0 : ℕ → D → ℝ} {f0 : ℕ → D → E} (hf : WeightedClasses.MemClass s w0 α f0) : LocalClass s K (fun (n : ℕ) (x : I) => w0 n) α fun (n : ℕ) (x : I) => f0 n

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

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

theorem NavierStokes.LocalizedWaveBounds.LocalClass.congr_germ {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α : ℝ} {f g : ℕ → I → D → E} (hf : LocalClass s K w α f) (he : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → f n i =ᶠ[nhds x] g n i) : LocalClass s K w α g

theorem NavierStokes.LocalizedWaveBounds.LocalClass.congr {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α : ℝ} {f g : ℕ → I → D → E} (hf : LocalClass s K w α f) (he : ∀ (n : ℕ) (i : I) (x : D), f n i x = g n i x) : LocalClass s K w α g

theorem NavierStokes.LocalizedWaveBounds.LocalClass.enlarge {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α : ℝ} {f : ℕ → I → D → E} {C : ℕ → I → Set D} (hf : LocalClass s C w α f) (hcover : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → x ∈ C n i ∨ f n i =ᶠ[nhds x] fun (x : D) => 0) : LocalClass s K w α f

Enlarge only the set on which a supported output is estimated. The input background need not have any estimate on the added points.

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

theorem NavierStokes.LocalizedWaveBounds.LocalClass.mono_exponent {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α β : ℝ} {f : ℕ → I → D → E} (hf : LocalClass s K w α f) (hβα : β ≤ α) : LocalClass s K w β f

theorem NavierStokes.LocalizedWaveBounds.LocalClass.mono_weight {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w v : ℕ → I → D → ℝ} {α : ℝ} {f : ℕ → I → D → E} (hf : LocalClass s K w α f) (hv : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, 0 ≤ v n i x) (hwv : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → w n i x ≤ v n i x) : LocalClass s K v α f

theorem NavierStokes.LocalizedWaveBounds.LocalClass.add {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α : ℝ} {f g : ℕ → I → D → E} (hf : LocalClass s K w α f) (hg : LocalClass s K w α g) : LocalClass s K w α fun (n : ℕ) (i : I) (x : D) => f n i x + g n i x

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

theorem NavierStokes.LocalizedWaveBounds.LocalClass.sub {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α : ℝ} {f g : ℕ → I → D → E} (hf : LocalClass s K w α f) (hg : LocalClass s K w α g) : LocalClass s K w α fun (n : ℕ) (i : I) (x : D) => f n i x - g n i x

theorem NavierStokes.LocalizedWaveBounds.LocalClass.zero {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α : ℝ} (hw : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, 0 ≤ w n i x) : LocalClass s K w α fun (x : ℕ) (x_1 : I) (x_2 : D) => 0

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

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

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

theorem NavierStokes.LocalizedWaveBounds.LocalClass.smul {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w v : ℕ → I → D → ℝ} {α β : ℝ} {f : ℕ → I → D → E} {r : ℕ → I → D → ℝ} (hr : LocalClass s K v β r) (hf : LocalClass s K w α f) : LocalClass s K (fun (n : ℕ) (i : I) (x : D) => v n i x * w n i x) (β + α) fun (n : ℕ) (i : I) (x : D) => r n i x • f n i x

theorem NavierStokes.LocalizedWaveBounds.LocalClass.mul {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w v : ℕ → I → D → ℝ} {α β : ℝ} {a b : ℕ → I → D → ℝ} (ha : LocalClass s K w α a) (hb : LocalClass s K v β b) : LocalClass s K (fun (n : ℕ) (i : I) (x : D) => w n i x * v n i x) (α + β) fun (n : ℕ) (i : I) (x : D) => a n i x * b n i x

theorem NavierStokes.LocalizedWaveBounds.LocalClass.band_smul {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α β : ℝ} {f : ℕ → I → D → E} {r : ℕ → ℝ} (hf : LocalClass s K w α f) (hr : WeightedClasses.BandBound s β r) : LocalClass s K w (α + β) fun (n : ℕ) (i : I) (x : D) => r n • f n i x

theorem NavierStokes.LocalizedWaveBounds.LocalClass.band_const {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {β : ℝ} {r : ℕ → ℝ} (hr : WeightedClasses.BandBound s β r) : LocalUnweighted s K β fun (n : ℕ) (x : I) (x_1 : D) => r n

theorem NavierStokes.LocalizedWaveBounds.unweighted_mul {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {α β : ℝ} {a b : ℕ → I → D → ℝ} (ha : LocalUnweighted s K α a) (hb : LocalUnweighted s K β b) : LocalUnweighted s K (α + β) fun (n : ℕ) (i : I) (x : D) => a n i x * b n i x

theorem NavierStokes.LocalizedWaveBounds.unweighted_smul {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α β : ℝ} {a : ℕ → I → D → ℝ} {f : ℕ → I → D → E} (ha : LocalUnweighted s K α a) (hf : LocalClass s K w β f) : LocalClass s K w (α + β) fun (n : ℕ) (i : I) (x : D) => a n i x • f n i x

theorem NavierStokes.LocalizedWaveBounds.real_mul_complex {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α β : ℝ} {a : ℕ → I → D → ℝ} {f : ℕ → I → D → ℂ} (ha : LocalUnweighted s K α a) (hf : LocalClass s K w β f) : LocalClass s K w (α + β) fun (n : ℕ) (i : I) (x : D) => ↑(a n i x) * f n i x

theorem NavierStokes.LocalizedWaveBounds.complex_mul_real {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α β : ℝ} {f : ℕ → I → D → ℂ} {a : ℕ → I → D → ℝ} (hf : LocalClass s K w α f) (ha : LocalUnweighted s K β a) : LocalClass s K w (α + β) fun (n : ℕ) (i : I) (x : D) => f n i x * ↑(a n i x)

theorem NavierStokes.LocalizedWaveBounds.constant_complex_mul {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α : ℝ} {f : ℕ → I → D → ℂ} (hf : LocalClass s K w α f) (c : ℂ) : LocalClass s K w α fun (n : ℕ) (i : I) (x : D) => c * f n i x

theorem NavierStokes.LocalizedWaveBounds.constant_real_mul {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α : ℝ} {f : ℕ → I → D → ℝ} (hf : LocalClass s K w α f) (c : ℝ) : LocalClass s K w α fun (n : ℕ) (i : I) (x : D) => c * f n i x

theorem NavierStokes.LocalizedWaveBounds.local_const {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} (c : E) : LocalUnweighted s K 0 fun (x : ℕ) (x_1 : I) (x_2 : D) => c

theorem NavierStokes.LocalizedWaveBounds.component_classes {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α : ℝ} {f : ℕ → I → D → HarmonicCalculus.ComplexVector} (hf : ∀ (j : Fin 3), LocalClass s K w α fun (n : ℕ) (i : I) (x : D) => f n i x j) : LocalClass s K w α f

theorem NavierStokes.LocalizedWaveBounds.angular_classes {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α : ℝ} {f : ℕ → I → D → HarmonicCalculus.ComplexVector} (hf : ∀ (j : Fin 3), LocalClass s K w α fun (n : ℕ) (i : I) (x : D) => f n i x j) (j : Fin 3) : LocalClass s K w α fun (n : ℕ) (i : I) (x : D) => HarmonicCalculus.angularGenerator (f n i x) j

noncomputable def NavierStokes.LocalizedWaveBounds.Dr {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : LinearWaveBounds.GraphDirections D) (f : ℕ → I → D → E) : ℕ → I → D → E

Dr, defined pointwise by along (d.radialField n) (f n i).

Equations

• NavierStokes.LocalizedWaveBounds.Dr d f n i = NavierStokes.HarmonicCalculus.along (d.radialField n) (f n i)

noncomputable def NavierStokes.LocalizedWaveBounds.Dz {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : LinearWaveBounds.GraphDirections D) (s : WeightedClasses.StripData D) (f : ℕ → I → D → E) : ℕ → I → D → E

Dz, defined pointwise by along (d.axialField s n) (f n i).

Equations

• NavierStokes.LocalizedWaveBounds.Dz d s f n i = NavierStokes.HarmonicCalculus.along (d.axialField s n) (f n i)

noncomputable def NavierStokes.LocalizedWaveBounds.Dt {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : LinearWaveBounds.GraphDirections D) (f : ℕ → I → D → E) : ℕ → I → D → E

Dt, defined pointwise by along (fun _ => d.slow) (f n i).

Equations

• NavierStokes.LocalizedWaveBounds.Dt d f n i = NavierStokes.HarmonicCalculus.along (fun (x : D) => d.slow) (f n i)

noncomputable def NavierStokes.LocalizedWaveBounds.Dfast {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : LinearWaveBounds.GraphDirections D) (f : ℕ → I → D → E) : ℕ → I → D → E

Dfast, defined pointwise by along (d.fastField n) (f n i).

Equations

• NavierStokes.LocalizedWaveBounds.Dfast d f n i = NavierStokes.HarmonicCalculus.along (d.fastField n) (f n i)

theorem NavierStokes.LocalizedWaveBounds.Dr_mem {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α κ : ℝ} (d : LinearWaveBounds.GraphDirections D) {f : ℕ → I → D → E} (hf : LocalClass s K w α f) (hρ : LocalUnweighted s K 0 fun (x : ℕ) (x_1 : I) => d.radialProfile) (hM : WeightedClasses.BandBound s (-κ) d.radialScale) (hκ : 0 ≤ κ) : LocalClass s K w (α - κ) (Dr d f)

theorem NavierStokes.LocalizedWaveBounds.Dz_mem {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α : ℝ} (d : LinearWaveBounds.GraphDirections D) {f : ℕ → I → D → E} (hf : LocalClass s K w α f) : LocalClass s K w (α + 1) (Dz d s f)

theorem NavierStokes.LocalizedWaveBounds.Dt_mem {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α : ℝ} (d : LinearWaveBounds.GraphDirections D) {f : ℕ → I → D → E} (hf : LocalClass s K w α f) : LocalClass s K w α (Dt d f)

theorem NavierStokes.LocalizedWaveBounds.Dfast_mem {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α : ℝ} (d : LinearWaveBounds.GraphDirections D) {f : ℕ → I → D → E} (hf : LocalClass s K w α f) (hfast : WeightedClasses.BandBound s 0 d.fastScale) : LocalClass s K w α (Dfast d f)

theorem NavierStokes.LocalizedWaveBounds.Dr_base_mem {D : Type u_1} {E : Type u_2} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α : ℝ} (d : LinearWaveBounds.GraphDirections D) {f : ℕ → I → D → E} (hf : LocalClass s K w α f) (haux : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → (fun (y : D) => (fderiv ℝ (f n i) y) d.auxiliary) =ᶠ[nhds x] fun (x : D) => 0) : LocalClass s K w α (Dr d f)

theorem NavierStokes.LocalizedWaveBounds.LocalClass.compact_comp {D : Type u_1} {E : Type u_2} {F : Type u_3} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {f : ℕ → I → D → E} (hf : LocalUnweighted s K 0 f) {g : E → F} {U Cset : Set E} (hU : IsOpen U) (hg : ContDiffOn ℝ (↑⊤) g U) (hCset : IsCompact Cset) (hCU : Cset ⊆ U) (hmap : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → f n i x ∈ Cset) : LocalUnweighted s K 0 fun (n : ℕ) (i : I) (x : D) => g (f n i x)

Only the outer function is bounded on a compact set. The inner jets are used at the native support point, never on the whole strip.

theorem NavierStokes.LocalizedWaveBounds.LocalClass.inv {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {f : ℕ → I → D → ℝ} (hf : LocalUnweighted s K 0 f) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → b ≤ |f n i x|) (hupper : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → |f n i x| ≤ M) : LocalUnweighted s K 0 fun (n : ℕ) (i : I) (x : D) => (f n i x)⁻¹

The same wave algebra with a uniform extra index

structure NavierStokes.LocalizedWaveBounds.WaveFamily (D : Type u_6) (I : Type u_7) : Type (max u_6 u_7)

Wave family data, collecting radius, radialBase, frequencyBase, axialBase, phase, amplitude and their compatibility conditions.

• radius : ℕ → I → D → ℝ

  Radius of WaveFamily, of type ℕ → I → D → ℝ.

• radialBase : ℕ → I → D → ℝ

  Radial base of WaveFamily, of type ℕ → I → D → ℝ.

• frequencyBase : ℕ → I → D → ℝ

  Frequency base of WaveFamily, of type ℕ → I → D → ℝ.

• axialBase : ℕ → I → D → ℝ

  Axial base of WaveFamily, of type ℕ → I → D → ℝ.

• phase : ℕ → I → D → ℝ

  Phase of WaveFamily, of type ℕ → I → D → ℝ.

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

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

• pressure : ℕ → I → D → ℂ

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

• frequency : ℕ → I → ℝ

  Frequency of WaveFamily, of type ℕ → I → ℝ.

noncomputable def NavierStokes.LocalizedWaveBounds.WaveFamily.coefficients {D : Type u_1} {I : Type u_5} (a : WaveFamily D I) (i : I) : LinearWaveBounds.WaveCoefficients D

Coefficients, bundling radius, radialBase, frequencyBase, axialBase and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.LocalizedWaveBounds.WaveFamily.ofCoefficients {D : Type u_1} {I : Type u_5} (a : I → LinearWaveBounds.WaveCoefficients D) : WaveFamily D I

Of coefficients, bundling radius, radialBase, frequencyBase, axialBase and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.LocalizedWaveBounds.WaveFamily.normal {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : WaveFamily D I) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) : ℕ → I → D → ProblemStatement.Space

Normal, defined pointwise by (a.coefficients i).normal s d n.

Equations

• a.normal s d n i = (a.coefficients i).normal s d n

noncomputable def NavierStokes.LocalizedWaveBounds.WaveFamily.defect {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : WaveFamily D I) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) : ℕ → I → D → ℝ

Defect, defined pointwise by (a.coefficients i).defect s d n.

Equations

• a.defect s d n i = (a.coefficients i).defect s d n

noncomputable def NavierStokes.LocalizedWaveBounds.WaveFamily.remainder {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : WaveFamily D I) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) : ℕ → I → D → HarmonicCalculus.ComplexVector

Remainder, defined pointwise by (a.coefficients i).remainder s d n.

Equations

• a.remainder s d n i = (a.coefficients i).remainder s d n

noncomputable def NavierStokes.LocalizedWaveBounds.WaveFamily.principalVelocity {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : WaveFamily D I) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (f : ℕ → I → D → HarmonicCalculus.ComplexVector) : ℕ → I → D → HarmonicCalculus.ComplexVector

Principal velocity, defined pointwise by (a.coefficients i).principalVelocity s d (fun n => f n i) n.

Equations

• a.principalVelocity s d f n i = (a.coefficients i).principalVelocity s d (fun (n : ℕ) => f n i) n

noncomputable def NavierStokes.LocalizedWaveBounds.WaveFamily.curlCorrection {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : WaveFamily D I) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) : ℕ → I → D → HarmonicCalculus.ComplexVector

Curl correction, defined pointwise by (a.coefficients i).curlCorrection s d n.

Equations

• a.curlCorrection s d n i = (a.coefficients i).curlCorrection s d n

noncomputable def NavierStokes.LocalizedWaveBounds.WaveFamily.addAmplitude {D : Type u_1} {I : Type u_5} (a : WaveFamily D I) (f : ℕ → I → D → HarmonicCalculus.ComplexVector) : WaveFamily D I

Add amplitude, given by { a with amplitude := fun n i x => a.amplitude n i x + f n i x }.

Equations

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

noncomputable def NavierStokes.LocalizedWaveBounds.WaveFamily.withCutoff {D : Type u_1} {I : Type u_5} (a : WaveFamily D I) (ψ : ℕ → I → D → ℝ) : WaveFamily D I

With cutoff, given by { a with amplitude := fun n i x => ψ n i x • a.amplitude n i x pressure := fun n i x => (ψ n i x : ℂ) * a.pressure n i x }.

Equations

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

noncomputable def NavierStokes.LocalizedWaveBounds.WaveFamily.retainedGood {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : WaveFamily D I) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) : ℕ → I → D → HarmonicCalculus.ComplexVector

Retained good, defined pointwise by a.principalVelocity s d (a.curlCorrection s d) n i x + (a.addAmplitude (a.curlCorrection s d)).remainder s d n i x.

Equations

• a.retainedGood s d n i x = a.principalVelocity s d (a.curlCorrection s d) n i x + (a.addAmplitude (a.curlCorrection s d)).remainder s d n i x

theorem NavierStokes.LocalizedWaveBounds.WaveFamily.outputs_zero_germs {I : Type u_5} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : WaveFamily D I) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) {n : ℕ} {i : I} {x : D} (ha : a.amplitude n i =ᶠ[nhds x] fun (x : D) => 0) (hp : a.pressure n i =ᶠ[nhds x] fun (x : D) => 0) : (a.curlCorrection s d n i =ᶠ[nhds x] fun (x : D) => 0) ∧ ((a.addAmplitude (a.curlCorrection s d)).amplitude n i =ᶠ[nhds x] fun (x : D) => 0) ∧ a.retainedGood s d n i =ᶠ[nhds x] fun (x : D) => 0

Outside the complete input support, all the derived coefficients vanish as germs, even if the background has no estimates there.

theorem NavierStokes.LocalizedWaveBounds.WaveFamily.input_germ_cover_of_tsupport {I : Type u_5} {D : Type} [NormedAddCommGroup D] (a : WaveFamily D I) {C : ℕ → I → Set D} (ha : ∀ (n : ℕ) (i : I), tsupport (a.amplitude n i) ⊆ C n i) (hp : ∀ (n : ℕ) (i : I), tsupport (a.pressure n i) ⊆ C n i) (n : ℕ) (i : I) (x : D) : x ∈ C n i ∨ (a.amplitude n i =ᶠ[nhds x] fun (x : D) => 0) ∧ a.pressure n i =ᶠ[nhds x] fun (x : D) => 0

Containment of the two closed input supports is enough to supply the local-estimate/zero-germ alternative; no output support is assumed.

structure NavierStokes.LocalizedWaveBounds.InputBounds {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (K : ℕ → I → Set D) (P : ℕ → I → D → ℝ) (α κ : ℝ) (d : LinearWaveBounds.GraphDirections D) (a : WaveFamily D I) : Prop

Primitive local hypotheses. The normal and the material defect are the actual expressions computed from the phase; their bounds are imposed only on the native cells. Auxiliary independence is a local identity.

• loss_nonneg : 0 ≤ κ
• radial_profile : LocalUnweighted s K 0 fun (x : ℕ) (x_1 : I) => d.radialProfile
• radial_scale : WeightedClasses.BandBound s (-κ) d.radialScale
• fast_scale : WeightedClasses.BandBound s 0 d.fastScale
• frequency_scale : LocalUnweighted s K (-(1 / 2)) fun (n : ℕ) (i : I) (x : D) => a.frequency n i
• radius : LocalUnweighted s K 0 a.radius
• inverse_radius : LocalUnweighted s K 0 fun (n : ℕ) (i : I) (x : D) => (a.radius n i x)⁻¹
• radial_base : LocalUnweighted s K 1 a.radialBase
• frequency_base : LocalUnweighted s K 0 a.frequencyBase
• axial_base : LocalUnweighted s K 0 a.axialBase
• radial_base_aux (n : ℕ) (i : I) (x : D) : x ∈ s.domain → x ∈ K n i → (fun (y : D) => (fderiv ℝ (a.radialBase n i) y) d.auxiliary) =ᶠ[nhds x] fun (x : D) => 0
• frequency_base_aux (n : ℕ) (i : I) (x : D) : x ∈ s.domain → x ∈ K n i → (fun (y : D) => (fderiv ℝ (a.frequencyBase n i) y) d.auxiliary) =ᶠ[nhds x] fun (x : D) => 0
• axial_base_aux (n : ℕ) (i : I) (x : D) : x ∈ s.domain → x ∈ K n i → (fun (y : D) => (fderiv ℝ (a.axialBase n i) y) d.auxiliary) =ᶠ[nhds x] fun (x : D) => 0
• normal : LocalUnweighted s K 0 (a.normal s d)
• defect : LocalUnweighted s K 1 (a.defect s d)
• amplitude (j : Fin 3) : LocalWave s K P α fun (n : ℕ) (i : I) (x : D) => a.amplitude n i x j
• pressure : LocalWave s K P (α + 1 / 2) a.pressure

theorem NavierStokes.LocalizedWaveBounds.frequency_mul {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α : ℝ} {f : ℕ → I → D → ℂ} {freq : ℕ → I → ℝ} (hf : LocalClass s K w α f) (hk : LocalUnweighted s K (-(1 / 2)) fun (n : ℕ) (i : I) (x : D) => freq n i) : LocalClass s K w (α - 1 / 2) fun (n : ℕ) (i : I) (x : D) => HarmonicCalculus.phaseFactor (freq n i) * f n i x

theorem NavierStokes.LocalizedWaveBounds.InputBounds.normal_component {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : WaveFamily D I} (h : InputBounds s K P α κ d a) (j : Fin 3) : LocalUnweighted s K 0 fun (n : ℕ) (i : I) (x : D) => (a.normal s d n i x).ofLp j

theorem NavierStokes.LocalizedWaveBounds.InputBounds.inverse_radius_sq {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : WaveFamily D I} (h : InputBounds s K P α κ d a) : LocalUnweighted s K 0 fun (n : ℕ) (i : I) (x : D) => (a.radius n i x ^ 2)⁻¹

theorem NavierStokes.LocalizedWaveBounds.InputBounds.base_components {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : WaveFamily D I} (h : InputBounds s K P α κ d a) (j : Fin 3) : LocalUnweighted s K 0 fun (n : ℕ) (i : I) (x : D) => LinearWaveResidual.base (a.radius n i) (a.radialBase n i) (a.frequencyBase n i) (a.axialBase n i) x j

theorem NavierStokes.LocalizedWaveBounds.InputBounds.slowTransport_mem {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : WaveFamily D I} (h : InputBounds s K P α κ d a) (j : Fin 3) : LocalWave s K P (α + 1 / 2 - 3 * κ) fun (n : ℕ) (i : I) (x : D) => LinearWaveResidual.slowTransport (s.epsilon n) (a.radialBase n i) (a.axialBase n i) (fun (x : D) => d.slow) (d.radialField n) (d.axialField s n) (a.amplitude n i) x j

theorem NavierStokes.LocalizedWaveBounds.InputBounds.phaseDefect_mem {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : WaveFamily D I} (h : InputBounds s K P α κ d a) (j : Fin 3) : LocalWave s K P (α + 1 / 2 - 3 * κ) fun (n : ℕ) (i : I) (x : D) => HarmonicCalculus.phaseFactor (a.frequency n i) * ↑(a.defect s d n i x) * a.amplitude n i x j

theorem NavierStokes.LocalizedWaveBounds.InputBounds.baseDerivativeRemainder_mem {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : WaveFamily D I} (h : InputBounds s K P α κ d a) (j : Fin 3) : LocalWave s K P (α + 1 / 2 - 3 * κ) fun (n : ℕ) (i : I) (x : D) => LinearWaveResidual.baseDerivativeRemainder (a.radius n i) (a.radialBase n i) (a.frequencyBase n i) (a.axialBase n i) (d.radialField n) (d.axialField s n) (a.amplitude n i) x j

theorem NavierStokes.LocalizedWaveBounds.InputBounds.pressureGradient_mem {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : WaveFamily D I} (h : InputBounds s K P α κ d a) (j : Fin 3) : LocalWave s K P (α + 1 / 2 - 3 * κ) fun (n : ℕ) (i : I) (x : D) => LinearWaveResidual.strippedPressureGradient (d.radialField n) (d.axialField s n) (a.pressure n i) x j

theorem NavierStokes.LocalizedWaveBounds.InputBounds.viscousRemainder_mem {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : WaveFamily D I} (h : InputBounds s K P α κ d a) (j : Fin 3) : LocalWave s K P (α - 1 / 2 - 3 * κ) fun (n : ℕ) (i : I) (x : D) => LinearWaveResidual.viscousRemainder (a.radius n i) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n) (a.frequency n i) (a.phase n i) (a.amplitude n i) x j

theorem NavierStokes.LocalizedWaveBounds.InputBounds.viscousPart_mem {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : WaveFamily D I} (h : InputBounds s K P α κ d a) (j : Fin 3) : LocalWave s K P (α + 1 / 2 - 3 * κ) fun (n : ℕ) (i : I) (x : D) => ↑(s.epsilon n) * LinearWaveResidual.viscousRemainder (a.radius n i) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n) (a.frequency n i) (a.phase n i) (a.amplitude n i) x j

theorem NavierStokes.LocalizedWaveBounds.InputBounds.remainder_components {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : WaveFamily D I} (h : InputBounds s K P α κ d a) (j : Fin 3) : LocalWave s K P (α + 1 / 2 - 3 * κ) fun (n : ℕ) (i : I) (x : D) => a.remainder s d n i x j

Every actual term of the linear-wave remainder retains its stated power, with constants uniform before every extra label and copy.

theorem NavierStokes.LocalizedWaveBounds.InputBounds.remainder_class {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : WaveFamily D I} (h : InputBounds s K P α κ d a) : LocalWave s K P (α + 1 / 2 - 3 * κ) (a.remainder s d)

theorem NavierStokes.LocalizedWaveBounds.InputBounds.normal_norm_sq {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : WaveFamily D I} (h : InputBounds s K P α κ d a) : LocalUnweighted s K 0 fun (n : ℕ) (i : I) (x : D) => ‖a.normal s d n i x‖ ^ 2

theorem NavierStokes.LocalizedWaveBounds.InputBounds.shear_mem {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : WaveFamily D I} (h : InputBounds s K P α κ d a) {β : ℝ} {f : ℕ → I → D → HarmonicCalculus.ComplexVector} (hf : ∀ (j : Fin 3), LocalWave s K P β fun (n : ℕ) (i : I) (x : D) => f n i x j) (j : Fin 3) : LocalWave s K P β fun (n : ℕ) (i : I) (x : D) => LinearWaveResidual.shear (a.radius n i) (a.frequencyBase n i) (a.axialBase n i) (d.radialField n) (f n i) x j

theorem NavierStokes.LocalizedWaveBounds.InputBounds.principalVelocity_components {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : WaveFamily D I} (h : InputBounds s K P α κ d a) {β : ℝ} {f : ℕ → I → D → HarmonicCalculus.ComplexVector} (hf : ∀ (j : Fin 3), LocalWave s K P β fun (n : ℕ) (i : I) (x : D) => f n i x j) (j : Fin 3) : LocalWave s K P β fun (n : ℕ) (i : I) (x : D) => a.principalVelocity s d f n i x j

theorem NavierStokes.LocalizedWaveBounds.InputBounds.principalVelocity_class {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : WaveFamily D I} (h : InputBounds s K P α κ d a) {β : ℝ} {f : ℕ → I → D → HarmonicCalculus.ComplexVector} (hf : ∀ (j : Fin 3), LocalWave s K P β fun (n : ℕ) (i : I) (x : D) => f n i x j) : LocalWave s K P β (a.principalVelocity s d f)

theorem NavierStokes.LocalizedWaveBounds.InputBounds.add_curl_amplitude {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : WaveFamily D I} (h : InputBounds s K P α κ d a) (hκ : κ ≤ 1 / 2) {f : ℕ → I → D → HarmonicCalculus.ComplexVector} (hf : ∀ (j : Fin 3), LocalWave s K P (α + 1 / 2 - κ) fun (n : ℕ) (i : I) (x : D) => f n i x j) : InputBounds s K P α κ d (a.addAmplitude f)

theorem NavierStokes.LocalizedWaveBounds.InputBounds.with_cutoff {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : WaveFamily D I} (h : InputBounds s K P α κ d a) {ψ : ℕ → I → D → ℝ} (hψ : LocalUnweighted s K 0 ψ) : InputBounds s K P α κ d (a.withCutoff ψ)

theorem NavierStokes.LocalizedWaveBounds.InputBounds.normalInverse_class {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : WaveFamily D I} (h : InputBounds s K P α κ d a) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → b ≤ ‖a.normal s d n i x‖) (hupper : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → ‖a.normal s d n i x‖ ≤ M) : LocalUnweighted s K 0 fun (n : ℕ) (i : I) (x : D) => (‖a.normal s d n i x‖ ^ 2)⁻¹

theorem NavierStokes.LocalizedWaveBounds.InputBounds.normalCoefficient_class {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : WaveFamily D I} (h : InputBounds s K P α κ d a) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → b ≤ ‖a.normal s d n i x‖) (hupper : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → ‖a.normal s d n i x‖ ≤ M) : LocalWave s K P α fun (n : ℕ) (i : I) (x : D) => CurlClassBounds.normalCoefficient (a.normal s d n i x) (a.amplitude n i x)

theorem NavierStokes.LocalizedWaveBounds.InputBounds.curlCorrection_class {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : WaveFamily D I} (h : InputBounds s K P α κ d a) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → b ≤ ‖a.normal s d n i x‖) (hupper : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → ‖a.normal s d n i x‖ ≤ M) (hfreq : LocalUnweighted s K (1 / 2) fun (n : ℕ) (i : I) (x : D) => 1 / a.frequency n i) : LocalWave s K P (α + 1 / 2 - κ) (a.curlCorrection s d)

The inverse-normal factor and the cylindrical curl are estimated from primitive local jets. Only support-local normal separation occurs.

theorem NavierStokes.LocalizedWaveBounds.InputBounds.retainedGood_class {D : Type u_1} {I : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : WaveFamily D I} (h : InputBounds s K P α κ d a) (hκ : κ ≤ 1 / 2) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → b ≤ ‖a.normal s d n i x‖) (hupper : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → ‖a.normal s d n i x‖ ≤ M) (hfreq : LocalUnweighted s K (1 / 2) fun (n : ℕ) (i : I) (x : D) => 1 / a.frequency n i) : LocalWave s K P (α + 1 / 2 - 3 * κ) (a.retainedGood s d)

The retained good coefficient is the literal principal operator of the curl difference plus the literal remainder of the corrected field.

theorem NavierStokes.LocalizedWaveBounds.InputBounds.classes_on_of_input_germs {I : Type u_5} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {C K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : WaveFamily D I} (h : InputBounds s C P α κ d a) (hκ : κ ≤ 1 / 2) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ C n i → b ≤ ‖a.normal s d n i x‖) (hupper : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ C n i → ‖a.normal s d n i x‖ ≤ M) (hfreq : LocalUnweighted s C (1 / 2) fun (n : ℕ) (i : I) (x : D) => 1 / a.frequency n i) (hcover : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → x ∈ C n i ∨ (a.amplitude n i =ᶠ[nhds x] fun (x : D) => 0) ∧ a.pressure n i =ᶠ[nhds x] fun (x : D) => 0) : LocalWave s K P α a.amplitude ∧ LocalWave s K P α (a.addAmplitude (a.curlCorrection s d)).amplitude ∧ LocalWave s K P (α + 1 / 2) a.pressure ∧ LocalWave s K P (α + 1 / 2 - κ) (a.curlCorrection s d) ∧ LocalWave s K P (α + 1 / 2 - 3 * κ) (a.retainedGood s d)

Primitive estimates may be restricted to a smaller native patch. Only the derived, supported outputs are extended to the whole copy cell.

Native copies and the whole lift

theorem NavierStokes.LocalizedWaveBounds.LocalClass.to_uniformLocalJets {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {L : Type u_6} {J : Type u_7} {s : WeightedClasses.StripData D} {K : L → ℕ → J → Set D} {w : L → ℕ → D → ℝ} {α : ℝ} {f : L → ℕ → J → D → E} (hf : LocalClass s (fun (n : ℕ) (i : L × J) => K i.1 n i.2) (fun (n : ℕ) (i : L × J) (x : D) => w i.1 n x) α fun (n : ℕ) (i : L × J) => f i.1 n i.2) : PeriodizedWaveBounds.UniformLocalJets s w α K f

theorem NavierStokes.LocalizedWaveBounds.LocalClass.of_uniformLocalJets {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {L : Type u_6} {J : Type u_7} {s : WeightedClasses.StripData D} {K : L → ℕ → J → Set D} {w : L → ℕ → D → ℝ} {α : ℝ} {f : L → ℕ → J → D → E} (hw : ∀ (l : L) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w l n x) (hf : PeriodizedWaveBounds.UniformLocalJets s w α K f) : LocalClass s (fun (n : ℕ) (i : L × J) => K i.1 n i.2) (fun (n : ℕ) (i : L × J) (x : D) => w i.1 n x) α fun (n : ℕ) (i : L × J) => f i.1 n i.2

noncomputable def NavierStokes.LocalizedWaveBounds.nativeFamily {D I : Type} (a : PeriodizedWaveBounds.CopyData D I) : WaveFamily D I

Native family, given by WaveFamily.ofCoefficients a.localized.

Equations

• NavierStokes.LocalizedWaveBounds.nativeFamily a = NavierStokes.LocalizedWaveBounds.WaveFamily.ofCoefficients a.localized

noncomputable def NavierStokes.LocalizedWaveBounds.rawFamily {D I : Type} (a : PeriodizedWaveBounds.CopyData D I) : WaveFamily D I

Raw family, given by WaveFamily.ofCoefficients a.raw.

Equations

• NavierStokes.LocalizedWaveBounds.rawFamily a = NavierStokes.LocalizedWaveBounds.WaveFamily.ofCoefficients a.raw

theorem NavierStokes.LocalizedWaveBounds.common_curl_germ {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : PeriodizedWaveBounds.CopyData D I) (K : PeriodizedWaveBounds.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.curlCorrection s d n =ᶠ[nhds x] (a.localized i).curlCorrection s d n

theorem NavierStokes.LocalizedWaveBounds.common_curl_zero_germ {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : PeriodizedWaveBounds.CopyData D I) (K : PeriodizedWaveBounds.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.curlCorrection s d n =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.LocalizedWaveBounds.common_bounds_from_native_local {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : PeriodizedWaveBounds.CopyData D I) (K : PeriodizedWaveBounds.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) (h : InputBounds s K.carrier (fun (n : ℕ) (x : I) => W n) α κ d (nativeFamily a)) (hκ : κ ≤ 1 / 2) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K.carrier n i → b ≤ ‖a.background.normal s d n x‖) (hupper : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K.carrier n i → ‖a.background.normal s d n x‖ ≤ M) (hfreq : LocalUnweighted s K.carrier (1 / 2) fun (n : ℕ) (x : I) (x_1 : D) => 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 local input estimates imply all five actual common-field classes. No global background normal, material defect, or remainder class is a premise. The unused region is handled by genuine zero germs.

theorem NavierStokes.LocalizedWaveBounds.common_bounds_from_raw_local {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : PeriodizedWaveBounds.CopyData D I) (K : PeriodizedWaveBounds.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) (h : InputBounds s K.carrier (fun (n : ℕ) (x : I) => W n) α κ d (rawFamily a)) (hψ : LocalUnweighted s K.carrier 0 a.cutoff) (hκ : κ ≤ 1 / 2) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K.carrier n i → b ≤ ‖a.background.normal s d n x‖) (hupper : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K.carrier n i → ‖a.background.normal s d n x‖ ≤ M) (hfreq : LocalUnweighted s K.carrier (1 / 2) fun (n : ℕ) (x : I) (x_1 : D) => 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)

theorem NavierStokes.LocalizedWaveBounds.common_bounds_from_supported_native {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : PeriodizedWaveBounds.CopyData D I) (K : PeriodizedWaveBounds.Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (C : ℕ → I → Set D) {s : WeightedClasses.StripData D} {d : LinearWaveBounds.GraphDirections D} {W : ℕ → D → ℝ} {α κ : ℝ} (hW : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W n x) (h : InputBounds s C (fun (n : ℕ) (x : I) => W n) α κ d (nativeFamily a)) (hκ : κ ≤ 1 / 2) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ C n i → b ≤ ‖a.background.normal s d n x‖) (hupper : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ C n i → ‖a.background.normal s d n x‖ ≤ M) (hfreq : LocalUnweighted s C (1 / 2) fun (n : ℕ) (x : I) (x_1 : D) => 1 / a.background.frequency n) (hcover : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K.carrier n i → x ∈ C n i ∨ ((a.localized i).amplitude n =ᶠ[nhds x] fun (x : D) => 0) ∧ (a.localized i).pressure n =ᶠ[nhds x] fun (x : D) => 0) : 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)

The copy cell may be larger than the native phase patch. Primitive jets are needed only on C; on the remaining points only the two input zero germs are required. In particular no normal or defect estimate is extended from C to K.carrier.

theorem NavierStokes.LocalizedWaveBounds.common_outputs_zero_germ {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : PeriodizedWaveBounds.CopyData D I) (K : PeriodizedWaveBounds.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.amplitude n =ᶠ[nhds x] fun (x : D) => 0) ∧ (a.common.pressure n =ᶠ[nhds x] fun (x : D) => 0) ∧ ((a.commonCorrected s d).amplitude n =ᶠ[nhds x] fun (x : D) => 0) ∧ (a.common.curlCorrection s d n =ᶠ[nhds x] fun (x : D) => 0) ∧ a.globalGood s d n =ᶠ[nhds x] fun (x : D) => 0

noncomputable def NavierStokes.LocalizedWaveBounds.jointNativeFamily {D I : Type} {L : Type u_6} (a : L → PeriodizedWaveBounds.CopyData D I) : WaveFamily D (L × I)

Joint native family, given by WaveFamily.ofCoefficients (fun j => (a j.1).localized j.2).

Equations

• NavierStokes.LocalizedWaveBounds.jointNativeFamily a = NavierStokes.LocalizedWaveBounds.WaveFamily.ofCoefficients fun (j : L × I) => (a j.1).localized j.2

theorem NavierStokes.LocalizedWaveBounds.uniform_common_bounds_from_native_local {D I : Type} {L : Type u_6} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : L → PeriodizedWaveBounds.CopyData D I) (K : L → PeriodizedWaveBounds.Cells D I) (hs : ∀ (l : L) (n : ℕ) (i : I), Function.support ((a l).cutoff n i) ⊆ (K l).carrier n i) {s : WeightedClasses.StripData D} {d : LinearWaveBounds.GraphDirections D} {W : L → ℕ → D → ℝ} {α κ : ℝ} (hW : ∀ (l : L) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W l n x) (h : InputBounds s (fun (n : ℕ) (j : L × I) => (K j.1).carrier n j.2) (fun (n : ℕ) (j : L × I) (x : D) => W j.1 n x) α κ d (jointNativeFamily a)) (hκ : κ ≤ 1 / 2) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (l : L) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ (K l).carrier n i → b ≤ ‖(a l).background.normal s d n x‖) (hupper : ∀ (l : L) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ (K l).carrier n i → ‖(a l).background.normal s d n x‖ ≤ M) (hfreq : LocalUnweighted s (fun (n : ℕ) (j : L × I) => (K j.1).carrier n j.2) (1 / 2) fun (n : ℕ) (j : L × I) (x : D) => 1 / (a j.1).background.frequency n) : (LabelSumBounds.UniformClass s (fun (l : L) (n : ℕ) (x : D) => √(s.zeta x) * W l n x) α fun (l : L) => (a l).common.amplitude) ∧ (LabelSumBounds.UniformClass s (fun (l : L) (n : ℕ) (x : D) => √(s.zeta x) * W l n x) α fun (l : L) => ((a l).commonCorrected s d).amplitude) ∧ (LabelSumBounds.UniformClass s (fun (l : L) (n : ℕ) (x : D) => √(s.zeta x) * W l n x) (α + 1 / 2) fun (l : L) => (a l).common.pressure) ∧ (LabelSumBounds.UniformClass s (fun (l : L) (n : ℕ) (x : D) => √(s.zeta x) * W l n x) (α + 1 / 2 - κ) fun (l : L) => (a l).common.curlCorrection s d) ∧ LabelSumBounds.UniformClass s (fun (l : L) (n : ℕ) (x : D) => √(s.zeta x) * W l n x) (α + 1 / 2 - 3 * κ) fun (l : L) => (a l).globalGood s d

The same proof is uniform in an external spatial label. In particular, no bound is chosen after fixing a label and then incorrectly made uniform.

theorem NavierStokes.LocalizedWaveBounds.uniform_common_bounds_from_supported_native {D I : Type} {L : Type u_6} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : L → PeriodizedWaveBounds.CopyData D I) (K : L → PeriodizedWaveBounds.Cells D I) (hs : ∀ (l : L) (n : ℕ) (i : I), Function.support ((a l).cutoff n i) ⊆ (K l).carrier n i) (C : L → ℕ → I → Set D) {s : WeightedClasses.StripData D} {d : LinearWaveBounds.GraphDirections D} {W : L → ℕ → D → ℝ} {α κ : ℝ} (hW : ∀ (l : L) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W l n x) (h : InputBounds s (fun (n : ℕ) (j : L × I) => C j.1 n j.2) (fun (n : ℕ) (j : L × I) (x : D) => W j.1 n x) α κ d (jointNativeFamily a)) (hκ : κ ≤ 1 / 2) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (l : L) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ C l n i → b ≤ ‖(a l).background.normal s d n x‖) (hupper : ∀ (l : L) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ C l n i → ‖(a l).background.normal s d n x‖ ≤ M) (hfreq : LocalUnweighted s (fun (n : ℕ) (j : L × I) => C j.1 n j.2) (1 / 2) fun (n : ℕ) (j : L × I) (x : D) => 1 / (a j.1).background.frequency n) (hcover : ∀ (l : L) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ (K l).carrier n i → x ∈ C l n i ∨ (((a l).localized i).amplitude n =ᶠ[nhds x] fun (x : D) => 0) ∧ ((a l).localized i).pressure n =ᶠ[nhds x] fun (x : D) => 0) : (LabelSumBounds.UniformClass s (fun (l : L) (n : ℕ) (x : D) => √(s.zeta x) * W l n x) α fun (l : L) => (a l).common.amplitude) ∧ (LabelSumBounds.UniformClass s (fun (l : L) (n : ℕ) (x : D) => √(s.zeta x) * W l n x) α fun (l : L) => ((a l).commonCorrected s d).amplitude) ∧ (LabelSumBounds.UniformClass s (fun (l : L) (n : ℕ) (x : D) => √(s.zeta x) * W l n x) (α + 1 / 2) fun (l : L) => (a l).common.pressure) ∧ (LabelSumBounds.UniformClass s (fun (l : L) (n : ℕ) (x : D) => √(s.zeta x) * W l n x) (α + 1 / 2 - κ) fun (l : L) => (a l).common.curlCorrection s d) ∧ LabelSumBounds.UniformClass s (fun (l : L) (n : ℕ) (x : D) => √(s.zeta x) * W l n x) (α + 1 / 2 - 3 * κ) fun (l : L) => (a l).globalGood s d

Support-local primitive estimates, uniform over both labels and copies, imply the global uniform classes. The phase patch C is allowed to be strictly smaller than each closed copy cell.

Exact identities on an actual open native patch

structure NavierStokes.LocalizedWaveBounds.ExactOn {D : Type u_6} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : LinearWaveBounds.WaveCoefficients D) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) (U : Set D) : Prop

These are geometric and angular identities on one genuine native open set. They impose no condition on the rest of the fast lift.

• isOpen : IsOpen U
• radial_profile : ContDiffOn ℝ (↑⊤) d.radialProfile U
• phase : ContDiffOn ℝ (↑⊤) (a.phase n) U
• amplitude (j : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (x : D) => a.amplitude n x j) U
• radius (x : D) : x ∈ U → DifferentiableAt ℝ (a.radius n) x
• radial_base (x : D) : x ∈ U → DifferentiableAt ℝ (a.radialBase n) x
• frequency_base (x : D) : x ∈ U → DifferentiableAt ℝ (a.frequencyBase n) x
• axial_base (x : D) : x ∈ U → DifferentiableAt ℝ (a.axialBase n) x
• pressure (x : D) : x ∈ U → DifferentiableAt ℝ (a.pressure n) x
• radius_nonzero (x : D) : x ∈ U → a.radius n x ≠ 0
• radial_radius (x : D) : x ∈ U → HarmonicCalculus.along (d.radialField n) (a.radius n) x = 1
• base_angular (x : D) : x ∈ U → ∀ (j : Fin 3), HarmonicCalculus.along (fun (x : D) => d.angular) (fun (y : D) => LinearWaveResidual.base (a.radius n) (a.radialBase n) (a.frequencyBase n) (a.axialBase n) y j) x = 0
• amplitude_angular (j : Fin 3) : Set.EqOn (HarmonicCalculus.along (fun (x : D) => d.angular) fun (y : D) => a.amplitude n y j) (fun (x : D) => 0) U
• phase_angular : ∃ (p : ℝ), Set.EqOn (HarmonicCalculus.along (fun (x : D) => d.angular) (a.phase n)) (fun (x : D) => p) U
• pressure_angular (x : D) : x ∈ U → HarmonicCalculus.along (fun (x : D) => d.angular) (a.pressure n) x = 0

theorem NavierStokes.LocalizedWaveBounds.harmonicResidual_eq_on {D : Type u_6} [NormedAddCommGroup D] [NormedSpace ℝ D] {a : LinearWaveBounds.WaveCoefficients D} {s : WeightedClasses.StripData D} {d : LinearWaveBounds.GraphDirections D} {n : ℕ} {U : Set D} (h : ExactOn a s d n U) {x : D} (hx : x ∈ U) : a.harmonicResidual s d n x = fun (j : Fin 3) => (a.principal s d n x j + a.remainder s d n x j) * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x

theorem NavierStokes.LocalizedWaveBounds.principal_add_at {D : Type u_6} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : LinearWaveBounds.WaveCoefficients D) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (f : ℕ → D → HarmonicCalculus.ComplexVector) (n : ℕ) (x : D) (ha : ∀ (j : Fin 3), DifferentiableAt ℝ (fun (y : D) => a.amplitude n y j) x) (hf : ∀ (j : Fin 3), DifferentiableAt ℝ (fun (y : D) => f n y j) x) : (a.addAmplitude f).principal s d n x = a.principal s d n x + a.principalVelocity s d f n x

theorem NavierStokes.LocalizedWaveBounds.principal_cutoff_at {D : Type u_6} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : LinearWaveBounds.WaveCoefficients D) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (ψ : ℕ → D → ℝ) (source : ℕ → D → HarmonicCalculus.ComplexVector) (n : ℕ) (x : D) (ha : ∀ (j : Fin 3), DifferentiableAt ℝ (fun (y : D) => a.amplitude n y j) x) (hψ : DifferentiableAt ℝ (ψ n) x) : (a.withCutoff ψ).principal s d n x + source n x = ψ n x • (a.principal s d n x + source n x) + LinearWaveBounds.excludedSlotError d ψ a.amplitude source n x

theorem NavierStokes.LocalizedWaveBounds.corrected_coefficient_eq_good_add_excluded_at {D : Type u_6} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : LinearWaveBounds.WaveCoefficients D) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (ψ : ℕ → D → ℝ) (f source : ℕ → D → HarmonicCalculus.ComplexVector) (n : ℕ) (x : D) (ha : ∀ (j : Fin 3), DifferentiableAt ℝ (fun (y : D) => a.amplitude n y j) x) (hψ : DifferentiableAt ℝ (ψ n) x) (hf : ∀ (j : Fin 3), DifferentiableAt ℝ (fun (y : D) => f n y j) x) (hsolve : a.principal s d n x = -source n x) : ((a.withCutoff ψ).addAmplitude f).principal s d n x + ((a.withCutoff ψ).addAmplitude f).remainder s d n x + source n x = a.goodCoefficient s d ψ f n x + LinearWaveBounds.excludedSlotError d ψ a.amplitude source n x

theorem NavierStokes.LocalizedWaveBounds.harmonicResidual_eq_good_add_excluded_on {D : Type u_6} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : LinearWaveBounds.WaveCoefficients D) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (ψ : ℕ → D → ℝ) (f source : ℕ → D → HarmonicCalculus.ComplexVector) (n : ℕ) {U : Set D} (h : ExactOn ((a.withCutoff ψ).addAmplitude f) s d n U) {x : D} (hx : x ∈ U) (ha : ∀ (j : Fin 3), DifferentiableAt ℝ (fun (y : D) => a.amplitude n y j) x) (hψ : DifferentiableAt ℝ (ψ n) x) (hf : ∀ (j : Fin 3), DifferentiableAt ℝ (fun (y : D) => f n y j) x) (hsolve : a.principal s d n x = -source n x) : (((a.withCutoff ψ).addAmplitude f).harmonicResidual s d n x + fun (j : Fin 3) => source n x j * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x) = fun (j : Fin 3) => (a.goodCoefficient s d ψ f n x j + LinearWaveBounds.excludedSlotError d ψ a.amplitude source n x j) * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x

The cutoff/curl identity needs only native smoothness and actual equations on an open native patch. No global InputBounds occurs.