Smooth zero extension across both moving radial edges

The raw coefficient is used only inside the annulus. Gaussian bounds on its actual full derivative tensors prove that its literal zero extension has all derivatives zero on both moving boundary hypersurfaces.

noncomputable def NavierStokes.WaveEdgeExtension.window {D : Type u_1} (ρ : D → ℝ) (a b : ℝ) : Set D

Window, given by {x | a < ρ x ∧ ρ x < b}.

Equations

• NavierStokes.WaveEdgeExtension.window ρ a b = {x : D | a < ρ x ∧ ρ x < b}

noncomputable def NavierStokes.WaveEdgeExtension.windowDomain {D : Type u_1} (Ω : Set D) (ρ : D → ℝ) (a b : ℝ) : Set D

Window domain, given by Ω ∩ window ρ a b.

Equations

• NavierStokes.WaveEdgeExtension.windowDomain Ω ρ a b = Ω ∩ NavierStokes.WaveEdgeExtension.window ρ a b

noncomputable def NavierStokes.WaveEdgeExtension.extension {D : Type u_1} {E : Type u_2} [NormedAddCommGroup E] (ρ : D → ℝ) (a b : ℝ) (f : D → E) (x : D) : E

Extension as an element of E.

Equations

• NavierStokes.WaveEdgeExtension.extension ρ a b f x = if x ∈ NavierStokes.WaveEdgeExtension.window ρ a b then f x else 0

theorem NavierStokes.WaveEdgeExtension.extension_inside {D : Type u_1} {E : Type u_2} [NormedAddCommGroup E] (ρ : D → ℝ) (a b : ℝ) (f : D → E) {x : D} (hx : x ∈ window ρ a b) : extension ρ a b f x = f x

theorem NavierStokes.WaveEdgeExtension.extension_outside {D : Type u_1} {E : Type u_2} [NormedAddCommGroup E] (ρ : D → ℝ) (a b : ℝ) (f : D → E) {x : D} (hx : x ∉ window ρ a b) : extension ρ a b f x = 0

theorem NavierStokes.WaveEdgeExtension.windowDomain_open {D : Type u_1} [NormedAddCommGroup D] {Ω : Set D} (hΩ : IsOpen Ω) {ρ : D → ℝ} (hρ : ContinuousOn ρ Ω) (a b : ℝ) : IsOpen (windowDomain Ω ρ a b)

theorem NavierStokes.WaveEdgeExtension.extension_germ_inside {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedAddCommGroup E] {ρ : D → ℝ} (a b : ℝ) (f : D → E) {x : D} (hρ : ContinuousAt ρ x) (hx : x ∈ window ρ a b) : extension ρ a b f =ᶠ[nhds x] f

theorem NavierStokes.WaveEdgeExtension.extension_germ_left {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedAddCommGroup E] {ρ : D → ℝ} (a b : ℝ) (f : D → E) {x : D} (hρ : ContinuousAt ρ x) (hx : ρ x < a) : extension ρ a b f =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.WaveEdgeExtension.extension_germ_right {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedAddCommGroup E] {ρ : D → ℝ} (a b : ℝ) (f : D → E) {x : D} (hρ : ContinuousAt ρ x) (hx : b < ρ x) : extension ρ a b f =ᶠ[nhds x] fun (x : D) => 0

def NavierStokes.WaveEdgeExtension.EdgeControl {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedAddCommGroup E] (ρ : D → ℝ) (a b : ℝ) (d : D → ℝ) (c : ℝ) (g : D → E) (x : D) : Prop

A local bound on actual tensors from the interior side of an edge.

Equations

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

