Terminal heat tails and backward stress

All derivatives and integrals are actual analytic operations. The backward stress is defined independently of the separate global moment condition that identifies it with an axis-based stress primitive.

theorem NavierStokes.TerminalStress.contDiffAt_deriv {f : ℝ → ℝ} {r : ℝ} {m n : WithTop ℕ∞} (hf : ContDiffAt ℝ n f r) (hmn : m + 1 ≤ n) : ContDiffAt ℝ m (deriv f) r

noncomputable def NavierStokes.TerminalStress.viscousResidual (K f : ℝ → ℝ) (r : ℝ) : ℝ

Radial-viscosity terms left after cancelling the heat equation for K.

Equations

• NavierStokes.TerminalStress.viscousResidual K f r = -K r * (deriv (deriv f) r + deriv f r / r) - 2 * deriv K r * deriv f r

noncomputable def NavierStokes.TerminalStress.boundary (K f : ℝ → ℝ) (r : ℝ) : ℝ

Boundary, given by r ^ 2 * K r * deriv f r.

Equations

• NavierStokes.TerminalStress.boundary K f r = r ^ 2 * K r * deriv f r

noncomputable def NavierStokes.TerminalStress.correction (K f : ℝ → ℝ) (r : ℝ) : ℝ

Correction, given by (r * K r - r ^ 2 * deriv K r) * deriv f r.

Equations

• NavierStokes.TerminalStress.correction K f r = (r * K r - r ^ 2 * deriv K r) * deriv f r

noncomputable def NavierStokes.TerminalStress.backwardStress (R : ℝ → ℝ) (r : ℝ) : ℝ

Backward stress, given by (∫ u in Ioi r, u ^ 2 * R u) / r ^ 2.

Equations

• NavierStokes.TerminalStress.backwardStress R r = (∫ (u : ℝ) in Set.Ioi r, u ^ 2 * R u) / r ^ 2

theorem NavierStokes.TerminalStress.boundary_hasDerivAt {K f : ℝ → ℝ} {r : ℝ} (hr : r ≠ 0) (hK : DifferentiableAt ℝ K r) (hf : ContDiffAt ℝ 2 f r) : HasDerivAt (boundary K f) (correction K f r - r ^ 2 * viscousResidual K f r) r

theorem NavierStokes.TerminalStress.integral_viscousResidual {K f : ℝ → ℝ} {r : ℝ} (hr : 0 < r) (hK : ∀ u ∈ Set.Ici r, DifferentiableAt ℝ K u) (hf : ∀ u ∈ Set.Ici r, ContDiffAt ℝ 2 f u) (hv : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * viscousResidual K f u) (Set.Ioi r) MeasureTheory.volume) (hc : MeasureTheory.IntegrableOn (correction K f) (Set.Ioi r) MeasureTheory.volume) (hboundary : Filter.Tendsto (boundary K f) Filter.atTop (nhds 0)) : ∫ (u : ℝ) in Set.Ioi r, u ^ 2 * viscousResidual K f u = boundary K f r + ∫ (u : ℝ) in Set.Ioi r, correction K f u

The exact backward integration-by-parts identity. Integrability and the vanishing boundary at infinity are explicit local-tail hypotheses.

theorem NavierStokes.TerminalStress.backwardStress_formula {K f T : ℝ → ℝ} {r : ℝ} (hr : 0 < r) (hK : ∀ u ∈ Set.Ici r, DifferentiableAt ℝ K u) (hf : ∀ u ∈ Set.Ici r, ContDiffAt ℝ 2 f u) (hv : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * viscousResidual K f u) (Set.Ioi r) MeasureTheory.volume) (hc : MeasureTheory.IntegrableOn (correction K f) (Set.Ioi r) MeasureTheory.volume) (ht : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * T u) (Set.Ioi r) MeasureTheory.volume) (hboundary : Filter.Tendsto (boundary K f) Filter.atTop (nhds 0)) : backwardStress (fun (u : ℝ) => T u + viscousResidual K f u) r = K r * deriv f r + ((∫ (u : ℝ) in Set.Ioi r, u ^ 2 * T u) + ∫ (u : ℝ) in Set.Ioi r, correction K f u) / r ^ 2

theorem NavierStokes.TerminalStress.correction_nonneg {K f : ℝ → ℝ} {r : ℝ} (hr : 0 ≤ r) (hK : 0 ≤ K r) (hKr : deriv K r ≤ 0) (hfr : 0 ≤ deriv f r) : 0 ≤ correction K f r

theorem NavierStokes.TerminalStress.backwardStress_ge_boundary {K f T : ℝ → ℝ} {r : ℝ} (hr : 0 < r) (hK : ∀ u ∈ Set.Ici r, DifferentiableAt ℝ K u) (hf : ∀ u ∈ Set.Ici r, ContDiffAt ℝ 2 f u) (hv : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * viscousResidual K f u) (Set.Ioi r) MeasureTheory.volume) (hc : MeasureTheory.IntegrableOn (correction K f) (Set.Ioi r) MeasureTheory.volume) (ht : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * T u) (Set.Ioi r) MeasureTheory.volume) (hboundary : Filter.Tendsto (boundary K f) Filter.atTop (nhds 0)) (hKpos : ∀ u ∈ Set.Ioi r, 0 ≤ K u) (hKdec : ∀ u ∈ Set.Ioi r, deriv K u ≤ 0) (hfinc : ∀ u ∈ Set.Ioi r, 0 ≤ deriv f u) (hTpos : ∀ u ∈ Set.Ioi r, 0 ≤ T u) : K r * deriv f r ≤ backwardStress (fun (u : ℝ) => T u + viscousResidual K f u) r

