Joint smooth extension of even radial profiles

The input is a genuinely smooth even function of the signed radius on an open parameter strip. A fixed parameter window is chosen independently of the profile. Its squared-radius descent is smooth on the closed half-plane. The proved joint Taylor--Borel extension is applied after reflecting this half-plane and adding unused spatial coordinates. Restriction gives a global smooth function of (X, eta) with exactly the original physical values. No constant continuation at negative X is differentiated.

@[reducible, inline]

abbrev NavierStokes.ParametricRadialExtension.Plane : Type

Plane: an abbreviation for ℝ × ℝ.

Equations

• NavierStokes.ParametricRadialExtension.Plane = (ℝ × ℝ)

structure NavierStokes.ParametricRadialExtension.ParameterWindow (S : Set ℝ) : Type

The same window can be used for every order and every field component.

• inner : ℝ

  Inner of ParameterWindow, of type ℝ.

• outer : ℝ

  Outer of ParameterWindow, of type ℝ.

• one_lt_inner : 1 < self.inner
• inner_lt_outer : self.inner < self.outer
• outer_subset : Set.Ioo (-self.outer) self.outer ⊆ S

theorem NavierStokes.ParametricRadialExtension.exists_parameterWindow {S : Set ℝ} (hS : IsOpen S) (hI : Set.Icc (-1) 1 ⊆ S) : Nonempty (ParameterWindow S)

noncomputable def NavierStokes.ParametricRadialExtension.parameterWindow {S : Set ℝ} (hS : IsOpen S) (hI : Set.Icc (-1) 1 ⊆ S) : ParameterWindow S

Parameter window, given by Classical.choice (exists_parameterWindow hS hI).

Equations

• NavierStokes.ParametricRadialExtension.parameterWindow hS hI = Classical.choice ⋯

theorem NavierStokes.ParametricRadialExtension.ParameterWindow.inner_pos {S : Set ℝ} (w : ParameterWindow S) : 0 < w.inner

theorem NavierStokes.ParametricRadialExtension.ParameterWindow.outer_pos {S : Set ℝ} (w : ParameterWindow S) : 0 < w.outer

noncomputable def NavierStokes.ParametricRadialExtension.ParameterWindow.bump {S : Set ℝ} (w : ParameterWindow S) : ContDiffBump 0

Bump, bundling rIn, rOut, rIn_pos, rIn_lt_rOut.

Equations

• w.bump = { rIn := w.inner, rOut := w.outer, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

noncomputable def NavierStokes.ParametricRadialExtension.ParameterWindow.parameterMap {S : Set ℝ} (w : ParameterWindow S) (eta : ℝ) : ℝ

Parameter map, given by w.bump eta * eta.

Equations

• w.parameterMap eta = ↑w.bump eta * eta

theorem NavierStokes.ParametricRadialExtension.ParameterWindow.parameterMap_contDiff {S : Set ℝ} (w : ParameterWindow S) : ContDiff ℝ (↑⊤) w.parameterMap

theorem NavierStokes.ParametricRadialExtension.ParameterWindow.bump_one {S : Set ℝ} (w : ParameterWindow S) {eta : ℝ} (heta : |eta| ≤ w.inner) : ↑w.bump eta = 1

theorem NavierStokes.ParametricRadialExtension.ParameterWindow.bump_zero {S : Set ℝ} (w : ParameterWindow S) {eta : ℝ} (heta : w.outer ≤ |eta|) : ↑w.bump eta = 0

theorem NavierStokes.ParametricRadialExtension.ParameterWindow.parameterMap_eq {S : Set ℝ} (w : ParameterWindow S) {eta : ℝ} (heta : |eta| ≤ w.inner) : w.parameterMap eta = eta

theorem NavierStokes.ParametricRadialExtension.ParameterWindow.parameterMap_mem {S : Set ℝ} (w : ParameterWindow S) (eta : ℝ) : w.parameterMap eta ∈ S

theorem NavierStokes.ParametricRadialExtension.ParameterWindow.target_subset {S : Set ℝ} (w : ParameterWindow S) : Set.Ioo (-w.inner) w.inner ⊆ S

theorem NavierStokes.ParametricRadialExtension.ParameterWindow.unit_subset {S : Set ℝ} (w : ParameterWindow S) : Set.Icc (-1) 1 ⊆ Set.Ioo (-w.inner) w.inner

noncomputable def NavierStokes.ParametricRadialExtension.regularize {E : Type u_1} {S : Set ℝ} (w : ParameterWindow S) (F : Plane → E) (p : Plane) : E

A smooth global parameter substitution, equal to the original one on the target window. Its values remain inside the input parameter domain.

Equations

• NavierStokes.ParametricRadialExtension.regularize w F p = F (p.1, w.parameterMap p.2)

theorem NavierStokes.ParametricRadialExtension.regularize_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {S : Set ℝ} (w : ParameterWindow S) {F : Plane → E} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ S)) : ContDiff ℝ (↑⊤) (regularize w F)

