Canonical pressure of the physical terminal heat tail

The heat parameter is the physical time 1-t. The pressure is the actual improper radial integral. Its regularity is obtained by separating the pure heat tail from a compact taper correction.

noncomputable def NavierStokes.TerminalPressure.amplitudeExponent (h : ℝ) : ℝ

The exponent of the physical angular heat amplitude.

Equations

• NavierStokes.TerminalPressure.amplitudeExponent h = 1 / 2 + h

noncomputable def NavierStokes.TerminalPressure.heatJet (h : ℝ) (n : ℕ) (ν v : ℝ) : ℝ

Derivatives with respect to the actual scaled heat parameter.

Equations

• NavierStokes.TerminalPressure.heatJet h n ν v = (2 / v) ^ n * NavierStokes.RadialHeatProfile.profileJet (1 + h) n (2 * ν / v)

noncomputable def NavierStokes.TerminalPressure.heatJetBound (h : ℝ) (n : ℕ) : ℝ

Heat jet bound, given by 2 ^ n * ParametricHeatTail.heatJetBound h n.

Equations

• NavierStokes.TerminalPressure.heatJetBound h n = 2 ^ n * NavierStokes.ParametricHeatTail.heatJetBound h n

noncomputable def NavierStokes.TerminalPressure.pressureWeight (h v : ℝ) : ℝ

Pressure weight, given by v ^ (-2 * amplitudeExponent h - 1).

Equations

• NavierStokes.TerminalPressure.pressureWeight h v = v ^ (-2 * NavierStokes.TerminalPressure.amplitudeExponent h - 1)

noncomputable def NavierStokes.TerminalPressure.heatPressureJet (h : ℝ) (n : ℕ) (ν v : ℝ) : ℝ

Heat pressure jet, given by pressureWeight h v * ParametricHeatTail.jetProduct (fun i => heatJet h i ν v) (fun i => heatJet h i ν v) n.

Equations

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

noncomputable def NavierStokes.TerminalPressure.heatPressureFactor (h ν : ℝ) : ℝ

Dimensionless pure-heat pressure integral, including the zero-diffusion endpoint.

Equations

• NavierStokes.TerminalPressure.heatPressureFactor h ν = ∫ (v : ℝ) in Set.Ioi 1, NavierStokes.TerminalPressure.pressureWeight h v * NavierStokes.RadialHeatProfile.profile (1 + h) (2 * ν / v) ^ 2

theorem NavierStokes.TerminalPressure.heatJet_zero (h ν v : ℝ) : heatJet h 0 ν v = RadialHeatProfile.profile (1 + h) (2 * ν / v)

theorem NavierStokes.TerminalPressure.heatJet_hasDerivWithinAt {h ν v : ℝ} (hh : 0 < h) (hv : 0 < v) (hν : 0 ≤ ν) (n : ℕ) : HasDerivWithinAt (fun (u : ℝ) => heatJet h n u v) (heatJet h (n + 1) ν v) (Set.Ici 0) ν

theorem NavierStokes.TerminalPressure.heatJet_continuousOn {h ν : ℝ} (hh : 0 < h) (hν : 0 ≤ ν) (n : ℕ) : ContinuousOn (heatJet h n ν) (Set.Ioi 0)

theorem NavierStokes.TerminalPressure.heatJetBound_nonneg {h : ℝ} (hh : 0 < h) (n : ℕ) : 0 ≤ heatJetBound h n

theorem NavierStokes.TerminalPressure.heatJet_bound {h ν v : ℝ} (hh : 0 < h) (hν : 0 ≤ ν) (hv : 1 ≤ v) (n : ℕ) : |heatJet h n ν v| ≤ heatJetBound h n

theorem NavierStokes.TerminalPressure.pressureWeight_continuousOn (h : ℝ) : ContinuousOn (pressureWeight h) (Set.Ioi 0)

theorem NavierStokes.TerminalPressure.heatPressureJet_continuousOn {h ν : ℝ} (hh : 0 < h) (hν : 0 ≤ ν) (n : ℕ) : ContinuousOn (heatPressureJet h n ν) (Set.Ioi 0)

theorem NavierStokes.TerminalPressure.heatPressureJet_hasDerivWithinAt {h ν v : ℝ} (hh : 0 < h) (hv : 0 < v) (hν : 0 ≤ ν) (n : ℕ) : HasDerivWithinAt (fun (u : ℝ) => heatPressureJet h n u v) (heatPressureJet h (n + 1) ν v) (Set.Ici 0) ν

theorem NavierStokes.TerminalPressure.heatPressureJet_dominated {h : ℝ} (hh : 0 < h) : ParametricHeatTail.ChainDominated (heatPressureJet h) (MeasureTheory.volume.restrict (Set.Ioi 1))

theorem NavierStokes.TerminalPressure.heatPressureJet_measurable {h : ℝ} (hh : 0 < h) (n : ℕ) {ν : ℝ} (hν : 0 ≤ ν) : MeasureTheory.AEStronglyMeasurable (heatPressureJet h n ν) (MeasureTheory.volume.restrict (Set.Ioi 1))

theorem NavierStokes.TerminalPressure.heatPressureJet_zero (h ν v : ℝ) : heatPressureJet h 0 ν v = pressureWeight h v * RadialHeatProfile.profile (1 + h) (2 * ν / v) ^ 2

theorem NavierStokes.TerminalPressure.heatPressureFactor_contDiffOn {h : ℝ} (hh : 0 < h) : ContDiffOn ℝ (↑⊤) (heatPressureFactor h) (Set.Ici 0)

Every derivative of the heat-only improper integral is dominated by an integrable power, uniformly all the way to zero diffusion.

The compact taper correction

noncomputable def NavierStokes.TerminalPressure.heatDensity (h ν v : ℝ) : ℝ

Heat density, given by pressureWeight h v * RadialHeatProfile.profile (1 + h) (2 * ν / v) ^ 2.

Equations

• NavierStokes.TerminalPressure.heatDensity h ν v = NavierStokes.TerminalPressure.pressureWeight h v * NavierStokes.RadialHeatProfile.profile (1 + h) (2 * ν / v) ^ 2

noncomputable def NavierStokes.TerminalPressure.taperedDensity (h : ℝ) (f : ℝ → ℝ) (p : ℝ × ℝ) (v : ℝ) : ℝ