The backward stress controls the positive radial boundary term.

theorem NavierStokes.TerminalStress.backwardStress_ge_mass {K f T : ℝ → ℝ} {r c : ℝ} (hr : 0 < r) (hK : ∀ u ∈ Set.Ici r, DifferentiableAt ℝ K u) (hf : ∀ u ∈ Set.Ici r, ContDiffAt ℝ 2 f u) (hv : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * viscousResidual K f u) (Set.Ioi r) MeasureTheory.volume) (hc : MeasureTheory.IntegrableOn (correction K f) (Set.Ioi r) MeasureTheory.volume) (ht : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * T u) (Set.Ioi r) MeasureTheory.volume) (hboundary : Filter.Tendsto (boundary K f) Filter.atTop (nhds 0)) (hfi : MeasureTheory.IntegrableOn (deriv f) (Set.Ioi r) MeasureTheory.volume) (hflim : Filter.Tendsto f Filter.atTop (nhds 1)) (hKpos : ∀ u ∈ Set.Ici r, 0 ≤ K u) (hKdec : ∀ u ∈ Set.Ioi r, deriv K u ≤ 0) (hfinc : ∀ u ∈ Set.Ici r, 0 ≤ deriv f u) (hcompare : ∀ u ∈ Set.Ioi r, c * deriv f u ≤ u ^ 2 * T u) : c / r ^ 2 * (1 - f r) ≤ backwardStress (fun (u : ℝ) => T u + viscousResidual K f u) r

A precise version of the time-integral lower comparison. The extra coefficient comparison is distinct from mere monotonicity of K.

noncomputable def NavierStokes.TerminalStress.heatAmplitude (C a t r : ℝ) : ℝ

The heat carrier with the manuscript's arbitrary fixed normalization.

Equations

• NavierStokes.TerminalStress.heatAmplitude C a t r = C * NavierStokes.RadialHeatProfile.radialProfile a (1 - t) r

theorem NavierStokes.TerminalStress.heatAmplitude_pos {C a t r : ℝ} (hC : 0 < C) (ha : 1 < a) (ht : t < 1) (hr : 0 < r) : 0 < heatAmplitude C a t r

theorem NavierStokes.TerminalStress.heatAmplitude_deriv_neg {C a t r : ℝ} (hC : 0 < C) (ha : 1 < a) (ht : t < 1) (hr : 0 < r) : deriv (heatAmplitude C a t) r < 0

theorem NavierStokes.TerminalStress.heatAmplitude_heat_equation (C : ℝ) {a t r : ℝ} (ha : 1 < a) (ht : t < 1) (hr : 0 < r) : deriv (fun (t : ℝ) => heatAmplitude C a t r) t = deriv (deriv (heatAmplitude C a t)) r + deriv (heatAmplitude C a t) r / r - heatAmplitude C a t r / r ^ 2

theorem NavierStokes.TerminalStress.deriv_deriv_mul {f g : ℝ → ℝ} {r : ℝ} (hf : ContDiffAt ℝ 2 f r) (hg : ContDiffAt ℝ 2 g r) : deriv (deriv fun (u : ℝ) => f u * g u) r = deriv (deriv f) r * g r + 2 * deriv f r * deriv g r + f r * deriv (deriv g) r

theorem NavierStokes.TerminalStress.heatAmplitude_contDiffAt (C : ℝ) {a t r : ℝ} (ha : 1 < a) (ht : t < 1) (hr : 0 < r) : ContDiffAt ℝ (↑⊤) (heatAmplitude C a t) r

theorem NavierStokes.TerminalStress.heatAmplitude_time_differentiable (C : ℝ) {a t r : ℝ} (ha : 1 < a) (ht : t < 1) (hr : 0 < r) : DifferentiableAt ℝ (fun (t : ℝ) => heatAmplitude C a t r) t

theorem NavierStokes.TerminalStress.heat_times_factor_residual (C : ℝ) {a t r : ℝ} (ha : 1 < a) (ht : t < 1) (hr : 0 < r) {f : ℝ → ℝ → ℝ} (hft : DifferentiableAt ℝ (fun (t : ℝ) => f t r) t) (hfr : ContDiffAt ℝ 2 (f t) r) : deriv (fun (u : ℝ) => heatAmplitude C a u r * f u r) t - (deriv (deriv fun (u : ℝ) => heatAmplitude C a t u * f t u) r + deriv (fun (u : ℝ) => heatAmplitude C a t u * f t u) r / r - heatAmplitude C a t r * f t r / r ^ 2) = heatAmplitude C a t r * deriv (fun (u : ℝ) => f u r) t + viscousResidual (heatAmplitude C a t) (f t) r

Product expansion of the actual heat equation. No formal jet variables occur.

@[reducible, inline]

abbrev NavierStokes.TerminalStress.PhysicalPoint : Type

Physical point: an abbreviation for SimilarityProfile.PhysicalPoint.

Equations

• NavierStokes.TerminalStress.PhysicalPoint = NavierStokes.SimilarityProfile.PhysicalPoint

@[reducible, inline]

abbrev NavierStokes.TerminalStress.PhysicalProfile : Type

