A genuine smooth extension of the radial heat profile

For each fixed a > 1, the actual gamma-integral derivative kernels prescribe all right jets at zero. A constructed Taylor--Borel series realizes precisely these jets on the negative side. Gluing the two branches preserves the actual heat profile on the entire nonnegative half-line and gives a globally smooth function. No kernel formula at a negative argument is used.

Smooth gluing from matching one-sided derivative jets

If a real-parameter curve is smooth on each closed half-line and all of its one-sided derivatives agree at the common endpoint, its piecewise glue is smooth. The derivatives are actual iteratedDerivWithin values. No smooth extension across the endpoint is assumed for either branch.

This is the gluing step needed after the left endpoint regularity and the right Taylor--Borel construction in Lemmas 11.5--11.6. It does not construct a right branch with arbitrary prescribed jets.

noncomputable def NavierStokes.EndpointExtension.glue {V : Type u_1} (a : ℝ) (left right : ℝ → V) (x : ℝ) : V

Take the left branch through the joining point, and the right branch after it.

Equations

• NavierStokes.EndpointExtension.glue a left right x = if x ≤ a then left x else right x

theorem NavierStokes.EndpointExtension.glue_eq_left {V : Type u_1} {a x : ℝ} {left right : ℝ → V} (hx : x ≤ a) : glue a left right x = left x

theorem NavierStokes.EndpointExtension.glue_eq_right {V : Type u_1} {a x : ℝ} {left right : ℝ → V} (hx : a < x) : glue a left right x = right x

theorem NavierStokes.EndpointExtension.glue_eqOn_right {V : Type u_1} {a : ℝ} {left right : ℝ → V} (hvalue : left a = right a) : Set.EqOn (glue a left right) right (Set.Ici a)

Matching endpoint values let the glued function agree with the right branch on its entire closed half-line, including the joining point.

theorem NavierStokes.EndpointExtension.glue_vanishes_from {V : Type u_1} [Zero V] {a b : ℝ} {left right : ℝ → V} (hab : a ≤ b) (hvalue : left a = right a) (hzero : ∀ (x : ℝ), b ≤ x → right x = 0) (x : ℝ) : b ≤ x → glue a left right x = 0

Gluing preserves a right-hand time-support bound.

theorem NavierStokes.EndpointExtension.hasDerivAt_glue {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℝ} {left right leftDeriv rightDeriv : ℝ → V} (hleft : ∀ x ≤ a, HasDerivWithinAt left (leftDeriv x) (Set.Iic a) x) (hright : ∀ (x : ℝ), a ≤ x → HasDerivWithinAt right (rightDeriv x) (Set.Ici a) x) (hvalue : left a = right a) (hderiv : leftDeriv a = rightDeriv a) (x : ℝ) : HasDerivAt (glue a left right) (glue a leftDeriv rightDeriv x) x

First-order gluing: compatible one-sided derivatives combine into an ordinary derivative at the join, as well as away from it.

noncomputable def NavierStokes.EndpointExtension.gluedJet {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℝ) (left right : ℝ → V) (n : ℕ) : ℝ → V

Glue the genuine n-th derivatives on the two closed half-lines.

Equations

• NavierStokes.EndpointExtension.gluedJet a left right n = NavierStokes.EndpointExtension.glue a (iteratedDerivWithin n left (Set.Iic a)) (iteratedDerivWithin n right (Set.Ici a))

theorem NavierStokes.EndpointExtension.hasDerivAt_gluedJet {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℝ} {left right : ℝ → V} (hleft : ContDiffOn ℝ (↑⊤) left (Set.Iic a)) (hright : ContDiffOn ℝ (↑⊤) right (Set.Ici a)) (hmatch : ∀ (n : ℕ), iteratedDerivWithin n left (Set.Iic a) a = iteratedDerivWithin n right (Set.Ici a) a) (n : ℕ) (x : ℝ) : HasDerivAt (gluedJet a left right n) (gluedJet a left right (n + 1) x) x

Smoothness on each side supplies the next derivative; matching endpoint jets makes every glued jet ordinarily differentiable across the endpoint.

