The canonical zeroth stress is the explicit leading stress

The weighted stresses have regular primitives through the axis. Their actual derivatives are the negative weighted residuals, so the lower integration endpoint fixes the constant and identifies the constructed stress.

noncomputable def NavierStokes.ZerothStressIdentity.leadingProfiles {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h C : ℝ) : SlowExpansionResidual.SlowProfiles

Leading profiles, bundling phi, axial, flux, pressure.

Equations

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

theorem NavierStokes.ZerothStressIdentity.T_const_mul (h b C : ℝ) {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : DifferentiableAt ℝ f w) : SimilarityProfile.T h b (fun (p : SimilarityProfile.InnerPoint) => C * f p) w = C * SimilarityProfile.T h b f w

theorem NavierStokes.ZerothStressIdentity.Z_const_mul (h b C : ℝ) {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : DifferentiableAt ℝ f w) : SimilarityProfile.Z h b (fun (p : SimilarityProfile.InnerPoint) => C * f p) w = C * SimilarityProfile.Z h b f w

theorem NavierStokes.ZerothStressIdentity.leading_angular_coefficient {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h C : ℝ) {w : SimilarityProfile.InnerPoint} (hw : w ∈ Ω.carrier) (hX : w.1 ≠ 0) (hf : P.f w ≠ 0) (hL : CoordinateAlgebra.L h w.2 ≠ 0) : SlowExpansionResidual.angularCoefficient h (leadingProfiles P h C) 0 w = C * (-P.f w * LeadingStress.sourceTheta P h w / CoordinateAlgebra.L h w.2 - 2 * (w.1 * SimilarityProfile.partialX (SimilarityProfile.partialX P.f) w + 2 * SimilarityProfile.partialX P.f w))

theorem NavierStokes.ZerothStressIdentity.leading_axial_coefficient {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h C : ℝ) {w : SimilarityProfile.InnerPoint} (hw : w ∈ Ω.carrier) (hL : CoordinateAlgebra.L h w.2 ≠ 0) : SlowExpansionResidual.axialCoefficient h (leadingProfiles P h C) 0 w = -LeadingStress.sourceAxial P h w / CoordinateAlgebra.L h w.2 - 2 * (w.1 * SimilarityProfile.partialX (SimilarityProfile.partialX P.U) w + SimilarityProfile.partialX P.U w)

noncomputable def NavierStokes.ZerothStressIdentity.weightedTheta {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h R eta : ℝ) : ℝ

Regular formula for R² times the angular stress, with no inverse X.

Equations

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

noncomputable def NavierStokes.ZerothStressIdentity.weightedAxial {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h R eta : ℝ) : ℝ

Regular formula for R times the axial stress.

Equations

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

@[simp]

theorem NavierStokes.ZerothStressIdentity.weightedTheta_zero {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h eta : ℝ) : weightedTheta P h 0 eta = 0

@[simp]

theorem NavierStokes.ZerothStressIdentity.weightedAxial_zero {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h eta : ℝ) : weightedAxial P h 0 eta = 0

theorem NavierStokes.ZerothStressIdentity.square_half_hasDerivAt (R : ℝ) : HasDerivAt (fun (r : ℝ) => r ^ 2 / 2) R R

theorem NavierStokes.ZerothStressIdentity.weightedTheta_hasDerivAt {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) {R eta : ℝ} (hw : (R ^ 2 / 2, eta) ∈ Ω.carrier) : HasDerivAt (fun (r : ℝ) => weightedTheta P h r eta) (R * P.angularSource h (R ^ 2 / 2, eta) / CoordinateAlgebra.L h eta + 4 * R ^ 3 * SimilarityProfile.partialX P.f (R ^ 2 / 2, eta) + R ^ 5 * SimilarityProfile.partialX (SimilarityProfile.partialX P.f) (R ^ 2 / 2, eta)) R

theorem NavierStokes.ZerothStressIdentity.weightedAxial_hasDerivAt {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) {R eta : ℝ} (hw : (R ^ 2 / 2, eta) ∈ Ω.carrier) : HasDerivAt (fun (r : ℝ) => weightedAxial P h r eta) (R * P.axialSource h (R ^ 2 / 2, eta) / CoordinateAlgebra.L h eta + 2 * R * SimilarityProfile.partialX P.U (R ^ 2 / 2, eta) + R ^ 3 * SimilarityProfile.partialX (SimilarityProfile.partialX P.U) (R ^ 2 / 2, eta)) R