Physical profile: an abbreviation for SimilarityProfile.PhysicalProfile.

Equations

• NavierStokes.TerminalStress.PhysicalProfile = NavierStokes.SimilarityProfile.PhysicalProfile

noncomputable def NavierStokes.TerminalStress.radiusPoint (t r z : ℝ) : PhysicalPoint

Radius point, given by (t, (r ^ 2 / 2, z)).

Equations

• NavierStokes.TerminalStress.radiusPoint t r z = (t, r ^ 2 / 2, z)

noncomputable def NavierStokes.TerminalStress.radialSlice (G : PhysicalProfile) (t z r : ℝ) : ℝ

Radial slice, given by G (radiusPoint t r z).

Equations

• NavierStokes.TerminalStress.radialSlice G t z r = G (NavierStokes.TerminalStress.radiusPoint t r z)

theorem NavierStokes.TerminalStress.radiusPoint_contDiff (t z : ℝ) : ContDiff ℝ ↑⊤ fun (r : ℝ) => radiusPoint t r z

theorem NavierStokes.TerminalStress.radialSlice_hasDerivAt {G : PhysicalProfile} {t r z : ℝ} (hG : DifferentiableAt ℝ G (radiusPoint t r z)) : HasDerivAt (radialSlice G t z) (r * SimilarityProfile.partialS G (radiusPoint t r z)) r

theorem NavierStokes.TerminalStress.timeSlice_hasDerivAt {G : PhysicalProfile} {p : PhysicalPoint} (hG : DifferentiableAt ℝ G p) : HasDerivAt (fun (t : ℝ) => G (t, p.2)) (SimilarityProfile.partialT G p) p.1

theorem NavierStokes.TerminalStress.partialS_contDiffAt {G : PhysicalProfile} {p : PhysicalPoint} {m n : WithTop ℕ∞} (hG : ContDiffAt ℝ n G p) (hmn : m + 1 ≤ n) : ContDiffAt ℝ m (SimilarityProfile.partialS G) p

theorem NavierStokes.TerminalStress.radialSlice_second {G : PhysicalProfile} {t r z : ℝ} (hG : ContDiffAt ℝ 2 G (radiusPoint t r z)) : deriv (deriv (radialSlice G t z)) r = SimilarityProfile.partialS G (radiusPoint t r z) + r ^ 2 * SimilarityProfile.partialS (SimilarityProfile.partialS G) (radiusPoint t r z)

theorem NavierStokes.TerminalStress.angular_radial_operator {F : PhysicalProfile} {t r z : ℝ} (hr : r ≠ 0) (hF : ContDiffAt ℝ 2 F (radiusPoint t r z)) : deriv (deriv fun (u : ℝ) => u * radialSlice F t z u) r + deriv (fun (u : ℝ) => u * radialSlice F t z u) r / r - r * radialSlice F t z r / r ^ 2 = r * (2 * (radiusPoint t r z).2.1 * SimilarityProfile.partialS (SimilarityProfile.partialS F) (radiusPoint t r z) + 4 * SimilarityProfile.partialS F (radiusPoint t r z))

The actual cylindrical angular radial Laplacian of r F.

noncomputable def NavierStokes.TerminalStress.flattening (h : ℝ) (f : ℝ → ℝ) (p : PhysicalPoint) : ℝ

The terminal flattening factor is an actual function of logarithmic X.

Equations

• NavierStokes.TerminalStress.flattening h f p = f (Real.log (NavierStokes.SimilarityProfile.X h p))

theorem NavierStokes.TerminalStress.flattening_contDiffAt {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) {f : ℝ → ℝ} (hf : ContDiffAt ℝ 2 f (Real.log (SimilarityProfile.X h p))) : ContDiffAt ℝ 2 (flattening h f) p

theorem NavierStokes.TerminalStress.flattening_time_hasDerivAt {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) {f : ℝ → ℝ} (hf : DifferentiableAt ℝ f (Real.log (SimilarityProfile.X h p))) : HasDerivAt (fun (t : ℝ) => flattening h f (t, p.2)) (deriv f (Real.log (SimilarityProfile.X h p)) / (SimilarityProfile.q h p * CoordinateAlgebra.L h (SimilarityProfile.eta h p))) p.1

theorem NavierStokes.TerminalStress.flattening_radial_hasDerivAt {h t r z : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) (hr : 0 < r) {f : ℝ → ℝ} (hf : DifferentiableAt ℝ f (Real.log (SimilarityProfile.X h (radiusPoint t r z)))) : HasDerivAt (radialSlice (flattening h f) t z) (2 * deriv f (Real.log (SimilarityProfile.X h (radiusPoint t r z))) / r) r

theorem NavierStokes.TerminalStress.terminal_radial_residual (C : ℝ) {h t r z : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) (hr : 0 < r) {f : ℝ → ℝ} (hf : ContDiffAt ℝ 2 f (Real.log (SimilarityProfile.X h (radiusPoint t r z)))) : deriv (fun (u : ℝ) => heatAmplitude C (1 + h) u r * flattening h f (radiusPoint u r z)) t - (deriv (deriv fun (u : ℝ) => heatAmplitude C (1 + h) t u * radialSlice (flattening h f) t z u) r + deriv (fun (u : ℝ) => heatAmplitude C (1 + h) t u * radialSlice (flattening h f) t z u) r / r - heatAmplitude C (1 + h) t r * radialSlice (flattening h f) t z r / r ^ 2) = heatAmplitude C (1 + h) t r * (deriv f (Real.log (SimilarityProfile.X h (radiusPoint t r z))) / (SimilarityProfile.q h (radiusPoint t r z) * CoordinateAlgebra.L h (SimilarityProfile.eta h (radiusPoint t r z)))) + viscousResidual (heatAmplitude C (1 + h) t) (radialSlice (flattening h f) t z) r

