The actual positive-order divergence primitive

Equation (21) is derived from genuine radial averages of a jointly smooth axial profile. Its radial derivative is the actual similarity axial operator, and its physical reconstruction satisfies the flux form of incompressibility.

noncomputable def NavierStokes.SlowDivergence.radialFlux (h lam : ℝ) (U : ProfileHistories.Field) (p : ProfileHistories.Point) : ℝ

The positive-order radial flux, with an arbitrary exponent increment lam.

Equations

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

theorem NavierStokes.SlowDivergence.radialFlux_at_axis (h lam η : ℝ) (U : ProfileHistories.Field) : radialFlux h lam U (0, η) = 0

theorem NavierStokes.SlowDivergence.radialFlux_div_radial (h lam : ℝ) (U : ProfileHistories.Field) {p : ProfileHistories.Point} (hX : p.1 ≠ 0) : radialFlux h lam U p / p.1 = (CoordinateAlgebra.L h p.2)⁻¹ * (2 * p.2 * U p - 2 * p.2 * (CoordinateAlgebra.D h + lam) * ProfileHistories.average U p - CoordinateAlgebra.d p.2 * SimilarityProfile.partialEta (ProfileHistories.average U) p)

theorem NavierStokes.SlowDivergence.radialFlux_eq_histories (Ω : ProfileHistories.RadialDomain) {U : ProfileHistories.Field} (hU : ContDiffOn ℝ (↑⊤) U Ω.carrier) (h lam : ℝ) {p : ProfileHistories.Point} (hp : p ∈ Ω.carrier) : radialFlux h lam U p = (2 * p.2 * (p.1 * U p) - 2 * p.2 * (CoordinateAlgebra.D h + lam) * ProfileHistories.primitive U p - CoordinateAlgebra.d p.2 * ProfileHistories.primitive (ProfileHistories.parameterPartial U) p) / CoordinateAlgebra.L h p.2

Rewriting the formula through actual radial histories removes every division by X and permits differentiation at the axis.

theorem NavierStokes.SlowDivergence.radialFlux_smoothAt (Ω : ProfileHistories.RadialDomain) {U : ProfileHistories.Field} (hU : ContDiffOn ℝ (↑⊤) U Ω.carrier) (h lam : ℝ) {p : ProfileHistories.Point} (hp : p ∈ Ω.carrier) (hL : CoordinateAlgebra.L h p.2 ≠ 0) : ContDiffAt ℝ (↑⊤) (radialFlux h lam U) p

theorem NavierStokes.SlowDivergence.radialFlux_smooth (Ω : ProfileHistories.RadialDomain) {U : ProfileHistories.Field} (hU : ContDiffOn ℝ (↑⊤) U Ω.carrier) (h lam : ℝ) (hL : ∀ p ∈ Ω.carrier, CoordinateAlgebra.L h p.2 ≠ 0) : ContDiffOn ℝ (↑⊤) (radialFlux h lam U) Ω.carrier

Joint C∞ regularity on every open profile domain avoiding L=0.

theorem NavierStokes.SlowDivergence.radialFlux_hasDerivAt (Ω : ProfileHistories.RadialDomain) {U : ProfileHistories.Field} (hU : ContDiffOn ℝ (↑⊤) U Ω.carrier) (h lam : ℝ) {p : ProfileHistories.Point} (hp : p ∈ Ω.carrier) : HasDerivAt (fun (x : ℝ) => radialFlux h lam U (x, p.2)) (-SimilarityProfile.Z h (-CoordinateAlgebra.A h + lam) U p) p.1

The first identity in (21), derived by FTC from the actual histories. The scalar radial statement also holds under total division when L=0.

theorem NavierStokes.SlowDivergence.partialX_radialFlux (Ω : ProfileHistories.RadialDomain) {U : ProfileHistories.Field} (hU : ContDiffOn ℝ (↑⊤) U Ω.carrier) (h lam : ℝ) {p : ProfileHistories.Point} (hp : p ∈ Ω.carrier) (hL : CoordinateAlgebra.L h p.2 ≠ 0) : SimilarityProfile.partialX (radialFlux h lam U) p = -SimilarityProfile.Z h (-CoordinateAlgebra.A h + lam) U p

Equality with the partial derivative used by the similarity calculus.

theorem NavierStokes.SlowDivergence.axial_source_intervalIntegrable (Ω : ProfileHistories.RadialDomain) {U : ProfileHistories.Field} (hU : ContDiffOn ℝ (↑⊤) U Ω.carrier) (h b : ℝ) {p : ProfileHistories.Point} (hp : p ∈ Ω.carrier) : IntervalIntegrable (fun (x : ℝ) => -SimilarityProfile.Z h b U (x, p.2)) MeasureTheory.volume 0 p.1

theorem NavierStokes.SlowDivergence.radialFlux_eq_integral (Ω : ProfileHistories.RadialDomain) {U : ProfileHistories.Field} (hU : ContDiffOn ℝ (↑⊤) U Ω.carrier) (h lam : ℝ) {p : ProfileHistories.Point} (hp : p ∈ Ω.carrier) : radialFlux h lam U p = ∫ (x : ℝ) in 0..p.1, -SimilarityProfile.Z h (-CoordinateAlgebra.A h + lam) U (x, p.2)

The printed expression is precisely the zero-axis integral of -Z U.

theorem NavierStokes.SlowDivergence.physical_flux_axial_balance (Ω : ProfileHistories.RadialDomain) {U : ProfileHistories.Field} (hU : ContDiffOn ℝ (↑⊤) U Ω.carrier) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (lam : ℝ) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) (hi : SimilarityProfile.inner h p ∈ Ω.carrier) : SimilarityProfile.partialS (SimilarityProfile.pullback h lam (radialFlux h lam U)) p + SimilarityProfile.partialZ (SimilarityProfile.pullback h (-CoordinateAlgebra.A h + lam) U) p = 0

Physical incompressibility in flux coordinates (t,s,z), s=r²/2. The radial flux has power q^lam and the axial velocity has power q^(-A+lam).

theorem NavierStokes.SlowDivergence.slow_order_divergence (Ω : ProfileHistories.RadialDomain) {U : ProfileHistories.Field} (hU : ContDiffOn ℝ (↑⊤) U Ω.carrier) (h : ℝ) (n : ℕ) {p : ProfileHistories.Point} (hp : p ∈ Ω.carrier) (hL : CoordinateAlgebra.L h p.2 ≠ 0) : SimilarityProfile.partialX (radialFlux h (2 * ↑n * h) U) p + SimilarityProfile.Z h (-CoordinateAlgebra.A h + 2 * ↑n * h) U p = 0

Specialization to the manuscript's lam_n = 2nh, with n represented honestly as a natural-number order.