theorem NavierStokes.ZerothStressIdentity.weightedTheta_eq {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) {R eta : ℝ} (hR : 0 < R) (hf : P.f (R ^ 2 / 2, eta) ≠ 0) (hL : CoordinateAlgebra.L h eta ≠ 0) : weightedTheta P h R eta = R ^ 2 * LeadingStress.theta P h (R ^ 2 / 2, eta)

theorem NavierStokes.ZerothStressIdentity.weightedAxial_eq {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) {R eta : ℝ} (hR : 0 < R) (hL : CoordinateAlgebra.L h eta ≠ 0) : weightedAxial P h R eta = R * LeadingStress.axial P h (R ^ 2 / 2, eta)

theorem NavierStokes.ZerothStressIdentity.leading_thetaDensity {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h C : ℝ) (hC : C ≠ 0) {R eta : ℝ} (hR : 0 < R) (hw : (R ^ 2 / 2, eta) ∈ Ω.carrier) (hf : P.f (R ^ 2 / 2, eta) ≠ 0) (hL : CoordinateAlgebra.L h eta ≠ 0) : SlowResidualMatching.thetaDensity h C (leadingProfiles P h C) 0 (R, eta) = -(R * P.angularSource h (R ^ 2 / 2, eta) / CoordinateAlgebra.L h eta + 4 * R ^ 3 * SimilarityProfile.partialX P.f (R ^ 2 / 2, eta) + R ^ 5 * SimilarityProfile.partialX (SimilarityProfile.partialX P.f) (R ^ 2 / 2, eta))

theorem NavierStokes.ZerothStressIdentity.leading_zDensity {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h C : ℝ) {R eta : ℝ} (hw : (R ^ 2 / 2, eta) ∈ Ω.carrier) (hL : CoordinateAlgebra.L h eta ≠ 0) : SlowResidualMatching.zDensity h (leadingProfiles P h C) 0 (R, eta) = -(R * P.axialSource h (R ^ 2 / 2, eta) / CoordinateAlgebra.L h eta + 2 * R * SimilarityProfile.partialX P.U (R ^ 2 / 2, eta) + R ^ 3 * SimilarityProfile.partialX (SimilarityProfile.partialX P.U) (R ^ 2 / 2, eta))

theorem NavierStokes.ZerothStressIdentity.stress_eq_of_weighted_derivative (m : ℕ) (F : SimilarityProfile.InnerProfile) (G : ℝ → ℝ) {R eta : ℝ} (hR : 0 < R) (hG : ContinuousOn G (Set.Icc 0 R)) (hG0 : G 0 = 0) (hD : ∀ r ∈ Set.Ioo 0 R, HasDerivAt G (-F (r, eta)) r) (hF : IntervalIntegrable (fun (r : ℝ) => F (r, eta)) MeasureTheory.volume 0 R) : SlowStressSupport.stress m F (R, eta) = G R / R ^ m

FTC determines the constant of the canonical negative primitive from the actual zero-axis value of the weighted potential.

theorem NavierStokes.ZerothStressIdentity.weightedTheta_continuous {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) {eta : ℝ} (hD : ∀ (X : ℝ), 0 ≤ X → (X, eta) ∈ Ω.carrier) : Continuous fun (R : ℝ) => weightedTheta P h R eta

theorem NavierStokes.ZerothStressIdentity.weightedAxial_continuous {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) {eta : ℝ} (hD : ∀ (X : ℝ), 0 ≤ X → (X, eta) ∈ Ω.carrier) : Continuous fun (R : ℝ) => weightedAxial P h R eta

A scheme whose actual order-zero fields come from P