The displayed terminal angular residual, before axial viscosity, is an identity of actual time and radial derivatives of K f_o.

noncomputable def NavierStokes.TerminalStress.physicalHeat (C a : ℝ) (p : PhysicalPoint) : ℝ

The angular heat carrier expressed in the regular coordinate s.

Equations

• NavierStokes.TerminalStress.physicalHeat C a p = C * NavierStokes.RadialHeatProfile.spatialProfile a (1 - p.1) p.2.1

noncomputable def NavierStokes.TerminalStress.swirlCoefficient (C h : ℝ) (f : ℝ → ℝ) (p : PhysicalPoint) : ℝ

The regular Cartesian swirl coefficient: the physical angular velocity is r F.

Equations

• NavierStokes.TerminalStress.swirlCoefficient C h f p = NavierStokes.TerminalStress.physicalHeat C (1 + h) p * NavierStokes.TerminalStress.flattening h f p / √(2 * p.2.1)

theorem NavierStokes.TerminalStress.physicalHeat_contDiffAt (C : ℝ) {a : ℝ} (ha : 1 < a) {p : PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) : ContDiffAt ℝ (↑⊤) (physicalHeat C a) p

theorem NavierStokes.TerminalStress.swirlCoefficient_contDiffAt (C : ℝ) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) {f : ℝ → ℝ} (hf : ContDiffAt ℝ 2 f (Real.log (SimilarityProfile.X h p))) : ContDiffAt ℝ 2 (swirlCoefficient C h f) p

theorem NavierStokes.TerminalStress.swirlCoefficient_amplitude (C h : ℝ) (f : ℝ → ℝ) (t z : ℝ) {r : ℝ} (hr : 0 < r) : r * swirlCoefficient C h f (radiusPoint t r z) = heatAmplitude C (1 + h) t r * radialSlice (flattening h f) t z r

theorem NavierStokes.TerminalStress.regular_leading_residual {F : PhysicalProfile} {t r z : ℝ} (hr : r ≠ 0) (hF : ContDiffAt ℝ 2 F (radiusPoint t r z)) : r * (SimilarityProfile.partialT F (radiusPoint t r z) - 2 * (radiusPoint t r z).2.1 * SimilarityProfile.partialS (SimilarityProfile.partialS F) (radiusPoint t r z) - 4 * SimilarityProfile.partialS F (radiusPoint t r z)) = deriv (fun (u : ℝ) => r * F (radiusPoint u r z)) t - (deriv (deriv fun (u : ℝ) => u * radialSlice F t z u) r + deriv (fun (u : ℝ) => u * radialSlice F t z u) r / r - r * radialSlice F t z r / r ^ 2)

Transfer from regular Cartesian swirl derivatives to the actual radial operator.

noncomputable def NavierStokes.TerminalStress.leadingResidual (C h : ℝ) (f : ℝ → ℝ) (t r z : ℝ) : ℝ

Leading residual, constructed using heatAmplitude.

Equations

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

theorem NavierStokes.TerminalStress.swirlCoefficient_leading_residual (C : ℝ) {h t r z : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) (hr : 0 < r) {f : ℝ → ℝ} (hf : ContDiffAt ℝ 2 f (Real.log (SimilarityProfile.X h (radiusPoint t r z)))) : r * (SimilarityProfile.partialT (swirlCoefficient C h f) (radiusPoint t r z) - 2 * (radiusPoint t r z).2.1 * SimilarityProfile.partialS (SimilarityProfile.partialS (swirlCoefficient C h f)) (radiusPoint t r z) - 4 * SimilarityProfile.partialS (swirlCoefficient C h f) (radiusPoint t r z)) = leadingResidual C h f t r z

noncomputable def NavierStokes.TerminalStress.canonicalPressure (F : PhysicalProfile) (p : PhysicalPoint) : ℝ

Canonical pressure, normalized at infinity, in the regular coordinate.

Equations

• NavierStokes.TerminalStress.canonicalPressure F p = -∫ (s : ℝ) in Set.Ioi p.2.1, F (p.1, s, p.2.2) ^ 2

theorem NavierStokes.TerminalStress.neg_tailIntegral_hasDerivAt {g : ℝ → ℝ} {a b : ℝ} (hab : a < b) (hi : MeasureTheory.IntegrableOn g (Set.Ioi a) MeasureTheory.volume) (hc : ContinuousOn g (Set.Ioi a)) : HasDerivAt (fun (x : ℝ) => -∫ (u : ℝ) in Set.Ioi x, g u) (g b) b

theorem NavierStokes.TerminalStress.canonicalPressure_partialS {F : PhysicalProfile} {p : PhysicalPoint} {a : ℝ} (ha : a < p.2.1) (hi : MeasureTheory.IntegrableOn (fun (s : ℝ) => F (p.1, s, p.2.2) ^ 2) (Set.Ioi a) MeasureTheory.volume) (hc : ContinuousOn (fun (s : ℝ) => F (p.1, s, p.2.2) ^ 2) (Set.Ioi a)) (hp : DifferentiableAt ℝ (canonicalPressure F) p) : SimilarityProfile.partialS (canonicalPressure F) p = F p ^ 2

