Gaussian coverage for the actual scaled particular solves

The cutoff used by the inverse is the separate Gaussian slot cutoff times the padded native-clock cutoff. The dyadic, radial, and slow source masks remain in the source and amplitude. Whole-path support, rather than a pointwise zero of the source, supplies zero germs for the actual Volterra solution.

Gaussian cutoff errors from support-local primitive estimates

The analytic phase patch may be smaller than the closed periodization cell. Only primitive amplitude/source/cutoff jets on that patch enter the Gaussian estimate. On the remainder of the cell, actual input zero germs imply a zero germ of the two-term cutoff error. The global source complement is retained once, exactly as in CopyData.globalGaussian.

theorem NavierStokes.LocalizedGaussianBounds.localJets_extend_by_zero {D : Type u_1} {E : Type u_2} {I : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {C K : ℕ → I → Set D} {f : ℕ → I → D → E} (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) (hf : PeriodizedWaveBounds.LocalJets s w α C f) (hz : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → x ∉ C n i → f n i =ᶠ[nhds x] fun (x : D) => 0) : PeriodizedWaveBounds.LocalJets s w α K f

Enlarging the set of estimated points through zero neighborhoods preserves the actual native derivative constants.

theorem NavierStokes.LocalizedGaussianBounds.localGaussian_zero_of_cutoff_source {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : PeriodizedWaveBounds.CopyData D I) (d : LinearWaveBounds.GraphDirections D) {n : ℕ} {i : I} {x : D} (hψ : a.cutoff 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

A zero cutoff alone leaves the source. Both zero germs are used.

theorem NavierStokes.LocalizedGaussianBounds.localGaussian_zero_of_inactive {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : PeriodizedWaveBounds.CopyData D I) (d : LinearWaveBounds.GraphDirections D) {n : ℕ} {i : I} {x : D} (h : ((a.cutoff n i =ᶠ[nhds x] fun (x : D) => 0) ∧ a.source n =ᶠ[nhds x] fun (x : D) => 0) ∨ (a.amplitude n i =ᶠ[nhds x] fun (x : D) => 0) ∧ a.source n =ᶠ[nhds x] fun (x : D) => 0) : a.localGaussian d n i =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.LocalizedGaussianBounds.localGaussian_all_gains_from_supported_native {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : PeriodizedWaveBounds.CopyData D I) {s : WeightedClasses.StripData D} (d : LinearWaveBounds.GraphDirections D) (C K : ℕ → I → Set D) {W : ℕ → D → ℝ} {α c : ℝ} (hWnonneg : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W n x) (hψ : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 C a.cutoff) (hfast : WeightedClasses.BandBound s 0 d.fastScale) (hu : PeriodizedWaveBounds.LocalJets s (fun (n : ℕ) (x : D) => √(s.zeta x) * W n x) α C a.amplitude) (hf : PeriodizedWaveBounds.LocalJets s (fun (n : ℕ) (x : D) => √(s.zeta x) * W n x) α C 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 ∈ C n i → W n x ≤ Real.exp (-c * (θ n i x - 1 / 2) ^ 2 * L n)) (hcentral : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ C 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) (houtside : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → x ∉ C n i → ((a.cutoff n i =ᶠ[nhds x] fun (x : D) => 0) ∧ a.source n =ᶠ[nhds x] fun (x : D) => 0) ∨ (a.amplitude n i =ᶠ[nhds x] fun (x : D) => 0) ∧ a.source n =ᶠ[nhds x] fun (x : D) => 0) (β : ℝ) : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) β K (a.localGaussian d)

Gaussian and plateau hypotheses are imposed only on the analytic patch C. No raw-field derivative bound on K \ C is assumed.

theorem NavierStokes.LocalizedGaussianBounds.globalGaussian_all_gains_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) {s : WeightedClasses.StripData D} (d : LinearWaveBounds.GraphDirections D) (C : ℕ → I → Set D) {W : ℕ → D → ℝ} {α c : ℝ} (hWnonneg : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W n x) (hψ : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 C a.cutoff) (hfast : WeightedClasses.BandBound s 0 d.fastScale) (hu : PeriodizedWaveBounds.LocalJets s (fun (n : ℕ) (x : D) => √(s.zeta x) * W n x) α C a.amplitude) (hf : PeriodizedWaveBounds.LocalJets s (fun (n : ℕ) (x : D) => √(s.zeta x) * W n x) α C 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 ∈ C n i → W n x ≤ Real.exp (-c * (θ n i x - 1 / 2) ^ 2 * L n)) (hcentral : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ C 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) (houtside : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K.carrier n i → x ∉ C n i → ((a.cutoff n i =ᶠ[nhds x] fun (x : D) => 0) ∧ a.source n =ᶠ[nhds x] fun (x : D) => 0) ∨ (a.amplitude n i =ᶠ[nhds x] fun (x : D) => 0) ∧ a.source n =ᶠ[nhds x] fun (x : D) => 0) (β : ℝ) (hcomplement : PeriodizedWaveBounds.ComplementJets s (fun (x : ℕ) (x_1 : D) => 1) β K.carrier a.source) : WeightedClasses.UnweightedClass s β (a.globalGaussian d)

The source on the complement of all cells is kept and estimated through hcomplement; it is not replaced by a copywise sum of sources.

theorem NavierStokes.LocalizedGaussianBounds.source_complement_of_zero {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : PeriodizedWaveBounds.CopyData D I) (s : WeightedClasses.StripData D) (K : PeriodizedWaveBounds.Cells D I) (hzero : a.source = fun (x : ℕ) (x_1 : D) => 0) (β : ℝ) : PeriodizedWaveBounds.ComplementJets s (fun (x : ℕ) (x_1 : D) => 1) β K.carrier a.source

Gaussian absorption with an arbitrary extra index

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

The index may be the pair (spatial label, lattice copy). Both the Gaussian envelope and the native length are allowed to depend on it.

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

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

Actual source jets on the uncovered set, with constants chosen before the spatial label as well as the band and point.

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

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

theorem NavierStokes.LocalizedGaussianBounds.UniformComplementJets.of_zero_germs {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} {L : Type u_2} {I : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : WeightedClasses.StripData D) (w : L → ℕ → D → ℝ) (α : ℝ) (K : L → ℕ → I → Set D) (f : L → ℕ → D → E) (hg : ∀ (l : L) (n : ℕ), ∀ x ∈ s.domain, (∀ (i : I), x ∉ K l n i) → f l n =ᶠ[nhds x] fun (x : D) => 0) : UniformComplementJets s w α K f

theorem NavierStokes.LocalizedGaussianBounds.UniformComplementJets.of_germs {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} {L : Type u_2} {I : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : L → ℕ → D → ℝ} {α : ℝ} {K : L → ℕ → I → Set D} {f g : L → ℕ → D → E} (hg : LabelSumBounds.UniformClass s w α g) (he : ∀ (l : L) (n : ℕ), ∀ x ∈ s.domain, (∀ (i : I), x ∉ K l n i) → f l n =ᶠ[nhds x] g l n) : UniformComplementJets s w α K f

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

Primitive cutoff errors, uniformly over spatial labels