theorem NavierStokes.ZerothStressIdentity.scheme_leading_germs {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ Ω.carrier) (hbase : s.base = AssembledSlowBase.baseFields ⋯ C P hD) {p : SimilarityProfile.InnerPoint} (hX : 0 < p.1) (heta : p.2 ∈ S) : (GlobalSlowProfiles.asSlowProfiles s).phi 0 =ᶠ[nhds p] (leadingProfiles P h C).phi 0 ∧ (GlobalSlowProfiles.asSlowProfiles s).axial 0 =ᶠ[nhds p] (leadingProfiles P h C).axial 0 ∧ (GlobalSlowProfiles.asSlowProfiles s).flux 0 =ᶠ[nhds p] (leadingProfiles P h C).flux 0 ∧ (GlobalSlowProfiles.asSlowProfiles s).pressure 0 =ᶠ[nhds p] (leadingProfiles P h C).pressure 0

theorem NavierStokes.ZerothStressIdentity.scheme_zero_coefficients_eq {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ Ω.carrier) (hbase : s.base = AssembledSlowBase.baseFields ⋯ C P hD) {p : SimilarityProfile.InnerPoint} (hX : 0 < p.1) (heta : p.2 ∈ S) : SlowExpansionResidual.angularCoefficient h (GlobalSlowProfiles.asSlowProfiles s) 0 p = SlowExpansionResidual.angularCoefficient h (leadingProfiles P h C) 0 p ∧ SlowExpansionResidual.axialCoefficient h (GlobalSlowProfiles.asSlowProfiles s) 0 p = SlowExpansionResidual.axialCoefficient h (leadingProfiles P h C) 0 p

theorem NavierStokes.ZerothStressIdentity.scheme_zero_densities_eq {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ Ω.carrier) (hbase : s.base = AssembledSlowBase.baseFields ⋯ C P hD) (R : ℝ) {eta : ℝ} (heta : eta ∈ S) : SlowResidualMatching.thetaDensity h C (GlobalSlowProfiles.asSlowProfiles s) 0 (R, eta) = SlowResidualMatching.thetaDensity h C (leadingProfiles P h C) 0 (R, eta) ∧ SlowResidualMatching.zDensity h (GlobalSlowProfiles.asSlowProfiles s) 0 (R, eta) = SlowResidualMatching.zDensity h (leadingProfiles P h C) 0 (R, eta)

theorem NavierStokes.ZerothStressIdentity.raw_stresses_eq {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) {S : Set ℝ} {h C rho core : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A core) (B0 : GlobalSlowProfiles.BaseAgreement s A core) (Z0 : AssembledSlowBase.ZeroOrderSolved s core) (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ Ω.carrier) (hbase : s.base = AssembledSlowBase.baseFields ⋯ C P hD) {R eta : ℝ} (hR : 0 < R) (heta : eta ∈ S) (hf : ∀ (X : ℝ), 0 < X → X ≤ R ^ 2 / 2 → P.f (X, eta) ≠ 0) : SlowStressSupport.stress 2 (SlowResidualMatching.thetaDensity h C (GlobalSlowProfiles.asSlowProfiles s) 0) (R, eta) = LeadingStress.theta P h (R ^ 2 / 2, eta) ∧ SlowStressSupport.stress 1 (SlowResidualMatching.zDensity h (GlobalSlowProfiles.asSlowProfiles s) 0) (R, eta) = LeadingStress.axial P h (R ^ 2 / 2, eta)

theorem NavierStokes.ZerothStressIdentity.coefficients_stress_zero_eq {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) {S : Set ℝ} {h C rho core : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A core) (B0 : GlobalSlowProfiles.BaseAgreement s A core) (Z0 : AssembledSlowBase.ZeroOrderSolved s core) (hI : Set.Icc (-1) 1 ⊆ S) (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ Ω.carrier) (hbase : s.base = AssembledSlowBase.baseFields ⋯ C P hD) {p : SimilarityProfile.InnerPoint} (hX : 0 ≤ p.1) (heta : |p.2| ≤ 1) (hf : ∀ (X : ℝ), 0 < X → X ≤ p.1 → P.f (X, p.2) ≠ 0) : (AssembledSlowBase.coefficients L B0 Z0 hI).stressTheta 0 p = LeadingStress.theta P h p ∧ (AssembledSlowBase.coefficients L B0 Z0 hI).stressAxial 0 p = LeadingStress.axial P h p

The actual extended stress slots equal the literal leading stress pair. The only nonvanishing condition is on the fixed radial slice being evaluated.