The radial pressure balance is derived from the defining improper integral. Joint pressure differentiability is a separate analytic regularity hypothesis.

noncomputable def NavierStokes.TerminalStress.residualCoefficient (F : PhysicalProfile) (p : PhysicalPoint) : ℝ

Residual coefficient, given by partialT F p - 2 * p.2.1 * partialS (partialS F) p - 4 * partialS F p - partialZ (partialZ F) p.

Equations

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

theorem NavierStokes.TerminalStress.pureSwirl_navierStokesResidual {F P : PhysicalProfile} {t : ℝ} {x : ProblemStatement.Space} (hF : ContDiffAt ℝ 2 F (AxisymmetricFields.profilePoint t x)) (hP : DifferentiableAt ℝ P (AxisymmetricFields.profilePoint t x)) : ProblemStatement.navierStokesResidual (AxisymmetricResidual.velocity (fun (x : AxisymmetricFields.ProfilePoint) => 0) F fun (x : AxisymmetricFields.ProfilePoint) => 0) (AxisymmetricResidual.pressure P) t x = AxisymmetricResidual.pack (x.ofLp 0 * (SimilarityProfile.partialS P (AxisymmetricFields.profilePoint t x) - F (AxisymmetricFields.profilePoint t x) ^ 2) - x.ofLp 1 * residualCoefficient F (AxisymmetricFields.profilePoint t x)) (x.ofLp 1 * (SimilarityProfile.partialS P (AxisymmetricFields.profilePoint t x) - F (AxisymmetricFields.profilePoint t x) ^ 2) + x.ofLp 0 * residualCoefficient F (AxisymmetricFields.profilePoint t x)) (SimilarityProfile.partialZ P (AxisymmetricFields.profilePoint t x))

The actual Cartesian residual of a purely angular velocity.

noncomputable def NavierStokes.TerminalStress.axialViscosity (C h : ℝ) (f : ℝ → ℝ) (p : PhysicalPoint) : ℝ

Exact axial viscosity retained in the terminal physical residual.

Equations

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

noncomputable def NavierStokes.TerminalStress.terminalVelocity (C h : ℝ) (f : ℝ → ℝ) : ProblemStatement.VelocityField

Terminal velocity, given by AxisymmetricResidual.velocity (fun _ => 0) (swirlCoefficient C h f) (fun _ => 0).

Equations

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

noncomputable def NavierStokes.TerminalStress.terminalPressure (C h : ℝ) (f : ℝ → ℝ) : ProblemStatement.PressureField

Terminal pressure, given by AxisymmetricResidual.pressure (canonicalPressure (swirlCoefficient C h f)).

Equations

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

theorem NavierStokes.TerminalStress.radiusPoint_profilePoint {t : ℝ} {x : ProblemStatement.Space} (hs : 0 ≤ AxisymmetricFields.radialEnergy x) : radiusPoint t (√(2 * AxisymmetricFields.radialEnergy x)) (x.ofLp 2) = AxisymmetricFields.profilePoint t x

theorem NavierStokes.TerminalStress.terminal_navierStokesResidual (C : ℝ) {h t : ℝ} {x : ProblemStatement.Space} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) (hs : 0 < AxisymmetricFields.radialEnergy x) {f : ℝ → ℝ} (hf : ContDiffAt ℝ 2 f (Real.log (SimilarityProfile.X h (AxisymmetricFields.profilePoint t x)))) {a : ℝ} (ha : a < AxisymmetricFields.radialEnergy x) (hi : MeasureTheory.IntegrableOn (fun (s : ℝ) => swirlCoefficient C h f (t, s, x.ofLp 2) ^ 2) (Set.Ioi a) MeasureTheory.volume) (hc : ContinuousOn (fun (s : ℝ) => swirlCoefficient C h f (t, s, x.ofLp 2) ^ 2) (Set.Ioi a)) (hP : DifferentiableAt ℝ (canonicalPressure (swirlCoefficient C h f)) (AxisymmetricFields.profilePoint t x)) : ProblemStatement.navierStokesResidual (terminalVelocity C h f) (terminalPressure C h f) t x = AxisymmetricResidual.pack (-x.ofLp 1 / √(2 * AxisymmetricFields.radialEnergy x) * (leadingResidual C h f t (√(2 * AxisymmetricFields.radialEnergy x)) (x.ofLp 2) - axialViscosity C h f (AxisymmetricFields.profilePoint t x))) (x.ofLp 0 / √(2 * AxisymmetricFields.radialEnergy x) * (leadingResidual C h f t (√(2 * AxisymmetricFields.radialEnergy x)) (x.ofLp 2) - axialViscosity C h f (AxisymmetricFields.profilePoint t x))) (SimilarityProfile.partialZ (canonicalPressure (swirlCoefficient C h f)) (AxisymmetricFields.profilePoint t x))

Full terminal residual, with canonical radial balance and the omitted axial-viscosity term displayed. The pressure's joint differentiability and the tail-integral hypotheses are explicit and do not impose a residual identity.

theorem NavierStokes.TerminalStress.backwardStress_divergence {R : ℝ → ℝ} {a r : ℝ} (hr : r ≠ 0) (ha : a < r) (hi : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * R u) (Set.Ioi a) MeasureTheory.volume) (hc : ContinuousOn (fun (u : ℝ) => u ^ 2 * R u) (Set.Ioi a)) : deriv (backwardStress R) r + 2 * backwardStress R r / r = -R r

