The radial heat continuation profile

The profile is defined by the actual gamma-normalized improper integral in Lemma 4.4. Its derivative kernels have gamma-integrable bounds on the whole closed half-line of nonnegative profile arguments.

noncomputable def NavierStokes.RadialHeatProfile.kernel (a : ℝ) (n : ℕ) (z v : ℝ) : ℝ

The unsigned kernel for the n-th derivative.

Equations

• NavierStokes.RadialHeatProfile.kernel a n z v = Real.exp (-v) * v ^ (a + ↑n - 1) * (1 + z * v) ^ (1 - a - ↑n)

noncomputable def NavierStokes.RadialHeatProfile.moment (a : ℝ) (n : ℕ) (z : ℝ) : ℝ

Moment, given by ∫ v in Ioi (0 : ℝ), kernel a n z v.

Equations

• NavierStokes.RadialHeatProfile.moment a n z = ∫ (v : ℝ) in Set.Ioi 0, NavierStokes.RadialHeatProfile.kernel a n z v

noncomputable def NavierStokes.RadialHeatProfile.profile (a z : ℝ) : ℝ

The manuscript's normalized radial heat profile, with a = 1 + h.

Equations

• NavierStokes.RadialHeatProfile.profile a z = (Real.Gamma a)⁻¹ * NavierStokes.RadialHeatProfile.moment a 0 z

theorem NavierStokes.RadialHeatProfile.base_one_le {z v : ℝ} (hz : 0 ≤ z) (hv : 0 ≤ v) : 1 ≤ 1 + z * v

theorem NavierStokes.RadialHeatProfile.base_pos {z v : ℝ} (hz : 0 ≤ z) (hv : 0 ≤ v) : 0 < 1 + z * v

theorem NavierStokes.RadialHeatProfile.kernel_pos (a : ℝ) (n : ℕ) {z v : ℝ} (hz : 0 ≤ z) (hv : 0 < v) : 0 < kernel a n z v

theorem NavierStokes.RadialHeatProfile.kernel_le_gamma {a : ℝ} (ha : 1 < a) (n : ℕ) {z v : ℝ} (hz : 0 ≤ z) (hv : 0 < v) : kernel a n z v ≤ Real.exp (-v) * v ^ (a + ↑n - 1)

theorem NavierStokes.RadialHeatProfile.kernel_norm_le_gamma {a : ℝ} (ha : 1 < a) (n : ℕ) {z v : ℝ} (hz : 0 ≤ z) (hv : 0 < v) : ‖kernel a n z v‖ ≤ Real.exp (-v) * v ^ (a + ↑n - 1)

theorem NavierStokes.RadialHeatProfile.kernel_continuousOn_v (a : ℝ) (n : ℕ) {z : ℝ} (hz : 0 ≤ z) : ContinuousOn (kernel a n z) (Set.Ioi 0)

theorem NavierStokes.RadialHeatProfile.kernel_integrable {a : ℝ} (ha : 1 < a) (n : ℕ) {z : ℝ} (hz : 0 ≤ z) : MeasureTheory.IntegrableOn (kernel a n z) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.RadialHeatProfile.kernel_hasDerivAt_z (a : ℝ) (n : ℕ) {z v : ℝ} (hz : 0 ≤ z) (hv : 0 < v) : HasDerivAt (fun (z : ℝ) => kernel a n z v) ((1 - a - ↑n) * kernel a (n + 1) z v) z

theorem NavierStokes.RadialHeatProfile.moment_pos {a : ℝ} (ha : 1 < a) (n : ℕ) {z : ℝ} (hz : 0 ≤ z) : 0 < moment a n z

theorem NavierStokes.RadialHeatProfile.moment_le_gamma {a : ℝ} (ha : 1 < a) (n : ℕ) {z : ℝ} (hz : 0 ≤ z) : moment a n z ≤ Real.Gamma (a + ↑n)

theorem NavierStokes.RadialHeatProfile.moment_zero {a : ℝ} (ha : 1 < a) (n : ℕ) : moment a n 0 = Real.Gamma (a + ↑n)