theorem NavierStokes.ParametricRadialExtension.regularize_even {E : Type u_1} {S : Set ℝ} (w : ParameterWindow S) {F : Plane → E} (he : ∀ eta ∈ S, ∀ (r : ℝ), F (-r, eta) = F (r, eta)) (eta r : ℝ) : regularize w F (-r, eta) = regularize w F (r, eta)

noncomputable def NavierStokes.ParametricRadialExtension.descent {E : Type u_1} (F : Plane → E) (p : Plane) : E

Descent, given by F (Real.sqrt (2 * p.1), p.2).

Equations

• NavierStokes.ParametricRadialExtension.descent F p = F (√(2 * p.1), p.2)

theorem NavierStokes.ParametricRadialExtension.descent_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {F : Plane → E} (hF : ContDiff ℝ (↑⊤) F) (he : ∀ (eta r : ℝ), F (-r, eta) = F (r, eta)) : ContDiffOn ℝ (↑⊤) (descent F) (Set.Ici 0 ×ˢ Set.univ)

The factor 2 is the physical convention X = R^2 / 2.

noncomputable def NavierStokes.ParametricRadialExtension.halfPlaneLift {E : Type u_1} (g : Plane → E) (z : ProblemStatement.SpaceTime) : E

Embed the two-variable half-plane into the already proved joint half-space extension theorem. The extra spatial coordinates are unused.

Equations

• NavierStokes.ParametricRadialExtension.halfPlaneLift g z = g (-z.1, z.2.ofLp 0)

theorem NavierStokes.ParametricRadialExtension.halfPlaneLift_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : Plane → E} (hg : ContDiffOn ℝ (↑⊤) g (Set.Ici 0 ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (halfPlaneLift g) (SpacetimeGluing.past 0)

noncomputable def NavierStokes.ParametricRadialExtension.halfPlaneExtension {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : Plane → E) (hg : ContDiffOn ℝ (↑⊤) g (Set.Ici 0 ×ˢ Set.univ)) (p : Plane) : E

Half plane extension, constructed using SpacetimeGluing.smoothExtension.

Equations

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

theorem NavierStokes.ParametricRadialExtension.halfPlaneExtension_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {g : Plane → E} (hg : ContDiffOn ℝ (↑⊤) g (Set.Ici 0 ×ˢ Set.univ)) : ContDiff ℝ (↑⊤) (halfPlaneExtension g hg)

theorem NavierStokes.ParametricRadialExtension.halfPlaneExtension_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : Plane → E} (hg : ContDiffOn ℝ (↑⊤) g (Set.Ici 0 ×ˢ Set.univ)) {p : Plane} (hp : 0 ≤ p.1) : halfPlaneExtension g hg p = g p

theorem NavierStokes.ParametricRadialExtension.halfPlaneExtension_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : Plane → E} (hg : ContDiffOn ℝ (↑⊤) g (Set.Ici 0 ×ˢ Set.univ)) {p : Plane} (hp : p.1 ≤ -1) : halfPlaneExtension g hg p = 0