Tapered density, given by heatDensity h p.1 v * f (p.2 + Real.log v) ^ 2.

Equations

• NavierStokes.TerminalPressure.taperedDensity h f p v = NavierStokes.TerminalPressure.heatDensity h p.1 v * f (p.2 + Real.log v) ^ 2

noncomputable def NavierStokes.TerminalPressure.deficitDensity (h : ℝ) (f : ℝ → ℝ) (p : ℝ × ℝ) (v : ℝ) : ℝ

Deficit density, given by heatDensity h p.1 v * (1 - f (p.2 + Real.log v) ^ 2).

Equations

• NavierStokes.TerminalPressure.deficitDensity h f p v = NavierStokes.TerminalPressure.heatDensity h p.1 v * (1 - f (p.2 + Real.log v) ^ 2)

noncomputable def NavierStokes.TerminalPressure.taperedPressureFactor (h : ℝ) (f : ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Tapered pressure factor, given by ∫ v in Ioi (1 : ℝ), taperedDensity h f p v.

Equations

• NavierStokes.TerminalPressure.taperedPressureFactor h f p = ∫ (v : ℝ) in Set.Ioi 1, NavierStokes.TerminalPressure.taperedDensity h f p v

noncomputable def NavierStokes.TerminalPressure.compactDeficit (h : ℝ) (f : ℝ → ℝ) (B : ℝ) (p : ℝ × ℝ) : ℝ

Compact deficit, given by (B - 1) * ∫ u in (0 : ℝ)..1, deficitDensity h f p (1 + (B - 1) * u).

Equations

• NavierStokes.TerminalPressure.compactDeficit h f B p = (B - 1) * ∫ (u : ℝ) in 0..1, NavierStokes.TerminalPressure.deficitDensity h f p (1 + (B - 1) * u)

theorem NavierStokes.TerminalPressure.heatDensity_continuousOn {h ν : ℝ} (hh : 0 < h) (hν : 0 ≤ ν) : ContinuousOn (heatDensity h ν) (Set.Ioi 0)

theorem NavierStokes.TerminalPressure.heatDensity_bounds {h ν v : ℝ} (hh : 0 < h) (hν : 0 ≤ ν) (hv : 0 < v) : 0 ≤ heatDensity h ν v ∧ heatDensity h ν v ≤ pressureWeight h v

theorem NavierStokes.TerminalPressure.heatDensity_integrable {h ν : ℝ} (hh : 0 < h) (hν : 0 ≤ ν) : MeasureTheory.IntegrableOn (heatDensity h ν) (Set.Ioi 1) MeasureTheory.volume

theorem NavierStokes.TerminalPressure.taperedDensity_continuousOn {h ν y : ℝ} {f : ℝ → ℝ} (hh : 0 < h) (hν : 0 ≤ ν) (hf : Continuous f) : ContinuousOn (taperedDensity h f (ν, y)) (Set.Ioi 0)

theorem NavierStokes.TerminalPressure.taperedDensity_integrable {h ν y : ℝ} {f : ℝ → ℝ} (hh : 0 < h) (hν : 0 ≤ ν) (hf : Continuous f) (hb : ∀ (y : ℝ), 0 ≤ f y ∧ f y ≤ 1) : MeasureTheory.IntegrableOn (taperedDensity h f (ν, y)) (Set.Ioi 1) MeasureTheory.volume

theorem NavierStokes.TerminalPressure.deficitDensity_integrable {h ν y : ℝ} {f : ℝ → ℝ} (hh : 0 < h) (hν : 0 ≤ ν) (hf : Continuous f) (hb : ∀ (y : ℝ), 0 ≤ f y ∧ f y ≤ 1) : MeasureTheory.IntegrableOn (deficitDensity h f (ν, y)) (Set.Ioi 1) MeasureTheory.volume

theorem NavierStokes.TerminalPressure.compactDeficit_eq_interval (h B : ℝ) (f : ℝ → ℝ) (p : ℝ × ℝ) : compactDeficit h f B p = ∫ (v : ℝ) in 1..B, deficitDensity h f p v

theorem NavierStokes.TerminalPressure.integral_tail_eq_interval {g : ℝ → ℝ} {a B : ℝ} (hB : a ≤ B) (hg : ∀ (v : ℝ), B < v → g v = 0) : ∫ (v : ℝ) in Set.Ioi a, g v = ∫ (v : ℝ) in a..B, g v

theorem NavierStokes.TerminalPressure.deficitDensity_zero {h B Y : ℝ} {f : ℝ → ℝ} {p : ℝ × ℝ} (hB : 0 < B) (hy : Y ≤ p.2 + Real.log B) (hplateau : ∀ (y : ℝ), Y ≤ y → f y = 1) {v : ℝ} (hv : B < v) : deficitDensity h f p v = 0

theorem NavierStokes.TerminalPressure.taperedPressureFactor_eq {h B Y : ℝ} {f : ℝ → ℝ} {p : ℝ × ℝ} (hh : 0 < h) (hν : 0 ≤ p.1) (hf : Continuous f) (hb : ∀ (y : ℝ), 0 ≤ f y ∧ f y ≤ 1) (hB : 1 ≤ B) (hy : Y ≤ p.2 + Real.log B) (hplateau : ∀ (y : ℝ), Y ≤ y → f y = 1) : taperedPressureFactor h f p = heatPressureFactor h p.1 - compactDeficit h f B p

theorem NavierStokes.TerminalPressure.deficitDensity_contDiffAt {h : ℝ} {f : ℝ → ℝ} {p : ℝ × ℝ} {v : ℝ} (hh : 0 < h) (hf : ContDiff ℝ (↑⊤) f) (hν : 0 < p.1) (hv : 0 < v) : ContDiffAt ℝ (↑⊤) (fun (z : (ℝ × ℝ) × ℝ) => deficitDensity h f z.1 z.2) (p, v)

theorem NavierStokes.TerminalPressure.compactDeficit_integrand_smooth {h B : ℝ} {f : ℝ → ℝ} (hh : 0 < h) (hf : ContDiff ℝ (↑⊤) f) (hB : 1 ≤ B) (p : ℝ × ℝ) (hν : 0 < p.1) (u : ℝ) (hu : u ∈ Set.Icc 0 1) : ContDiffAt ℝ (↑⊤) (fun (z : (ℝ × ℝ) × ℝ) => deficitDensity h f z.1 (1 + (B - 1) * z.2)) (p, u)

theorem NavierStokes.TerminalPressure.compactDeficit_contDiffOn {h B : ℝ} {f : ℝ → ℝ} (hh : 0 < h) (hf : ContDiff ℝ (↑⊤) f) (hB : 1 ≤ B) : ContDiffOn ℝ (↑⊤) (compactDeficit h f B) {p : ℝ × ℝ | 0 < p.1}

theorem NavierStokes.TerminalPressure.taperedPressureFactor_contDiffAt {h Y : ℝ} {f : ℝ → ℝ} {p : ℝ × ℝ} (hh : 0 < h) (hf : ContDiff ℝ (↑⊤) f) (hb : ∀ (y : ℝ), 0 ≤ f y ∧ f y ≤ 1) (hplateau : ∀ (y : ℝ), Y ≤ y → f y = 1) (hν : 0 < p.1) : ContDiffAt ℝ (↑⊤) (taperedPressureFactor h f) p

Genuine joint smoothness of the tapered improper integral. Only the compact taper correction depends on the logarithmic radial coordinate.

Actual differentiation in the logarithmic radial parameter

noncomputable def NavierStokes.TerminalPressure.taperDerivativeDensity (h : ℝ) (f : ℝ → ℝ) (p : ℝ × ℝ) (v : ℝ) : ℝ

Taper derivative density, given by heatDensity h p.1 v * f (p.2 + Real.log v) * deriv f (p.2 + Real.log v).

Equations

• NavierStokes.TerminalPressure.taperDerivativeDensity h f p v = NavierStokes.TerminalPressure.heatDensity h p.1 v * f (p.2 + Real.log v) * deriv f (p.2 + Real.log v)

noncomputable def NavierStokes.TerminalPressure.taperDerivativeIntegral (h : ℝ) (f : ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Taper derivative integral, given by ∫ v in Ioi (1 : ℝ), taperDerivativeDensity h f p v.

Equations

• NavierStokes.TerminalPressure.taperDerivativeIntegral h f p = ∫ (v : ℝ) in Set.Ioi 1, NavierStokes.TerminalPressure.taperDerivativeDensity h f p v

theorem NavierStokes.TerminalPressure.parameterPartial_hasDerivAt {G : ℝ × ℝ → ℝ} {p : ℝ × ℝ} (hG : DifferentiableAt ℝ G p) : HasDerivAt (fun (y : ℝ) => G (p.1, y)) (ProfileHistories.parameterPartial G p) p.2

theorem NavierStokes.TerminalPressure.deficitDensity_hasDerivAt_y (h ν v y : ℝ) {f : ℝ → ℝ} (hf : DifferentiableAt ℝ f (y + Real.log v)) : HasDerivAt (fun (u : ℝ) => deficitDensity h f (ν, u) v) (-2 * taperDerivativeDensity h f (ν, y) v) y

theorem NavierStokes.TerminalPressure.deriv_zero_after_plateau {f : ℝ → ℝ} {Y y : ℝ} (hplateau : ∀ (x : ℝ), Y ≤ x → f x = 1) (hy : Y < y) : deriv f y = 0

theorem NavierStokes.TerminalPressure.taperDerivativeDensity_zero {h B Y : ℝ} {f : ℝ → ℝ} {p : ℝ × ℝ} (hB : 0 < B) (hy : Y ≤ p.2 + Real.log B) (hplateau : ∀ (y : ℝ), Y ≤ y → f y = 1) {v : ℝ} (hv : B < v) : taperDerivativeDensity h f p v = 0

theorem NavierStokes.TerminalPressure.compactDeficit_hasDerivAt_y {h B : ℝ} {f : ℝ → ℝ} {p : ℝ × ℝ} (hh : 0 < h) (hf : ContDiff ℝ (↑⊤) f) (hB : 1 ≤ B) (hν : 0 < p.1) : HasDerivAt (fun (y : ℝ) => compactDeficit h f B (p.1, y)) (-2 * (B - 1) * ∫ (u : ℝ) in 0..1, taperDerivativeDensity h f p (1 + (B - 1) * u)) p.2

theorem NavierStokes.TerminalPressure.taperedPressureFactor_hasDerivAt_y {h Y : ℝ} {f : ℝ → ℝ} {p : ℝ × ℝ} (hh : 0 < h) (hf : ContDiff ℝ (↑⊤) f) (hb : ∀ (y : ℝ), 0 ≤ f y ∧ f y ≤ 1) (hplateau : ∀ (y : ℝ), Y ≤ y → f y = 1) (hν : 0 < p.1) : HasDerivAt (fun (y : ℝ) => taperedPressureFactor h f (p.1, y)) (2 * taperDerivativeIntegral h f p) p.2

The derivative is obtained from the defining improper integral; the derivative integrand is compactly supported by the actual taper plateau.

Identification with the physical canonical pressure

noncomputable def NavierStokes.TerminalPressure.pressureCoordinates (h : ℝ) (p : SimilarityProfile.PhysicalPoint) : ℝ × ℝ

Pressure coordinates, given by ((1 - p.1) / p.2.1, Real.log (SimilarityProfile.X h p)).

Equations

• NavierStokes.TerminalPressure.pressureCoordinates h p = ((1 - p.1) / p.2.1, Real.log (NavierStokes.SimilarityProfile.X h p))

theorem NavierStokes.TerminalPressure.swirlCoefficient_sq (C h : ℝ) (f : ℝ → ℝ) {p : SimilarityProfile.PhysicalPoint} (hs : 0 < p.2.1) : TerminalStress.swirlCoefficient C h f p ^ 2 = C ^ 2 / 2 * p.2.1 ^ (-2 * amplitudeExponent h - 1) * RadialHeatProfile.profile (1 + h) (2 * (1 - p.1) / p.2.1) ^ 2 * f (Real.log (SimilarityProfile.X h p)) ^ 2

theorem NavierStokes.TerminalPressure.swirlCoefficient_sq_scaled (C : ℝ) {h : ℝ} (f : ℝ → ℝ) {p : SimilarityProfile.PhysicalPoint} (hq : 0 < SimilarityProfile.q h p) (hs : 0 < p.2.1) {v : ℝ} (hv : 0 < v) : TerminalStress.swirlCoefficient C h f (p.1, p.2.1 * v, p.2.2) ^ 2 = C ^ 2 / 2 * p.2.1 ^ (-2 * amplitudeExponent h - 1) * taperedDensity h f (pressureCoordinates h p) v

theorem NavierStokes.TerminalPressure.swirlCoefficient_sq_integrable (C : ℝ) {h : ℝ} {f : ℝ → ℝ} {p : SimilarityProfile.PhysicalPoint} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : p.1 < 1) (hs : 0 < p.2.1) (hf : Continuous f) (hb : ∀ (y : ℝ), 0 ≤ f y ∧ f y ≤ 1) : MeasureTheory.IntegrableOn (fun (s : ℝ) => TerminalStress.swirlCoefficient C h f (p.1, s, p.2.2) ^ 2) (Set.Ioi p.2.1) MeasureTheory.volume

theorem NavierStokes.TerminalPressure.canonicalPressure_eq (C : ℝ) {h : ℝ} (f : ℝ → ℝ) {p : SimilarityProfile.PhysicalPoint} (hq : 0 < SimilarityProfile.q h p) (hs : 0 < p.2.1) : TerminalStress.canonicalPressure (TerminalStress.swirlCoefficient C h f) p = -(C ^ 2 / 2) * p.2.1 ^ (-2 * amplitudeExponent h) * taperedPressureFactor h f (pressureCoordinates h p)

Scaling is performed in the physical radial integral. In particular the argument of the heat profile is 2(1-t)/s, rather than a fixed diffusion parameter.

theorem NavierStokes.TerminalPressure.pressureCoordinates_contDiffAt {h : ℝ} {p : SimilarityProfile.PhysicalPoint} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : p.1 < 1) (hs : 0 < p.2.1) : ContDiffAt ℝ (↑⊤) (pressureCoordinates h) p