theorem NavierStokes.RadialHeatProfile.profile_pos {a z : ℝ} (ha : 1 < a) (hz : 0 ≤ z) : 0 < profile a z

theorem NavierStokes.RadialHeatProfile.profile_zero {a : ℝ} (ha : 1 < a) : profile a 0 = 1

theorem NavierStokes.RadialHeatProfile.profile_le_one {a z : ℝ} (ha : 1 < a) (hz : 0 ≤ z) : profile a z ≤ 1

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

Continuity includes the endpoint, by a bound independent of z ≥ 0.

theorem NavierStokes.RadialHeatProfile.moment_hasDerivAt {a z : ℝ} (ha : 1 < a) (n : ℕ) (hz : 0 < z) : HasDerivAt (moment a n) ((1 - a - ↑n) * moment a (n + 1) z) z

theorem NavierStokes.RadialHeatProfile.moment_hasDerivWithinAt {a z : ℝ} (ha : 1 < a) (n : ℕ) (hz : 0 ≤ z) : HasDerivWithinAt (moment a n) ((1 - a - ↑n) * moment a (n + 1) z) (Set.Ici 0) z

The same derivative formula holds from the right at zero.

noncomputable def NavierStokes.RadialHeatProfile.derivativeCoeff (a : ℝ) : ℕ → ℝ

Falling coefficients of the genuine derivative kernels.

Equations

• NavierStokes.RadialHeatProfile.derivativeCoeff a 0 = 1
• NavierStokes.RadialHeatProfile.derivativeCoeff a n.succ = NavierStokes.RadialHeatProfile.derivativeCoeff a n * (1 - a - ↑n)

noncomputable def NavierStokes.RadialHeatProfile.profileJet (a : ℝ) (n : ℕ) (z : ℝ) : ℝ

Profile jet, given by (Real.Gamma a)⁻¹ * derivativeCoeff a n * moment a n z.

Equations

• NavierStokes.RadialHeatProfile.profileJet a n z = (Real.Gamma a)⁻¹ * NavierStokes.RadialHeatProfile.derivativeCoeff a n * NavierStokes.RadialHeatProfile.moment a n z

theorem NavierStokes.RadialHeatProfile.profileJet_hasDerivWithinAt {a z : ℝ} (ha : 1 < a) (n : ℕ) (hz : 0 ≤ z) : HasDerivWithinAt (profileJet a n) (profileJet a (n + 1) z) (Set.Ici 0) z

theorem NavierStokes.RadialHeatProfile.iteratedDerivWithin_profile {a : ℝ} (ha : 1 < a) (n : ℕ) {z : ℝ} (hz : 0 ≤ z) : iteratedDerivWithin n (profile a) (Set.Ici 0) z = profileJet a n z

theorem NavierStokes.RadialHeatProfile.profile_contDiffOn {a : ℝ} (ha : 1 < a) : ContDiffOn ℝ (↑⊤) (profile a) (Set.Ici 0)

Genuine C∞ regularity on the closed half-line, including zero.

theorem NavierStokes.RadialHeatProfile.profile_derivative_bound {a : ℝ} (ha : 1 < a) (n : ℕ) {z : ℝ} (hz : 0 ≤ z) : |iteratedDerivWithin n (profile a) (Set.Ici 0) z| ≤ |(Real.Gamma a)⁻¹ * derivativeCoeff a n| * Real.Gamma (a + ↑n)

Every fixed derivative has a finite bound uniform on the whole half-line.

theorem NavierStokes.RadialHeatProfile.iteratedDeriv_profile {a z : ℝ} (ha : 1 < a) (n : ℕ) (hz : 0 < z) : iteratedDeriv n (profile a) z = profileJet a n z

The vanishing boundary term and the actual ODE

noncomputable def NavierStokes.RadialHeatProfile.boundaryTerm (a z v : ℝ) : ℝ

Boundary term, given by Real.exp (-v) * v ^ a * (1 + z * v) ^ (-a).