theorem NavierStokes.EndpointExtension.iteratedDeriv_glue {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℝ} {left right : ℝ → V} (hleft : ContDiffOn ℝ (↑⊤) left (Set.Iic a)) (hright : ContDiffOn ℝ (↑⊤) right (Set.Ici a)) (hmatch : ∀ (n : ℕ), iteratedDerivWithin n left (Set.Iic a) a = iteratedDerivWithin n right (Set.Ici a) a) (n : ℕ) : iteratedDeriv n (glue a left right) = gluedJet a left right n

Every ordinary derivative of the glued function is exactly the appropriate piecewise one-sided derivative, including at the joining point.

theorem NavierStokes.EndpointExtension.contDiff_glue {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℝ} {left right : ℝ → V} (hleft : ContDiffOn ℝ (↑⊤) left (Set.Iic a)) (hright : ContDiffOn ℝ (↑⊤) right (Set.Ici a)) (hmatch : ∀ (n : ℕ), iteratedDerivWithin n left (Set.Iic a) a = iteratedDerivWithin n right (Set.Ici a) a) : ContDiff ℝ (↑⊤) (glue a left right)

Main smooth gluing theorem. The inputs require smoothness only on each closed half-line and matching actual one-sided jets.

theorem NavierStokes.EndpointExtension.iteratedDeriv_glue_at_join {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℝ} {left right : ℝ → V} (hleft : ContDiffOn ℝ (↑⊤) left (Set.Iic a)) (hright : ContDiffOn ℝ (↑⊤) right (Set.Ici a)) (hmatch : ∀ (n : ℕ), iteratedDerivWithin n left (Set.Iic a) a = iteratedDerivWithin n right (Set.Ici a) a) (n : ℕ) : iteratedDeriv n (glue a left right) a = iteratedDerivWithin n left (Set.Iic a) a

The smooth glue preserves every prescribed endpoint jet.