theorem NavierStokes.TerminalPressure.canonicalPressure_contDiffAt (C : ℝ) {h Y : ℝ} {f : ℝ → ℝ} {p : SimilarityProfile.PhysicalPoint} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : p.1 < 1) (hs : 0 < p.2.1) (hf : ContDiff ℝ (↑⊤) f) (hb : ∀ (y : ℝ), 0 ≤ f y ∧ f y ≤ 1) (hplateau : ∀ (y : ℝ), Y ≤ y → f y = 1) : ContDiffAt ℝ (↑⊤) (TerminalStress.canonicalPressure (TerminalStress.swirlCoefficient C h f)) p

The actual canonical pressure is jointly smooth throughout the presingular, positive-radius domain. No differentiability of the pressure is an input.

The axial derivative of the physical pressure

noncomputable def NavierStokes.TerminalPressure.logScaleDerivative (h : ℝ) (p : SimilarityProfile.PhysicalPoint) : ℝ

Log scale derivative, given by CoordinateAlgebra.qAxial (SimilarityProfile.q h p) h (SimilarityProfile.eta h p) / SimilarityProfile.q h p.

Equations

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

theorem NavierStokes.TerminalPressure.logX_hasDerivAt_z {h : ℝ} {p : SimilarityProfile.PhysicalPoint} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : p.1 < 1) (hs : 0 < p.2.1) : HasDerivAt (fun (z : ℝ) => Real.log (SimilarityProfile.X h (p.1, p.2.1, z))) (-logScaleDerivative h p) p.2.2