Equations

• NavierStokes.RadialHeatProfile.boundaryTerm a z v = Real.exp (-v) * v ^ a * (1 + z * v) ^ (-a)

theorem NavierStokes.RadialHeatProfile.rpow_add_two {x : ℝ} (hx : 0 < x) (p : ℝ) : x ^ (p + 2) = x ^ p * x ^ 2

theorem NavierStokes.RadialHeatProfile.boundaryTerm_hasDerivAt (a : ℝ) {z v : ℝ} (hz : 0 ≤ z) (hv : 0 < v) : HasDerivAt (boundaryTerm a z) (a * z ^ 2 * kernel a 2 z v - (1 + 2 * a * z) * kernel a 1 z v + a * kernel a 0 z v) v

theorem NavierStokes.RadialHeatProfile.boundaryTerm_zero {a : ℝ} (ha : 1 < a) (z : ℝ) : boundaryTerm a z 0 = 0

theorem NavierStokes.RadialHeatProfile.boundaryTerm_continuous_zero {a : ℝ} (ha : 1 < a) (z : ℝ) : ContinuousWithinAt (boundaryTerm a z) (Set.Ici 0) 0

theorem NavierStokes.RadialHeatProfile.boundaryTerm_tendsto_zero {a z : ℝ} (ha : 1 < a) (hz : 0 ≤ z) : Filter.Tendsto (boundaryTerm a z) Filter.atTop (nhds 0)

theorem NavierStokes.RadialHeatProfile.moment_ode {a z : ℝ} (ha : 1 < a) (hz : 0 ≤ z) : a * z ^ 2 * moment a 2 z - (1 + 2 * a * z) * moment a 1 z + a * moment a 0 z = 0

The improper integration by parts identity, with both boundary terms proved zero.

theorem NavierStokes.RadialHeatProfile.profileJet_ode {a z : ℝ} (ha : 1 < a) (hz : 0 ≤ z) : z ^ 2 * profileJet a 2 z + (1 + 2 * a * z) * profileJet a 1 z + a * (a - 1) * profile a z = 0

theorem NavierStokes.RadialHeatProfile.profile_ode_within {a z : ℝ} (ha : 1 < a) (hz : 0 ≤ z) : z ^ 2 * iteratedDerivWithin 2 (profile a) (Set.Ici 0) z + (1 + 2 * a * z) * derivWithin (profile a) (Set.Ici 0) z + a * (a - 1) * profile a z = 0

The stated ODE holds at the endpoint with derivatives within the half-line.

theorem NavierStokes.RadialHeatProfile.profile_ode {a z : ℝ} (ha : 1 < a) (hz : 0 < z) : z ^ 2 * iteratedDeriv 2 (profile a) z + (1 + 2 * a * z) * deriv (profile a) z + a * (a - 1) * profile a z = 0

On the open half-line these are the ordinary first and second derivatives.

Strict slope control and a quantitative first-order estimate

theorem NavierStokes.RadialHeatProfile.kernel_slope_gap_pos (a : ℝ) {z v : ℝ} (hz : 0 ≤ z) (hv : 0 < v) : 0 < kernel a 0 z v - z * kernel a 1 z v

theorem NavierStokes.RadialHeatProfile.moment_slope_gap_pos {a z : ℝ} (ha : 1 < a) (hz : 0 ≤ z) : 0 < moment a 0 z - z * moment a 1 z

theorem NavierStokes.RadialHeatProfile.profile_hasDerivWithinAt {a z : ℝ} (ha : 1 < a) (hz : 0 ≤ z) : HasDerivWithinAt (profile a) (profileJet a 1 z) (Set.Ici 0) z

theorem NavierStokes.RadialHeatProfile.profile_derivWithin {a z : ℝ} (ha : 1 < a) (hz : 0 ≤ z) : derivWithin (profile a) (Set.Ici 0) z = (Real.Gamma a)⁻¹ * (1 - a) * moment a 1 z