noncomputable def NavierStokes.LocalizedGaussianBounds.indexedCutoffError {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (d : LinearWaveBounds.GraphDirections D) (ψ : ℕ → I → D → ℝ) (u f : ℕ → I → D → HarmonicCalculus.ComplexVector) (n : ℕ) (i : I) (x : D) : HarmonicCalculus.ComplexVector

Indexed cutoff error, given by d.Dfast (fun n => ψ n i) n x • u n i x + (1 - ψ n i x) • f n i x.

Equations

• NavierStokes.LocalizedGaussianBounds.indexedCutoffError d ψ u f n i x = d.Dfast (fun (n : ℕ) => ψ n i) n x • u n i x + (1 - ψ n i x) • f n i x

theorem NavierStokes.LocalizedGaussianBounds.indexedCutoffError_wave_class {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} (d : LinearWaveBounds.GraphDirections D) {K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α : ℝ} {ψ : ℕ → I → D → ℝ} {u f : ℕ → I → D → HarmonicCalculus.ComplexVector} (hψ : LocalizedWaveBounds.LocalUnweighted s K 0 ψ) (hfast : WeightedClasses.BandBound s 0 d.fastScale) (hu : LocalizedWaveBounds.LocalClass s K w α u) (hf : LocalizedWaveBounds.LocalClass s K w α f) : LocalizedWaveBounds.LocalClass s K w α (indexedCutoffError d ψ u f)

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

theorem NavierStokes.LocalizedGaussianBounds.uniform_globalGaussian_class_with_complement {D I L : Type} [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) (hg : PeriodizedWaveBounds.UniformLocalJets s w α (fun (l : L) => (K l).carrier) fun (l : L) => (a l).localGaussian d) (hf : UniformComplementJets s w α (fun (l : L) => (K l).carrier) fun (l : L) => (a l).source) : LabelSumBounds.UniformClass s w α fun (l : L) => (a l).globalGaussian d

theorem NavierStokes.LocalizedGaussianBounds.uniform_globalGaussian_all_gains_from_supported_native {D I L : Type} [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) (C : L → ℕ → I → Set D) {W : L → ℕ → D → ℝ} {α c : ℝ} (hWnonneg : ∀ (l : L) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W l n x) (hψ : PeriodizedWaveBounds.UniformLocalJets s (fun (x : L) (x_1 : ℕ) (x_2 : D) => 1) 0 C fun (l : L) => (a l).cutoff) (hfast : WeightedClasses.BandBound s 0 d.fastScale) (hu : PeriodizedWaveBounds.UniformLocalJets s (fun (l : L) (n : ℕ) (x : D) => √(s.zeta x) * W l n x) α C fun (l : L) => (a l).amplitude) (hf : PeriodizedWaveBounds.UniformLocalJets s (fun (l : L) (n : ℕ) (x : D) => √(s.zeta x) * W l n x) α C fun (l : L) (n : ℕ) (x : I) => (a l).source n) (edges : GaussianTailFlat.FlatEdges s) (scales : GaussianTailFlat.BandScaleControl s) (θ : L → ℕ → I → D → ℝ) (length : L → ℕ → ℝ) (hL : ∀ (l : L) (n : ℕ), 0 < length l n) (ell : ℝ) (hell : 0 < ell) (hLell : ∀ (l : L) (n : ℕ), ell * ChartScales.S n ≤ length l n) (hc : 0 < c) (hW : ∀ (l : L) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ C l n i → W l n x ≤ Real.exp (-c * (θ l n i x - 1 / 2) ^ 2 * length l n)) (hcentral : ∀ (l : L) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ C l n i → |θ l n i x - 1 / 2| < 1 / 5 → ((a l).cutoff n i =ᶠ[nhds x] fun (x : D) => 1) ∨ ((a l).amplitude n i =ᶠ[nhds x] fun (x : D) => 0) ∧ (a l).source n =ᶠ[nhds x] fun (x : D) => 0) (houtside : ∀ (l : L) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ (K l).carrier n i → x ∉ C l n i → (((a l).cutoff n i =ᶠ[nhds x] fun (x : D) => 0) ∧ (a l).source n =ᶠ[nhds x] fun (x : D) => 0) ∨ ((a l).amplitude n i =ᶠ[nhds x] fun (x : D) => 0) ∧ (a l).source n =ᶠ[nhds x] fun (x : D) => 0) (β : ℝ) (hcomplement : UniformComplementJets s (fun (x : L) (x_1 : ℕ) (x_2 : D) => 1) β (fun (l : L) => (K l).carrier) fun (l : L) => (a l).source) : LabelSumBounds.UniformClass s (fun (x : L) (x_1 : ℕ) (x_2 : D) => 1) β fun (l : L) => (a l).globalGaussian d

The constants precede every spatial label, band and native copy. The uncovered source is included with its own equally uniform jet bound.

theorem NavierStokes.LocalizedGaussianBounds.uniform_source_complement_of_zero {D I L : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : L → PeriodizedWaveBounds.CopyData D I) (s : WeightedClasses.StripData D) (K : L → PeriodizedWaveBounds.Cells D I) (hzero : ∀ (l : L), (a l).source = fun (x : ℕ) (x_1 : D) => 0) (β : ℝ) : UniformComplementJets s (fun (x : L) (x_1 : ℕ) (x_2 : D) => 1) β (fun (l : L) => (K l).carrier) fun (l : L) => (a l).source

theorem NavierStokes.LocalizedGaussianBounds.uniform_source_patch_jets_of_zero {D I L : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : L → PeriodizedWaveBounds.CopyData D I) (s : WeightedClasses.StripData D) (C : L → ℕ → I → Set D) (hzero : ∀ (l : L), (a l).source = fun (x : ℕ) (x_1 : D) => 0) (w : L → ℕ → D → ℝ) (α : ℝ) : PeriodizedWaveBounds.UniformLocalJets s w α C fun (l : L) (n : ℕ) (x : I) => (a l).source n

The literal harmonic residual supplies the complement

theorem NavierStokes.LocalizedGaussianBounds.source_complement_of_harmonicSupport {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (a : PeriodizedWaveBounds.CopyData ((P × ℝ) × TorusInverse.Plane) TorusInverse.Frequency) (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)) (g : ℕ → CommonCoverSolve.Geometry) (K : ℕ → Set TorusInverse.Plane) (hK : ∀ (n : ℕ), IsCompact (K n)) {U : Set (P × TorusInverse.Plane)} (hU : IsOpen U) (hs : HarmonicSourceSupport.InputSupportOn U (fun (n : ℕ) => HarmonicSourceSupport.nativeUnion (g n) (K n)) b G A) (s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)) (hdom : ∀ x ∈ s.domain, (x.1.1, x.2) ∈ U) (j : ℤ) (hsource : a.source = ParticularWaveAssembly.sourceFamily c u b G A j) (β : ℝ) : PeriodizedWaveBounds.ComplementJets s (fun (x : ℕ) (x_1 : (P × ℝ) × TorusInverse.Plane) => 1) β (fun (n : ℕ) => PeriodizedWaveBounds.nativeCell (g n) (K n)) a.source

theorem NavierStokes.LocalizedGaussianBounds.uniform_source_complement_of_harmonicSupport {P L : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (a : L → PeriodizedWaveBounds.CopyData ((P × ℝ) × TorusInverse.Plane) TorusInverse.Frequency) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : L → CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : L → HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (g : L → ℕ → CommonCoverSolve.Geometry) (K : L → ℕ → Set TorusInverse.Plane) (hK : ∀ (l : L) (n : ℕ), IsCompact (K l n)) {U : Set (P × TorusInverse.Plane)} (hU : IsOpen U) (hs : ∀ (l : L), HarmonicSourceSupport.InputSupportOn U (fun (n : ℕ) => HarmonicSourceSupport.nativeUnion (g l n) (K l n)) (b l) (G l) (A l)) (s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)) (hdom : ∀ x ∈ s.domain, (x.1.1, x.2) ∈ U) (j : L → ℤ) (hsource : ∀ (l : L), (a l).source = ParticularWaveAssembly.sourceFamily c u (b l) (G l) (A l) (j l)) (β : ℝ) : UniformComplementJets s (fun (x : L) (x_1 : ℕ) (x_2 : (P × ℝ) × TorusInverse.Plane) => 1) β (fun (l : L) (n : ℕ) => PeriodizedWaveBounds.nativeCell (g l n) (K l n)) fun (l : L) => (a l).source

theorem NavierStokes.LocalizedGaussianBounds.uniform_source_complement_of_excluded_class {P L : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (a : L → PeriodizedWaveBounds.CopyData ((P × ℝ) × TorusInverse.Plane) TorusInverse.Frequency) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : L → CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : L → HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (g : L → ℕ → CommonCoverSolve.Geometry) (K : L → ℕ → Set TorusInverse.Plane) (hK : ∀ (l : L) (n : ℕ), IsCompact (K l n)) {U : Set (P × TorusInverse.Plane)} (hU : IsOpen U) (hv : ∀ (l : L) (n : ℕ) (i : Fin 3), HarmonicSourceSupport.NonzeroSupportedOn U (HarmonicSourceSupport.nativeUnion (g l n) (K l n)) (HarmonicResidual.realCoefficients ((b l).velocity n i))) (hp : ∀ (l : L) (n : ℕ), HarmonicSourceSupport.NonzeroSupportedOn U (HarmonicSourceSupport.nativeUnion (g l n) (K l n)) (HarmonicResidual.realCoefficients ((b l).pressure n))) (s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)) (hdom : ∀ x ∈ s.domain, (x.1.1, x.2) ∈ U) (j : L → ℤ) (hsource : ∀ (l : L), (a l).source = ParticularWaveAssembly.sourceFamily c u (b l) (G l) (A l) (j l)) {w : L → ℕ → (P × ℝ) × TorusInverse.Plane → ℝ} {β : ℝ} (he : LabelSumBounds.UniformClass s w β fun (l : L) (n : ℕ) => ParticularWaveAssembly.angleLift (HarmonicSourceSupport.excludedSource (G l) (A l) (j l) n)) : UniformComplementJets s w β (fun (l : L) (n : ℕ) => PeriodizedWaveBounds.nativeCell (g l n) (K l n)) fun (l : L) => (a l).source

If an excluded harmonic tail remains outside the cells, its actual uniform class transfers to the literal incoming source. It is kept in the final global Gaussian, not set to zero.

The normalized clock and the actual envelope

theorem NavierStokes.ActualGaussianCoverage.normalized_clock {L c : ℝ} (hL : L ≠ 0) (_hc : c ≠ 0) (v : ℝ) : c * v / L = v / (L / c)

theorem NavierStokes.ActualGaussianCoverage.slotCutoff_clock {L c : ℝ} (hL : L ≠ 0) (hc : c ≠ 0) (v : ℝ) : GaussianTailFlat.slotCutoff L (c * v) = GaussianTailFlat.slotCutoff (L / c) v

noncomputable def NavierStokes.ActualGaussianCoverage.gaussianRate (lam u : ℝ) : ℝ

Gaussian rate, given by u * GaussianEnvelope.referenceMinSlope lam u / 2.

Equations

