The renormalized angular moment and physical axial viscosity

The nonintegrable reference power is independent of physical axial position. It is subtracted before integration. Local constancy of the exterior heat carrier supplies compact support for every axial derivative of the difference.

Smooth integrals of locally uniformly supported differences

noncomputable def NavierStokes.RenormalizedHeatMoment.parameterJet (F : ℝ × ℝ → ℝ) (n : ℕ) (p : ℝ × ℝ) : ℝ

Parameter jet, given by iteratedDeriv n (fun z => F (z, p.2)) p.1.

Equations

• NavierStokes.RenormalizedHeatMoment.parameterJet F n p = iteratedDeriv n (fun (z : ℝ) => F (z, p.2)) p.1

theorem NavierStokes.RenormalizedHeatMoment.parameterJet_continuous {F : ℝ × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (n : ℕ) : Continuous (parameterJet F n)

theorem NavierStokes.RenormalizedHeatMoment.iteratedDeriv_zero_function (n : ℕ) : (iteratedDeriv n fun (x : ℝ) => 0) = fun (x : ℝ) => 0

def NavierStokes.RenormalizedHeatMoment.LocallyUniformSupport (F : ℝ × ℝ → ℝ) : Prop

Only the positive integration half-line needs a common support radius.

Equations

• NavierStokes.RenormalizedHeatMoment.LocallyUniformSupport F = ∀ (z : ℝ), ∃ (ε : ℝ) (B : ℝ), 0 < ε ∧ 0 < B ∧ ∀ y ∈ Metric.ball z ε, ∀ (r : ℝ), B ≤ r → F (y, r) = 0

theorem NavierStokes.RenormalizedHeatMoment.parameterJet_zero_of_support {F : ℝ × ℝ → ℝ} {z ε B y r : ℝ} (hs : ∀ x ∈ Metric.ball z ε, ∀ (r : ℝ), B ≤ r → F (x, r) = 0) (hy : y ∈ Metric.ball z ε) (hr : B ≤ r) (n : ℕ) : parameterJet F n (y, r) = 0

theorem NavierStokes.RenormalizedHeatMoment.supported_locally_dominated {F : ℝ × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : LocallyUniformSupport F) : SmoothParameterIntegral.LocallyDominatedDeriv (fun (z r : ℝ) => F (z, r)) (MeasureTheory.volume.restrict (Set.Ioi 0))

theorem NavierStokes.RenormalizedHeatMoment.parameterJet_measurable {F : ℝ × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (n : ℕ) (z : ℝ) : MeasureTheory.AEStronglyMeasurable (fun (r : ℝ) => parameterJet F n (z, r)) (MeasureTheory.volume.restrict (Set.Ioi 0))

theorem NavierStokes.RenormalizedHeatMoment.parameterJet_integrable {F : ℝ × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : LocallyUniformSupport F) (n : ℕ) (z : ℝ) : MeasureTheory.IntegrableOn (fun (r : ℝ) => parameterJet F n (z, r)) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.RenormalizedHeatMoment.iteratedDeriv_integral_supported {F : ℝ × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : LocallyUniformSupport F) (n : ℕ) (z : ℝ) : iteratedDeriv n (fun (y : ℝ) => ∫ (r : ℝ) in Set.Ioi 0, F (y, r)) z = ∫ (r : ℝ) in Set.Ioi 0, parameterJet F n (z, r)

noncomputable def NavierStokes.RenormalizedHeatMoment.centered (u : ℝ × ℝ → ℝ) (z0 : ℝ) (p : ℝ × ℝ) : ℝ

Centered, given by p.2 ^ 2 * (u p - u (z0, p.2)).

Equations

• NavierStokes.RenormalizedHeatMoment.centered u z0 p = p.2 ^ 2 * (u p - u (z0, p.2))

noncomputable def NavierStokes.RenormalizedHeatMoment.renormalizedMoment (u : ℝ × ℝ → ℝ) (reference : ℝ → ℝ) (z : ℝ) : ℝ

Renormalized moment, given by ∫ r in Ioi (0 : ℝ), r ^ 2 * (u (z, r) - reference r).

Equations

• NavierStokes.RenormalizedHeatMoment.renormalizedMoment u reference z = ∫ (r : ℝ) in Set.Ioi 0, r ^ 2 * (u (z, r) - reference r)

theorem NavierStokes.RenormalizedHeatMoment.centered_contDiff {u : ℝ × ℝ → ℝ} (hu : ContDiff ℝ (↑⊤) u) (z0 : ℝ) : ContDiff ℝ (↑⊤) (centered u z0)

def NavierStokes.RenormalizedHeatMoment.CommonExterior (u : ℝ × ℝ → ℝ) (tail : ℝ → ℝ) : Prop

A locally common exterior carrier is independent of the axial parameter.

Equations

• NavierStokes.RenormalizedHeatMoment.CommonExterior u tail = ∀ (z : ℝ), ∃ (ε : ℝ) (B : ℝ), 0 < ε ∧ 0 < B ∧ ∀ y ∈ Metric.ball z ε, ∀ (r : ℝ), B ≤ r → u (y, r) = tail r

theorem NavierStokes.RenormalizedHeatMoment.centered_support {u : ℝ × ℝ → ℝ} {tail : ℝ → ℝ} (he : CommonExterior u tail) (z0 : ℝ) : LocallyUniformSupport (centered u z0)

theorem NavierStokes.RenormalizedHeatMoment.centered_jet {u : ℝ × ℝ → ℝ} (hu : ContDiff ℝ (↑⊤) u) (z0 : ℝ) (n : ℕ) (hn : 0 < n) (z r : ℝ) : parameterJet (centered u z0) n (z, r) = r ^ 2 * iteratedDeriv n (fun (y : ℝ) => u (y, r)) z

theorem NavierStokes.RenormalizedHeatMoment.renormalized_moment_derivative {u : ℝ × ℝ → ℝ} {reference tail : ℝ → ℝ} (hu : ContDiff ℝ (↑⊤) u) (he : CommonExterior u tail) (hi : ∀ (z : ℝ), MeasureTheory.IntegrableOn (fun (r : ℝ) => r ^ 2 * (u (z, r) - reference r)) (Set.Ioi 0) MeasureTheory.volume) (n : ℕ) (hn : 0 < n) (z : ℝ) : MeasureTheory.IntegrableOn (fun (r : ℝ) => r ^ 2 * iteratedDeriv n (fun (y : ℝ) => u (y, r)) z) (Set.Ioi 0) MeasureTheory.volume ∧ iteratedDeriv n (renormalizedMoment u reference) z = ∫ (r : ℝ) in Set.Ioi 0, r ^ 2 * iteratedDeriv n (fun (y : ℝ) => u (y, r)) z

Differentiation of the actual renormalized improper moment. The tail is subtracted before integration, and all positive-order integrands are proved integrable by local compact support.

theorem NavierStokes.RenormalizedHeatMoment.axial_viscosity_moment_zero {u : ℝ × ℝ → ℝ} {reference tail : ℝ → ℝ} (hu : ContDiff ℝ (↑⊤) u) (he : CommonExterior u tail) (hi : ∀ (z : ℝ), MeasureTheory.IntegrableOn (fun (r : ℝ) => r ^ 2 * (u (z, r) - reference r)) (Set.Ioi 0) MeasureTheory.volume) (hm : ∀ (z : ℝ), renormalizedMoment u reference z = 0) (z : ℝ) : MeasureTheory.IntegrableOn (fun (r : ℝ) => r ^ 2 * iteratedDeriv 2 (fun (y : ℝ) => u (y, r)) z) (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (r : ℝ) in Set.Ioi 0, r ^ 2 * iteratedDeriv 2 (fun (y : ℝ) => u (y, r)) z = 0

The actual implicit physical coordinates

noncomputable def NavierStokes.RenormalizedHeatMoment.A (h : ℝ) : ℝ

A, given by 1 / 2 + h.

Equations

• NavierStokes.RenormalizedHeatMoment.A h = 1 / 2 + h

noncomputable def NavierStokes.RenormalizedHeatMoment.Q (h τ z : ℝ) : ℝ

Q, given by SimilarityCoordinates.coordinateQ (2 * h) (τ, z).

Equations

• NavierStokes.RenormalizedHeatMoment.Q h τ z = NavierStokes.SimilarityCoordinates.coordinateQ (2 * h) (τ, z)

noncomputable def NavierStokes.RenormalizedHeatMoment.eta (h τ z : ℝ) : ℝ

Eta, given by SimilarityCoordinates.coordinateEta (2 * h) (τ, z).

Equations

• NavierStokes.RenormalizedHeatMoment.eta h τ z = NavierStokes.SimilarityCoordinates.coordinateEta (2 * h) (τ, z)

noncomputable def NavierStokes.RenormalizedHeatMoment.referencePower (h C r : ℝ) : ℝ

Reference power, given by C * (r ^ 2 / 2) ^ (-A h).

Equations

• NavierStokes.RenormalizedHeatMoment.referencePower h C r = C * (r ^ 2 / 2) ^ (-NavierStokes.RenormalizedHeatMoment.A h)

noncomputable def NavierStokes.RenormalizedHeatMoment.heatCarrier (h C τ r : ℝ) : ℝ

Heat carrier, given by C * RadialHeatProfile.radialProfile (1 + h) τ r.

Equations

• NavierStokes.RenormalizedHeatMoment.heatCarrier h C τ r = C * NavierStokes.RadialHeatProfile.radialProfile (1 + h) τ r

noncomputable def NavierStokes.RenormalizedHeatMoment.velocity (h τ : ℝ) (F : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

F is the signed radial angular profile, with parameter second.

Equations

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

theorem NavierStokes.RenormalizedHeatMoment.Q_pos {h τ : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hτ : 0 < τ) (z : ℝ) : 0 < Q h τ z

theorem NavierStokes.RenormalizedHeatMoment.Q_implicit {h τ : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hτ : 0 < τ) (z : ℝ) : Q h τ z - z ^ 2 * Q h τ z ^ (2 * h) = τ

theorem NavierStokes.RenormalizedHeatMoment.eta_mem {h τ : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hτ : 0 < τ) (z : ℝ) : eta h τ z ∈ Set.Ioo (-1) 1

theorem NavierStokes.RenormalizedHeatMoment.diffusion_identity {h τ : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hτ : 0 < τ) (z : ℝ) : 1 - eta h τ z ^ 2 = τ / Q h τ z

theorem NavierStokes.RenormalizedHeatMoment.normalized_coordinates {h e : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (he : e ∈ Set.Ioo (-1) 1) : e ^ 2 < 1 ∧ Q h (1 - e ^ 2) e = 1 ∧ eta h (1 - e ^ 2) e = e

Every interior profile parameter is realized at a physical point with q=1, namely t=eta^2 and z=eta.

theorem NavierStokes.RenormalizedHeatMoment.Q_contDiff {h τ : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hτ : 0 < τ) : ContDiff ℝ (↑⊤) (Q h τ)

theorem NavierStokes.RenormalizedHeatMoment.eta_contDiff {h τ : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hτ : 0 < τ) : ContDiff ℝ (↑⊤) (eta h τ)

theorem NavierStokes.RenormalizedHeatMoment.velocity_contDiff {h τ : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hτ : 0 < τ) {F : ℝ × ℝ → ℝ} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ Set.Ioo (-1) 1)) : ContDiff ℝ (↑⊤) (velocity h τ F)

theorem NavierStokes.RenormalizedHeatMoment.referencePower_scaling (h C : ℝ) {q : ℝ} (hq : 0 < q) (r : ℝ) : q ^ (-A h) * referencePower h C (r / √q) = referencePower h C r

theorem NavierStokes.RenormalizedHeatMoment.heatCarrier_scaling (h C : ℝ) {q τ ν r : ℝ} (hq : 0 < q) (hr : 0 < r) (hν : ν = τ / q) : q ^ (-A h) * heatCarrier h C ν (r / √q) = heatCarrier h C τ r

theorem NavierStokes.RenormalizedHeatMoment.velocity_commonExterior {h τ C B : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hτ : 0 < τ) (hB : 0 < B) {F : ℝ × ℝ → ℝ} (he : ∀ eta ∈ Set.Ioo (-1) 1, ∀ (R : ℝ), B ≤ R → F (R, eta) = heatCarrier h C (1 - eta ^ 2) R) : CommonExterior (velocity h τ F) (heatCarrier h C τ)

noncomputable def NavierStokes.RenormalizedHeatMoment.radialDifference (h C : ℝ) (F : ℝ × ℝ → ℝ) (eta r : ℝ) : ℝ

Radial difference, given by r ^ 2 * (F (r, eta) - referencePower h C r).

Equations

• NavierStokes.RenormalizedHeatMoment.radialDifference h C F eta r = r ^ 2 * (F (r, eta) - NavierStokes.RenormalizedHeatMoment.referencePower h C r)

noncomputable def NavierStokes.RenormalizedHeatMoment.profileMoment (h C : ℝ) (F : ℝ × ℝ → ℝ) (eta : ℝ) : ℝ

Profile moment, given by ∫ r in Ioi (0 : ℝ), radialDifference h C F eta r.

Equations

• NavierStokes.RenormalizedHeatMoment.profileMoment h C F eta = ∫ (r : ℝ) in Set.Ioi 0, NavierStokes.RenormalizedHeatMoment.radialDifference h C F eta r

theorem NavierStokes.RenormalizedHeatMoment.physical_difference_scaling {h τ : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hτ : 0 < τ) (C : ℝ) (F : ℝ × ℝ → ℝ) (z r : ℝ) : r ^ 2 * (velocity h τ F (z, r) - referencePower h C r) = Q h τ z * Q h τ z ^ (-A h) * radialDifference h C F (eta h τ z) (r / √(Q h τ z))

theorem NavierStokes.RenormalizedHeatMoment.profileMoment_integrable_physical {h τ C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hτ : 0 < τ) {F : ℝ × ℝ → ℝ} (hi : ∀ eta ∈ Set.Ioo (-1) 1, MeasureTheory.IntegrableOn (radialDifference h C F eta) (Set.Ioi 0) MeasureTheory.volume) (z : ℝ) : MeasureTheory.IntegrableOn (fun (r : ℝ) => r ^ 2 * (velocity h τ F (z, r) - referencePower h C r)) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.RenormalizedHeatMoment.physical_moment_scaling {h τ : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hτ : 0 < τ) (C : ℝ) (F : ℝ × ℝ → ℝ) (z : ℝ) : renormalizedMoment (velocity h τ F) (referencePower h C) z = Q h τ z ^ (1 - h) * profileMoment h C F (eta h τ z)

Integrability at the axis and at infinity

theorem NavierStokes.RenormalizedHeatMoment.weighted_referencePower (h C : ℝ) {r : ℝ} (hr : 0 < r) : r ^ 2 * referencePower h C r = C * 2 ^ A h * r ^ (1 - 2 * h)

theorem NavierStokes.RenormalizedHeatMoment.weighted_referencePower_nonneg_radius {h : ℝ} (hh1 : h < 1 / 2) (C : ℝ) {r : ℝ} (hr : 0 ≤ r) : r ^ 2 * referencePower h C r = C * 2 ^ A h * r ^ (1 - 2 * h)

theorem NavierStokes.RenormalizedHeatMoment.radialDifference_continuousOn {h C : ℝ} {F : ℝ × ℝ → ℝ} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ Set.Ioo (-1) 1)) {eta : ℝ} (hη : eta ∈ Set.Ioo (-1) 1) : ContinuousOn (radialDifference h C F eta) (Set.Ioi 0)

theorem NavierStokes.RenormalizedHeatMoment.radialDifference_integrable_near_axis {h C B : ℝ} (hh1 : h < 1 / 2) {F : ℝ × ℝ → ℝ} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ Set.Ioo (-1) 1)) {eta : ℝ} (hη : eta ∈ Set.Ioo (-1) 1) : MeasureTheory.IntegrableOn (radialDifference h C F eta) (Set.Icc 0 B) MeasureTheory.volume