theorem NavierStokes.EndpointExtension.iteratedDerivWithin_zero_curve {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (s : Set ℝ) (n : ℕ) : iteratedDerivWithin n (fun (x : ℝ) => 0) s = fun (x : ℝ) => 0

Every within-derivative of the zero curve is zero.

theorem NavierStokes.EndpointExtension.contDiff_zero_extension {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℝ} {left : ℝ → V} (hleft : ContDiffOn ℝ (↑⊤) left (Set.Iic a)) (hflat : ∀ (n : ℕ), iteratedDerivWithin n left (Set.Iic a) a = 0) : ContDiff ℝ (↑⊤) (glue a left fun (x : ℝ) => 0)

An actually constructed extension in the flat case: if all left jets vanish, extension by zero to the right is smooth.

noncomputable def NavierStokes.HeatProfileExtension.endpointJet (a : ℝ) (n : ℕ) : ℝ

The actual right endpoint jets, as derived from the integral kernels.

Equations

• NavierStokes.HeatProfileExtension.endpointJet a n = NavierStokes.RadialHeatProfile.profileJet a n 0

theorem NavierStokes.HeatProfileExtension.endpointJet_eq_gamma {a : ℝ} (ha : 1 < a) (n : ℕ) : endpointJet a n = (Real.Gamma a)⁻¹ * RadialHeatProfile.derivativeCoeff a n * Real.Gamma (a + ↑n)

theorem NavierStokes.HeatProfileExtension.endpointJet_eq_right_derivative {a : ℝ} (ha : 1 < a) (n : ℕ) : endpointJet a n = iteratedDerivWithin n (RadialHeatProfile.profile a) (Set.Ici 0) 0

theorem NavierStokes.HeatProfileExtension.profileJet_continuousOn {a : ℝ} (ha : 1 < a) (n : ℕ) : ContinuousOn (RadialHeatProfile.profileJet a n) (Set.Ici 0)

noncomputable def NavierStokes.HeatProfileExtension.leftBranch (a : ℝ) : ℝ → ℝ

The negative branch is the actual compactly supported Borel series.

Equations

• NavierStokes.HeatProfileExtension.leftBranch a = NavierStokes.BorelExtension.extension (NavierStokes.HeatProfileExtension.endpointJet a)

theorem NavierStokes.HeatProfileExtension.leftBranch_contDiff (a : ℝ) : ContDiff ℝ (↑⊤) (leftBranch a)

theorem NavierStokes.HeatProfileExtension.leftBranch_jets (a : ℝ) (n : ℕ) : iteratedDeriv n (leftBranch a) 0 = endpointJet a n

theorem NavierStokes.HeatProfileExtension.leftBranch_left_jets (a : ℝ) (n : ℕ) : iteratedDerivWithin n (leftBranch a) (Set.Iic 0) 0 = endpointJet a n

theorem NavierStokes.HeatProfileExtension.leftBranch_zero (a : ℝ) : leftBranch a 0 = RadialHeatProfile.profile a 0

theorem NavierStokes.HeatProfileExtension.matching_jets {a : ℝ} (ha : 1 < a) (n : ℕ) : iteratedDerivWithin n (leftBranch a) (Set.Iic 0) 0 = iteratedDerivWithin n (RadialHeatProfile.profile a) (Set.Ici 0) 0

noncomputable def NavierStokes.HeatProfileExtension.extension (a : ℝ) : ℝ → ℝ

The globally defined extension. The original profile is used at every positive argument, and matching zeroth jets preserve it at zero as well.

Equations

• NavierStokes.HeatProfileExtension.extension a = NavierStokes.EndpointExtension.glue 0 (NavierStokes.HeatProfileExtension.leftBranch a) (NavierStokes.RadialHeatProfile.profile a)

theorem NavierStokes.HeatProfileExtension.extension_contDiff {a : ℝ} (ha : 1 < a) : ContDiff ℝ (↑⊤) (extension a)

theorem NavierStokes.HeatProfileExtension.extension_eq_profile (a : ℝ) {z : ℝ} (hz : 0 ≤ z) : extension a z = RadialHeatProfile.profile a z

theorem NavierStokes.HeatProfileExtension.extension_eq_leftBranch (a : ℝ) {z : ℝ} (hz : z ≤ 0) : extension a z = leftBranch a z

theorem NavierStokes.HeatProfileExtension.extension_zero {a : ℝ} (ha : 1 < a) : extension a 0 = 1

theorem NavierStokes.HeatProfileExtension.iteratedDeriv_extension_eq_profileJet {a : ℝ} (ha : 1 < a) (n : ℕ) {z : ℝ} (hz : 0 ≤ z) : iteratedDeriv n (extension a) z = RadialHeatProfile.profileJet a n z

Ordinary derivatives of the smooth extension preserve every actual one-sided profile derivative throughout the closed nonnegative half-line.

theorem NavierStokes.HeatProfileExtension.iteratedDeriv_extension_zero {a : ℝ} (ha : 1 < a) (n : ℕ) : iteratedDeriv n (extension a) 0 = endpointJet a n

theorem NavierStokes.HeatProfileExtension.extension_preserves_right_jets {a : ℝ} (ha : 1 < a) (n : ℕ) : iteratedDeriv n (extension a) 0 = iteratedDerivWithin n (RadialHeatProfile.profile a) (Set.Ici 0) 0

theorem NavierStokes.HeatProfileExtension.extension_pos {a z : ℝ} (ha : 1 < a) (hz : 0 ≤ z) : 0 < extension a z

theorem NavierStokes.HeatProfileExtension.extension_zero_of_le_neg_one (a : ℝ) {z : ℝ} (hz : z ≤ -1) : extension a z = 0

Global fixed-order derivative bounds

noncomputable def NavierStokes.HeatProfileExtension.leftBound (a : ℝ) (n : ℕ) : ℝ

The convergent majorant from the actual Borel construction.

Equations

• NavierStokes.HeatProfileExtension.leftBound a n = ∑' (j : ℕ), NavierStokes.BorelExtension.majorant (NavierStokes.HeatProfileExtension.endpointJet a) n j

theorem NavierStokes.HeatProfileExtension.leftBranch_derivative_bound (a : ℝ) (n : ℕ) (z : ℝ) : ‖iteratedDeriv n (leftBranch a) z‖ ≤ leftBound a n

theorem NavierStokes.HeatProfileExtension.leftBound_nonneg (a : ℝ) (n : ℕ) : 0 ≤ leftBound a n

noncomputable def NavierStokes.HeatProfileExtension.derivativeBound (a : ℝ) (n : ℕ) : ℝ

A finite bound at every fixed order, uniform over the entire real line.

Equations

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

theorem NavierStokes.HeatProfileExtension.derivativeBound_nonneg (a : ℝ) (n : ℕ) : 0 ≤ derivativeBound a n

theorem NavierStokes.HeatProfileExtension.extension_derivative_bound {a : ℝ} (ha : 1 < a) (n : ℕ) (z : ℝ) : ‖iteratedDeriv n (extension a) z‖ ≤ derivativeBound a n

theorem NavierStokes.HeatProfileExtension.extension_sub_one_bound {a : ℝ} (ha : 1 < a) (z : ℝ) : |extension a z - 1| ≤ derivativeBound a 1 * |z|

The first-order error has a global linear bound, including negative arguments. It is useful for domination of the extended tail integrals.

theorem NavierStokes.HeatProfileExtension.extension_positive_near_zero {a : ℝ} (ha : 1 < a) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (z : ℝ), |z| < δ → 1 / 2 < extension a z ∧ extension a z < 3 / 2

Positivity persists on a genuine two-sided neighborhood of the origin.

theorem NavierStokes.HeatProfileExtension.extension_positive_on_collar {a : ℝ} (ha : 1 < a) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (z : ℝ), -δ < z → 0 < extension a z

Physical parameter composition

noncomputable def NavierStokes.HeatProfileExtension.scaledProfile (a X ν : ℝ) : ℝ

Diffusion-parametrized profile; negative diffusion uses only the Borel extension, never the original gamma-integral expression.

Equations

• NavierStokes.HeatProfileExtension.scaledProfile a X ν = NavierStokes.HeatProfileExtension.extension a (2 * ν / X)

theorem NavierStokes.HeatProfileExtension.scaledProfile_contDiffOn {a : ℝ} (ha : 1 < a) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℝ) => scaledProfile a p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)