• NavierStokes.ActualGaussianCoverage.gaussianRate lam u = u * NavierStokes.GaussianEnvelope.referenceMinSlope lam u / 2

theorem NavierStokes.ActualGaussianCoverage.gaussianRate_pos {lam u : ℝ} (hlam : 0 < lam) (hu : 0 < u) : 0 < gaussianRate lam u

theorem NavierStokes.ActualGaussianCoverage.gaussianRate_mono {a b u : ℝ} (hu : 0 < u) (hab : a ≤ b) : gaussianRate a u ≤ gaussianRate b u

theorem NavierStokes.ActualGaussianCoverage.referenceP_scaled_bound {lam u L c : ℝ} (hlam : 0 < lam) (hu : 0 < u) (hL : 0 < L) (hc : 0 < c) {v : ℝ} (hv : v ∈ Set.Icc 0 (L / c)) : PrimaryPulseBounds.referenceP lam u L (c * v) ≤ Real.exp (-(gaussianRate lam u * c) * (v / (L / c) - 1 / 2) ^ 2 * (L / c))

noncomputable def NavierStokes.ActualGaussianCoverage.theta {Label : Type} {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (l : Label) (n : ℕ) (v : ℝ) : ℝ

Theta, given by clock.value l n * v / F.L (l, n).

Equations

• NavierStokes.ActualGaussianCoverage.theta F clock l n v = clock.value l n * v / F.L (l, n)

theorem NavierStokes.ActualGaussianCoverage.theta_eq {Label : Type} {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (l : Label) (n : ℕ) (v : ℝ) : theta F clock l n v = v / ScaledActualParticularControl.length F clock l n

theorem NavierStokes.ActualGaussianCoverage.envelope_uniform_bound {Label : Type} {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) {lam0 u0 : ℝ} (_hlam0 : 0 < lam0) (hu0 : 0 < u0) (hlam : ∀ (l : Label) (n : ℕ), lam0 ≤ F.lam (l, n)) (hu : ∀ (l : Label) (n : ℕ), F.u (l, n) = u0) (l : Label) (n : ℕ) {v : ℝ} (hv : v ∈ Set.Icc 0 (ScaledActualParticularControl.length F clock l n)) : ScaledActualParticularControl.envelope F clock l n v ≤ Real.exp (-(gaussianRate lam0 u0 * clock.lower) * (theta F clock l n v - 1 / 2) ^ 2 * ScaledActualParticularControl.length F clock l n)

theorem NavierStokes.ActualGaussianCoverage.length_uniform_lower {Label : Type} {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) {ell : ℝ} (hL : ∀ (l : Label) (n : ℕ), ell * ChartScales.S n ≤ F.L (l, n)) (l : Label) (n : ℕ) : ell / clock.upper * ChartScales.S n ≤ ScaledActualParticularControl.length F clock l n

Compact whole-path zero germs for the genuine Volterra solve

theorem NavierStokes.ActualGaussianCoverage.whole_path_zero_germ {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) {a b : ℝ} {f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector} {x : P × TorusInverse.Plane} (hf : ∀ v ∈ Set.Icc a b, f =ᶠ[nhds (x.1, g.path k x.2 v)] fun (x : P × TorusInverse.Plane) => 0) : ∀ᶠ (y : P × TorusInverse.Plane) in nhds x, ∀ v ∈ Set.Icc a b, f (y.1, g.path k y.2 v) = 0

theorem NavierStokes.ActualGaussianCoverage.complexCopyVelocity_zero_germ {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k : TorusInverse.Frequency) {f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector} {x : P × TorusInverse.Plane} (hf : ∀ v ∈ Set.Icc a b, f =ᶠ[nhds (x.1, g.path k x.2 v)] fun (x : P × TorusInverse.Plane) => 0) : ParticularWaveBounds.complexCopyVelocity t f g hab k =ᶠ[nhds x] fun (x : P × TorusInverse.Plane) => 0

The separate Gaussian cutoff and its genuine outer padding

noncomputable def NavierStokes.ActualGaussianCoverage.padding (r L : ℝ) : ℝ

Padding, given by min r L / 16.

Equations

• NavierStokes.ActualGaussianCoverage.padding r L = min r L / 16

theorem NavierStokes.ActualGaussianCoverage.padding_pos {r L : ℝ} (hr : 0 < r) (hL : 0 < L) : 0 < padding r L

noncomputable def NavierStokes.ActualGaussianCoverage.referenceWindow (r L : ℝ) (hr : 0 < r) (hL : 0 < L) : PeriodicPhaseAssembly.ClockWindow

Reference window, bundling lower, upper, padding, padding_pos.

Equations

• NavierStokes.ActualGaussianCoverage.referenceWindow r L hr hL = { lower := (-r, 0), upper := (r, L), padding := NavierStokes.ActualGaussianCoverage.padding r L, padding_pos := ⋯ }

theorem NavierStokes.ActualGaussianCoverage.referenceWindow_core (r L : ℝ) (hr : 0 < r) (hL : 0 < L) : (referenceWindow r L hr hL).core = WaveEnvelopeTransport.rectangle r L

noncomputable def NavierStokes.ActualGaussianCoverage.nativeCutoff (r L : ℝ) (hr : 0 < r) (hL : 0 < L) (c : ℝ) : TorusInverse.Plane → ℝ

This cutoff is separate from every dyadic, radial and slow source mask. The outer padding is transported together with the Gaussian.

Equations

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

noncomputable def NavierStokes.ActualGaussianCoverage.outerCell (r L c : ℝ) : Set TorusInverse.Plane

Outer cell, given by Icc (-r - 2 * padding r L) (r + 2 * padding r L) ×ˢ Icc ((-2 * padding r L) / c) ((L + 2 * padding r L) / c).

Equations

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

noncomputable def NavierStokes.ActualGaussianCoverage.sourceCell (r L c : ℝ) : Set TorusInverse.Plane

The support inherited from a Gaussian slot profile has a strict temporal margin at both ends of the full Volterra integration interval.

Equations

• NavierStokes.ActualGaussianCoverage.sourceCell r L c = Set.Icc (-r) r ×ˢ Set.Icc (L / c / 6) (5 * (L / c) / 6)

theorem NavierStokes.ActualGaussianCoverage.outerCell_compact (r L c : ℝ) : IsCompact (outerCell r L c)

theorem NavierStokes.ActualGaussianCoverage.sourceCell_compact (r L c : ℝ) : IsCompact (sourceCell r L c)

theorem NavierStokes.ActualGaussianCoverage.mem_outerCell {r L c : ℝ} (hr : 0 < r) (hL : 0 < L) (hc : 0 < c) (z : TorusInverse.Plane) : z ∈ outerCell r L c ↔ CopySolveCompatibility.nativeTimeMap 0 c z ∈ (referenceWindow r L hr hL).outer

theorem NavierStokes.ActualGaussianCoverage.sourceCell_time {r L c : ℝ} (hL : 0 < L) (hc : 0 < c) {z : TorusInverse.Plane} (hz : z ∈ sourceCell r L c) : z.2 ∈ Set.Ioo 0 (L / c)

theorem NavierStokes.ActualGaussianCoverage.sourceCell_subset_outer {r L c : ℝ} (hr : 0 < r) (hL : 0 < L) (hc : 0 < c) : sourceCell r L c ⊆ outerCell r L c

theorem NavierStokes.ActualGaussianCoverage.nativeCutoff_support {r L c : ℝ} (hr : 0 < r) (hL : 0 < L) (hc : 0 < c) : Function.support (nativeCutoff r L hr hL c) ⊆ outerCell r L c

theorem NavierStokes.ActualGaussianCoverage.nativeCutoff_central_germ {r L c : ℝ} (hr : 0 < r) (hL : 0 < L) (hc : 0 < c) {z : TorusInverse.Plane} (hz : z ∈ WaveEnvelopeTransport.rectangle r (L / c)) (hcentral : |z.2 / (L / c) - 1 / 2| < 1 / 5) : nativeCutoff r L hr hL c =ᶠ[nhds z] fun (x : TorusInverse.Plane) => 1

theorem NavierStokes.ActualGaussianCoverage.nativeCutoff_time_zero_germ {r L c : ℝ} (hr : 0 < r) (hL : 0 < L) (hc : 0 < c) {z : TorusInverse.Plane} (hz : z.2 ∉ Set.Ioo 0 (L / c)) : nativeCutoff r L hr hL c =ᶠ[nhds z] fun (x : TorusInverse.Plane) => 0

Source support controls the entire native path

theorem NavierStokes.ActualGaussianCoverage.coordinates_path_outer (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) {Y : TorusInverse.Plane} {r L c v : ℝ} (hr : 0 < r) (hL : 0 < L) (hc : 0 < c) (hY : g.coordinates k Y ∈ outerCell r L c) (hv : v ∈ Set.Icc 0 (L / c)) : g.coordinates k (g.path k Y v) ∈ outerCell r L c

theorem NavierStokes.ActualGaussianCoverage.other_sourceCell_excluded (g : CommonCoverSolve.Geometry) {r L c : ℝ} (hr : 0 < r) (hL : 0 < L) (hc : 0 < c) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' outerCell r L c)) {k : TorusInverse.Frequency} {Y : TorusInverse.Plane} (hY : g.coordinates k Y ∈ outerCell r L c) (hn : g.coordinates k Y ∉ sourceCell r L c) (i : TorusInverse.Frequency) : g.coordinates i Y ∉ sourceCell r L c

theorem NavierStokes.ActualGaussianCoverage.path_sourceCell_excluded (g : CommonCoverSolve.Geometry) {r L c : ℝ} (hr : 0 < r) (hL : 0 < L) (hc : 0 < c) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' outerCell r L c)) {k : TorusInverse.Frequency} {Y : TorusInverse.Plane} (hY : g.coordinates k Y ∈ outerCell r L c) (hxi : (g.coordinates k Y).1 ∉ Set.Icc (-r) r) (v : ℝ) : v ∈ Set.Icc 0 (L / c) → ∀ (i : TorusInverse.Frequency), g.coordinates i (g.path k Y v) ∉ sourceCell r L c

noncomputable def NavierStokes.ActualGaussianCoverage.sourceRegion {P : Type} (S : Set P) (g : CommonCoverSolve.Geometry) (r L rate : ℝ) : Set (P × TorusInverse.Plane)

Source region, given by Prod.fst ⁻¹' S ∩ HarmonicSourceSupport.nativeUnion g (sourceCell r L rate).

Equations

• NavierStokes.ActualGaussianCoverage.sourceRegion S g r L rate = Prod.fst ⁻¹' S ∩ NavierStokes.HarmonicSourceSupport.nativeUnion g (NavierStokes.ActualGaussianCoverage.sourceCell r L rate)

theorem NavierStokes.ActualGaussianCoverage.sourceRegion_closed {P : Type} [NormedAddCommGroup P] {S : Set P} (hS : IsClosed S) (g : CommonCoverSolve.Geometry) (r L rate : ℝ) : IsClosed (sourceRegion S g r L rate)

theorem NavierStokes.ActualGaussianCoverage.sourceFamily_zero_germ {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (ctx : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) {U : Set (P × TorusInverse.Plane)} {K : ℕ → Set (P × TorusInverse.Plane)} (hU : IsOpen U) (hK : ∀ (n : ℕ), IsClosed (K n)) (hs : HarmonicSourceSupport.InputSupportOn U K b G A) (j : ℤ) (n : ℕ) {x : (P × ℝ) × TorusInverse.Plane} (hx : (x.1.1, x.2) ∈ U) (hn : (x.1.1, x.2) ∉ K n) : ParticularWaveAssembly.sourceFamily ctx u b G A j n =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0

theorem NavierStokes.ActualGaussianCoverage.sourceSupport_mono {P : Type} {U : Set (P × TorusInverse.Plane)} {K T : ℕ → Set (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} (hs : HarmonicSourceSupport.InputSupportOn U K b G A) (hKT : ∀ (n : ℕ), K n ⊆ T n) : HarmonicSourceSupport.InputSupportOn U T b G A

theorem NavierStokes.ActualGaussianCoverage.transported_outer_injective (g : CommonCoverSolve.Geometry) (gap : ℕ) {r L c : ℝ} (hr : 0 < r) (hL : 0 < L) (hc : 0 < c) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' (referenceWindow r L hr hL).outer)) : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (CopySolveCompatibility.transportGeometry g gap 0 c ⋯).center + (CopySolveCompatibility.transportGeometry g gap 0 c ⋯).basis z) '' outerCell r L c)

theorem NavierStokes.ActualGaussianCoverage.reference_outer_separated (g : CommonCoverSolve.Geometry) {r L : ℝ} (hr : 0 < r) (hL : 0 < L) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' (referenceWindow r L hr hL).outer)) : WaveEnvelopeTransport.Separated g r L

One literal family of scaled solves and cutoffs

noncomputable def NavierStokes.ActualGaussianCoverage.cutoffFamily {Label : Type} {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) (l : Label) (n : ℕ) : TorusInverse.Plane → ℝ

Cutoff family, given by nativeCutoff (r l n) (F.L (l,n)) (hr l n) (F.L_pos (l,n)) (clock.value l n).

Equations

• NavierStokes.ActualGaussianCoverage.cutoffFamily F clock r hr l n = NavierStokes.ActualGaussianCoverage.nativeCutoff (r l n) (F.L (l, n)) ⋯ ⋯ (clock.value l n)

noncomputable def NavierStokes.ActualGaussianCoverage.outerFamily {Label : Type} {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (r : Label → ℕ → ℝ) (l : Label) (n : ℕ) : Set TorusInverse.Plane

Outer family, given by outerCell (r l n) (F.L (l,n)) (clock.value l n).

Equations

• NavierStokes.ActualGaussianCoverage.outerFamily F clock r l n = NavierStokes.ActualGaussianCoverage.outerCell (r l n) (F.L (l, n)) (clock.value l n)

noncomputable def NavierStokes.ActualGaussianCoverage.sourceRegions {Label P : Type} {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (S : Label → ℕ → Set P) (l : Label) (n : ℕ) : Set (P × TorusInverse.Plane)

Source regions, given by sourceRegion (S l n) (ScaledActualParticularControl.geometry reference gap clock l n) (r l n) (F.L (l,n)) (clock.value l n).

Equations

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

noncomputable def NavierStokes.ActualGaussianCoverage.analyticPatches {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (s : WeightedClasses.StripData P) (χ : P →L[ℝ] PhaseCalculus.Slow) (φ : Label × ℕ → PhaseCalculus.Slow →L[ℝ] PhaseCalculus.Slow) : Label → ℕ → TorusInverse.Frequency → Set ((P × ℝ) × TorusInverse.Plane)

Analytic patches, constructed using ScaledActualParticularControl.patch.

Equations

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

noncomputable def NavierStokes.ActualGaussianCoverage.data {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) (base : Label → LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (tangent : Label → ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space) (ctx : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : Label → CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : Label → HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (l : Label) : PeriodizedWaveBounds.CopyData ((P × ℝ) × TorusInverse.Plane) TorusInverse.Frequency

The same actual complex solve as the correction step, with entry zero, exit Lref/clock, and a single transported Gaussian-times-padding cutoff.

Equations

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

theorem NavierStokes.ActualGaussianCoverage.data_cutoff_support {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) (base : Label → LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (tangent : Label → ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space) (ctx : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : Label → CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : Label → HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (l : Label) (n : ℕ) (k : TorusInverse.Frequency) : Function.support ((data F clock reference gap r hr base tangent ctx u b G A j l).cutoff n k) ⊆ PeriodizedWaveBounds.nativeCell (ScaledActualParticularControl.geometry reference gap clock l n) (outerFamily F clock r l n) k

theorem NavierStokes.ActualGaussianCoverage.data_central {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) (base : Label → LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (tangent : Label → ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space) (ctx : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : Label → CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : Label → HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (s : WeightedClasses.StripData P) (χ : P →L[ℝ] PhaseCalculus.Slow) (φ : Label × ℕ → PhaseCalculus.Slow →L[ℝ] PhaseCalculus.Slow) (l : Label) (n : ℕ) (k : TorusInverse.Frequency) {x : (P × ℝ) × TorusInverse.Plane} (hx : x ∈ analyticPatches F clock reference gap r s χ φ l n k) (hm : |theta F clock l n ((ScaledActualParticularControl.geometry reference gap clock l n).coordinates k x.2).2 - 1 / 2| < 1 / 5) : (data F clock reference gap r hr base tangent ctx u b G A j l).cutoff n k =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 1

theorem NavierStokes.ActualGaussianCoverage.data_source_zero_germ {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) (base : Label → LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (tangent : Label → ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space) (ctx : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : Label → CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : Label → HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (s : WeightedClasses.StripData P) (S : Label → ℕ → Set P) (hS : ∀ (l : Label) (n : ℕ), IsClosed (S l n)) (hsupport : ∀ (l : Label), HarmonicSourceSupport.InputSupportOn (s.domain ×ˢ Set.univ) (sourceRegions F clock reference gap r S l) (b l) (G l) (A l)) (l : Label) (n : ℕ) {x : (P × ℝ) × TorusInverse.Plane} (hx : x.1.1 ∈ s.domain) (hn : (x.1.1, x.2) ∉ sourceRegions F clock reference gap r S l n) : (data F clock reference gap r hr base tangent ctx u b G A j l).source n =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0

theorem NavierStokes.ActualGaussianCoverage.data_amplitude_zero_germ {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) (base : Label → LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (tangent : Label → ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space) (ctx : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : Label → CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : Label → HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (s : WeightedClasses.StripData P) (S : Label → ℕ → Set P) (hS : ∀ (l : Label) (n : ℕ), IsClosed (S l n)) (hsupport : ∀ (l : Label), HarmonicSourceSupport.InputSupportOn (s.domain ×ˢ Set.univ) (sourceRegions F clock reference gap r S l) (b l) (G l) (A l)) (l : Label) (n : ℕ) (k : TorusInverse.Frequency) {x : (P × ℝ) × TorusInverse.Plane} (hx : x.1.1 ∈ s.domain) (hn : ∀ v ∈ Set.Icc 0 (ScaledActualParticularControl.length F clock l n), (x.1.1, (ScaledActualParticularControl.geometry reference gap clock l n).path k x.2 v) ∉ sourceRegions F clock reference gap r S l n) : (data F clock reference gap r hr base tangent ctx u b G A j l).amplitude n k =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0

theorem NavierStokes.ActualGaussianCoverage.data_outside {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) (base : Label → LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (tangent : Label → ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space) (ctx : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : Label → CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : Label → HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (s : WeightedClasses.StripData P) (S : Label → ℕ → Set P) (hS : ∀ (l : Label) (n : ℕ), IsClosed (S l n)) (hsupport : ∀ (l : Label), HarmonicSourceSupport.InputSupportOn (s.domain ×ˢ Set.univ) (sourceRegions F clock reference gap r S l) (b l) (G l) (A l)) (χ : P →L[ℝ] PhaseCalculus.Slow) (φ : Label × ℕ → PhaseCalculus.Slow →L[ℝ] PhaseCalculus.Slow) (hinside : ∀ (l : Label) (n : ℕ), ∀ p ∈ s.domain, p ∈ S l n → (φ (l, n)) (χ p) ∈ D.carrier (l, n)) (hinj : ∀ (l : Label) (n : ℕ), Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (reference l n).center + (reference l n).basis z) '' (referenceWindow (r l n) (F.L (l, n)) ⋯ ⋯).outer)) (l : Label) (n : ℕ) (k : TorusInverse.Frequency) {x : (P × ℝ) × TorusInverse.Plane} (hx : x ∈ (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip s)).domain) (hk : x ∈ PeriodizedWaveBounds.nativeCell (ScaledActualParticularControl.geometry reference gap clock l n) (outerFamily F clock r l n) k) (hnot : x ∉ analyticPatches F clock reference gap r s χ φ l n k) : (((data F clock reference gap r hr base tangent ctx u b G A j l).cutoff n k =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0) ∧ (data F clock reference gap r hr base tangent ctx u b G A j l).source n =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0) ∨ ((data F clock reference gap r hr base tangent ctx u b G A j l).amplitude n k =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0) ∧ (data F clock reference gap r hr base tangent ctx u b G A j l).source n =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0

The source is supported in an actual closed slow core and in the Gaussian support rectangle. On the rest of a padded copy, either the Gaussian cutoff is zero or the entire source path is zero.

theorem NavierStokes.ActualGaussianCoverage.data_source_complement {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) (base : Label → LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (tangent : Label → ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space) (ctx : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : Label → CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : Label → HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (s : WeightedClasses.StripData P) (S : Label → ℕ → Set P) (hsupport : ∀ (l : Label), HarmonicSourceSupport.InputSupportOn (s.domain ×ˢ Set.univ) (sourceRegions F clock reference gap r S l) (b l) (G l) (A l)) (β : ℝ) : LocalizedGaussianBounds.UniformComplementJets (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip s)) (fun (x : Label) (x_1 : ℕ) (x_2 : (P × ℝ) × TorusInverse.Plane) => 1) β (fun (l : Label) (n : ℕ) => PeriodizedWaveBounds.nativeCell (ScaledActualParticularControl.geometry reference gap clock l n) (outerFamily F clock r l n)) fun (l : Label) => (data F clock reference gap r hr base tangent ctx u b G A j l).source

Uniform jets of the actual Gaussian clock cutoff

theorem NavierStokes.ActualGaussianCoverage.affine_profile_uniform_jets {X Label I : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (s : WeightedClasses.StripData X) (C : Label → ℕ → I → Set X) (A : Label → ℕ → X →L[ℝ] ℝ) (b : Label → ℕ → I → ℝ) (hA : ∃ (K : ℝ), 1 ≤ K ∧ ∃ (p : ℕ), ∀ (l : Label) (n : ℕ), ‖A l n‖ ≤ K * s.slow n ^ p) : PeriodizedWaveBounds.UniformLocalJets s (fun (x : Label) (x_1 : ℕ) (x_2 : X) => 1) 0 C fun (l : Label) (n : ℕ) (i : I) (x : X) => GaussianTailFlat.profile (b l n i + (A l n) x)

Translated native copies share the same constants: only the linear part of their normalized clock enters the estimate.

theorem NavierStokes.ActualGaussianCoverage.inverse_length_bound {Label : Type} {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) {u0 : ℝ} (hu0 : 0 < u0) (hu : ∀ (l : Label) (n : ℕ), F.u (l, n) = u0) (l : Label) (n : ℕ) : (ScaledActualParticularControl.length F clock l n)⁻¹ ≤ clock.upper * F.M / u0

The primitive rate bound for the selected phase family controls the inverse transported slot length without any loss in the copy index.

noncomputable def NavierStokes.ActualGaussianCoverage.normalizedLinear {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CommonCoverSolve.Geometry) (L : ℝ) : P × TorusInverse.Plane →L[ℝ] ℝ

Normalized linear, given by L⁻¹ • ((ContinuousLinearMap.snd ℝ ℝ ℝ).comp (g.coordinateLinear.comp (ContinuousLinearMap.snd ℝ P Plane))).

Equations

• NavierStokes.ActualGaussianCoverage.normalizedLinear g L = L⁻¹ • ContinuousLinearMap.snd ℝ ℝ ℝ ∘SL g.coordinateLinear ∘SL ContinuousLinearMap.snd ℝ P NavierStokes.TorusInverse.Plane

theorem NavierStokes.ActualGaussianCoverage.normalizedLinear_apply {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CommonCoverSolve.Geometry) (L : ℝ) (x : P × TorusInverse.Plane) : (normalizedLinear g L) x = (g.coordinateLinear x.2).2 / L

theorem NavierStokes.ActualGaussianCoverage.normalized_coordinate_affine {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CommonCoverSolve.Geometry) (L : ℝ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) : (g.coordinates k x.2).2 / L = (g.coordinates k 0).2 / L + (normalizedLinear g L) x

theorem NavierStokes.ActualGaussianCoverage.normalizedLinear_norm {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CommonCoverSolve.Geometry) {L : ℝ} (hL : 0 < L) : ‖normalizedLinear g L‖ ≤ L⁻¹ * CommonCoverClass.argumentCost g

theorem NavierStokes.ActualGaussianCoverage.gaussian_clock_uniform_jets {P Label : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (s : WeightedClasses.StripData (P × TorusInverse.Plane)) (C : Label → ℕ → TorusInverse.Frequency → Set (P × TorusInverse.Plane)) (g : Label → ℕ → CommonCoverSolve.Geometry) {u0 : ℝ} (hu0 : 0 < u0) (hu : ∀ (l : Label) (n : ℕ), F.u (l, n) = u0) (hcost : ∃ (K : ℝ), 1 ≤ K ∧ ∃ (p : ℕ), ∀ (l : Label) (n : ℕ), CommonCoverClass.argumentCost (g l n) ≤ K * s.slow n ^ p) : PeriodizedWaveBounds.UniformLocalJets s (fun (x : Label) (x_1 : ℕ) (x_2 : P × TorusInverse.Plane) => 1) 0 C fun (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) => GaussianTailFlat.profile (theta F clock l n ((g l n).coordinates k x.2).2)

theorem NavierStokes.ActualGaussianCoverage.data_cutoff_gaussian_germ {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) (base : Label → LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (tangent : Label → ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space) (ctx : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : Label → CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : Label → HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (s : WeightedClasses.StripData P) (χ : P →L[ℝ] PhaseCalculus.Slow) (φ : Label × ℕ → PhaseCalculus.Slow →L[ℝ] PhaseCalculus.Slow) (l : Label) (n : ℕ) (k : TorusInverse.Frequency) {x : (P × ℝ) × TorusInverse.Plane} (hx : x ∈ analyticPatches F clock reference gap r s χ φ l n k) : (data F clock reference gap r hr base tangent ctx u b G A j l).cutoff n k =ᶠ[nhds x] fun (y : (P × ℝ) × TorusInverse.Plane) => GaussianTailFlat.profile (theta F clock l n ((ScaledActualParticularControl.geometry reference gap clock l n).coordinates k y.2).2)

On the analytic native cell the outer padding is identically one nearby, leaving exactly the normalized Gaussian profile.

theorem NavierStokes.ActualGaussianCoverage.data_cutoff_jets {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) (base : Label → LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (tangent : Label → ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space) (ctx : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : Label → CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : Label → HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (s : WeightedClasses.StripData P) (χ : P →L[ℝ] PhaseCalculus.Slow) (φ : Label × ℕ → PhaseCalculus.Slow →L[ℝ] PhaseCalculus.Slow) {u0 : ℝ} (hu0 : 0 < u0) (hu : ∀ (l : Label) (n : ℕ), F.u (l, n) = u0) (hcost : ∃ (K : ℝ), 1 ≤ K ∧ ∃ (p : ℕ), ∀ (l : Label) (n : ℕ), CommonCoverClass.argumentCost (ScaledActualParticularControl.geometry reference gap clock l n) ≤ K * s.slow n ^ p) : PeriodizedWaveBounds.UniformLocalJets (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip s)) (fun (x : Label) (x_1 : ℕ) (x_2 : (P × ℝ) × TorusInverse.Plane) => 1) 0 (analyticPatches F clock reference gap r s χ φ) fun (l : Label) => (data F clock reference gap r hr base tangent ctx u b G A j l).cutoff

The actual complex solve inherits the modal amplitude estimates

theorem NavierStokes.ActualGaussianCoverage.complex_amplitude_uniform_jets {P Label : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [Countable Label] [Nonempty Label] {s : WeightedClasses.StripData (P × TorusInverse.Plane)} {α : ℝ} (t : Label → ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space) (source : Label → ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : Label → ℕ → CommonCoverSolve.Geometry) (L : Label → ℕ → ℝ) (hL : ∀ (l : Label) (n : ℕ), 0 < L l n) (envelope : Label → ℕ → ℝ → ℝ) (W : Label → ℕ → P × TorusInverse.Plane → ℝ) (d : Label → ℕ → PrimaryODE.FrameData (P × ℝ)) (harmonic : ℤ) (C : Label → ℕ → TorusInverse.Frequency → Set (P × TorusInverse.Plane)) (hr : ParticularCopyBounds.UniformModalControl s α d (fun (l : Label) (n : ℕ) => ParticularWaveBounds.realData (t l n) (source l n)) harmonic g L envelope C) (hi : ParticularCopyBounds.UniformModalControl s α d (fun (l : Label) (n : ℕ) => ParticularWaveBounds.imagData (t l n) (source l n)) harmonic g L envelope C) (hW : ∀ (l : Label) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W l n x) (hcompare : ∀ (l : Label) (n : ℕ) (k : TorusInverse.Frequency), ∀ x ∈ s.domain, x ∈ C l n k → envelope l n ((g l n).coordinates k x.2).2 ≤ W l n x) : PeriodizedWaveBounds.UniformLocalJets s (fun (l : Label) (n : ℕ) (x : P × TorusInverse.Plane) => √(s.zeta x) * W l n x) α C fun (l : Label) (n : ℕ) (k : TorusInverse.Frequency) => ParticularWaveBounds.complexCopyVelocity (t l n) (source l n) (g l n) ⋯ k

The all-powers bound for the assembled, actual Gaussian error

noncomputable def NavierStokes.ActualGaussianCoverage.fieldEnvelope {Label P : Type} {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) : Label → ℕ → (P × ℝ) × TorusInverse.Plane → ℝ

Field envelope, constructed using ActualParticularControl.groupedEnvelope.

Equations

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

theorem NavierStokes.ActualGaussianCoverage.fieldEnvelope_nonneg {Label P : Type} {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (l : Label) (n : ℕ) (x : (P × ℝ) × TorusInverse.Plane) : 0 ≤ fieldEnvelope F clock reference gap r l n x

theorem NavierStokes.ActualGaussianCoverage.fieldEnvelope_eq {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) (s : WeightedClasses.StripData P) (χ : P →L[ℝ] PhaseCalculus.Slow) (φ : Label × ℕ → PhaseCalculus.Slow →L[ℝ] PhaseCalculus.Slow) (hinj : ∀ (l : Label) (n : ℕ), Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (reference l n).center + (reference l n).basis z) '' (referenceWindow (r l n) (F.L (l, n)) ⋯ ⋯).outer)) {l : Label} {n : ℕ} {k : TorusInverse.Frequency} {x : (P × ℝ) × TorusInverse.Plane} (hx : x ∈ analyticPatches F clock reference gap r s χ φ l n k) : fieldEnvelope F clock reference gap r l n x = ScaledActualParticularControl.envelope F clock l n ((ScaledActualParticularControl.geometry reference gap clock l n).coordinates k x.2).2

noncomputable def NavierStokes.ActualGaussianCoverage.cells {Label P : Type} [NormedAddCommGroup P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) (hinj : ∀ (l : Label) (n : ℕ), Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (reference l n).center + (reference l n).basis z) '' (referenceWindow (r l n) (F.L (l, n)) ⋯ ⋯).outer)) (l : Label) : PeriodizedWaveBounds.Cells ((P × ℝ) × TorusInverse.Plane) TorusInverse.Frequency

Cells, constructed using nativeCells.

Equations

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

theorem NavierStokes.ActualGaussianCoverage.globalGaussian_all_gains {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) [Countable Label] [Nonempty Label] (base : Label → LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (tangent : Label → ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space) (ctx : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : Label → CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : Label → HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (s : WeightedClasses.StripData P) (χ : P →L[ℝ] PhaseCalculus.Slow) (φ : Label × ℕ → PhaseCalculus.Slow →L[ℝ] PhaseCalculus.Slow) (frame : Label → ℕ → PrimaryODE.FrameData ((P × ℝ) × ℝ)) {α lam0 u0 ell : ℝ} (hlam0 : 0 < lam0) (hu0 : 0 < u0) (hell : 0 < ell) (hlam : ∀ (l : Label) (n : ℕ), lam0 ≤ F.lam (l, n)) (hu : ∀ (l : Label) (n : ℕ), F.u (l, n) = u0) (hL : ∀ (l : Label) (n : ℕ), ell * ChartScales.S n ≤ F.L (l, n)) (hinj : ∀ (l : Label) (n : ℕ), Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (reference l n).center + (reference l n).basis z) '' (referenceWindow (r l n) (F.L (l, n)) ⋯ ⋯).outer)) (S : Label → ℕ → Set P) (hS : ∀ (l : Label) (n : ℕ), IsClosed (S l n)) (hsupport : ∀ (l : Label), HarmonicSourceSupport.InputSupportOn (s.domain ×ˢ Set.univ) (sourceRegions F clock reference gap r S l) (b l) (G l) (A l)) (hinside : ∀ (l : Label) (n : ℕ), ∀ p ∈ s.domain, p ∈ S l n → (φ (l, n)) (χ p) ∈ D.carrier (l, n)) (hreal : ParticularCopyBounds.UniformModalControl (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip s)) α frame (fun (l : Label) (n : ℕ) => ParticularWaveBounds.realData (tangent l n) (ParticularWaveAssembly.sourceFamily ctx u (b l) (G l) (A l) j n)) j (ScaledActualParticularControl.geometry reference gap clock) (ScaledActualParticularControl.length F clock) (ScaledActualParticularControl.envelope F clock) (analyticPatches F clock reference gap r s χ φ)) (himag : ParticularCopyBounds.UniformModalControl (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip s)) α frame (fun (l : Label) (n : ℕ) => ParticularWaveBounds.imagData (tangent l n) (ParticularWaveAssembly.sourceFamily ctx u (b l) (G l) (A l) j n)) j (ScaledActualParticularControl.geometry reference gap clock) (ScaledActualParticularControl.length F clock) (ScaledActualParticularControl.envelope F clock) (analyticPatches F clock reference gap r s χ φ)) (hsource : PeriodizedWaveBounds.UniformLocalJets (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip s)) (fun (l : Label) (n : ℕ) (x : (P × ℝ) × TorusInverse.Plane) => √(s.zeta x.1.1) * fieldEnvelope F clock reference gap r l n x) α (analyticPatches F clock reference gap r s χ φ) fun (l : Label) (n : ℕ) (x : TorusInverse.Frequency) => ParticularWaveAssembly.sourceFamily ctx u (b l) (G l) (A l) j n) (dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)) (hfast : WeightedClasses.BandBound (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip s)) 0 dirs.fastScale) (edges : GaussianTailFlat.FlatEdges (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip s))) (scales : GaussianTailFlat.BandScaleControl (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip s))) (β : ℝ) : LabelSumBounds.UniformClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip s)) (fun (x : Label) (x_1 : ℕ) (x_2 : (P × ℝ) × TorusInverse.Plane) => 1) β fun (l : Label) => (data F clock reference gap r hr base tangent ctx u b G A j l).globalGaussian dirs

Every real power is gained by the literal global Gaussian error, including its uncovered-source term. The source support assumptions are on the incoming harmonic coefficients; all output zero germs and all cutoff estimates are derived. The modal controls are precisely those constructed by ScaledActualParticularControl.

theorem NavierStokes.ActualGaussianCoverage.source_jets_of_residual_classes {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (s : WeightedClasses.StripData P) (χ : P →L[ℝ] PhaseCalculus.Slow) (φ : Label × ℕ → PhaseCalculus.Slow →L[ℝ] PhaseCalculus.Slow) (ctx : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : Label → CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : Label → HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (α : ℝ) (h : ∀ (i : Fin 3), LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip s) (ActualParticularControl.groupedEnvelope (ScaledActualParticularControl.geometry reference gap clock) r (ScaledActualParticularControl.length F clock) (ScaledActualParticularControl.envelope F clock)) α fun (l : Label) (n : ℕ) (x : P × TorusInverse.Plane) => ((HarmonicResidual.residualBlock ctx u (b l) (G l) (A l)).velocity n i).coeff j x) : PeriodizedWaveBounds.UniformLocalJets (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip s)) (fun (l : Label) (n : ℕ) (x : (P × ℝ) × TorusInverse.Plane) => √(s.zeta x.1.1) * fieldEnvelope F clock reference gap r l n x) α (analyticPatches F clock reference gap r s χ φ) fun (l : Label) (n : ℕ) (x : TorusInverse.Frequency) => ParticularWaveAssembly.sourceFamily ctx u (b l) (G l) (A l) j n

The local source estimate consumed above follows from the actual current harmonic residual classes, with the angular variable inserted by the literal source-family definition.

Bindings to the selected reference window and primary family

noncomputable def NavierStokes.ActualGaussianCoverage.referenceCutoff (r L : ℝ) (hr : 0 < r) (hL : 0 < L) (z : TorusInverse.Plane) : ℝ

Reference cutoff, given by (referenceWindow r L hr hL).cutoff z * GaussianTailFlat.slotCutoff L z.2.

Equations

• NavierStokes.ActualGaussianCoverage.referenceCutoff r L hr hL z = (NavierStokes.ActualGaussianCoverage.referenceWindow r L hr hL).cutoff z * NavierStokes.GaussianTailFlat.slotCutoff L z.2

theorem NavierStokes.ActualGaussianCoverage.nativeCutoff_eq_reference_transport {r L c : ℝ} (hr : 0 < r) (hL : 0 < L) : nativeCutoff r L hr hL c = referenceCutoff r L hr hL ∘ CopySolveCompatibility.nativeTimeMap 0 c

theorem NavierStokes.ActualGaussianCoverage.referenceCutoff_support {r L : ℝ} (hr : 0 < r) (hL : 0 < L) : Function.support (referenceCutoff r L hr hL) ⊆ Set.univ ×ˢ Set.Icc 0 L

theorem NavierStokes.ActualGaussianCoverage.mem_sourceCell_clock {r L c : ℝ} (hc : 0 < c) (z : TorusInverse.Plane) : z ∈ sourceCell r L c ↔ CopySolveCompatibility.nativeTimeMap 0 c z ∈ sourceCell r L 1

theorem NavierStokes.ActualGaussianCoverage.actual_slot_length_pos {D h : ℝ} {vr vt : TorusInverse.Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (m : ℕ) : 0 < ChartScales.slotLength sys.radius h m

theorem NavierStokes.ActualGaussianCoverage.referenceWindow_eq_actual {D h : ℝ} {vr vt : TorusInverse.Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (m : ℕ) : referenceWindow sys.radius (ChartScales.slotLength sys.radius h m) ⋯ ⋯ = ActualSignedGeometry.clockWindow sys m

theorem NavierStokes.ActualGaussianCoverage.actual_outer_injective {D h : ℝ} {vr vt : TorusInverse.Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (hh : 0 ≤ h) {l : SlotColoring.Label} (hl : 4 ≤ l.1) (gap : ℕ) : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (ActualSignedGeometry.slotGeometry sys hdet l gap).center + (ActualSignedGeometry.slotGeometry sys hdet l gap).basis z) '' (referenceWindow sys.radius (ChartScales.slotLength sys.radius h l.1) ⋯ ⋯).outer)

The actual slot system supplies the geometric injectivity needed for finite periodization cells, including their outer padding.

theorem NavierStokes.ActualGaussianCoverage.actual_scaled_slot_lower {D h : ℝ} {vr vt : TorusInverse.Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hh : 0 ≤ h) {m : ℕ} (hm : 4 ≤ m) {c upper : ℝ} (hc : 0 < c) (hcU : c ≤ upper) : 2 * sys.radius / upper * ChartScales.S m ≤ ChartScales.slotLength sys.radius h m / c

theorem NavierStokes.ActualGaussianCoverage.prepared_lambda_lower {profile : OutgoingProfile.Profile} {W : NominalProfile.Witness profile} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (sign : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) : a.M⁻¹ ≤ (PrimaryGeometryAssembly.construction H v a hr0 sign).lam L

theorem NavierStokes.ActualGaussianCoverage.prepared_gaussian_rate_pos {profile : OutgoingProfile.Profile} {W : NominalProfile.Witness profile} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) : 0 < gaussianRate a.M⁻¹ a.u

noncomputable def NavierStokes.ActualGaussianCoverage.actualSlowCore {profile : OutgoingProfile.Profile} {W : NominalProfile.Witness profile} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (L : PrimaryGeometryAssembly.Index W a.N) : Set PhaseCalculus.Slow

The closed slow support is the actual one-mesh primary mask. Its inclusion in the two-mesh analytic phase cell has a genuine margin.

Equations

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

theorem NavierStokes.ActualGaussianCoverage.actualSlowCore_closed {profile : OutgoingProfile.Profile} {W : NominalProfile.Witness profile} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (L : PrimaryGeometryAssembly.Index W a.N) : IsClosed (actualSlowCore H v a L)

theorem NavierStokes.ActualGaussianCoverage.actualSlowCore_inside {profile : OutgoingProfile.Profile} {W : NominalProfile.Witness profile} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (L : PrimaryGeometryAssembly.Index W a.N) {p : PhaseCalculus.Slow} (hp : p ∈ actualSlowCore H v a L) (ht : 0 < p.2.2) : p ∈ (PrimaryGeometryAssembly.domain W a.N).carrier L

noncomputable def NavierStokes.ActualGaussianCoverage.actualSourceCore {profile : OutgoingProfile.Profile} {W : NominalProfile.Witness profile} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (L : PrimaryGeometryAssembly.Index W a.N) : Set ActualSignedGeometry.Native

Actual source core, given by actualSlowCore H v a L ×ˢ sourceCell r0 (ChartScales.slotLength r0 profile.data.h (BaseChartJets.cellBand L)) 1.

Equations

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

theorem NavierStokes.ActualGaussianCoverage.actualSourceCore_closed {profile : OutgoingProfile.Profile} {W : NominalProfile.Witness profile} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (L : PrimaryGeometryAssembly.Index W a.N) : IsClosed (actualSourceCore H v a L)

theorem NavierStokes.ActualGaussianCoverage.actualMask_support {profile : OutgoingProfile.Profile} {W : NominalProfile.Witness profile} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (L : PrimaryGeometryAssembly.Index W a.N) : Function.support (ActualSignedGeometry.nativeCutoff H v a L) ⊆ actualSourceCore H v a L

The full actual source mask retains all its factors. Its support is contained in the closed slow core and the Gaussian support rectangle; none of the dyadic or radial factors is asserted to equal one.

theorem NavierStokes.ActualGaussianCoverage.actualMask_tsupport {profile : OutgoingProfile.Profile} {W : NominalProfile.Witness profile} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (L : PrimaryGeometryAssembly.Index W a.N) : tsupport (ActualSignedGeometry.nativeCutoff H v a L) ⊆ actualSourceCore H v a L

theorem NavierStokes.ActualGaussianCoverage.actualMask_jet_support {profile : OutgoingProfile.Profile} {W : NominalProfile.Witness profile} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (L : PrimaryGeometryAssembly.Index W a.N) (m : ℕ) : tsupport (iteratedFDeriv ℝ m (ActualSignedGeometry.nativeCutoff H v a L)) ⊆ actualSourceCore H v a L

theorem NavierStokes.ActualGaussianCoverage.actualMask_transported_support {profile : OutgoingProfile.Profile} {W : NominalProfile.Witness profile} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (L : PrimaryGeometryAssembly.Index W a.N) (χ : P →L[ℝ] PhaseCalculus.Slow) (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) {c : ℝ} (hc : 0 < c) : (Function.support fun (x : P × TorusInverse.Plane) => ActualSignedGeometry.nativeCutoff H v a L (χ x.1, CopySolveCompatibility.nativeTimeMap 0 c (g.coordinates k x.2))) ⊆ sourceRegion (⇑χ ⁻¹' actualSlowCore H v a L) g r0 (ChartScales.slotLength r0 profile.data.h (BaseChartJets.cellBand L)) c

Clock transport of the full actual mask supplies the exact closed source region used above. The spatial mask remains part of the source.

theorem NavierStokes.ActualGaussianCoverage.actualMask_transported_tsupport {profile : OutgoingProfile.Profile} {W : NominalProfile.Witness profile} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (L : PrimaryGeometryAssembly.Index W a.N) (χ : P →L[ℝ] PhaseCalculus.Slow) (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) {c : ℝ} (hc : 0 < c) : (tsupport fun (x : P × TorusInverse.Plane) => ActualSignedGeometry.nativeCutoff H v a L (χ x.1, CopySolveCompatibility.nativeTimeMap 0 c (g.coordinates k x.2))) ⊆ sourceRegion (⇑χ ⁻¹' actualSlowCore H v a L) g r0 (ChartScales.slotLength r0 profile.data.h (BaseChartJets.cellBand L)) c

theorem NavierStokes.ActualGaussianCoverage.actualMask_transported_jet_support {profile : OutgoingProfile.Profile} {W : NominalProfile.Witness profile} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (L : PrimaryGeometryAssembly.Index W a.N) (χ : P →L[ℝ] PhaseCalculus.Slow) (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) {c : ℝ} (hc : 0 < c) (m : ℕ) : tsupport (iteratedFDeriv ℝ m fun (x : P × TorusInverse.Plane) => ActualSignedGeometry.nativeCutoff H v a L (χ x.1, CopySolveCompatibility.nativeTimeMap 0 c (g.coordinates k x.2))) ⊆ sourceRegion (⇑χ ⁻¹' actualSlowCore H v a L) g r0 (ChartScales.slotLength r0 profile.data.h (BaseChartJets.cellBand L)) c

A weighted companion for physical edge estimates

theorem NavierStokes.ActualGaussianCoverage.gaussian_epsilon_shift {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (s : WeightedClasses.StripData X) (scales : GaussianTailFlat.BandScaleControl s) {c : ℝ} (hc : 0 < c) (α β : ℝ) : ∃ (B : ℝ), 0 < B ∧ ∀ (n : ℕ), s.epsilon n ^ α * Real.exp (-c * ChartScales.S n) ≤ B * s.epsilon n ^ β

Only the dyadic exponent is absorbed. The flat edge weight is retained for the subsequent physical extension estimate.

theorem NavierStokes.ActualGaussianCoverage.indexed_gaussian_weighted_all_gains {X E I : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData X} {K : ℕ → I → Set X} {W : ℕ → I → X → ℝ} {α c : ℝ} {f : ℕ → I → X → E} (hf : LocalizedWaveBounds.LocalWave s K W α f) (scales : GaussianTailFlat.BandScaleControl s) (θ : ℕ → I → X → ℝ) (L : ℕ → I → ℝ) (hL : ∀ (n : ℕ) (i : I), 0 < L n i) (ell : ℝ) (hell : 0 < ell) (hLell : ∀ (n : ℕ) (i : I), ell * ChartScales.S n ≤ L n i) (hc : 0 < c) (hW : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → W n i x ≤ Real.exp (-c * (θ n i x - 1 / 2) ^ 2 * L n i)) (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 : X) => 0) (β : ℝ) : LocalizedWaveBounds.LocalClass s K (fun (x : ℕ) (x_1 : I) (x_2 : X) => √(s.zeta x_2)) β f

The Gaussian gain preserves sqrt(zeta) exactly. Unlike the unweighted absorption theorem, this estimate retains its original polynomial inverse-edge degree; the positive edge weight remains available to absorb that degree in physical coordinates.

theorem NavierStokes.ActualGaussianCoverage.uniform_globalGaussian_weighted_from_supported_native {X I Label : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (a : Label → PeriodizedWaveBounds.CopyData X I) (K : Label → PeriodizedWaveBounds.Cells X I) (hs : ∀ (l : Label) (n : ℕ) (i : I), Function.support ((a l).cutoff n i) ⊆ (K l).carrier n i) {s : WeightedClasses.StripData X} (d : LinearWaveBounds.GraphDirections X) (C : Label → ℕ → I → Set X) {W : Label → ℕ → X → ℝ} {α c : ℝ} (hWnonneg : ∀ (l : Label) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W l n x) (hψ : PeriodizedWaveBounds.UniformLocalJets s (fun (x : Label) (x_1 : ℕ) (x_2 : X) => 1) 0 C fun (l : Label) => (a l).cutoff) (hfast : WeightedClasses.BandBound s 0 d.fastScale) (hu : PeriodizedWaveBounds.UniformLocalJets s (fun (l : Label) (n : ℕ) (x : X) => √(s.zeta x) * W l n x) α C fun (l : Label) => (a l).amplitude) (hf : PeriodizedWaveBounds.UniformLocalJets s (fun (l : Label) (n : ℕ) (x : X) => √(s.zeta x) * W l n x) α C fun (l : Label) (n : ℕ) (x : I) => (a l).source n) (scales : GaussianTailFlat.BandScaleControl s) (θ : Label → ℕ → I → X → ℝ) (length : Label → ℕ → ℝ) (hL : ∀ (l : Label) (n : ℕ), 0 < length l n) (ell : ℝ) (hell : 0 < ell) (hLell : ∀ (l : Label) (n : ℕ), ell * ChartScales.S n ≤ length l n) (hc : 0 < c) (hW : ∀ (l : Label) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ C l n i → W l n x ≤ Real.exp (-c * (θ l n i x - 1 / 2) ^ 2 * length l n)) (hcentral : ∀ (l : Label) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ C l n i → |θ l n i x - 1 / 2| < 1 / 5 → ((a l).cutoff n i =ᶠ[nhds x] fun (x : X) => 1) ∨ ((a l).amplitude n i =ᶠ[nhds x] fun (x : X) => 0) ∧ (a l).source n =ᶠ[nhds x] fun (x : X) => 0) (houtside : ∀ (l : Label) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ (K l).carrier n i → x ∉ C l n i → (((a l).cutoff n i =ᶠ[nhds x] fun (x : X) => 0) ∧ (a l).source n =ᶠ[nhds x] fun (x : X) => 0) ∨ ((a l).amplitude n i =ᶠ[nhds x] fun (x : X) => 0) ∧ (a l).source n =ᶠ[nhds x] fun (x : X) => 0) (β : ℝ) (hcomplement : LocalizedGaussianBounds.UniformComplementJets s (fun (x : Label) (x_1 : ℕ) (x_2 : X) => √(s.zeta x_2)) β (fun (l : Label) => (K l).carrier) fun (l : Label) => (a l).source) : LabelSumBounds.UniformClass s (fun (x : Label) (x_1 : ℕ) (x_2 : X) => √(s.zeta x_2)) β fun (l : Label) => (a l).globalGaussian d

Weighted counterpart of the frozen LGB gluing theorem. The source complement retains the same edge weight and still occurs exactly once.

theorem NavierStokes.ActualGaussianCoverage.globalGaussian_weighted_all_gains {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) [Countable Label] [Nonempty Label] (base : Label → LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (tangent : Label → ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space) (ctx : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : Label → CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : Label → HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (s : WeightedClasses.StripData P) (χ : P →L[ℝ] PhaseCalculus.Slow) (φ : Label × ℕ → PhaseCalculus.Slow →L[ℝ] PhaseCalculus.Slow) (frame : Label → ℕ → PrimaryODE.FrameData ((P × ℝ) × ℝ)) {α lam0 u0 ell : ℝ} (hlam0 : 0 < lam0) (hu0 : 0 < u0) (hell : 0 < ell) (hlam : ∀ (l : Label) (n : ℕ), lam0 ≤ F.lam (l, n)) (hu : ∀ (l : Label) (n : ℕ), F.u (l, n) = u0) (hL : ∀ (l : Label) (n : ℕ), ell * ChartScales.S n ≤ F.L (l, n)) (hinj : ∀ (l : Label) (n : ℕ), Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (reference l n).center + (reference l n).basis z) '' (referenceWindow (r l n) (F.L (l, n)) ⋯ ⋯).outer)) (S : Label → ℕ → Set P) (hS : ∀ (l : Label) (n : ℕ), IsClosed (S l n)) (hsupport : ∀ (l : Label), HarmonicSourceSupport.InputSupportOn (s.domain ×ˢ Set.univ) (sourceRegions F clock reference gap r S l) (b l) (G l) (A l)) (hinside : ∀ (l : Label) (n : ℕ), ∀ p ∈ s.domain, p ∈ S l n → (φ (l, n)) (χ p) ∈ D.carrier (l, n)) (hreal : ParticularCopyBounds.UniformModalControl (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip s)) α frame (fun (l : Label) (n : ℕ) => ParticularWaveBounds.realData (tangent l n) (ParticularWaveAssembly.sourceFamily ctx u (b l) (G l) (A l) j n)) j (ScaledActualParticularControl.geometry reference gap clock) (ScaledActualParticularControl.length F clock) (ScaledActualParticularControl.envelope F clock) (analyticPatches F clock reference gap r s χ φ)) (himag : ParticularCopyBounds.UniformModalControl (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip s)) α frame (fun (l : Label) (n : ℕ) => ParticularWaveBounds.imagData (tangent l n) (ParticularWaveAssembly.sourceFamily ctx u (b l) (G l) (A l) j n)) j (ScaledActualParticularControl.geometry reference gap clock) (ScaledActualParticularControl.length F clock) (ScaledActualParticularControl.envelope F clock) (analyticPatches F clock reference gap r s χ φ)) (hsource : PeriodizedWaveBounds.UniformLocalJets (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip s)) (fun (l : Label) (n : ℕ) (x : (P × ℝ) × TorusInverse.Plane) => √(s.zeta x.1.1) * fieldEnvelope F clock reference gap r l n x) α (analyticPatches F clock reference gap r s χ φ) fun (l : Label) (n : ℕ) (x : TorusInverse.Frequency) => ParticularWaveAssembly.sourceFamily ctx u (b l) (G l) (A l) j n) (dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)) (hfast : WeightedClasses.BandBound (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip s)) 0 dirs.fastScale) (scales : GaussianTailFlat.BandScaleControl (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip s))) (β : ℝ) : LabelSumBounds.UniformClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip s)) (fun (x : Label) (x_1 : ℕ) (x_2 : (P × ℝ) × TorusInverse.Plane) => √(s.zeta x_2.1.1)) β fun (l : Label) => (data F clock reference gap r hr base tangent ctx u b G A j l).globalGaussian dirs

The actual Gaussian error retains precisely the flat sqrt(zeta) weight at every decay exponent. This companion is suitable for the physical local-source bounds; no completed edge extension is assumed.