theorem NavierStokes.RenormalizedHeatMoment.weighted_heat_difference_bound {h ν r : ℝ} (hh : 0 < h) (hν : ν ∈ Set.Icc 0 1) (hr : 0 < r) (C : ℝ) : |r ^ 2 * (heatCarrier h C ν r - referencePower h C r)| ≤ 4 * |C| * 2 ^ A h * h * (1 + h) * r ^ (-1 - 2 * h)

theorem NavierStokes.RenormalizedHeatMoment.radialDifference_integrable {h C B : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hB : 0 < B) {F : ℝ × ℝ → ℝ} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ Set.Ioo (-1) 1)) (he : ∀ eta ∈ Set.Ioo (-1) 1, ∀ (R : ℝ), B ≤ R → F (R, eta) = heatCarrier h C (1 - eta ^ 2) R) {eta : ℝ} (hη : eta ∈ Set.Ioo (-1) 1) : MeasureTheory.IntegrableOn (radialDifference h C F eta) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.RenormalizedHeatMoment.physical_axial_viscosity_moment_zero {h τ C B : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hτ : 0 < τ) (hB : 0 < B) {F : ℝ × ℝ → ℝ} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ Set.Ioo (-1) 1)) (he : ∀ eta ∈ Set.Ioo (-1) 1, ∀ (R : ℝ), B ≤ R → F (R, eta) = heatCarrier h C (1 - eta ^ 2) R) (hm : ∀ eta ∈ Set.Ioo (-1) 1, profileMoment h C F eta = 0) (z : ℝ) : MeasureTheory.IntegrableOn (fun (r : ℝ) => r ^ 2 * iteratedDeriv 2 (fun (y : ℝ) => velocity h τ F (y, r)) z) (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (r : ℝ) in Set.Ioi 0, r ^ 2 * iteratedDeriv 2 (fun (y : ℝ) => velocity h τ F (y, r)) z = 0

The nominal X-moment and the literal physical velocity

theorem NavierStokes.RenormalizedHeatMoment.squareHalf_image : (fun (r : ℝ) => r ^ 2 / 2) '' Set.Ioi 0 = Set.Ioi 0

theorem NavierStokes.RenormalizedHeatMoment.squareHalf_injective : Set.InjOn (fun (r : ℝ) => r ^ 2 / 2) (Set.Ioi 0)

theorem NavierStokes.RenormalizedHeatMoment.squareHalf_derivative (r : ℝ) : HasDerivAt (fun (r : ℝ) => r ^ 2 / 2) r r

theorem NavierStokes.RenormalizedHeatMoment.profileMoment_eq_X_integral (h C : ℝ) (F : ℝ × ℝ → ℝ) (eta : ℝ) : profileMoment h C F eta = ∫ (X : ℝ) in Set.Ioi 0, √(2 * X) * (F (√(2 * X), eta) - C * X ^ (-A h))

noncomputable def NavierStokes.RenormalizedHeatMoment.xMoment (h C : ℝ) (E : ℝ × ℝ → ℝ) (eta : ℝ) : ℝ

X moment, given by ∫ X in Ioi (0 : ℝ), Real.sqrt (2 * X) * (E (X, eta) - C * X ^ (-A h)).

Equations

• NavierStokes.RenormalizedHeatMoment.xMoment h C E eta = ∫ (X : ℝ) in Set.Ioi 0, √(2 * X) * (E (X, eta) - C * X ^ (-NavierStokes.RenormalizedHeatMoment.A h))

theorem NavierStokes.RenormalizedHeatMoment.profileMoment_eq_xMoment (h C : ℝ) {F E : ℝ × ℝ → ℝ} (hFE : ∀ (R : ℝ), 0 < R → ∀ eta ∈ Set.Ioo (-1) 1, F (R, eta) = E (R ^ 2 / 2, eta)) {eta : ℝ} (hη : eta ∈ Set.Ioo (-1) 1) : profileMoment h C F eta = xMoment h C E eta

noncomputable def NavierStokes.RenormalizedHeatMoment.profileVelocity (h τ : ℝ) (E : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Profile velocity, given by Q h τ p.1 ^ (-A h) * E (p.2 ^ 2 / (2 * Q h τ p.1), eta h τ p.1).

Equations

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

noncomputable def NavierStokes.RenormalizedHeatMoment.uTheta (h : ℝ) (E : ℝ × ℝ → ℝ) (t r z : ℝ) : ℝ

U theta, given by profileVelocity h (1 - t) E (z, r).

Equations

• NavierStokes.RenormalizedHeatMoment.uTheta h E t r z = NavierStokes.RenormalizedHeatMoment.profileVelocity h (1 - t) E (z, r)

theorem NavierStokes.RenormalizedHeatMoment.velocity_eq_profileVelocity {h τ : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hτ : 0 < τ) {F E : ℝ × ℝ → ℝ} (hFE : ∀ (R : ℝ), 0 < R → ∀ eta ∈ Set.Ioo (-1) 1, F (R, eta) = E (R ^ 2 / 2, eta)) {r : ℝ} (hr : 0 < r) (z : ℝ) : velocity h τ F (z, r) = profileVelocity h τ E (z, r)

theorem NavierStokes.RenormalizedHeatMoment.radial_exterior_of_X_exterior {h C T : ℝ} (hT : 0 < T) {F E : ℝ × ℝ → ℝ} (hFE : ∀ (R : ℝ), 0 < R → ∀ eta ∈ Set.Ioo (-1) 1, F (R, eta) = E (R ^ 2 / 2, eta)) (he : ∀ eta ∈ Set.Ioo (-1) 1, ∀ (X : ℝ), T ≤ X → E (X, eta) = C * X ^ (-A h) * RadialHeatProfile.profile (1 + h) (2 * (1 - eta ^ 2) / X)) (eta : ℝ) : eta ∈ Set.Ioo (-1) 1 → ∀ (R : ℝ), √(2 * T) ≤ R → F (R, eta) = heatCarrier h C (1 - eta ^ 2) R

theorem NavierStokes.RenormalizedHeatMoment.physical_axial_viscosity_zero_of_X_profile {h τ C T : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hτ : 0 < τ) (hT : 0 < T) {F E : ℝ × ℝ → ℝ} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ Set.Ioo (-1) 1)) (hFE : ∀ (R : ℝ), 0 < R → ∀ eta ∈ Set.Ioo (-1) 1, F (R, eta) = E (R ^ 2 / 2, eta)) (he : ∀ eta ∈ Set.Ioo (-1) 1, ∀ (X : ℝ), T ≤ X → E (X, eta) = C * X ^ (-A h) * RadialHeatProfile.profile (1 + h) (2 * (1 - eta ^ 2) / X)) (hm : ∀ eta ∈ Set.Ioo (-1) 1, xMoment h C E eta = 0) (z : ℝ) : MeasureTheory.IntegrableOn (fun (r : ℝ) => r ^ 2 * iteratedDeriv 2 (fun (y : ℝ) => profileVelocity h τ E (y, r)) z) (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (r : ℝ) in Set.Ioi 0, r ^ 2 * iteratedDeriv 2 (fun (y : ℝ) => profileVelocity h τ E (y, r)) z = 0

The only nominal input involving an integral is the original renormalized moment itself. Its differentiated moment is derived, not assumed.

theorem NavierStokes.RenormalizedHeatMoment.uTheta_axial_viscosity_integral {h t C T : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) (hT : 0 < T) {F E : ℝ × ℝ → ℝ} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ Set.Ioo (-1) 1)) (hFE : ∀ (R : ℝ), 0 < R → ∀ eta ∈ Set.Ioo (-1) 1, F (R, eta) = E (R ^ 2 / 2, eta)) (he : ∀ eta ∈ Set.Ioo (-1) 1, ∀ (X : ℝ), T ≤ X → E (X, eta) = C * X ^ (-A h) * RadialHeatProfile.profile (1 + h) (2 * (1 - eta ^ 2) / X)) (hm : ∀ eta ∈ Set.Ioo (-1) 1, xMoment h C E eta = 0) (z : ℝ) : ∫ (r : ℝ) in Set.Ioi 0, r ^ 2 * deriv (deriv (uTheta h E t r)) z = 0