A backward stress solves the actual radial divergence equation without any hypothesis about its integral over the whole radius.

noncomputable def NavierStokes.TerminalStress.forwardStress (R : ℝ → ℝ) (r : ℝ) : ℝ

Forward stress, given by -(∫ u in (0 : ℝ)..r, u ^ 2 * R u) / r ^ 2.

Equations

• NavierStokes.TerminalStress.forwardStress R r = (-∫ (u : ℝ) in 0..r, u ^ 2 * R u) / r ^ 2

theorem NavierStokes.TerminalStress.forward_eq_backward_iff {R : ℝ → ℝ} {r : ℝ} (hr : 0 < r) (hi : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * R u) (Set.Ioi 0) MeasureTheory.volume) : forwardStress R r = backwardStress R r ↔ ∫ (u : ℝ) in Set.Ioi 0, u ^ 2 * R u = 0

The missing global matching condition is exactly the zero total weighted residual. It is not part of the definition of either stress primitive.

noncomputable def NavierStokes.TerminalStress.timeDenominator (h t z : ℝ) : ℝ

Time denominator, given by SimilarityProfile.q h (t, (0, z)) * CoordinateAlgebra.L h (SimilarityProfile.eta h (t, (0, z))).

Equations

• NavierStokes.TerminalStress.timeDenominator h t z = NavierStokes.SimilarityProfile.q h (t, 0, z) * NavierStokes.CoordinateAlgebra.L h (NavierStokes.SimilarityProfile.eta h (t, 0, z))

noncomputable def NavierStokes.TerminalStress.timeResidual (C h : ℝ) (f : ℝ → ℝ) (t z r : ℝ) : ℝ

Time residual, given by heatAmplitude C (1 + h) t r * deriv f (Real.log (SimilarityProfile.X h (radiusPoint t r z))) / timeDenominator h t z.

Equations

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

theorem NavierStokes.TerminalStress.timeDenominator_pos {h t z : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) : 0 < timeDenominator h t z

theorem NavierStokes.TerminalStress.leadingResidual_eq_time_add (C h : ℝ) (f : ℝ → ℝ) (t r z : ℝ) : leadingResidual C h f t r z = timeResidual C h f t z r + viscousResidual (heatAmplitude C (1 + h) t) (radialSlice (flattening h f) t z) r

theorem NavierStokes.TerminalStress.timeResidual_nonneg {C h t r z : ℝ} (hC : 0 < C) (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) (hr : 0 < r) {f : ℝ → ℝ} (hf : 0 ≤ deriv f (Real.log (SimilarityProfile.X h (radiusPoint t r z)))) : 0 ≤ timeResidual C h f t z r

theorem NavierStokes.TerminalStress.terminal_correction_nonneg {C h t r z : ℝ} (hC : 0 < C) (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) (hr : 0 < r) {f : ℝ → ℝ} (hf : DifferentiableAt ℝ f (Real.log (SimilarityProfile.X h (radiusPoint t r z)))) (hfpos : 0 ≤ deriv f (Real.log (SimilarityProfile.X h (radiusPoint t r z)))) : 0 ≤ correction (heatAmplitude C (1 + h) t) (radialSlice (flattening h f) t z) r

theorem NavierStokes.TerminalStress.heatAmplitude_antitoneOn {C a t : ℝ} (hC : 0 < C) (ha : 1 < a) (ht : t < 1) : AntitoneOn (heatAmplitude C a t) (Set.Ioi 0)

theorem NavierStokes.TerminalStress.weighted_timeResidual {C h t r z : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) (hr : 0 < r) {f : ℝ → ℝ} (hf : DifferentiableAt ℝ f (Real.log (SimilarityProfile.X h (radiusPoint t r z)))) : r ^ 2 * timeResidual C h f t z r = r ^ 3 * heatAmplitude C (1 + h) t r / (2 * timeDenominator h t z) * deriv (radialSlice (flattening h f) t z) r

The actual logarithmic time term is a positive weight times ∂r f_o.

theorem NavierStokes.TerminalStress.timeResidual_lower_comparison {C h t r u R z : ℝ} (hC : 0 < C) (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) (hr : 0 < r) (hru : r ≤ u) (huR : u ≤ R) {f : ℝ → ℝ} (hf : DifferentiableAt ℝ f (Real.log (SimilarityProfile.X h (radiusPoint t u z)))) (hfpos : 0 ≤ deriv f (Real.log (SimilarityProfile.X h (radiusPoint t u z)))) : r ^ 3 * heatAmplitude C (1 + h) t R / (2 * timeDenominator h t z) * deriv (radialSlice (flattening h f) t z) u ≤ u ^ 2 * timeResidual C h f t z u

On a finite remaining radius interval, positivity and decreasing K give a concrete time-weight comparison for the mass lower bound.

noncomputable def NavierStokes.TerminalStress.terminalStress (C h : ℝ) (f : ℝ → ℝ) (t z r : ℝ) : ℝ

Terminal stress, given by backwardStress (fun u => leadingResidual C h f t u z) r.

Equations

• NavierStokes.TerminalStress.terminalStress C h f t z r = NavierStokes.TerminalStress.backwardStress (fun (u : ℝ) => NavierStokes.TerminalStress.leadingResidual C h f t u z) r