theorem NavierStokes.TerminalPressure.physicalHeat_sq_div (C h : ℝ) {p : SimilarityProfile.PhysicalPoint} (hs : 0 < p.2.1) : TerminalStress.physicalHeat C (1 + h) p ^ 2 / p.2.1 = C ^ 2 * p.2.1 ^ (-2 * amplitudeExponent h - 1) * RadialHeatProfile.profile (1 + h) (2 * (1 - p.1) / p.2.1) ^ 2

noncomputable def NavierStokes.TerminalPressure.axialPressureIntegral (C h : ℝ) (f : ℝ → ℝ) (p : SimilarityProfile.PhysicalPoint) : ℝ

Axial pressure integral as an element of ℝ.

Equations

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

theorem NavierStokes.TerminalPressure.axialPressureIntegral_eq (C : ℝ) {h : ℝ} (f : ℝ → ℝ) {p : SimilarityProfile.PhysicalPoint} (hq : 0 < SimilarityProfile.q h p) (hs : 0 < p.2.1) : axialPressureIntegral C h f p = C ^ 2 * p.2.1 ^ (-2 * amplitudeExponent h) * taperDerivativeIntegral h f (pressureCoordinates h p)

theorem NavierStokes.TerminalPressure.canonicalPressure_hasDerivAt_z (C : ℝ) {h Y : ℝ} {f : ℝ → ℝ} {p : SimilarityProfile.PhysicalPoint} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : p.1 < 1) (hs : 0 < p.2.1) (hf : ContDiff ℝ (↑⊤) f) (hb : ∀ (y : ℝ), 0 ≤ f y ∧ f y ≤ 1) (hplateau : ∀ (y : ℝ), Y ≤ y → f y = 1) : HasDerivAt (fun (z : ℝ) => TerminalStress.canonicalPressure (TerminalStress.swirlCoefficient C h f) (p.1, p.2.1, z)) (logScaleDerivative h p * axialPressureIntegral C h f p) p.2.2

theorem NavierStokes.TerminalPressure.canonicalPressure_partialZ (C : ℝ) {h Y : ℝ} {f : ℝ → ℝ} {p : SimilarityProfile.PhysicalPoint} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : p.1 < 1) (hs : 0 < p.2.1) (hf : ContDiff ℝ (↑⊤) f) (hb : ∀ (y : ℝ), 0 ≤ f y ∧ f y ≤ 1) (hplateau : ∀ (y : ℝ), Y ≤ y → f y = 1) : SimilarityProfile.partialZ (TerminalStress.canonicalPressure (TerminalStress.swirlCoefficient C h f)) p = logScaleDerivative h p * axialPressureIntegral C h f p

Exact axial derivative of the canonical pressure, including the dependence of the heat profile on the physical time and of the taper on q(t,z).