theorem NavierStokes.RadialHeatProfile.profile_deriv {a z : ℝ} (ha : 1 < a) (hz : 0 < z) : deriv (profile a) z = (Real.Gamma a)⁻¹ * (1 - a) * moment a 1 z

theorem NavierStokes.RadialHeatProfile.profile_derivWithin_neg {a z : ℝ} (ha : 1 < a) (hz : 0 ≤ z) : derivWithin (profile a) (Set.Ici 0) z < 0

theorem NavierStokes.RadialHeatProfile.profile_logSlopeWithin_lt {a z : ℝ} (ha : 1 < a) (hz : 0 ≤ z) : -z * derivWithin (profile a) (Set.Ici 0) z / profile a z < a - 1

The logarithmic slope is strictly less than a - 1 = h, including the endpoint.

theorem NavierStokes.RadialHeatProfile.profile_logSlope_lt {a z : ℝ} (ha : 1 < a) (hz : 0 < z) : -z * deriv (profile a) z / profile a z < a - 1

theorem NavierStokes.RadialHeatProfile.profile_first_derivative_bound {a z : ℝ} (ha : 1 < a) (hz : 0 ≤ z) : |derivWithin (profile a) (Set.Ici 0) z| ≤ a * (a - 1)

theorem NavierStokes.RadialHeatProfile.profile_sub_one_bound {a z : ℝ} (ha : 1 < a) (hz : 0 ≤ z) : |profile a z - 1| ≤ a * (a - 1) * z

An explicit version of H(z) - 1 = O_h(z), with C_h = h(1+h).

The radial heat equation with the source exponent

noncomputable def NavierStokes.RadialHeatProfile.spatialExponent (a : ℝ) : ℝ

This is -A, since A = 1/2 + h and a = 1 + h.

Equations

• NavierStokes.RadialHeatProfile.spatialExponent a = 1 / 2 - a

noncomputable def NavierStokes.RadialHeatProfile.spatialProfile (a τ s : ℝ) : ℝ

The physical profile in the coordinate s = r²/2, at backward time τ.

Equations

• NavierStokes.RadialHeatProfile.spatialProfile a τ s = s ^ NavierStokes.RadialHeatProfile.spatialExponent a * NavierStokes.RadialHeatProfile.profile a (2 * τ / s)

noncomputable def NavierStokes.RadialHeatProfile.spatialFirst (a τ s : ℝ) : ℝ

Spatial first, given by s ^ (spatialExponent a - 1) * (spatialExponent a * profile a (2 * τ / s) - (2 * τ / s) * profileJet a 1 (2 * τ / s)).

Equations

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

noncomputable def NavierStokes.RadialHeatProfile.spatialSecond (a τ s : ℝ) : ℝ

Spatial second, constructed using s.

Equations

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

theorem NavierStokes.RadialHeatProfile.profile_hasDerivAt {a z : ℝ} (ha : 1 < a) (hz : 0 < z) : HasDerivAt (profile a) (profileJet a 1 z) z

theorem NavierStokes.RadialHeatProfile.profileJet_hasDerivAt {a z : ℝ} (ha : 1 < a) (n : ℕ) (hz : 0 < z) : HasDerivAt (profileJet a n) (profileJet a (n + 1) z) z

theorem NavierStokes.RadialHeatProfile.ratio_hasDerivAt {τ s : ℝ} (hs : 0 < s) : HasDerivAt (fun (s : ℝ) => 2 * τ / s) (-(2 * τ) / s ^ 2) s

theorem NavierStokes.RadialHeatProfile.spatialProfile_hasDerivAt_s {a τ s : ℝ} (ha : 1 < a) (hτ : 0 < τ) (hs : 0 < s) : HasDerivAt (spatialProfile a τ) (spatialFirst a τ s) s

theorem NavierStokes.RadialHeatProfile.spatialFirst_hasDerivAt_s {a τ s : ℝ} (ha : 1 < a) (hτ : 0 < τ) (hs : 0 < s) : HasDerivAt (spatialFirst a τ) (spatialSecond a τ s) s