noncomputable def NavierStokes.ParametricRadialExtension.extension {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {S : Set ℝ} (w : ParameterWindow S) (F : Plane → E) (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ S)) (he : ∀ eta ∈ S, ∀ (r : ℝ), F (-r, eta) = F (r, eta)) (p : Plane) : E

The global smooth extension. The outer parameter cutoff and the negative radial support bound are independent of the input profile.

Equations

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

theorem NavierStokes.ParametricRadialExtension.extension_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {S : Set ℝ} (w : ParameterWindow S) {F : Plane → E} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ S)) (he : ∀ eta ∈ S, ∀ (r : ℝ), F (-r, eta) = F (r, eta)) : ContDiff ℝ (↑⊤) (extension w F hF he)

theorem NavierStokes.ParametricRadialExtension.extension_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {S : Set ℝ} (w : ParameterWindow S) {F : Plane → E} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ S)) (he : ∀ eta ∈ S, ∀ (r : ℝ), F (-r, eta) = F (r, eta)) {p : Plane} (hX : 0 ≤ p.1) (heta : |p.2| ≤ w.inner) : extension w F hF he p = F (√(2 * p.1), p.2)

theorem NavierStokes.ParametricRadialExtension.extension_zero_negative {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {S : Set ℝ} (w : ParameterWindow S) {F : Plane → E} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ S)) (he : ∀ eta ∈ S, ∀ (r : ℝ), F (-r, eta) = F (r, eta)) {p : Plane} (hX : p.1 ≤ -1) : extension w F hF he p = 0

theorem NavierStokes.ParametricRadialExtension.extension_zero_parameter {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {S : Set ℝ} (w : ParameterWindow S) {F : Plane → E} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ S)) (he : ∀ eta ∈ S, ∀ (r : ℝ), F (-r, eta) = F (r, eta)) {p : Plane} (heta : w.outer ≤ |p.2|) : extension w F hF he p = 0

theorem NavierStokes.ParametricRadialExtension.extension_eqOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {S : Set ℝ} (w : ParameterWindow S) {F : Plane → E} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ S)) (he : ∀ eta ∈ S, ∀ (r : ℝ), F (-r, eta) = F (r, eta)) : Set.EqOn (extension w F hF he) (descent F) (Set.Ici 0 ×ˢ Set.Ioo (-w.inner) w.inner)

theorem NavierStokes.ParametricRadialExtension.extension_mixed_jets {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {S : Set ℝ} (w : ParameterWindow S) {F : Plane → E} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ S)) (he : ∀ eta ∈ S, ∀ (r : ℝ), F (-r, eta) = F (r, eta)) (n : ℕ) {p : Plane} (hp : p ∈ Set.Ici 0 ×ˢ Set.Ioo (-w.inner) w.inner) : iteratedFDeriv ℝ n (extension w F hF he) p = iteratedFDerivWithin ℝ n (descent F) (Set.Ici 0 ×ˢ Set.Ioo (-w.inner) w.inner) p

Every full mixed derivative of the extension, including at the axis, is the genuine derivative within the physical closed half-plane.

theorem NavierStokes.ParametricRadialExtension.extension_pullback {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {S : Set ℝ} (w : ParameterWindow S) {F : Plane → E} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ S)) (he : ∀ eta ∈ S, ∀ (r : ℝ), F (-r, eta) = F (r, eta)) (r : ℝ) {eta : ℝ} (heta : |eta| ≤ w.inner) : extension w F hF he (r ^ 2 / 2, eta) = F (r, eta)

Exact recovery on the signed radius. This also covers the axis.