Quantitative pressure estimates from monotonicity of the heat carrier

theorem NavierStokes.TerminalPressure.spatialHeat_antitoneOn {h ν : ℝ} (hh : 0 < h) (hν : 0 < ν) : AntitoneOn (RadialHeatProfile.spatialProfile (1 + h) ν) (Set.Ioi 0)

theorem NavierStokes.TerminalPressure.heatDensity_eq_profileSq (h ν : ℝ) {v : ℝ} (hv : 0 < v) : heatDensity h ν v = RadialHeatProfile.spatialProfile (1 + h) ν v ^ 2 / v

theorem NavierStokes.TerminalPressure.taperDerivativeDensity_continuousOn {h ν y : ℝ} {f : ℝ → ℝ} (hh : 0 < h) (hν : 0 ≤ ν) (hf : ContDiff ℝ (↑⊤) f) : ContinuousOn (taperDerivativeDensity h f (ν, y)) (Set.Ioi 0)

theorem NavierStokes.TerminalPressure.taperDerivativeIntegral_bound {h Y : ℝ} {f : ℝ → ℝ} {p : ℝ × ℝ} (hh : 0 < h) (hf : ContDiff ℝ (↑⊤) f) (hb : ∀ (y : ℝ), 0 ≤ f y ∧ f y ≤ 1) (hmono : ∀ (y : ℝ), 0 ≤ deriv f y) (hplateau : ∀ (y : ℝ), Y ≤ y → f y = 1) (hν : 0 < p.1) : 0 ≤ taperDerivativeIntegral h f p ∧ taperDerivativeIntegral h f p ≤ RadialHeatProfile.profile (1 + h) (2 * p.1) ^ 2 * (1 - f p.2)

theorem NavierStokes.TerminalPressure.physicalHeat_sq (C h : ℝ) {p : SimilarityProfile.PhysicalPoint} (hs : 0 < p.2.1) : TerminalStress.physicalHeat C (1 + h) p ^ 2 = C ^ 2 * p.2.1 ^ (-2 * amplitudeExponent h) * RadialHeatProfile.profile (1 + h) (2 * (1 - p.1) / p.2.1) ^ 2

theorem NavierStokes.TerminalPressure.axialPressureIntegral_bound (C : ℝ) {h Y : ℝ} {f : ℝ → ℝ} {p : SimilarityProfile.PhysicalPoint} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : p.1 < 1) (hs : 0 < p.2.1) (hf : ContDiff ℝ (↑⊤) f) (hb : ∀ (y : ℝ), 0 ≤ f y ∧ f y ≤ 1) (hmono : ∀ (y : ℝ), 0 ≤ deriv f y) (hplateau : ∀ (y : ℝ), Y ≤ y → f y = 1) : 0 ≤ axialPressureIntegral C h f p ∧ axialPressureIntegral C h f p ≤ TerminalStress.physicalHeat C (1 + h) p ^ 2 * (1 - f (Real.log (SimilarityProfile.X h p)))

theorem NavierStokes.TerminalPressure.canonicalPressure_partialZ_bound (C : ℝ) {h Y : ℝ} {f : ℝ → ℝ} {p : SimilarityProfile.PhysicalPoint} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : p.1 < 1) (hs : 0 < p.2.1) (hf : ContDiff ℝ (↑⊤) f) (hb : ∀ (y : ℝ), 0 ≤ f y ∧ f y ≤ 1) (hmono : ∀ (y : ℝ), 0 ≤ deriv f y) (hplateau : ∀ (y : ℝ), Y ≤ y → f y = 1) : |SimilarityProfile.partialZ (TerminalStress.canonicalPressure (TerminalStress.swirlCoefficient C h f)) p| ≤ |logScaleDerivative h p| * TerminalStress.physicalHeat C (1 + h) p ^ 2 * (1 - f (Real.log (SimilarityProfile.X h p)))

theorem NavierStokes.TerminalPressure.logScaleDerivative_eq {h : ℝ} {p : SimilarityProfile.PhysicalPoint} (hq : 0 < SimilarityProfile.q h p) : logScaleDerivative h p = 2 * SimilarityProfile.eta h p / (SimilarityProfile.q h p ^ CoordinateAlgebra.D h * CoordinateAlgebra.L h (SimilarityProfile.eta h p))

theorem NavierStokes.TerminalPressure.logScaleDerivative_bound {h : ℝ} {p : SimilarityProfile.PhysicalPoint} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : p.1 < 1) : |logScaleDerivative h p| ≤ 2 / (1 - 2 * h) * SimilarityProfile.q h p ^ (-CoordinateAlgebra.D h)

The actual outgoing taper and its terminal edge estimate

noncomputable def NavierStokes.TerminalPressure.outgoingTaper (d : OutgoingTail.TailData) (y0 y : ℝ) : ℝ

Outgoing taper, given by OutgoingTail.tailShape d (y - y0).

Equations

• NavierStokes.TerminalPressure.outgoingTaper d y0 y = NavierStokes.OutgoingTail.tailShape d (y - y0)