theorem NavierStokes.RadialHeatProfile.spatialProfile_hasDerivAt_time {a τ s : ℝ} (ha : 1 < a) (hτ : 0 < τ) (hs : 0 < s) : HasDerivAt (fun (τ : ℝ) => spatialProfile a τ s) (2 * s ^ (spatialExponent a - 1) * profileJet a 1 (2 * τ / s)) τ

theorem NavierStokes.RadialHeatProfile.spatial_heat_identity {a τ s : ℝ} (ha : 1 < a) (hτ : 0 < τ) (hs : 0 < s) : -(2 * s ^ (spatialExponent a - 1) * profileJet a 1 (2 * τ / s)) = 2 * s * spatialSecond a τ s + 2 * spatialFirst a τ s - spatialProfile a τ s / (2 * s)

The angular radial Laplacian in the variable s = r²/2.

noncomputable def NavierStokes.RadialHeatProfile.radialProfile (a τ r : ℝ) : ℝ

The radial velocity profile in physical radius and backward time.

Equations

• NavierStokes.RadialHeatProfile.radialProfile a τ r = NavierStokes.RadialHeatProfile.spatialProfile a τ (r ^ 2 / 2)

noncomputable def NavierStokes.RadialHeatProfile.radialFirst (a τ r : ℝ) : ℝ

Radial first, given by spatialFirst a τ (r ^ 2 / 2) * r.

Equations

• NavierStokes.RadialHeatProfile.radialFirst a τ r = NavierStokes.RadialHeatProfile.spatialFirst a τ (r ^ 2 / 2) * r

noncomputable def NavierStokes.RadialHeatProfile.radialSecond (a τ r : ℝ) : ℝ

Radial second, given by spatialSecond a τ (r ^ 2 / 2) * r ^ 2 + spatialFirst a τ (r ^ 2 / 2).

Equations

• NavierStokes.RadialHeatProfile.radialSecond a τ r = NavierStokes.RadialHeatProfile.spatialSecond a τ (r ^ 2 / 2) * r ^ 2 + NavierStokes.RadialHeatProfile.spatialFirst a τ (r ^ 2 / 2)

theorem NavierStokes.RadialHeatProfile.radiusSquared_hasDerivAt (r : ℝ) : HasDerivAt (fun (r : ℝ) => r ^ 2 / 2) r r

theorem NavierStokes.RadialHeatProfile.radialProfile_hasDerivAt_radius {a τ r : ℝ} (ha : 1 < a) (hτ : 0 < τ) (hr : 0 < r) : HasDerivAt (radialProfile a τ) (radialFirst a τ r) r

theorem NavierStokes.RadialHeatProfile.radialFirst_hasDerivAt_radius {a τ r : ℝ} (ha : 1 < a) (hτ : 0 < τ) (hr : 0 < r) : HasDerivAt (radialFirst a τ) (radialSecond a τ r) r

theorem NavierStokes.RadialHeatProfile.radialProfile_first_derivative {a τ r : ℝ} (ha : 1 < a) (hτ : 0 < τ) (hr : 0 < r) : deriv (radialProfile a τ) r = radialFirst a τ r

theorem NavierStokes.RadialHeatProfile.radialProfile_second_derivative {a τ r : ℝ} (ha : 1 < a) (hτ : 0 < τ) (hr : 0 < r) : iteratedDeriv 2 (radialProfile a τ) r = radialSecond a τ r

theorem NavierStokes.RadialHeatProfile.radialProfile_hasDerivAt_time {a τ r : ℝ} (ha : 1 < a) (hτ : 0 < τ) (hr : 0 < r) : HasDerivAt (fun (τ : ℝ) => radialProfile a τ r) (2 * (r ^ 2 / 2) ^ (spatialExponent a - 1) * profileJet a 1 (2 * τ / (r ^ 2 / 2))) τ