theorem NavierStokes.TerminalStress.flattening_radial_contDiffAt {h t r z : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) (hr : 0 < r) {f : ℝ → ℝ} (hf : ContDiff ℝ 2 f) : ContDiffAt ℝ 2 (radialSlice (flattening h f) t z) r

theorem NavierStokes.TerminalStress.terminalStress_formula (C : ℝ) {h t r z : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) (hr : 0 < r) {f : ℝ → ℝ} (hf : ContDiff ℝ 2 f) (hv : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * viscousResidual (heatAmplitude C (1 + h) t) (radialSlice (flattening h f) t z) u) (Set.Ioi r) MeasureTheory.volume) (hc : MeasureTheory.IntegrableOn (correction (heatAmplitude C (1 + h) t) (radialSlice (flattening h f) t z)) (Set.Ioi r) MeasureTheory.volume) (hT : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * timeResidual C h f t z u) (Set.Ioi r) MeasureTheory.volume) (hb : Filter.Tendsto (boundary (heatAmplitude C (1 + h) t) (radialSlice (flattening h f) t z)) Filter.atTop (nhds 0)) : terminalStress C h f t z r = heatAmplitude C (1 + h) t r * deriv (radialSlice (flattening h f) t z) r + ((∫ (u : ℝ) in Set.Ioi r, u ^ 2 * timeResidual C h f t z u) + ∫ (u : ℝ) in Set.Ioi r, correction (heatAmplitude C (1 + h) t) (radialSlice (flattening h f) t z) u) / r ^ 2

Backward formula instantiated with the actual heat carrier and actual logarithmic flattening factor. The integrability and boundary conditions are ordinary conditions on these functions, not assumed stress identities.

theorem NavierStokes.TerminalStress.terminalStress_ge_boundary {C h t r z : ℝ} (hC : 0 < C) (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) (hr : 0 < r) {f : ℝ → ℝ} (hf : ContDiff ℝ 2 f) (hmono : ∀ (y : ℝ), 0 ≤ deriv f y) (hv : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * viscousResidual (heatAmplitude C (1 + h) t) (radialSlice (flattening h f) t z) u) (Set.Ioi r) MeasureTheory.volume) (hc : MeasureTheory.IntegrableOn (correction (heatAmplitude C (1 + h) t) (radialSlice (flattening h f) t z)) (Set.Ioi r) MeasureTheory.volume) (hT : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * timeResidual C h f t z u) (Set.Ioi r) MeasureTheory.volume) (hb : Filter.Tendsto (boundary (heatAmplitude C (1 + h) t) (radialSlice (flattening h f) t z)) Filter.atTop (nhds 0)) : heatAmplitude C (1 + h) t r * deriv (radialSlice (flattening h f) t z) r ≤ terminalStress C h f t z r

theorem NavierStokes.TerminalStress.terminalStress_nonneg {C h t r z : ℝ} (hC : 0 < C) (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) (hr : 0 < r) {f : ℝ → ℝ} (hf : ContDiff ℝ 2 f) (hmono : ∀ (y : ℝ), 0 ≤ deriv f y) (hv : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * viscousResidual (heatAmplitude C (1 + h) t) (radialSlice (flattening h f) t z) u) (Set.Ioi r) MeasureTheory.volume) (hc : MeasureTheory.IntegrableOn (correction (heatAmplitude C (1 + h) t) (radialSlice (flattening h f) t z)) (Set.Ioi r) MeasureTheory.volume) (hT : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * timeResidual C h f t z u) (Set.Ioi r) MeasureTheory.volume) (hb : Filter.Tendsto (boundary (heatAmplitude C (1 + h) t) (radialSlice (flattening h f) t z)) Filter.atTop (nhds 0)) : 0 ≤ terminalStress C h f t z r

theorem NavierStokes.TerminalStress.deriv_eventually_zero_of_eventually_const {g : ℝ → ℝ} {c : ℝ} (hg : g =ᶠ[Filter.atTop] fun (x : ℝ) => c) : deriv g =ᶠ[Filter.atTop] fun (x : ℝ) => 0

A plateau at infinity automatically removes the radial boundary term, irrespective of the behavior of the heat carrier there.

theorem NavierStokes.TerminalStress.boundary_tendsto_zero_of_plateau (K : ℝ → ℝ) {g : ℝ → ℝ} {c : ℝ} (hg : g =ᶠ[Filter.atTop] fun (x : ℝ) => c) : Filter.Tendsto (boundary K g) Filter.atTop (nhds 0)

theorem NavierStokes.TerminalStress.logX_radial_tendsto {h t z : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) : Filter.Tendsto (fun (r : ℝ) => Real.log (SimilarityProfile.X h (radiusPoint t r z))) Filter.atTop Filter.atTop

theorem NavierStokes.TerminalStress.radial_flattening_plateau {h t z c : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) {f : ℝ → ℝ} (hf : f =ᶠ[Filter.atTop] fun (x : ℝ) => c) : radialSlice (flattening h f) t z =ᶠ[Filter.atTop] fun (x : ℝ) => c

theorem NavierStokes.TerminalStress.outgoing_boundary_tendsto_zero (d : OutgoingTail.TailData) (C y₀ : ℝ) {t z : ℝ} (ht : t < 1) : Filter.Tendsto (boundary (heatAmplitude C (1 + d.h) t) (radialSlice (flattening d.h fun (y : ℝ) => OutgoingTail.tailShape d (y - y₀)) t z)) Filter.atTop (nhds 0)