theorem NavierStokes.RenormalizedHeatMoment.uTheta_eq_similarity_pullback (h : ℝ) (E : ℝ × ℝ → ℝ) (t r z : ℝ) : uTheta h E t r z = SimilarityProfile.pullback h (-A h) E (t, r ^ 2 / 2, z)

theorem NavierStokes.RenormalizedHeatMoment.integral_weighted_radial_scale (b : ℝ) {q : ℝ} (hq : 0 < q) (g : ℝ → ℝ) : ∫ (r : ℝ) in Set.Ioi 0, r ^ 2 * (q ^ b * g (r / √q)) = q ^ (b + 3 / 2) * ∫ (R : ℝ) in Set.Ioi 0, R ^ 2 * g R

The scaling used to transfer the physical order-one viscosity moment to the radial profile moment: r = sqrt(q) R contributes q^(3/2).

theorem NavierStokes.RenormalizedHeatMoment.integral_axial_scale (h : ℝ) {q : ℝ} (hq : 0 < q) (g : ℝ → ℝ) : ∫ (r : ℝ) in Set.Ioi 0, r ^ 2 * (q ^ (-A h - 2 * CoordinateAlgebra.D h) * g (r / √q)) = q ^ h * ∫ (R : ℝ) in Set.Ioi 0, R ^ 2 * g R