theorem NavierStokes.HeatProfileExtension.scaledProfile_eq_profile (a : ℝ) {X ν : ℝ} (hX : 0 < X) (hν : 0 ≤ ν) : scaledProfile a X ν = RadialHeatProfile.profile a (2 * ν / X)

theorem NavierStokes.HeatProfileExtension.iteratedDeriv_scaledProfile {a : ℝ} (ha : 1 < a) (n : ℕ) (X ν : ℝ) : iteratedDeriv n (scaledProfile a X) ν = (2 / X) ^ n * iteratedDeriv n (extension a) (2 * ν / X)

Every ordinary diffusion derivative is an actual derivative of the constructed smooth extension, including at and below zero diffusion.

theorem NavierStokes.HeatProfileExtension.scaledProfile_derivative_bound {a X : ℝ} (ha : 1 < a) (hX : 0 < X) (n : ℕ) (ν : ℝ) : |iteratedDeriv n (scaledProfile a X) ν| ≤ (2 / X) ^ n * derivativeBound a n

theorem NavierStokes.HeatProfileExtension.scaledProfile_sub_one_bound {a : ℝ} (ha : 1 < a) {X : ℝ} (hX : 0 < X) (ν : ℝ) : |scaledProfile a X ν - 1| ≤ 2 * derivativeBound a 1 * |ν| / X

On a bounded diffusion set this supplies a uniform inverse-radius majorant on either side of zero diffusion.

noncomputable def NavierStokes.HeatProfileExtension.physicalProfile (a X η : ℝ) : ℝ

Physical profile, given by scaledProfile a X (1 - η ^ 2).

Equations

• NavierStokes.HeatProfileExtension.physicalProfile a X η = NavierStokes.HeatProfileExtension.scaledProfile a X (1 - η ^ 2)

theorem NavierStokes.HeatProfileExtension.physicalProfile_contDiffOn {a : ℝ} (ha : 1 < a) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℝ) => physicalProfile a p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)

The physical profile now has an ordinary smooth neighborhood beyond both endpoints eta = ±1, for every positive radius coordinate.

theorem NavierStokes.HeatProfileExtension.physicalProfile_eq_profile (a : ℝ) {X η : ℝ} (hX : 0 < X) (hη : η ∈ Set.Icc (-1) 1) : physicalProfile a X η = RadialHeatProfile.profile a (2 * (1 - η ^ 2) / X)