theorem NavierStokes.TerminalPressure.outgoingTaper_contDiff (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (outgoingTaper d y0)

theorem NavierStokes.TerminalPressure.outgoingTaper_deriv (d : OutgoingTail.TailData) (y0 y : ℝ) : deriv (outgoingTaper d y0) y = OutgoingTail.tailShapeDeriv d (y - y0)

theorem NavierStokes.TerminalPressure.outgoingTaper_bounds (d : OutgoingTail.TailData) (y0 y : ℝ) : 0 ≤ outgoingTaper d y0 y ∧ outgoingTaper d y0 y ≤ 1

theorem NavierStokes.TerminalPressure.outgoingTaper_deriv_nonneg (d : OutgoingTail.TailData) (y0 y : ℝ) : 0 ≤ deriv (outgoingTaper d y0) y

theorem NavierStokes.TerminalPressure.outgoingTaper_plateau (d : OutgoingTail.TailData) (y0 y : ℝ) (hy : y0 + 3 ≤ y) : outgoingTaper d y0 y = 1

noncomputable def NavierStokes.TerminalPressure.outgoingPressure (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : SimilarityProfile.PhysicalProfile

Outgoing pressure, given by TerminalStress.canonicalPressure (TerminalStress.swirlCoefficient C d.h (outgoingTaper d y0)).

Equations

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

theorem NavierStokes.TerminalPressure.outgoingPressure_contDiffAt (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) : ContDiffAt ℝ (↑⊤) (outgoingPressure C d y0) p

theorem NavierStokes.TerminalPressure.outgoingPressure_partialZ (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) : SimilarityProfile.partialZ (outgoingPressure C d y0) p = logScaleDerivative d.h p * ∫ (s : ℝ) in Set.Ioi p.2.1, TerminalStress.physicalHeat C (1 + d.h) (p.1, s, p.2.2) ^ 2 * OutgoingTail.tailShape d (Real.log (s / SimilarityProfile.q d.h p) - y0) * OutgoingTail.tailShapeDeriv d (Real.log (s / SimilarityProfile.q d.h p) - y0) / s

Fully expanded formula for the actual pressure derivative needed in the terminal edge chart. The integration coordinate is the physical s=r^2/2.

theorem NavierStokes.TerminalPressure.outgoingPressure_partialZ_bound (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) : |SimilarityProfile.partialZ (outgoingPressure C d y0) p| ≤ 2 / (1 - 2 * d.h) * SimilarityProfile.q d.h p ^ (-CoordinateAlgebra.D d.h) * TerminalStress.physicalHeat C (1 + d.h) p ^ 2 * (1 - OutgoingTail.tailShape d (Real.log (SimilarityProfile.X d.h p) - y0))

theorem NavierStokes.TerminalPressure.outgoingPressure_edge_bound (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) {p : SimilarityProfile.PhysicalPoint} {δ : ℝ} (ht : p.1 < 1) (hs : 0 < p.2.1) (hδ : Real.log (SimilarityProfile.X d.h p) = y0 + 3 - δ) : |SimilarityProfile.partialZ (outgoingPressure C d y0) p| ≤ 2 / (1 - 2 * d.h) * SimilarityProfile.q d.h p ^ (-CoordinateAlgebra.D d.h) * TerminalStress.physicalHeat C (1 + d.h) p ^ 2 * (d.rho * FlatCutoff.edge 4 δ * TerminalStress.taperFactor δ)

Compact support of the terminal forcing and its positive mass

theorem NavierStokes.TerminalPressure.integrableOn_Ioi_of_eventually_zero {g : ℝ → ℝ} {r : ℝ} (hr : 0 < r) (hg : ContinuousOn g (Set.Ioi 0)) (hz : g =ᶠ[Filter.atTop] fun (x : ℝ) => 0) : MeasureTheory.IntegrableOn g (Set.Ioi r) MeasureTheory.volume

theorem NavierStokes.TerminalPressure.logX_radial_contDiffAt {h t z r : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) (hr : 0 < r) : ContDiffAt ℝ (↑⊤) (fun (u : ℝ) => Real.log (SimilarityProfile.X h (TerminalStress.radiusPoint t u z))) r

theorem NavierStokes.TerminalPressure.terminal_forcing_integrable (C : ℝ) {h t z r Y : ℝ} {f : ℝ → ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) (hr : 0 < r) (hf : ContDiff ℝ (↑⊤) f) (hplateau : ∀ (y : ℝ), Y ≤ y → f y = 1) : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * TerminalStress.viscousResidual (TerminalStress.heatAmplitude C (1 + h) t) (TerminalStress.radialSlice (TerminalStress.flattening h f) t z) u) (Set.Ioi r) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (TerminalStress.correction (TerminalStress.heatAmplitude C (1 + h) t) (TerminalStress.radialSlice (TerminalStress.flattening h f) t z)) (Set.Ioi r) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * TerminalStress.timeResidual C h f t z u) (Set.Ioi r) MeasureTheory.volume

theorem NavierStokes.TerminalPressure.logX_radial_strict {h t z r R : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) (hr : 0 < r) (hrR : r < R) : Real.log (SimilarityProfile.X h (TerminalStress.radiusPoint t r z)) < Real.log (SimilarityProfile.X h (TerminalStress.radiusPoint t R z))

theorem NavierStokes.TerminalPressure.terminalStress_ge_mass {C h t z r R Y : ℝ} {f : ℝ → ℝ} (hC : 0 < C) (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) (hr : 0 < r) (hrR : r ≤ R) (hf : ContDiff ℝ (↑⊤) f) (hmono : ∀ (y : ℝ), 0 ≤ deriv f y) (hplateau : ∀ (y : ℝ), Y ≤ y → f y = 1) (hR : Y ≤ Real.log (SimilarityProfile.X h (TerminalStress.radiusPoint t R z))) : r * TerminalStress.heatAmplitude C (1 + h) t R / (2 * TerminalStress.timeDenominator h t z) * (1 - f (Real.log (SimilarityProfile.X h (TerminalStress.radiusPoint t r z)))) ≤ TerminalStress.terminalStress C h f t z r

A positive lower bound for the actual backward angular stress. Every tail integrability hypothesis is discharged using the taper's genuine plateau.

The genuine backward axial pressure stress

theorem NavierStokes.TerminalPressure.canonicalPressure_partialZ_contDiffAt (C : ℝ) {h Y : ℝ} {f : ℝ → ℝ} {p : SimilarityProfile.PhysicalPoint} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : p.1 < 1) (hs : 0 < p.2.1) (hf : ContDiff ℝ (↑⊤) f) (hb : ∀ (y : ℝ), 0 ≤ f y ∧ f y ≤ 1) (hplateau : ∀ (y : ℝ), Y ≤ y → f y = 1) : ContDiffAt ℝ (↑⊤) (SimilarityProfile.partialZ (TerminalStress.canonicalPressure (TerminalStress.swirlCoefficient C h f))) p

noncomputable def NavierStokes.TerminalPressure.axialBackwardStress (C h : ℝ) (f : ℝ → ℝ) (t z r : ℝ) : ℝ

Since ds = r dr, this is the cylindrical backward primitive with weight r. It uses the actual axial derivative of the canonical pressure.

Equations

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

theorem NavierStokes.TerminalPressure.physicalHeat_pos {C h : ℝ} {p : SimilarityProfile.PhysicalPoint} (hC : 0 < C) (hh : 0 < h) (ht : p.1 < 1) (hs : 0 < p.2.1) : 0 < TerminalStress.physicalHeat C (1 + h) p