theorem NavierStokes.RenormalizedHeatMoment.exterior_second_derivative_zero {u : ℝ × ℝ → ℝ} {tail : ℝ → ℝ} (he : CommonExterior u tail) (z : ℝ) : ∃ (B : ℝ), 0 < B ∧ ∀ (r : ℝ), B ≤ r → iteratedDeriv 2 (fun (y : ℝ) => u (y, r)) z = 0

The reference normalization of the constructed outgoing schedule

noncomputable def NavierStokes.RenormalizedHeatMoment.outgoingPowerAmplitude (P : OutgoingProfile.Profile) (XR : ℝ) : ℝ

Outgoing power amplitude, given by OutgoingTail.powerConstant P.data * XR ^ A P.data.h.

Equations

• NavierStokes.RenormalizedHeatMoment.outgoingPowerAmplitude P XR = NavierStokes.OutgoingTail.powerConstant P.data * XR ^ NavierStokes.RenormalizedHeatMoment.A P.data.h

theorem NavierStokes.RenormalizedHeatMoment.outgoing_powerH (P : OutgoingProfile.Profile) {XR X : ℝ} (hXR : 0 < XR) (hX : 0 < X) : OutgoingDilation.powerH P XR X = √(2 * X) * (outgoingPowerAmplitude P XR * X ^ (-A P.data.h))