theorem NavierStokes.RadialHeatProfile.radial_heat_equation {a τ r : ℝ} (ha : 1 < a) (hτ : 0 < τ) (hr : 0 < r) : -deriv (fun (τ : ℝ) => radialProfile a τ r) τ = iteratedDeriv 2 (radialProfile a τ) r + deriv (radialProfile a τ) r / r - radialProfile a τ r / r ^ 2

The actual angular radial heat equation in radius and backward time. The second radial derivative and both first derivatives are genuine derivs.

theorem NavierStokes.RadialHeatProfile.forward_radial_heat_equation {a t r : ℝ} (ha : 1 < a) (ht : t < 1) (hr : 0 < r) : deriv (fun (t : ℝ) => radialProfile a (1 - t) r) t = iteratedDeriv 2 (radialProfile a (1 - t)) r + deriv (radialProfile a (1 - t)) r / r - radialProfile a (1 - t) r / r ^ 2

With τ = 1 - t, the sign is the forward heat sign in the manuscript.

theorem NavierStokes.RadialHeatProfile.spatialFirst_neg {a τ s : ℝ} (ha : 1 < a) (hτ : 0 < τ) (hs : 0 < s) : spatialFirst a τ s < 0

theorem NavierStokes.RadialHeatProfile.radialProfile_derivative_neg {a τ r : ℝ} (ha : 1 < a) (hτ : 0 < τ) (hr : 0 < r) : deriv (radialProfile a τ) r < 0

theorem NavierStokes.RadialHeatProfile.spatialProfile_joint_contDiffOn {a : ℝ} (ha : 1 < a) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℝ) => spatialProfile a p.2 p.1) {p : ℝ × ℝ | 0 < p.1 ∧ 0 ≤ p.2}

Joint smoothness in the physical coordinate and backward time, also at τ = 0.

theorem NavierStokes.RadialHeatProfile.radialProfile_joint_contDiffOn {a : ℝ} (ha : 1 < a) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℝ) => radialProfile a p.2 p.1) {p : ℝ × ℝ | 0 < p.1 ∧ 0 ≤ p.2}

theorem NavierStokes.RadialHeatProfile.profile_eq_integral (a z : ℝ) : profile a z = (Real.Gamma a)⁻¹ * ∫ (v : ℝ) in Set.Ioi 0, Real.exp (-v) * v ^ (a - 1) * (1 + z * v) ^ (1 - a)

This is exactly the displayed integral in Lemma 4.4.

theorem NavierStokes.RadialHeatProfile.radialProfile_source_formula (h τ r : ℝ) : radialProfile (1 + h) τ r = (r ^ 2 / 2) ^ (-(1 / 2 + h)) * profile (1 + h) (2 * τ / (r ^ 2 / 2))

The physical power is exactly s^(-A), where A = 1/2 + h.

theorem NavierStokes.RadialHeatProfile.profile_h_sub_one_bound {h z : ℝ} (hh : 0 < h) (hz : 0 ≤ z) : |profile (1 + h) z - 1| ≤ h * (1 + h) * z

theorem NavierStokes.RadialHeatProfile.profile_h_logSlope_lt {h z : ℝ} (hh : 0 < h) (hz : 0 < z) : -z * deriv (profile (1 + h)) z / profile (1 + h) z < h

theorem NavierStokes.RadialHeatProfile.scaled_forward_radial_heat_equation (C : ℝ) {a t r : ℝ} (ha : 1 < a) (ht : t < 1) (hr : 0 < r) : deriv (fun (t : ℝ) => C * radialProfile a (1 - t) r) t = iteratedDeriv 2 (fun (r : ℝ) => C * radialProfile a (1 - t) r) r + deriv (fun (r : ℝ) => C * radialProfile a (1 - t) r) r / r - C * radialProfile a (1 - t) r / r ^ 2

Any fixed normalization constant preserves the actual forward heat equation.

theorem NavierStokes.RadialHeatProfile.scaled_radialProfile_derivative_neg {C a τ r : ℝ} (hC : 0 < C) (ha : 1 < a) (hτ : 0 < τ) (hr : 0 < r) : deriv (fun (r : ℝ) => C * radialProfile a τ r) r < 0