theorem NavierStokes.TerminalPressure.physicalHeat_radial_le {C h t z a s : ℝ} (hC : 0 < C) (hh : 0 < h) (ht : t < 1) (ha : 0 < a) (has : a ≤ s) : TerminalStress.physicalHeat C (1 + h) (t, s, z) ≤ TerminalStress.physicalHeat C (1 + h) (t, a, z)

theorem NavierStokes.TerminalPressure.axialBackwardStress_bound {C h t z r R Y : ℝ} {f : ℝ → ℝ} (hC : 0 < C) (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) (hr : 0 < r) (hrR : r ≤ R) (hf : ContDiff ℝ (↑⊤) f) (hb : ∀ (y : ℝ), 0 ≤ f y ∧ f y ≤ 1) (hmono : ∀ (y : ℝ), 0 ≤ deriv f y) (hplateau : ∀ (y : ℝ), Y ≤ y → f y = 1) (hR : Y ≤ Real.log (SimilarityProfile.X h (TerminalStress.radiusPoint t R z))) : MeasureTheory.IntegrableOn (fun (s : ℝ) => SimilarityProfile.partialZ (TerminalStress.canonicalPressure (TerminalStress.swirlCoefficient C h f)) (t, s, z)) (Set.Ioi (r ^ 2 / 2)) MeasureTheory.volume ∧ |axialBackwardStress C h f t z r| ≤ (R ^ 2 - r ^ 2) / (2 * r) * |logScaleDerivative h (TerminalStress.radiusPoint t r z)| * TerminalStress.heatAmplitude C (1 + h) t r ^ 2 * (1 - f (Real.log (SimilarityProfile.X h (TerminalStress.radiusPoint t r z))))

Coarse angular/axial tilt on a fixed terminal annulus

theorem NavierStokes.TerminalPressure.heatProfile_antitoneOn {h : ℝ} (hh : 0 < h) : AntitoneOn (RadialHeatProfile.profile (1 + h)) (Set.Ioi 0)

theorem NavierStokes.TerminalPressure.heatAmplitude_annulus_lower {C h t r R Λ : ℝ} (hC : 0 < C) (hh : 0 < h) (ht : t < 1) (hr : 0 < r) (hrR : r ≤ R) (hΛ : 1 ≤ Λ) (hRΛ : R ^ 2 ≤ Λ * r ^ 2) : Λ ^ (-amplitudeExponent h) * TerminalStress.heatAmplitude C (1 + h) t r ≤ TerminalStress.heatAmplitude C (1 + h) t R

theorem NavierStokes.TerminalPressure.timeDenominator_le_q {h t z : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) : TerminalStress.timeDenominator h t z ≤ SimilarityProfile.q h (t, 0, z)

noncomputable def NavierStokes.TerminalPressure.tiltConstant (h Λ : ℝ) : ℝ

Tilt constant, given by (2 / (1 - 2 * h)) * (Λ - 1) / Λ ^ (-amplitudeExponent h).

Equations

• NavierStokes.TerminalPressure.tiltConstant h Λ = 2 / (1 - 2 * h) * (Λ - 1) / Λ ^ (-NavierStokes.TerminalPressure.amplitudeExponent h)

theorem NavierStokes.TerminalPressure.terminal_tilt_bound {C h t z r R Y Λ : ℝ} {f : ℝ → ℝ} (hC : 0 < C) (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) (hr : 0 < r) (hrR : r ≤ R) (hf : ContDiff ℝ (↑⊤) f) (hb : ∀ (y : ℝ), 0 ≤ f y ∧ f y ≤ 1) (hmono : ∀ (y : ℝ), 0 ≤ deriv f y) (hplateau : ∀ (y : ℝ), Y ≤ y → f y = 1) (hR : Y ≤ Real.log (SimilarityProfile.X h (TerminalStress.radiusPoint t R z))) (hΛ : 1 ≤ Λ) (hRΛ : R ^ 2 ≤ Λ * r ^ 2) (hinside : f (Real.log (SimilarityProfile.X h (TerminalStress.radiusPoint t r z))) < 1) : 0 < TerminalStress.terminalStress C h f t z r ∧ |axialBackwardStress C h f t z r| / TerminalStress.terminalStress C h f t z r ≤ tiltConstant h Λ * SimilarityProfile.q h (TerminalStress.radiusPoint t r z) ^ (1 - CoordinateAlgebra.D h) * TerminalStress.heatAmplitude C (1 + h) t r

Actual backward stresses satisfy the coarse tilt estimate on any fixed annulus. The factor q^(1-D) K is subsequently bounded by the released amplitude.

Uniform smallness from the constructed release

theorem NavierStokes.TerminalPressure.outgoingAmplitude_suppressed (d : OutgoingTail.TailData) : HeatTailEdit.outgoingAmplitude d ≤ 4 * OutgoingTail.finalAngular d (d.releaseStart, 0) * d.h ^ 4

noncomputable def NavierStokes.TerminalPressure.releasedNormalization (d : OutgoingTail.TailData) (K : ℝ) : ℝ

The normalization is exactly the physical carrier normalization in ParametricHeatTail.physicalEdit_heat_carrier.

Equations

• NavierStokes.TerminalPressure.releasedNormalization d K = NavierStokes.HeatTailEdit.outgoingAmplitude d * K ^ NavierStokes.TerminalPressure.amplitudeExponent d.h

theorem NavierStokes.TerminalPressure.releasedNormalization_pos (d : OutgoingTail.TailData) {K : ℝ} (hK : 0 < K) : 0 < releasedNormalization d K

theorem NavierStokes.TerminalPressure.physicalEdit_eq_released_carrier (d : OutgoingTail.TailData) {K : ℝ} (hK : 0 < K) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) (hfull : 1 / 2 ≤ Real.log (SimilarityProfile.X d.h p / K) + 1 / 5) : SimilarityProfile.q d.h p ^ (-amplitudeExponent d.h) * ParametricHeatTail.physicalEdit d K (SimilarityProfile.eta d.h p) (SimilarityProfile.X d.h p) = TerminalStress.physicalHeat (releasedNormalization d K) (1 + d.h) p * outgoingTaper d (Real.log K - 1 / 5) (Real.log (SimilarityProfile.X d.h p))