In particular, the actual outgoing taper gives the zero boundary at infinity.

The actual terminal taper and its Gaussian edge

theorem NavierStokes.TerminalStress.edge_half (δ : ℝ) : FlatCutoff.edge 1 (δ / 2) = FlatCutoff.edge 4 δ

noncomputable def NavierStokes.TerminalStress.taperDenominator (δ : ℝ) : ℝ

Taper denominator, given by FlatCutoff.edge 1 (1 - δ / 2) + FlatCutoff.edge 4 δ.

Equations

• NavierStokes.TerminalStress.taperDenominator δ = NavierStokes.FlatCutoff.edge 1 (1 - δ / 2) + NavierStokes.FlatCutoff.edge 4 δ

theorem NavierStokes.TerminalStress.taperDenominator_pos (δ : ℝ) : 0 < taperDenominator δ

theorem NavierStokes.TerminalStress.taperDenominator_contDiff : ContDiff ℝ (↑⊤) taperDenominator

noncomputable def NavierStokes.TerminalStress.taperFactor (δ : ℝ) : ℝ

Taper factor, given by (taperDenominator δ)⁻¹.

Equations

• NavierStokes.TerminalStress.taperFactor δ = (NavierStokes.TerminalStress.taperDenominator δ)⁻¹

theorem NavierStokes.TerminalStress.taperFactor_contDiff : ContDiff ℝ (↑⊤) taperFactor

theorem NavierStokes.TerminalStress.taperFactor_pos (δ : ℝ) : 0 < taperFactor δ

theorem NavierStokes.TerminalStress.tailShape_deficit (d : OutgoingTail.TailData) (δ : ℝ) : 1 - OutgoingTail.tailShape d (3 - δ) = d.rho * FlatCutoff.edge 4 δ * taperFactor δ

The actual outgoing taper has the precise exp(-4/δ²) deficit.

noncomputable def NavierStokes.TerminalStress.taperSlopeFactor (d : OutgoingTail.TailData) (δ : ℝ) : ℝ

Taper slope factor, given by d.rho * (8 * taperFactor δ + δ ^ 3 * deriv taperFactor δ).

Equations

• NavierStokes.TerminalStress.taperSlopeFactor d δ = d.rho * (8 * NavierStokes.TerminalStress.taperFactor δ + δ ^ 3 * deriv NavierStokes.TerminalStress.taperFactor δ)

theorem NavierStokes.TerminalStress.taperSlopeFactor_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (taperSlopeFactor d)

theorem NavierStokes.TerminalStress.taperSlopeFactor_zero_pos (d : OutgoingTail.TailData) : 0 < taperSlopeFactor d 0

theorem NavierStokes.TerminalStress.tailShapeDeriv_factorization (d : OutgoingTail.TailData) (δ : ℝ) : OutgoingTail.tailShapeDeriv d (3 - δ) = FlatCutoff.edge 4 δ / δ ^ 3 * taperSlopeFactor d δ

The actual taper derivative has a smooth positive limiting coefficient after division by the edge factor exp(-4/δ²) δ⁻³.

noncomputable def NavierStokes.TerminalStress.edgeStress {E : Type u_1} (c : ℝ) (b a : E × ℝ → ℝ) (y : E × ℝ) : ℝ

The boundary term and actual backward integrals after the edge change of variables.

Equations

• NavierStokes.TerminalStress.edgeStress c b a y = NavierStokes.FlatCutoff.edge c y.2 / y.2 ^ 3 * b y + NavierStokes.ParametricFlatFactor.primitive c 3 a y

noncomputable def NavierStokes.TerminalStress.normalizedEdgeStress {E : Type u_1} (c : ℝ) (b a : E × ℝ → ℝ) (y : E × ℝ) : ℝ

Normalized edge stress, given by b y + y.2 ^ 3 * ParametricFlatFactor.factor c 3 a y.

Equations

• NavierStokes.TerminalStress.normalizedEdgeStress c b a y = b y + y.2 ^ 3 * NavierStokes.ParametricFlatFactor.factor c 3 a y

theorem NavierStokes.TerminalStress.edgeStress_factorization {E : Type u_1} (c : ℝ) (b a : E × ℝ → ℝ) (y : E × ℝ) : edgeStress c b a y = FlatCutoff.edge c y.2 / y.2 ^ 3 * normalizedEdgeStress c b a y

Actual integral factorization, including auxiliary parameters.

theorem NavierStokes.TerminalStress.normalizedEdgeStress_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {c : ℝ} (hc : 0 < c) {b a : E × ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (ha : ContDiff ℝ (↑⊤) a) : ContDiff ℝ (↑⊤) (normalizedEdgeStress c b a)

theorem NavierStokes.TerminalStress.normalizedEdgeStress_zero {E : Type u_1} (c : ℝ) (b a : E × ℝ → ℝ) (p : E) : normalizedEdgeStress c b a (p, 0) = b (p, 0)

theorem NavierStokes.TerminalStress.normalizedEdgeStress_eventually_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {c : ℝ} (hc : 0 < c) {b a : E × ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (ha : ContDiff ℝ (↑⊤) a) (p : E) (hbp : 0 < b (p, 0)) : ∀ᶠ (y : E × ℝ) in nhds (p, 0), 0 < normalizedEdgeStress c b a y