theorem NavierStokes.WaveEdgeExtension.hasFDerivAt_extension_boundary {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {ρ d : D → ℝ} {a b c : ℝ} {g : D → E} {x : D} (hc : 0 < c) (hx : x ∉ window ρ a b) (hd : DifferentiableAt ℝ d x) (hdx : d x = 0) (hB : EdgeControl ρ a b d c g x) : HasFDerivAt (extension ρ a b g) 0 x

A smooth defining function may replace the straight edge coordinate. Its actual derivative controls its distance by ambient distance.

noncomputable def NavierStokes.WaveEdgeExtension.logCoordinate {D : Type u_1} (ρ : D → ℝ) (a : ℝ) (x : D) : ℝ

Log coordinate, given by WeightedRadialPrimitive.logPosition a (ρ x).

Equations

• NavierStokes.WaveEdgeExtension.logCoordinate ρ a x = NavierStokes.WeightedRadialPrimitive.logPosition a (ρ x)

theorem NavierStokes.WaveEdgeExtension.logCoordinate_differentiableAt {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {ρ : D → ℝ} {a : ℝ} (ha : 0 < a) {x : D} (hρ : DifferentiableAt ℝ ρ x) (hx : 0 < ρ x) : DifferentiableAt ℝ (logCoordinate ρ a) x

def NavierStokes.WaveEdgeExtension.BoundaryControls {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (Ω : Set D) (ρ : D → ℝ) (a b cL cR : ℝ) (f : D → E) : Prop

Boundary controls as an element of Prop.

Equations

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

noncomputable def NavierStokes.WaveEdgeExtension.extendedJets {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (ρ : D → ℝ) (a b : ℝ) (f : D → E) (x : D) : FormalMultilinearSeries ℝ D E

Extended jets, defined pointwise by extension ρ a b (iteratedFDeriv ℝ n f) x.

Equations

• NavierStokes.WaveEdgeExtension.extendedJets ρ a b f x n = NavierStokes.WaveEdgeExtension.extension ρ a b (iteratedFDeriv ℝ n f) x

theorem NavierStokes.WaveEdgeExtension.extendedJets_hasFDerivAt {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Set D} (hΩ : IsOpen Ω) {ρ : D → ℝ} (hρ : ContDiffOn ℝ (↑⊤) ρ Ω) {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) {f : D → E} (hf : ContDiffOn ℝ (↑⊤) f (windowDomain Ω ρ a b)) (hB : BoundaryControls Ω ρ a b cL cR f) (n : ℕ) {x : D} (hx : x ∈ Ω) : HasFDerivAt (fun (y : D) => extendedJets ρ a b f y n) (extendedJets ρ a b f x (n + 1)).curryLeft x

theorem NavierStokes.WaveEdgeExtension.hasFTaylorSeriesUpToOn_extension {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Set D} (hΩ : IsOpen Ω) {ρ : D → ℝ} (hρ : ContDiffOn ℝ (↑⊤) ρ Ω) {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) {f : D → E} (hf : ContDiffOn ℝ (↑⊤) f (windowDomain Ω ρ a b)) (hB : BoundaryControls Ω ρ a b cL cR f) : HasFTaylorSeriesUpToOn (↑⊤) (extension ρ a b f) (extendedJets ρ a b f) Ω

theorem NavierStokes.WaveEdgeExtension.extension_contDiffOn {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Set D} (hΩ : IsOpen Ω) {ρ : D → ℝ} (hρ : ContDiffOn ℝ (↑⊤) ρ Ω) {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) {f : D → E} (hf : ContDiffOn ℝ (↑⊤) f (windowDomain Ω ρ a b)) (hB : BoundaryControls Ω ρ a b cL cR f) : ContDiffOn ℝ (↑⊤) (extension ρ a b f) Ω

theorem NavierStokes.WaveEdgeExtension.iteratedFDeriv_extension {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Set D} (hΩ : IsOpen Ω) {ρ : D → ℝ} (hρ : ContDiffOn ℝ (↑⊤) ρ Ω) {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) {f : D → E} (hf : ContDiffOn ℝ (↑⊤) f (windowDomain Ω ρ a b)) (hB : BoundaryControls Ω ρ a b cL cR f) (n : ℕ) {x : D} (hx : x ∈ Ω) : iteratedFDeriv ℝ n (extension ρ a b f) x = extension ρ a b (iteratedFDeriv ℝ n f) x

theorem NavierStokes.WaveEdgeExtension.iteratedFDeriv_extension_edge {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Set D} (hΩ : IsOpen Ω) {ρ : D → ℝ} (hρ : ContDiffOn ℝ (↑⊤) ρ Ω) {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) {f : D → E} (hf : ContDiffOn ℝ (↑⊤) f (windowDomain Ω ρ a b)) (hB : BoundaryControls Ω ρ a b cL cR f) (n : ℕ) {x : D} (hx : x ∈ Ω) (hedge : ρ x = a ∨ ρ x = b) : iteratedFDeriv ℝ n (extension ρ a b f) x = 0

Explicit two-edge Gaussian bounds

theorem NavierStokes.WaveEdgeExtension.sqrt_zeta {L t : ℝ} (ht : t ∈ Set.Ioo 0 L) (cL cR : ℝ) : √(WeightedRadialPrimitive.zeta cL cR L t) = WeightedRadialPrimitive.zeta (cL / 2) (cR / 2) L t

theorem NavierStokes.WaveEdgeExtension.half_weight_left {cL cR L t : ℝ} (hcR : 0 ≤ cR) (ht : 0 < t) (ht1 : t ≤ 1) (htL : t ≤ L / 2) (m : ℕ) : max 1 (WeightedRadialPrimitive.delta L t)⁻¹ ^ m * √(WeightedRadialPrimitive.zeta cL cR L t) ≤ FlatCutoff.edge (cL / 2) t / t ^ m

theorem NavierStokes.WaveEdgeExtension.half_weight_right {cL cR L t : ℝ} (hcL : 0 ≤ cL) (ht : t < L) (ht1 : L - t ≤ 1) (htL : L / 2 ≤ t) (m : ℕ) : max 1 (WeightedRadialPrimitive.delta L t)⁻¹ ^ m * √(WeightedRadialPrimitive.zeta cL cR L t) ≤ FlatCutoff.edge (cR / 2) (L - t) / (L - t) ^ m

noncomputable def NavierStokes.WaveEdgeExtension.flatWeight {D : Type u_1} (ρ : D → ℝ) (a b cL cR : ℝ) (x : D) : ℝ

Flat weight, given by WeightedRadialPrimitive.zeta cL cR (WeightedRadialPrimitive.logLength a b) (logCoordinate ρ a x).

Equations

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

noncomputable def NavierStokes.WaveEdgeExtension.edgeGrowth {D : Type u_1} (ρ : D → ℝ) (a b : ℝ) (x : D) : ℝ

Edge growth, given by max 1 (WeightedRadialPrimitive.delta (WeightedRadialPrimitive.logLength a b) (logCoordinate ρ a x))⁻¹.

Equations

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

theorem NavierStokes.WaveEdgeExtension.edgeGrowth_one_le {D : Type u_1} (ρ : D → ℝ) (a b : ℝ) (x : D) : 1 ≤ edgeGrowth ρ a b x

theorem NavierStokes.WaveEdgeExtension.boundaryControls_of_majorants {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Set D} (hΩ : IsOpen Ω) {ρ P : D → ℝ} (hρ : ContDiffOn ℝ (↑⊤) ρ Ω) (hP : ContinuousOn P Ω) {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) {f : D → E} (hb : ∀ (m : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∃ (N : ℕ), ∀ y ∈ windowDomain Ω ρ a b, ‖iteratedFDeriv ℝ m f y‖ ≤ C * edgeGrowth ρ a b y ^ N * √(flatWeight ρ a b cL cR y) * P y) : BoundaryControls Ω ρ a b (cL / 2) (cR / 2) f

The actual square-root two-edge weight supplies both boundary controls. The envelope only needs to be continuous near the boundary, where its local bound is absorbed into the constant.

theorem NavierStokes.WaveEdgeExtension.native_jet_majorant {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {ι : Type u_3} {V : PrimaryCopyBounds.JetDomain ι X} {Ω : Set X} {ρ : X → ℝ} {a b cL cR : ℝ} {A S : ι → ℝ} {P : ι → X → ℝ} {f : ι → X → E} (hf : PrimaryCopyBounds.NativeJets V (fun (i : ι) (x : X) => A i * √(flatWeight ρ a b cL cR x) * P i x) f) (hA : ∀ (i : ι), 0 ≤ A i) (hS : ∀ (i : ι), 1 ≤ S i) (hP : ∀ (i : ι), ∀ x ∈ Ω, 0 ≤ P i x) (hdom : ∀ (i : ι), windowDomain Ω ρ a b ⊆ V.carrier i) (q : ℕ) (hG : ∀ (i : ι), ∀ x ∈ windowDomain Ω ρ a b, V.growth i x ≤ S i * edgeGrowth ρ a b x ^ q) (i : ι) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (N : ℕ), ∀ x ∈ windowDomain Ω ρ a b, ‖iteratedFDeriv ℝ m (f i) x‖ ≤ C * edgeGrowth ρ a b x ^ N * √(flatWeight ρ a b cL cR x) * P i x

Reduce the actual native class estimate without differentiating the weight or discarding any of its flat-edge factor.

theorem NavierStokes.WaveEdgeExtension.NativeJets.moving_zero_extension {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {ι : Type u_3} {V : PrimaryCopyBounds.JetDomain ι X} {Ω : Set X} (hΩ : IsOpen Ω) {ρ : X → ℝ} (hρ : ContDiffOn ℝ (↑⊤) ρ Ω) {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) {A S : ι → ℝ} {P : ι → X → ℝ} {f : ι → X → E} (hf : PrimaryCopyBounds.NativeJets V (fun (i : ι) (x : X) => A i * √(flatWeight ρ a b cL cR x) * P i x) f) (hA : ∀ (i : ι), 0 ≤ A i) (hS : ∀ (i : ι), 1 ≤ S i) (hP : ∀ (i : ι), ContinuousOn (P i) Ω) (hP0 : ∀ (i : ι), ∀ x ∈ Ω, 0 ≤ P i x) (hdom : ∀ (i : ι), windowDomain Ω ρ a b ⊆ V.carrier i) (q : ℕ) (hG : ∀ (i : ι), ∀ x ∈ windowDomain Ω ρ a b, V.growth i x ≤ S i * edgeGrowth ρ a b x ^ q) (i : ι) : ContDiffOn ℝ (↑⊤) (extension ρ a b (f i)) Ω ∧ (∀ (n : ℕ), ∀ x ∈ Ω, iteratedFDeriv ℝ n (extension ρ a b (f i)) x = extension ρ a b (iteratedFDeriv ℝ n (f i)) x) ∧ ∀ (n : ℕ), ∀ x ∈ Ω, ρ x = a ∨ ρ x = b → iteratedFDeriv ℝ n (extension ρ a b (f i)) x = 0

Smooth zero extension of an actual native coefficient. No smoothness of the raw coefficient is assumed outside the open moving annulus.

The actual moving radial profile in native coordinates

@[reducible, inline]

abbrev NavierStokes.WaveEdgeExtension.NativePoint : Type

Native point: an abbreviation for PhaseCalculus.Slow × TorusInverse.Plane.

Equations

• NavierStokes.WaveEdgeExtension.NativePoint = (NavierStokes.PhaseCalculus.Slow × NavierStokes.TorusInverse.Plane)

noncomputable def NavierStokes.WaveEdgeExtension.nativeSlowDomain : Set NativePoint

Native slow domain, given by {x | 0 < x.1.2.2}.

Equations

• NavierStokes.WaveEdgeExtension.nativeSlowDomain = {x : NavierStokes.WaveEdgeExtension.NativePoint | 0 < x.1.2.2}

noncomputable def NavierStokes.WaveEdgeExtension.nativeRadius (h : ℝ) (x : NativePoint) : ℝ

Native radius, given by PrimaryTargetBounds.profileRadius h x.1.

Equations

• NavierStokes.WaveEdgeExtension.nativeRadius h x = NavierStokes.PrimaryTargetBounds.profileRadius h x.1

theorem NavierStokes.WaveEdgeExtension.nativeSlowDomain_open : IsOpen nativeSlowDomain

theorem NavierStokes.WaveEdgeExtension.nativeRadius_eq_qLength (h : ℝ) (x : NativePoint) : nativeRadius h x = x.1.1 / VariableGaugeMean.qLength (2 * h) (x.1.2.2, x.1.2.1)

theorem NavierStokes.WaveEdgeExtension.nativeRadius_smooth {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) : ContDiffOn ℝ (↑⊤) (nativeRadius h) nativeSlowDomain

noncomputable def NavierStokes.WaveEdgeExtension.nativeExtension {E : Type u_2} [NormedAddCommGroup E] {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (f : NativePoint → E) : NativePoint → E

Native extension, given by extension (nativeRadius F.data.h) (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W) f.

Equations

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

theorem NavierStokes.WaveEdgeExtension.native_flatWeight {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (x : NativePoint) : flatWeight (nativeRadius F.data.h) (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W) (FinalSlowBase.edgeExponent W / 4) 1 x = PrimaryTargetBounds.movingWeight W x.1

theorem NavierStokes.WaveEdgeExtension.nativeExtension_inside {E : Type u_2} [NormedAddCommGroup E] {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (f : NativePoint → E) {x : NativePoint} (hx : nativeRadius F.data.h x ∈ Set.Ioo (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W)) : nativeExtension W f x = f x

theorem NavierStokes.WaveEdgeExtension.nativeExtension_outside {E : Type u_2} [NormedAddCommGroup E] {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (f : NativePoint → E) {x : NativePoint} (hx : nativeRadius F.data.h x ∉ Set.Ioo (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W)) : nativeExtension W f x = 0

theorem NavierStokes.WaveEdgeExtension.nativeExtension_nonpositive {E : Type u_2} [NormedAddCommGroup E] {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (f : NativePoint → E) {x : NativePoint} (hR : x.1.1 ≤ 0) : nativeExtension W f x = 0

The literal extension is zero on all nonpositive physical radii.

theorem NavierStokes.WaveEdgeExtension.NativeJets.native_zero_extension {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {ι : Type u_3} {V : PrimaryCopyBounds.JetDomain ι NativePoint} {A S : ι → ℝ} {P : ι → NativePoint → ℝ} {f : ι → NativePoint → E} (hf : PrimaryCopyBounds.NativeJets V (fun (i : ι) (x : NativePoint) => A i * √(PrimaryTargetBounds.movingWeight W x.1) * P i x) f) (hA : ∀ (i : ι), 0 ≤ A i) (hS : ∀ (i : ι), 1 ≤ S i) (hP : ∀ (i : ι), ContinuousOn (P i) nativeSlowDomain) (hP0 : ∀ (i : ι), ∀ x ∈ nativeSlowDomain, 0 ≤ P i x) (hdom : ∀ (i : ι), windowDomain nativeSlowDomain (nativeRadius F.data.h) (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W) ⊆ V.carrier i) (q : ℕ) (hG : ∀ (i : ι), ∀ x ∈ windowDomain nativeSlowDomain (nativeRadius F.data.h) (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W), V.growth i x ≤ S i * edgeGrowth (nativeRadius F.data.h) (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W) x ^ q) (i : ι) : ContDiffOn ℝ (↑⊤) (nativeExtension W (f i)) nativeSlowDomain ∧ (∀ (n : ℕ), ∀ x ∈ nativeSlowDomain, iteratedFDeriv ℝ n (nativeExtension W (f i)) x = nativeExtension W (iteratedFDeriv ℝ n (f i)) x) ∧ ∀ (n : ℕ), ∀ x ∈ nativeSlowDomain, nativeRadius F.data.h x = PrimaryTargetBounds.leftRadius W ∨ nativeRadius F.data.h x = PrimaryTargetBounds.rightRadius W → iteratedFDeriv ℝ n (nativeExtension W (f i)) x = 0

Direct adapter for the exact moving weight used by the primary and signed constructions, in the native (R,Z,T,u,v) variable ordering.

Exact comparison with the inner-coordinate edge distance

theorem NavierStokes.WaveEdgeExtension.inner_edgeDistance_eq {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {r : ℝ} (hr : 0 < r) (η : ℝ) : FinalSlowBase.edgeDistance W (r ^ 2 / 2, η) = min 1 (min (2 * WeightedRadialPrimitive.logPosition (PrimaryTargetBounds.leftRadius W) r) (2 * (WeightedRadialPrimitive.logLength (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W) - WeightedRadialPrimitive.logPosition (PrimaryTargetBounds.leftRadius W) r)))

theorem NavierStokes.WaveEdgeExtension.inner_edgeGrowth_le_native {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {x : NativePoint} (hT : x ∈ nativeSlowDomain) (hx : nativeRadius F.data.h x ∈ Set.Ioo (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W)) : max 1 (FinalSlowBase.edgeDistance W (BaseChartJets.normalizedCoordinates F.data.h x.1).2)⁻¹ ≤ edgeGrowth (nativeRadius F.data.h) (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W) x

The inverse edge factor in the actual inner-coordinate estimates is bounded by the radial logarithmic factor, with constant exactly one.

structure NavierStokes.WaveEdgeExtension.NativeRegularity {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (f : NativePoint → E) : Prop

Regularity of the literal native extension, including its exact full-tensor values at both moving edges.

• smooth : ContDiffOn ℝ (↑⊤) (nativeExtension W f) nativeSlowDomain
• jets (n : ℕ) (x : NativePoint) : x ∈ nativeSlowDomain → iteratedFDeriv ℝ n (nativeExtension W f) x = nativeExtension W (iteratedFDeriv ℝ n f) x
• edge (n : ℕ) (x : NativePoint) : x ∈ nativeSlowDomain → nativeRadius F.data.h x = PrimaryTargetBounds.leftRadius W ∨ nativeRadius F.data.h x = PrimaryTargetBounds.rightRadius W → iteratedFDeriv ℝ n (nativeExtension W f) x = 0

theorem NavierStokes.WaveEdgeExtension.NativeRegularity.jet_inside {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {f : NativePoint → E} (h : NativeRegularity W f) (n : ℕ) {x : NativePoint} (hx : x ∈ nativeSlowDomain) (hi : nativeRadius F.data.h x ∈ Set.Ioo (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W)) : iteratedFDeriv ℝ n (nativeExtension W f) x = iteratedFDeriv ℝ n f x

theorem NavierStokes.WaveEdgeExtension.NativeRegularity.jet_outside {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {f : NativePoint → E} (h : NativeRegularity W f) (n : ℕ) {x : NativePoint} (hx : x ∈ nativeSlowDomain) (hi : nativeRadius F.data.h x ∉ Set.Ioo (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W)) : iteratedFDeriv ℝ n (nativeExtension W f) x = 0

theorem NavierStokes.WaveEdgeExtension.NativeJets.native_regular_of_inner_growth {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {ι : Type u_3} {V : PrimaryCopyBounds.JetDomain ι NativePoint} {A S : ι → ℝ} {P : ι → NativePoint → ℝ} {f : ι → NativePoint → E} (hf : PrimaryCopyBounds.NativeJets V (fun (i : ι) (x : NativePoint) => A i * √(PrimaryTargetBounds.movingWeight W x.1) * P i x) f) (hA : ∀ (i : ι), 0 ≤ A i) (hS : ∀ (i : ι), 1 ≤ S i) (hP : ∀ (i : ι), ContinuousOn (P i) nativeSlowDomain) (hP0 : ∀ (i : ι), ∀ x ∈ nativeSlowDomain, 0 ≤ P i x) (hdom : ∀ (i : ι), windowDomain nativeSlowDomain (nativeRadius F.data.h) (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W) ⊆ V.carrier i) (q : ℕ) (hG : ∀ (i : ι), ∀ x ∈ windowDomain nativeSlowDomain (nativeRadius F.data.h) (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W), V.growth i x ≤ S i * max 1 (FinalSlowBase.edgeDistance W (BaseChartJets.normalizedCoordinates F.data.h x.1).2)⁻¹ ^ q) (i : ι) : NativeRegularity W (f i)

The constructed primary pulse and its actual envelope

theorem NavierStokes.WaveEdgeExtension.pulseEnvelope_continuousOn {ι : Type u_3} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (χ : ι → NativePoint → PhaseCalculus.Slow × ℝ) (hχ : ∀ (i : ι), ContinuousOn (fun (x : NativePoint) => (χ i x).2) nativeSlowDomain) (j : Fin 2) (i : ι) : ContinuousOn (PrimaryCopyBounds.pulseEnvelope F χ j i) nativeSlowDomain

theorem NavierStokes.WaveEdgeExtension.pulseEnvelope_nonneg {ι : Type u_3} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (χ : ι → NativePoint → PhaseCalculus.Slow × ℝ) (j : Fin 2) (i : ι) (x : NativePoint) : 0 ≤ PrimaryCopyBounds.pulseEnvelope F χ j i x

theorem NavierStokes.WaveEdgeExtension.primaryVelocity_native_regular {F₀ : OutgoingProfile.Profile} (W : NominalProfile.Witness F₀) {ι : Type u_3} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ι → ℝ) (χ : ι → NativePoint → PhaseCalculus.Slow × ℝ) (ε : ι → ℝ) (T : ι → NativePoint → SmoothCovariance.Vec2) (mask : ι → NativePoint → ℝ) {V : PrimaryCopyBounds.JetDomain ι NativePoint} (j : Fin 2) (hf : PrimaryCopyBounds.NativeJets V (fun (i : ι) (x : NativePoint) => √(ε i) * (√(PrimaryTargetBounds.movingWeight W x.1) * PrimaryCopyBounds.pulseEnvelope F χ j i x)) (PrimaryCopyBounds.primaryVelocity F pref χ ε T mask j)) {S : ι → ℝ} (hS : ∀ (i : ι), 1 ≤ S i) (hχ : ∀ (i : ι), ContinuousOn (fun (x : NativePoint) => (χ i x).2) nativeSlowDomain) (hdom : ∀ (i : ι), windowDomain nativeSlowDomain (nativeRadius F₀.data.h) (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W) ⊆ V.carrier i) (q : ℕ) (hG : ∀ (i : ι), ∀ x ∈ windowDomain nativeSlowDomain (nativeRadius F₀.data.h) (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W), V.growth i x ≤ S i * max 1 (FinalSlowBase.edgeDistance W (BaseChartJets.normalizedCoordinates F₀.data.h x.1).2)⁻¹ ^ q) (i : ι) : NativeRegularity W (PrimaryCopyBounds.primaryVelocity F pref χ ε T mask j i)

Apply the extension construction directly to the actual Cramer-scaled homogeneous pulse. The only raw regularity premise is its already-derived native interior jet estimate.

Localization before radial extension

theorem NavierStokes.WaveEdgeExtension.NativeJets.on_zero_germ_cover {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {ι : Type u_3} {V V' : PrimaryCopyBounds.JetDomain ι X} {w : ι → X → ℝ} {f : ι → X → E} (hf : PrimaryCopyBounds.NativeJets V w f) (hcover : ∀ (i : ι), ∀ x ∈ V'.carrier i, x ∈ V.carrier i ∨ f i =ᶠ[nhds x] fun (x : X) => 0) (hw : ∀ (i : ι), ∀ x ∈ V'.carrier i, 0 ≤ w i x) (hG : ∀ (i : ι), ∀ x ∈ V'.carrier i, x ∈ V.carrier i → V.growth i x ≤ V'.growth i x) : PrimaryCopyBounds.NativeJets V' w f

Enlarge only the domain of an already localized coefficient. The same constants bound every derivative; outside the native chart its actual zero germ supplies all zero tensors.

noncomputable def NavierStokes.WaveEdgeExtension.nativeDomain {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {ι : Type u_3} (V : PrimaryCopyBounds.JetDomain ι NativePoint) (S : ι → ℝ) (q : ℕ) : PrimaryCopyBounds.JetDomain ι NativePoint

A domain for the literal localized field over the full open native annulus. Its growth allows the source chart scale and the given slow factor.

Equations

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

theorem NavierStokes.WaveEdgeExtension.NativeJets.native_regular_of_zero_germ_cover {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {ι : Type u_3} {V : PrimaryCopyBounds.JetDomain ι NativePoint} {A S : ι → ℝ} {P : ι → NativePoint → ℝ} {f : ι → NativePoint → E} (hf : PrimaryCopyBounds.NativeJets V (fun (i : ι) (x : NativePoint) => A i * √(PrimaryTargetBounds.movingWeight W x.1) * P i x) f) (hA : ∀ (i : ι), 0 ≤ A i) (hP : ∀ (i : ι), ContinuousOn (P i) nativeSlowDomain) (hP0 : ∀ (i : ι), ∀ x ∈ nativeSlowDomain, 0 ≤ P i x) (hcover : ∀ (i : ι), ∀ x ∈ windowDomain nativeSlowDomain (nativeRadius F.data.h) (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W), x ∈ V.carrier i ∨ f i =ᶠ[nhds x] fun (x : NativePoint) => 0) (q : ℕ) (hG : ∀ (i : ι), ∀ x ∈ windowDomain nativeSlowDomain (nativeRadius F.data.h) (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W), x ∈ V.carrier i → V.growth i x ≤ S i * max 1 (FinalSlowBase.edgeDistance W (BaseChartJets.normalizedCoordinates F.data.h x.1).2)⁻¹ ^ q) (i : ι) : NativeRegularity W (f i)

The source chart need only cover points where the actual localized formula has a nonzero germ. This permits slow-cell and outer-slot localization before taking the radial zero extension.

theorem NavierStokes.WaveEdgeExtension.primaryVelocity_native_regular_of_zero_germ_cover {F₀ : OutgoingProfile.Profile} (W : NominalProfile.Witness F₀) {ι : Type u_3} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ι → ℝ) (χ : ι → NativePoint → PhaseCalculus.Slow × ℝ) (ε : ι → ℝ) (T : ι → NativePoint → SmoothCovariance.Vec2) (mask : ι → NativePoint → ℝ) {V : PrimaryCopyBounds.JetDomain ι NativePoint} (j : Fin 2) (hf : PrimaryCopyBounds.NativeJets V (fun (i : ι) (x : NativePoint) => √(ε i) * (√(PrimaryTargetBounds.movingWeight W x.1) * PrimaryCopyBounds.pulseEnvelope F χ j i x)) (PrimaryCopyBounds.primaryVelocity F pref χ ε T mask j)) {S : ι → ℝ} (hχ : ∀ (i : ι), ContinuousOn (fun (x : NativePoint) => (χ i x).2) nativeSlowDomain) (hcover : ∀ (i : ι), ∀ x ∈ windowDomain nativeSlowDomain (nativeRadius F₀.data.h) (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W), x ∈ V.carrier i ∨ PrimaryCopyBounds.primaryVelocity F pref χ ε T mask j i =ᶠ[nhds x] fun (x : NativePoint) => 0) (q : ℕ) (hG : ∀ (i : ι), ∀ x ∈ windowDomain nativeSlowDomain (nativeRadius F₀.data.h) (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W), x ∈ V.carrier i → V.growth i x ≤ S i * max 1 (FinalSlowBase.edgeDistance W (BaseChartJets.normalizedCoordinates F₀.data.h x.1).2)⁻¹ ^ q) (i : ι) : NativeRegularity W (PrimaryCopyBounds.primaryVelocity F pref χ ε T mask j i)

theorem NavierStokes.WaveEdgeExtension.NativeRegularity.jet_bound {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {f : NativePoint → E} (h : NativeRegularity W f) (n : ℕ) {x : NativePoint} (hx : x ∈ nativeSlowDomain) {B : ℝ} (hB : 0 ≤ B) (hb : nativeRadius F.data.h x ∈ Set.Ioo (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W) → ‖iteratedFDeriv ℝ n f x‖ ≤ B) : ‖iteratedFDeriv ℝ n (nativeExtension W f) x‖ ≤ B

Extending by zero does not enlarge an interior tensor bound. This pointwise form keeps any constants already uniform in the external labels.

theorem NavierStokes.WaveEdgeExtension.NativeJets.nativeExtension_jets {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {ι : Type u_3} {V : PrimaryCopyBounds.JetDomain ι NativePoint} {w : ι → NativePoint → ℝ} {f : ι → NativePoint → E} (hf : PrimaryCopyBounds.NativeJets V w f) (hreg : ∀ (i : ι), NativeRegularity W (f i)) (hslow : ∀ (i : ι), V.carrier i ⊆ nativeSlowDomain) : PrimaryCopyBounds.NativeJets V w fun (i : ι) => nativeExtension W (f i)

Every pre-existing uniform native constant and polynomial degree is unchanged by the literal extension. The regularity at the new radial boundary is supplied by the construction above.

The same extension in the mean-field variable ordering

noncomputable def NavierStokes.WaveEdgeExtension.meanNative : LocalSignedRequest.Point ≃ₗᵢ[ℝ] NativePoint

The actual permutation from (R,((T,Z),Y)) to ((R,(Z,T)),Y).

Equations

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

theorem NavierStokes.WaveEdgeExtension.meanNative_apply (x : LocalSignedRequest.Point) : meanNative x = (PrimaryTargetBounds.meanPoint x, x.2.2)

theorem NavierStokes.WaveEdgeExtension.nativeRadius_meanNative {F : OutgoingProfile.Profile} (x : LocalSignedRequest.Point) : nativeRadius F.data.h (meanNative x) = (LocalSignedRequest.profileMap (2 * F.data.h) x).1

noncomputable def NavierStokes.WaveEdgeExtension.meanExtension {E : Type u_2} [NormedAddCommGroup E] {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (f : NativePoint → E) (x : LocalSignedRequest.Point) : E

Mean extension, given by nativeExtension W f (meanNative x).

Equations

• NavierStokes.WaveEdgeExtension.meanExtension W f x = NavierStokes.WaveEdgeExtension.nativeExtension W f (NavierStokes.WaveEdgeExtension.meanNative x)

theorem NavierStokes.WaveEdgeExtension.meanExtension_inside {E : Type u_2} [NormedAddCommGroup E] {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (f : NativePoint → E) {x : LocalSignedRequest.Point} (hx : (LocalSignedRequest.profileMap (2 * F.data.h) x).1 ∈ Set.Ioo (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W)) : meanExtension W f x = f (meanNative x)

theorem NavierStokes.WaveEdgeExtension.meanExtension_outside {E : Type u_2} [NormedAddCommGroup E] {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (f : NativePoint → E) {x : LocalSignedRequest.Point} (hx : (LocalSignedRequest.profileMap (2 * F.data.h) x).1 ∉ Set.Ioo (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W)) : meanExtension W f x = 0

theorem NavierStokes.WaveEdgeExtension.NativeRegularity.mean_smooth {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {f : NativePoint → E} (h : NativeRegularity W f) : ContDiffOn ℝ (↑⊤) (meanExtension W f) {x : LocalSignedRequest.Point | 0 < x.2.1.1}

theorem NavierStokes.WaveEdgeExtension.meanExtension_jet_norm {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (f : NativePoint → E) (n : ℕ) (x : LocalSignedRequest.Point) : ‖iteratedFDeriv ℝ n (meanExtension W f) x‖ = ‖iteratedFDeriv ℝ n (nativeExtension W f) (meanNative x)‖

Reordering the coordinates preserves the norm of every full tensor.

theorem NavierStokes.WaveEdgeExtension.NativeRegularity.mean_edge {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {f : NativePoint → E} (h : NativeRegularity W f) (n : ℕ) {x : LocalSignedRequest.Point} (hx : 0 < x.2.1.1) (he : (LocalSignedRequest.profileMap (2 * F.data.h) x).1 = PrimaryTargetBounds.leftRadius W ∨ (LocalSignedRequest.profileMap (2 * F.data.h) x).1 = PrimaryTargetBounds.rightRadius W) : iteratedFDeriv ℝ n (meanExtension W f) x = 0