The actual parametric heat edit agrees with this module's physical carrier. The diffusion identity is proved from the physical similarity coordinates.

theorem NavierStokes.TerminalPressure.released_heat_bound (d : OutgoingTail.TailData) {K : ℝ} (hK : 0 < K) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) (hX : K ≤ SimilarityProfile.X d.h p) : SimilarityProfile.q d.h p ^ (1 - CoordinateAlgebra.D d.h) * TerminalStress.physicalHeat (releasedNormalization d K) (1 + d.h) p ≤ HeatTailEdit.outgoingAmplitude d

theorem NavierStokes.TerminalPressure.tiltConstant_uniform {h Λ : ℝ} (hh : 0 < h) (hh4 : h ≤ 1 / 4) (hΛ : 1 ≤ Λ) : tiltConstant h Λ ≤ 4 * Λ * (Λ - 1)

theorem NavierStokes.TerminalPressure.outgoingTaper_lt_one (d : OutgoingTail.TailData) {y0 y : ℝ} (hy : y < y0 + 3) : outgoingTaper d y0 y < 1

theorem NavierStokes.TerminalPressure.released_terminal_tilt (d : OutgoingTail.TailData) {K y0 t z r R Λ : ℝ} (hK : 0 < K) (hh4 : d.h ≤ 1 / 4) (ht : t < 1) (hr : 0 < r) (hrR : r ≤ R) (hΛ : 1 ≤ Λ) (hRΛ : R ^ 2 ≤ Λ * r ^ 2) (hX : K ≤ SimilarityProfile.X d.h (TerminalStress.radiusPoint t r z)) (hR : y0 + 3 ≤ Real.log (SimilarityProfile.X d.h (TerminalStress.radiusPoint t R z))) (hinside : Real.log (SimilarityProfile.X d.h (TerminalStress.radiusPoint t r z)) < y0 + 3) : 0 < TerminalStress.terminalStress (releasedNormalization d K) d.h (outgoingTaper d y0) t z r ∧ |axialBackwardStress (releasedNormalization d K) d.h (outgoingTaper d y0) t z r| / TerminalStress.terminalStress (releasedNormalization d K) d.h (outgoingTaper d y0) t z r ≤ 16 * Λ * (Λ - 1) * OutgoingTail.finalAngular d (d.releaseStart, 0) * d.h ^ 4

The bound is uniform in spacetime, in the terminal scale K, and in the distance to the edge. The released amplitude contributes the proved factor h^4.

theorem NavierStokes.TerminalPressure.released_terminal_tilt_small (d : OutgoingTail.TailData) {K y0 t z r R Λ ε : ℝ} (hK : 0 < K) (hh4 : d.h ≤ 1 / 4) (ht : t < 1) (hr : 0 < r) (hrR : r ≤ R) (hΛ : 1 ≤ Λ) (hRΛ : R ^ 2 ≤ Λ * r ^ 2) (hX : K ≤ SimilarityProfile.X d.h (TerminalStress.radiusPoint t r z)) (hR : y0 + 3 ≤ Real.log (SimilarityProfile.X d.h (TerminalStress.radiusPoint t R z))) (hinside : Real.log (SimilarityProfile.X d.h (TerminalStress.radiusPoint t r z)) < y0 + 3) (hsmall : d.h ≤ ε / (1 + 16 * Λ * (Λ - 1) * OutgoingTail.finalAngular d (d.releaseStart, 0))) : |axialBackwardStress (releasedNormalization d K) d.h (outgoingTaper d y0) t z r| / TerminalStress.terminalStress (releasedNormalization d K) d.h (outgoingTaper d y0) t z r ≤ ε

theorem NavierStokes.TerminalPressure.outgoing_navierStokesResidual (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) {t : ℝ} {x : ProblemStatement.Space} (ht : t < 1) (hs : 0 < AxisymmetricFields.radialEnergy x) : ProblemStatement.navierStokesResidual (TerminalStress.terminalVelocity C d.h (outgoingTaper d y0)) (TerminalStress.terminalPressure C d.h (outgoingTaper d y0)) t x = AxisymmetricResidual.pack (-x.ofLp 1 / √(2 * AxisymmetricFields.radialEnergy x) * (TerminalStress.leadingResidual C d.h (outgoingTaper d y0) t (√(2 * AxisymmetricFields.radialEnergy x)) (x.ofLp 2) - TerminalStress.axialViscosity C d.h (outgoingTaper d y0) (AxisymmetricFields.profilePoint t x))) (x.ofLp 0 / √(2 * AxisymmetricFields.radialEnergy x) * (TerminalStress.leadingResidual C d.h (outgoingTaper d y0) t (√(2 * AxisymmetricFields.radialEnergy x)) (x.ofLp 2) - TerminalStress.axialViscosity C d.h (outgoingTaper d y0) (AxisymmetricFields.profilePoint t x))) (SimilarityProfile.partialZ (outgoingPressure C d y0) (AxisymmetricFields.profilePoint t x))

Full physical residual formula after discharging the pressure regularity and improper-integral assumptions. The axial viscosity of the swirl is retained.

theorem NavierStokes.TerminalPressure.axialBackwardStress_divergence {C h t z r R Y : ℝ} {f : ℝ → ℝ} (hC : 0 < C) (hh : 0 < h) (hh1 : h < 1 / 2) (ht : t < 1) (hr : 0 < r) (hrR : r ≤ R) (hf : ContDiff ℝ (↑⊤) f) (hb : ∀ (y : ℝ), 0 ≤ f y ∧ f y ≤ 1) (hmono : ∀ (y : ℝ), 0 ≤ deriv f y) (hplateau : ∀ (y : ℝ), Y ≤ y → f y = 1) (hR : Y ≤ Real.log (SimilarityProfile.X h (TerminalStress.radiusPoint t R z))) : deriv (axialBackwardStress C h f t z) r + axialBackwardStress C h f t z r / r = -SimilarityProfile.partialZ (TerminalStress.canonicalPressure (TerminalStress.swirlCoefficient C h f)) (TerminalStress.radiusPoint t r z)

The backward axial primitive has the required cylindrical divergence, computed from actual derivatives of the canonical pressure.