theorem NavierStokes.ParametricRadialExtension.extension_radial_jets {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {S : Set ℝ} (w : ParameterWindow S) {F : Plane → E} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ S)) (he : ∀ eta ∈ S, ∀ (r : ℝ), F (-r, eta) = F (r, eta)) (n : ℕ) {X eta : ℝ} (hX : 0 ≤ X) (heta : |eta| ≤ w.inner) : iteratedDeriv n (fun (Y : ℝ) => extension w F hF he (Y, eta)) X = iteratedDerivWithin n (fun (Y : ℝ) => F (√(2 * Y), eta)) (Set.Ici 0) X

Exact right jets of the literal descended radial profile.

theorem NavierStokes.ParametricRadialExtension.extension_radialJet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {S : Set ℝ} (w : ParameterWindow S) {F : Plane → E} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ S)) (he : ∀ eta ∈ S, ∀ (r : ℝ), F (-r, eta) = F (r, eta)) (n : ℕ) {X eta : ℝ} (hX : 0 ≤ X) (heta : |eta| ≤ w.inner) : iteratedDeriv n (fun (Y : ℝ) => extension w F hF he (Y, eta)) X = 2 ^ n • BoundaryAxisJets.axisJet F n (2 * X, eta)

Identification with the actual Hadamard derivative chain from BoundaryAxisJets; the factor 2^n comes from X = R^2/2.

theorem NavierStokes.ParametricRadialExtension.extension_axis_jets {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {S : Set ℝ} (w : ParameterWindow S) {F : Plane → E} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ S)) (he : ∀ eta ∈ S, ∀ (r : ℝ), F (-r, eta) = F (r, eta)) (n : ℕ) {eta : ℝ} (heta : |eta| ≤ w.inner) : iteratedDeriv n (fun (Y : ℝ) => extension w F hF he (Y, eta)) 0 = (2 ^ n * (↑n.factorial / ↑(2 * n).factorial)) • iteratedDeriv (2 * n) (fun (r : ℝ) => F (r, eta)) 0

The axis constants and every higher radial jet are preserved exactly.

theorem NavierStokes.ParametricRadialExtension.extension_zero_exterior {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {S : Set ℝ} (w : ParameterWindow S) {F : Plane → E} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ S)) (he : ∀ eta ∈ S, ∀ (r : ℝ), F (-r, eta) = F (r, eta)) {B : ℝ} (hB : 0 ≤ B) (hzero : ∀ eta ∈ S, ∀ (r : ℝ), B ≤ r → F (r, eta) = 0) {p : Plane} (hX : B ^ 2 / 2 ≤ p.1) : extension w F hF he p = 0

Exterior support is inherited globally in the parameter, not only on the interval where exact agreement with the input is required.

theorem NavierStokes.ParametricRadialExtension.extension_tsupport {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {S : Set ℝ} (w : ParameterWindow S) {F : Plane → E} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ S)) (he : ∀ eta ∈ S, ∀ (r : ℝ), F (-r, eta) = F (r, eta)) {B : ℝ} (hB : 0 ≤ B) (hzero : ∀ eta ∈ S, ∀ (r : ℝ), B ≤ r → F (r, eta) = 0) : tsupport (extension w F hF he) ⊆ Set.Icc (-1) (B ^ 2 / 2) ×ˢ Set.Icc (-w.outer) w.outer

A uniform support rectangle for all profiles with the same exterior radius. The negative extension occupies at most the fixed interval [-1,0].

theorem NavierStokes.ParametricRadialExtension.extension_hasCompactSupport {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {S : Set ℝ} (w : ParameterWindow S) {F : Plane → E} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ S)) (he : ∀ eta ∈ S, ∀ (r : ℝ), F (-r, eta) = F (r, eta)) {B : ℝ} (hB : 0 ≤ B) (hzero : ∀ eta ∈ S, ∀ (r : ℝ), B ≤ r → F (r, eta) = 0) : HasCompactSupport (extension w F hF he)