theorem NavierStokes.RenormalizedHeatMoment.outgoing_amplitude_eq_heat (P : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) : outgoingPowerAmplitude P XR = OutgoingDilation.carrierAmplitude P * OutgoingDilation.switchRadius P XR ^ HeatTailEdit.exponent P.data.h

theorem NavierStokes.RenormalizedHeatMoment.xMoment_eq_outgoing_reference (P : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (E : ℝ × ℝ → ℝ) (eta : ℝ) : xMoment P.data.h (outgoingPowerAmplitude P XR) E eta = ∫ (X : ℝ) in Set.Ioi 0, √(2 * X) * E (X, eta) - OutgoingDilation.powerH P XR X

noncomputable def NavierStokes.RenormalizedHeatMoment.heatThreshold (P : OutgoingProfile.Profile) (XR : ℝ) : ℝ

Heat threshold, given by OutgoingDilation.switchRadius P XR * Real.exp 3.

Equations

• NavierStokes.RenormalizedHeatMoment.heatThreshold P XR = NavierStokes.OutgoingDilation.switchRadius P XR * Real.exp 3

theorem NavierStokes.RenormalizedHeatMoment.heatThreshold_pos (P : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) : 0 < heatThreshold P XR

theorem NavierStokes.RenormalizedHeatMoment.heated_exterior (P : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) (eta : ℝ) {X : ℝ} (hX : heatThreshold P XR ≤ X) : HeatedOutgoing.E P XR c (X, eta) = outgoingPowerAmplitude P XR * X ^ (-A P.data.h) * RadialHeatProfile.profile (1 + P.data.h) (2 * (1 - eta ^ 2) / X)

theorem NavierStokes.RenormalizedHeatMoment.heated_nominal_axial_viscosity (P : OutgoingProfile.Profile) {XR cost t : ℝ} (w : HeatedOutgoing.CompensationWitness P XR cost) (hh1 : P.data.h < 1 / 2) (ht : t < 1) (L : ℝ) {F E : ℝ × ℝ → ℝ} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ Set.Ioo (-1) 1)) (hFE : ∀ (R : ℝ), 0 < R → ∀ eta ∈ Set.Ioo (-1) 1, F (R, eta) = E (R ^ 2 / 2, eta)) (hmatch : ∀ eta ∈ Set.Ioo (-1) 1, ∀ (X : ℝ), L ≤ X → E (X, eta) = HeatedOutgoing.E P XR w.coefficients (X, eta)) (hreset : ∀ eta ∈ Set.Ioo (-1) 1, ∫ (X : ℝ) in Set.Ioi 0, √(2 * X) * E (X, eta) - OutgoingDilation.powerH P XR X = ∫ (X : ℝ) in Set.Ioi 0, HeatedOutgoing.H P XR w.coefficients (X, eta) - OutgoingDilation.powerH P XR X) (z : ℝ) : MeasureTheory.IntegrableOn (fun (r : ℝ) => r ^ 2 * deriv (deriv (uTheta P.data.h E t r)) z) (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (r : ℝ) in Set.Ioi 0, r ^ 2 * deriv (deriv (uTheta P.data.h E t r)) z = 0

Specialization to the actual heated and compensated outgoing witness. The remaining upstream conditions are precisely the nominal axis gluing and its original reset moment, not an axial-viscosity moment or derivative bound.