Integrated tangential balances from actual radial differential expressions

All moments below are actual Bochner integrals. Compact radial support supplies the boundary cancellations, and parameter derivatives pass under integrals by the dominated differentiation theorem in TransportPrimitive.

noncomputable def NavierStokes.IntegratedMeanBalances.moment (n : ℕ) (f : ℝ → ℝ) : ℝ

Moment, given by ∫ r, r ^ n * f r.

Equations

• NavierStokes.IntegratedMeanBalances.moment n f = ∫ (r : ℝ), r ^ n * f r

theorem NavierStokes.IntegratedMeanBalances.weighted_integrable {f : ℝ → ℝ} (hf : Continuous f) (hs : HasCompactSupport f) (n : ℕ) : MeasureTheory.Integrable (fun (r : ℝ) => r ^ n * f r) MeasureTheory.volume

theorem NavierStokes.IntegratedMeanBalances.moment_add {f g : ℝ → ℝ} (n : ℕ) (hf : MeasureTheory.Integrable (fun (r : ℝ) => r ^ n * f r) MeasureTheory.volume) (hg : MeasureTheory.Integrable (fun (r : ℝ) => r ^ n * g r) MeasureTheory.volume) : (moment n fun (r : ℝ) => f r + g r) = moment n f + moment n g

theorem NavierStokes.IntegratedMeanBalances.moment_sub {f g : ℝ → ℝ} (n : ℕ) (hf : MeasureTheory.Integrable (fun (r : ℝ) => r ^ n * f r) MeasureTheory.volume) (hg : MeasureTheory.Integrable (fun (r : ℝ) => r ^ n * g r) MeasureTheory.volume) : (moment n fun (r : ℝ) => f r - g r) = moment n f - moment n g

theorem NavierStokes.IntegratedMeanBalances.moment_const_mul (n : ℕ) (c : ℝ) (f : ℝ → ℝ) : (moment n fun (r : ℝ) => c * f r) = c * moment n f

theorem NavierStokes.IntegratedMeanBalances.moment_mul_const (n : ℕ) (f : ℝ → ℝ) (c : ℝ) : (moment n fun (r : ℝ) => f r * c) = moment n f * c

theorem NavierStokes.IntegratedMeanBalances.deriv_smooth {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (deriv f)

theorem NavierStokes.IntegratedMeanBalances.ae_radial_ne_zero : ∀ᵐ (r : ℝ), r ≠ 0

theorem NavierStokes.IntegratedMeanBalances.integral_deriv_zero {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : HasCompactSupport f) : ∫ (r : ℝ), deriv f r = 0

theorem NavierStokes.IntegratedMeanBalances.moment_deriv_succ {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : HasCompactSupport f) (n : ℕ) : moment (n + 1) (deriv f) = -↑(n + 1) * moment n f

Weighted integration by parts; compact support supplies both endpoint terms.

noncomputable def NavierStokes.IntegratedMeanBalances.radialDivergence (c : ℝ) (f : ℝ → ℝ) (r : ℝ) : ℝ

Radial divergence, given by deriv f r + c / r * f r.

Equations

• NavierStokes.IntegratedMeanBalances.radialDivergence c f r = deriv f r + c / r * f r

noncomputable def NavierStokes.IntegratedMeanBalances.angularRadialViscosity (f : ℝ → ℝ) (r : ℝ) : ℝ

Angular radial viscosity, given by deriv (deriv f) r + deriv f r / r - f r / r ^ 2.

Equations

• NavierStokes.IntegratedMeanBalances.angularRadialViscosity f r = deriv (deriv f) r + deriv f r / r - f r / r ^ 2

noncomputable def NavierStokes.IntegratedMeanBalances.axialRadialViscosity (f : ℝ → ℝ) (r : ℝ) : ℝ

Axial radial viscosity, given by deriv (deriv f) r + deriv f r / r.

Equations

• NavierStokes.IntegratedMeanBalances.axialRadialViscosity f r = deriv (deriv f) r + deriv f r / r

theorem NavierStokes.IntegratedMeanBalances.weighted_angular_divergence_ae (f : ℝ → ℝ) : (fun (r : ℝ) => r ^ 2 * radialDivergence 2 f r) =ᵐ[MeasureTheory.volume] fun (r : ℝ) => r ^ 2 * deriv f r + 2 * (r * f r)

theorem NavierStokes.IntegratedMeanBalances.weighted_axial_divergence_ae (f : ℝ → ℝ) : (fun (r : ℝ) => r * radialDivergence 1 f r) =ᵐ[MeasureTheory.volume] fun (r : ℝ) => r * deriv f r + f r

theorem NavierStokes.IntegratedMeanBalances.angular_divergence_integrable {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : HasCompactSupport f) : MeasureTheory.Integrable (fun (r : ℝ) => r ^ 2 * radialDivergence 2 f r) MeasureTheory.volume

theorem NavierStokes.IntegratedMeanBalances.axial_divergence_integrable {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : HasCompactSupport f) : MeasureTheory.Integrable (fun (r : ℝ) => r * radialDivergence 1 f r) MeasureTheory.volume

theorem NavierStokes.IntegratedMeanBalances.moment_angular_divergence {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : HasCompactSupport f) : moment 2 (radialDivergence 2 f) = 0

theorem NavierStokes.IntegratedMeanBalances.moment_axial_divergence {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : HasCompactSupport f) : moment 1 (radialDivergence 1 f) = 0

theorem NavierStokes.IntegratedMeanBalances.pressure_moment {p g : ℝ → ℝ} (hp : ContDiff ℝ (↑⊤) p) (hs : HasCompactSupport p) (hd : ∀ (r : ℝ), deriv p r = g r) : moment 1 p = -(1 / 2) * moment 2 g

The radial pressure moment follows from the actual derivative equation.

theorem NavierStokes.IntegratedMeanBalances.pressure_moment_reconstructed {p g ρ : ℝ → ℝ} (P : ℝ) (hp : ContDiff ℝ (↑⊤) p) (hsp : HasCompactSupport p) (hg : Continuous g) (hsg : HasCompactSupport g) (hρ : Continuous ρ) (hsρ : HasCompactSupport ρ) (hd : ∀ (r : ℝ), deriv p r = g r - ρ r * P) : moment 1 p = -(1 / 2) * moment 2 g + moment 2 ρ / 2 * P

theorem NavierStokes.IntegratedMeanBalances.weighted_angular_viscosity_ae (f : ℝ → ℝ) : (fun (r : ℝ) => r ^ 2 * angularRadialViscosity f r) =ᵐ[MeasureTheory.volume] fun (r : ℝ) => r ^ 2 * deriv (deriv f) r + r * deriv f r - f r

theorem NavierStokes.IntegratedMeanBalances.weighted_axial_viscosity_ae (f : ℝ → ℝ) : (fun (r : ℝ) => r * axialRadialViscosity f r) =ᵐ[MeasureTheory.volume] fun (r : ℝ) => r * deriv (deriv f) r + deriv f r

theorem NavierStokes.IntegratedMeanBalances.angular_viscosity_integrable {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : HasCompactSupport f) : MeasureTheory.Integrable (fun (r : ℝ) => r ^ 2 * angularRadialViscosity f r) MeasureTheory.volume

theorem NavierStokes.IntegratedMeanBalances.axial_viscosity_integrable {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : HasCompactSupport f) : MeasureTheory.Integrable (fun (r : ℝ) => r * axialRadialViscosity f r) MeasureTheory.volume

theorem NavierStokes.IntegratedMeanBalances.moment_angular_viscosity {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : HasCompactSupport f) : moment 2 (angularRadialViscosity f) = 0

theorem NavierStokes.IntegratedMeanBalances.moment_axial_viscosity {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : HasCompactSupport f) : moment 1 (axialRadialViscosity f) = 0

theorem NavierStokes.IntegratedMeanBalances.positive_integral_eq_integral {a b : ℝ} (ha : 0 < a) {f : ℝ → ℝ} (hs : Function.support f ⊆ Set.Icc a b) : ∫ (r : ℝ) in Set.Ioi 0, f r = ∫ (r : ℝ), f r

Smooth compact radial families and their moments

noncomputable def NavierStokes.IntegratedMeanBalances.radialMoment {P : Type} (n : ℕ) (F : ℝ × P → ℝ) (p : P) : ℝ

Radial moment, given by moment n (fun r => F (r, p)).

Equations

• NavierStokes.IntegratedMeanBalances.radialMoment n F p = NavierStokes.IntegratedMeanBalances.moment n fun (r : ℝ) => F (r, p)

noncomputable def NavierStokes.IntegratedMeanBalances.parameterPartial {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (v : P) (F : ℝ × P → ℝ) (x : ℝ × P) : ℝ

Parameter partial, given by fderiv ℝ F x (0, v).

Equations

• NavierStokes.IntegratedMeanBalances.parameterPartial v F x = (fderiv ℝ F x) (0, v)

theorem NavierStokes.IntegratedMeanBalances.parameterPartial_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (v : P) {F : ℝ × P → ℝ} (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (parameterPartial v F)

theorem NavierStokes.IntegratedMeanBalances.parameterPartial_supported {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (v : P) {a b : ℝ} {F : ℝ × P → ℝ} (hs : RadialAlias.RadiallySupported a b F) : RadialAlias.RadiallySupported a b (parameterPartial v F)

theorem NavierStokes.IntegratedMeanBalances.radial_slice_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {F : ℝ × P → ℝ} (hF : ContDiff ℝ (↑⊤) F) (p : P) : ContDiff ℝ ↑⊤ fun (r : ℝ) => F (r, p)

theorem NavierStokes.IntegratedMeanBalances.radial_slice_compact {P : Type} {a b : ℝ} {F : ℝ × P → ℝ} (hs : RadialAlias.RadiallySupported a b F) (p : P) : HasCompactSupport fun (r : ℝ) => F (r, p)

theorem NavierStokes.IntegratedMeanBalances.radialMoment_eq_interval {P : Type} [NormedAddCommGroup P] {a b : ℝ} {F : ℝ × P → ℝ} (hF : Continuous F) (hs : RadialAlias.RadiallySupported a b F) (n : ℕ) (p : P) : radialMoment n F p = ∫ (r : ℝ) in a..b, r ^ n * F (r, p)

theorem NavierStokes.IntegratedMeanBalances.parameterIntegral_fderiv_apply {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {F : P × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (a b : ℝ) (p v : P) : (fderiv ℝ (fun (q : P) => ∫ (r : ℝ) in a..b, F (q, r)) p) v = ∫ (r : ℝ) in a..b, (fderiv ℝ F (p, r)) (v, 0)

theorem NavierStokes.IntegratedMeanBalances.weighted_swap_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {F : ℝ × P → ℝ} (hF : ContDiff ℝ (↑⊤) F) (n : ℕ) : ContDiff ℝ ↑⊤ fun (x : P × ℝ) => x.2 ^ n * F (x.2, x.1)

theorem NavierStokes.IntegratedMeanBalances.radialMoment_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {F : ℝ × P → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : RadialAlias.RadiallySupported a b F) (n : ℕ) : ContDiff ℝ (↑⊤) (radialMoment n F)

theorem NavierStokes.IntegratedMeanBalances.radialMoment_parameterPartial {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {F : ℝ × P → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : RadialAlias.RadiallySupported a b F) (n : ℕ) (p v : P) : (fderiv ℝ (radialMoment n F) p) v = radialMoment n (parameterPartial v F) p

theorem NavierStokes.IntegratedMeanBalances.zero_mass_parameterPartial {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {F : ℝ × P → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : RadialAlias.RadiallySupported a b F) (n : ℕ) (hm : radialMoment n F = 0) (p v : P) : radialMoment n (parameterPartial v F) p = 0

theorem NavierStokes.IntegratedMeanBalances.zero_mass_parameterPartial_twice {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {F : ℝ × P → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : RadialAlias.RadiallySupported a b F) (n : ℕ) (hm : radialMoment n F = 0) (p v w : P) : radialMoment n (parameterPartial w (parameterPartial v F)) p = 0

Actual torus averages annihilate the lift derivatives

noncomputable def NavierStokes.IntegratedMeanBalances.torusInner {P : Type} (F : (P × ℝ) × ℝ → ℝ) (q : P × ℝ) : ℝ

Torus inner, given by ∫ x in (0 : ℝ)..1, F (q, x).

Equations

• NavierStokes.IntegratedMeanBalances.torusInner F q = ∫ (x : ℝ) in 0..1, F (q, x)

noncomputable def NavierStokes.IntegratedMeanBalances.torusAverage {P : Type} (F : (P × ℝ) × ℝ → ℝ) (p : P) : ℝ

Torus average, given by ∫ y in (0 : ℝ)..1, torusInner F (p, y).

Equations

• NavierStokes.IntegratedMeanBalances.torusAverage F p = ∫ (y : ℝ) in 0..1, NavierStokes.IntegratedMeanBalances.torusInner F (p, y)

noncomputable def NavierStokes.IntegratedMeanBalances.fixedPartial {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (v : (P × ℝ) × ℝ) (F : (P × ℝ) × ℝ → ℝ) (q : (P × ℝ) × ℝ) : ℝ

Fixed partial, given by fderiv ℝ F q v.

Equations

• NavierStokes.IntegratedMeanBalances.fixedPartial v F q = (fderiv ℝ F q) v

noncomputable def NavierStokes.IntegratedMeanBalances.slowPartial {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (v : P) (F : (P × ℝ) × ℝ → ℝ) : (P × ℝ) × ℝ → ℝ

Slow partial, given by fixedPartial ((v, 0), 0) F.

Equations

• NavierStokes.IntegratedMeanBalances.slowPartial v F = NavierStokes.IntegratedMeanBalances.fixedPartial ((v, 0), 0) F

noncomputable def NavierStokes.IntegratedMeanBalances.torusPartial {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (v : ℝ × ℝ) (F : (P × ℝ) × ℝ → ℝ) : (P × ℝ) × ℝ → ℝ

Torus partial, given by fixedPartial ((0, v.2), v.1) F.

Equations

• NavierStokes.IntegratedMeanBalances.torusPartial v F = NavierStokes.IntegratedMeanBalances.fixedPartial ((0, v.2), v.1) F

structure NavierStokes.IntegratedMeanBalances.TorusPeriodic {P : Type} [NormedAddCommGroup P] (F : (P × ℝ) × ℝ → ℝ) : Prop

Torus periodic data, collecting first, second.

• first (q : (P × ℝ) × ℝ) : F (q + ((0, 0), 1)) = F q
• second (q : (P × ℝ) × ℝ) : F (q + ((0, 1), 0)) = F q

theorem NavierStokes.IntegratedMeanBalances.fixedPartial_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (v : (P × ℝ) × ℝ) {F : (P × ℝ) × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (fixedPartial v F)

theorem NavierStokes.IntegratedMeanBalances.fixedPartial_periodic {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (v : (P × ℝ) × ℝ) {F : (P × ℝ) × ℝ → ℝ} (hp : TorusPeriodic F) : TorusPeriodic (fixedPartial v F)

theorem NavierStokes.IntegratedMeanBalances.torusInner_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {F : (P × ℝ) × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (torusInner F)

theorem NavierStokes.IntegratedMeanBalances.torusAverage_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {F : (P × ℝ) × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (torusAverage F)

theorem NavierStokes.IntegratedMeanBalances.torusAverage_fderiv {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {F : (P × ℝ) × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (p v : P) : (fderiv ℝ (torusAverage F) p) v = torusAverage (slowPartial v F) p

Both parameter-integral interchanges are proved from joint smoothness on the compact torus coordinate square.

theorem NavierStokes.IntegratedMeanBalances.torusAverage_add {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {F G : (P × ℝ) × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hG : ContDiff ℝ (↑⊤) G) (p : P) : torusAverage (fun (q : (P × ℝ) × ℝ) => F q + G q) p = torusAverage F p + torusAverage G p

theorem NavierStokes.IntegratedMeanBalances.torusAverage_coeff_mul {P : Type} (a : P → ℝ) (F : (P × ℝ) × ℝ → ℝ) (p : P) : torusAverage (fun (q : (P × ℝ) × ℝ) => a q.1.1 * F q) p = a p * torusAverage F p

theorem NavierStokes.IntegratedMeanBalances.torusAverage_first_zero {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {F : (P × ℝ) × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hp : TorusPeriodic F) (p : P) : torusAverage (fixedPartial ((0, 0), 1) F) p = 0

theorem NavierStokes.IntegratedMeanBalances.torusAverage_second_zero {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {F : (P × ℝ) × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hp : TorusPeriodic F) (p : P) : torusAverage (fixedPartial ((0, 1), 0) F) p = 0

theorem NavierStokes.IntegratedMeanBalances.torusPartial_decompose {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (v : ℝ × ℝ) (F : (P × ℝ) × ℝ → ℝ) : torusPartial v F = fun (q : (P × ℝ) × ℝ) => v.1 * fixedPartial ((0, 0), 1) F q + v.2 * fixedPartial ((0, 1), 0) F q

theorem NavierStokes.IntegratedMeanBalances.torusAverage_torusPartial_zero {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (v : ℝ × ℝ) {F : (P × ℝ) × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hp : TorusPeriodic F) (p : P) : torusAverage (torusPartial v F) p = 0

noncomputable def NavierStokes.IntegratedMeanBalances.graphPartial {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (a : P → ℝ) (v : P) (w : ℝ × ℝ) (F : (P × ℝ) × ℝ → ℝ) (q : (P × ℝ) × ℝ) : ℝ

Graph partial, given by slowPartial v F q + a q.1.1 * torusPartial w F q.

Equations

• NavierStokes.IntegratedMeanBalances.graphPartial a v w F q = NavierStokes.IntegratedMeanBalances.slowPartial v F q + a q.1.1 * NavierStokes.IntegratedMeanBalances.torusPartial w F q

theorem NavierStokes.IntegratedMeanBalances.graphPartial_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a : P → ℝ} {F : (P × ℝ) × ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) a) (hF : ContDiff ℝ (↑⊤) F) (v : P) (w : ℝ × ℝ) : ContDiff ℝ (↑⊤) (graphPartial a v w F)

theorem NavierStokes.IntegratedMeanBalances.graphPartial_periodic {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (a : P → ℝ) (v : P) (w : ℝ × ℝ) {F : (P × ℝ) × ℝ → ℝ} (hp : TorusPeriodic F) : TorusPeriodic (graphPartial a v w F)

theorem NavierStokes.IntegratedMeanBalances.torusAverage_graphPartial {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a : P → ℝ} {F : (P × ℝ) × ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) a) (hF : ContDiff ℝ (↑⊤) F) (hp : TorusPeriodic F) (v p : P) (w : ℝ × ℝ) : torusAverage (graphPartial a v w F) p = (fderiv ℝ (torusAverage F) p) v

Graph lift terms integrate to zero; only the genuine slow derivative remains.

theorem NavierStokes.IntegratedMeanBalances.torusAverage_graphPartial_twice {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a : P → ℝ} {F : (P × ℝ) × ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) a) (hF : ContDiff ℝ (↑⊤) F) (hp : TorusPeriodic F) (v p : P) (w : ℝ × ℝ) : torusAverage (graphPartial a v w (graphPartial a v w F)) p = (fderiv ℝ (fun (q : P) => (fderiv ℝ (torusAverage F) q) v) p) v

The averaged chart balances and their exact weighted integrals

theorem NavierStokes.IntegratedMeanBalances.weighted_integrable_add {n : ℕ} {f g : ℝ → ℝ} (hf : MeasureTheory.Integrable (fun (r : ℝ) => r ^ n * f r) MeasureTheory.volume) (hg : MeasureTheory.Integrable (fun (r : ℝ) => r ^ n * g r) MeasureTheory.volume) : MeasureTheory.Integrable (fun (r : ℝ) => r ^ n * (f r + g r)) MeasureTheory.volume

theorem NavierStokes.IntegratedMeanBalances.weighted_integrable_sub {n : ℕ} {f g : ℝ → ℝ} (hf : MeasureTheory.Integrable (fun (r : ℝ) => r ^ n * f r) MeasureTheory.volume) (hg : MeasureTheory.Integrable (fun (r : ℝ) => r ^ n * g r) MeasureTheory.volume) : MeasureTheory.Integrable (fun (r : ℝ) => r ^ n * (f r - g r)) MeasureTheory.volume

theorem NavierStokes.IntegratedMeanBalances.weighted_integrable_const_mul {n : ℕ} {f : ℝ → ℝ} (hf : MeasureTheory.Integrable (fun (r : ℝ) => r ^ n * f r) MeasureTheory.volume) (c : ℝ) : MeasureTheory.Integrable (fun (r : ℝ) => r ^ n * (c * f r)) MeasureTheory.volume

theorem NavierStokes.IntegratedMeanBalances.moment_balance_algebra (n : ℕ) (α β δ : ℝ) (f g h j k l : ℝ → ℝ) (hf : MeasureTheory.Integrable (fun (r : ℝ) => r ^ n * f r) MeasureTheory.volume) (hg : MeasureTheory.Integrable (fun (r : ℝ) => r ^ n * g r) MeasureTheory.volume) (hh : MeasureTheory.Integrable (fun (r : ℝ) => r ^ n * h r) MeasureTheory.volume) (hj : MeasureTheory.Integrable (fun (r : ℝ) => r ^ n * j r) MeasureTheory.volume) (hk : MeasureTheory.Integrable (fun (r : ℝ) => r ^ n * k r) MeasureTheory.volume) (hl : MeasureTheory.Integrable (fun (r : ℝ) => r ^ n * l r) MeasureTheory.volume) : (moment n fun (r : ℝ) => α * f r + g r + β * h r - β * (j r + δ * k r) - l r) = α * moment n f + moment n g + β * moment n h - β * (moment n j + δ * moment n k) - moment n l

@[reducible, inline]

abbrev NavierStokes.IntegratedMeanBalances.MeanParameter : Type

Mean parameter: an abbreviation for ℝ × ℝ.

Equations

• NavierStokes.IntegratedMeanBalances.MeanParameter = (ℝ × ℝ)

@[reducible, inline]

abbrev NavierStokes.IntegratedMeanBalances.MeanPoint : Type

Mean point: an abbreviation for ℝ × MeanParameter.

Equations

• NavierStokes.IntegratedMeanBalances.MeanPoint = (ℝ × NavierStokes.IntegratedMeanBalances.MeanParameter)

@[reducible, inline]

abbrev NavierStokes.IntegratedMeanBalances.MeanField : Type

Mean field: an abbreviation for MeanPoint → ℝ.

Equations

• NavierStokes.IntegratedMeanBalances.MeanField = (NavierStokes.IntegratedMeanBalances.MeanPoint → ℝ)

structure NavierStokes.IntegratedMeanBalances.SmoothShell (a b : ℝ) (F : MeanField) : Prop

Joint smoothness and a common compact radial shell are genuine input regularity conditions on the pointwise fields, not conditions on their moments.

• smooth : ContDiff ℝ (↑⊤) F
• supported : RadialAlias.RadiallySupported a b F

theorem NavierStokes.IntegratedMeanBalances.SmoothShell.parameterDerivative {a b : ℝ} {F : MeanField} (hF : SmoothShell a b F) (v : MeanParameter) : SmoothShell a b (parameterPartial v F)

theorem NavierStokes.IntegratedMeanBalances.SmoothShell.add {a b : ℝ} {F G : MeanField} (hF : SmoothShell a b F) (hG : SmoothShell a b G) : SmoothShell a b fun (x : MeanPoint) => F x + G x

theorem NavierStokes.IntegratedMeanBalances.SmoothShell.slice_smooth {a b : ℝ} {F : MeanField} (hF : SmoothShell a b F) (p : MeanParameter) : ContDiff ℝ ↑⊤ fun (r : ℝ) => F (r, p)

theorem NavierStokes.IntegratedMeanBalances.SmoothShell.slice_compact {a b : ℝ} {F : MeanField} (hF : SmoothShell a b F) (p : MeanParameter) : HasCompactSupport fun (r : ℝ) => F (r, p)

theorem NavierStokes.IntegratedMeanBalances.SmoothShell.weighted_integrable {a b : ℝ} {F : MeanField} (hF : SmoothShell a b F) (n : ℕ) (p : MeanParameter) : MeasureTheory.Integrable (fun (r : ℝ) => r ^ n * F (r, p)) MeasureTheory.volume

noncomputable def NavierStokes.IntegratedMeanBalances.angularBalance (ε : ℝ) (v radialFlux axialFlux virtualFlux : MeanField) (x : MeanPoint) : ℝ

The angular line of (32), after the actual torus average. Coordinates are (R,(T,Z)); ε is constant on a chart. The supplied fluxes are full averages of the pointwise products in (32), and the last radial divergence is the virtual stress.

Equations

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

noncomputable def NavierStokes.IntegratedMeanBalances.axialBalance (ε : ℝ) (γ radialFlux axialFlux pressure virtualFlux : MeanField) (x : MeanPoint) : ℝ

The axial line of (32), with pressure retained inside the axial flux.

Equations

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

theorem NavierStokes.IntegratedMeanBalances.integrated_angular_balance {a b : ℝ} (ε : ℝ) {v radialFlux axialFlux virtualFlux : MeanField} (hv : SmoothShell a b v) (hr : SmoothShell a b radialFlux) (hz : SmoothShell a b axialFlux) (hT : SmoothShell a b virtualFlux) (hmass : radialMoment 2 v = 0) (p : MeanParameter) : radialMoment 2 (angularBalance ε v radialFlux axialFlux virtualFlux) p = ε * (fderiv ℝ (radialMoment 2 axialFlux) p) (0, 1)

The first identity in (34), derived from the pointwise angular balance.

theorem NavierStokes.IntegratedMeanBalances.integrated_axial_balance {a b : ℝ} (ε : ℝ) {γ radialFlux axialFlux pressure virtualFlux : MeanField} (hγ : SmoothShell a b γ) (hr : SmoothShell a b radialFlux) (hz : SmoothShell a b axialFlux) (hp : SmoothShell a b pressure) (hT : SmoothShell a b virtualFlux) (hmass : radialMoment 1 γ = 0) (p : MeanParameter) : radialMoment 1 (axialBalance ε γ radialFlux axialFlux pressure virtualFlux) p = ε * (fderiv ℝ (radialMoment 1 fun (x : ℝ × MeanParameter) => axialFlux x + pressure x) p) (0, 1)

The second tangential integral, before eliminating the pressure moment.

noncomputable def NavierStokes.IntegratedMeanBalances.pressureTotal (gr : MeanField) : MeanParameter → ℝ

Pressure total, given by radialMoment 0 gr.

Equations

• NavierStokes.IntegratedMeanBalances.pressureTotal gr = NavierStokes.IntegratedMeanBalances.radialMoment 0 gr

noncomputable def NavierStokes.IntegratedMeanBalances.pressureCoefficient (ρ : MeanField) (p : MeanParameter) : ℝ

Pressure coefficient, given by radialMoment 2 ρ p / 2.

Equations

• NavierStokes.IntegratedMeanBalances.pressureCoefficient ρ p = NavierStokes.IntegratedMeanBalances.radialMoment 2 ρ p / 2

noncomputable def NavierStokes.IntegratedMeanBalances.axialDefect (axialFlux gr : MeanField) (p : MeanParameter) : ℝ

Axial defect, given by radialMoment 1 axialFlux p - (1 / 2 : ℝ) * radialMoment 2 gr p.

Equations

• NavierStokes.IntegratedMeanBalances.axialDefect axialFlux gr p = NavierStokes.IntegratedMeanBalances.radialMoment 1 axialFlux p - 1 / 2 * NavierStokes.IntegratedMeanBalances.radialMoment 2 gr p

theorem NavierStokes.IntegratedMeanBalances.flux_pressure_moment {a b : ℝ} {axialFlux pressure gr ρ : MeanField} (hz : SmoothShell a b axialFlux) (hp : SmoothShell a b pressure) (hg : SmoothShell a b gr) (hρ : SmoothShell a b ρ) (hderiv : ∀ (r : ℝ) (p : MeanParameter), deriv (fun (s : ℝ) => pressure (s, p)) r = gr (r, p) - ρ (r, p) * pressureTotal gr p) : (radialMoment 1 fun (x : ℝ × MeanParameter) => axialFlux x + pressure x) = fun (p : MeanParameter) => axialDefect axialFlux gr p + pressureCoefficient ρ p * pressureTotal gr p

theorem NavierStokes.IntegratedMeanBalances.integrated_axial_reconstructed {a b : ℝ} (ε : ℝ) {γ radialFlux axialFlux pressure virtualFlux gr ρ : MeanField} (hγ : SmoothShell a b γ) (hr : SmoothShell a b radialFlux) (hz : SmoothShell a b axialFlux) (hp : SmoothShell a b pressure) (hT : SmoothShell a b virtualFlux) (hg : SmoothShell a b gr) (hρ : SmoothShell a b ρ) (hmass : radialMoment 1 γ = 0) (hderiv : ∀ (r : ℝ) (p : MeanParameter), deriv (fun (s : ℝ) => pressure (s, p)) r = gr (r, p) - ρ (r, p) * pressureTotal gr p) (p : MeanParameter) : radialMoment 1 (axialBalance ε γ radialFlux axialFlux pressure virtualFlux) p = ε * (fderiv ℝ (fun (q : MeanParameter) => axialDefect axialFlux gr q + pressureCoefficient ρ q * pressureTotal gr q) p) (0, 1)

The pressure coefficient stays inside the actual axial derivative, exactly as in (34); it may vary with both slow parameters.

Restriction to the physical positive radial half-line

theorem NavierStokes.IntegratedMeanBalances.zero_of_not_mem_interval {a b r : ℝ} {f : ℝ → ℝ} (hs : Function.support f ⊆ Set.Icc a b) (hr : r ∉ Set.Icc a b) : f r = 0

theorem NavierStokes.IntegratedMeanBalances.deriv_support_interval {a b : ℝ} {f : ℝ → ℝ} (hs : Function.support f ⊆ Set.Icc a b) : Function.support (deriv f) ⊆ Set.Icc a b

theorem NavierStokes.IntegratedMeanBalances.radialDivergence_supported {a b : ℝ} {f : ℝ → ℝ} (hs : Function.support f ⊆ Set.Icc a b) (c : ℝ) : Function.support (radialDivergence c f) ⊆ Set.Icc a b

theorem NavierStokes.IntegratedMeanBalances.angularViscosity_supported {a b : ℝ} {f : ℝ → ℝ} (hs : Function.support f ⊆ Set.Icc a b) : Function.support (angularRadialViscosity f) ⊆ Set.Icc a b

theorem NavierStokes.IntegratedMeanBalances.axialViscosity_supported {a b : ℝ} {f : ℝ → ℝ} (hs : Function.support f ⊆ Set.Icc a b) : Function.support (axialRadialViscosity f) ⊆ Set.Icc a b

theorem NavierStokes.IntegratedMeanBalances.SmoothShell.slice_support {a b : ℝ} {F : MeanField} (hF : SmoothShell a b F) (p : MeanParameter) : (Function.support fun (r : ℝ) => F (r, p)) ⊆ Set.Icc a b

theorem NavierStokes.IntegratedMeanBalances.SmoothShell.zero_of_not_mem {a b : ℝ} {F : MeanField} (hF : SmoothShell a b F) {x : MeanPoint} (hx : x.1 ∉ Set.Icc a b) : F x = 0

theorem NavierStokes.IntegratedMeanBalances.angularBalance_supported {a b : ℝ} (ε : ℝ) {v radialFlux axialFlux virtualFlux : MeanField} (hv : SmoothShell a b v) (hr : SmoothShell a b radialFlux) (hz : SmoothShell a b axialFlux) (hT : SmoothShell a b virtualFlux) : RadialAlias.RadiallySupported a b (angularBalance ε v radialFlux axialFlux virtualFlux)

theorem NavierStokes.IntegratedMeanBalances.axialBalance_supported {a b : ℝ} (ε : ℝ) {γ radialFlux axialFlux pressure virtualFlux : MeanField} (hγ : SmoothShell a b γ) (hr : SmoothShell a b radialFlux) (hz : SmoothShell a b axialFlux) (hp : SmoothShell a b pressure) (hT : SmoothShell a b virtualFlux) : RadialAlias.RadiallySupported a b (axialBalance ε γ radialFlux axialFlux pressure virtualFlux)

theorem NavierStokes.IntegratedMeanBalances.positive_radialMoment {a b : ℝ} (ha : 0 < a) {F : MeanField} (hs : RadialAlias.RadiallySupported a b F) (n : ℕ) (p : MeanParameter) : ∫ (r : ℝ) in Set.Ioi 0, r ^ n * F (r, p) = radialMoment n F p

theorem NavierStokes.IntegratedMeanBalances.integrated_angular_positive {a b : ℝ} (ha : 0 < a) (ε : ℝ) {v radialFlux axialFlux virtualFlux : MeanField} (hv : SmoothShell a b v) (hr : SmoothShell a b radialFlux) (hz : SmoothShell a b axialFlux) (hT : SmoothShell a b virtualFlux) (hmass : radialMoment 2 v = 0) (p : MeanParameter) : ∫ (r : ℝ) in Set.Ioi 0, r ^ 2 * angularBalance ε v radialFlux axialFlux virtualFlux (r, p) = ε * (fderiv ℝ (radialMoment 2 axialFlux) p) (0, 1)

theorem NavierStokes.IntegratedMeanBalances.integrated_axial_positive {a b : ℝ} (ha : 0 < a) (ε : ℝ) {γ radialFlux axialFlux pressure virtualFlux gr ρ : MeanField} (hγ : SmoothShell a b γ) (hr : SmoothShell a b radialFlux) (hz : SmoothShell a b axialFlux) (hp : SmoothShell a b pressure) (hT : SmoothShell a b virtualFlux) (hg : SmoothShell a b gr) (hρ : SmoothShell a b ρ) (hmass : radialMoment 1 γ = 0) (hderiv : ∀ (r : ℝ) (p : MeanParameter), deriv (fun (s : ℝ) => pressure (s, p)) r = gr (r, p) - ρ (r, p) * pressureTotal gr p) (p : MeanParameter) : ∫ (r : ℝ) in Set.Ioi 0, r * axialBalance ε γ radialFlux axialFlux pressure virtualFlux (r, p) = ε * (fderiv ℝ (fun (q : MeanParameter) => axialDefect axialFlux gr q + pressureCoefficient ρ q * pressureTotal gr q) p) (0, 1)

The actual pressure primitive (33), without a supplied derivative identity

theorem NavierStokes.IntegratedMeanBalances.constructed_pressure_moment {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : ℝ × ℝ) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (hper : PressureStream.TorusPeriodicLift f) (s : S) : (moment 1 fun (r : ℝ) => PressureStream.torusAverage (PressureStream.meanPressure d a b M hab v f) (r, s)) = (-(1 / 2) * moment 2 fun (r : ℝ) => PressureStream.torusAverage f (r, s)) + moment 2 (PressureStream.rho a b hab) / 2 * PressureStream.pressureMass f s

Exact moment of the constructed compact pressure, including its normalized mean correction. The derivative used in the proof is a theorem of the actual physical transport integral, not an assumption here.

noncomputable def NavierStokes.IntegratedMeanBalances.reconstructedMeanPressure (d a b M : ℝ) (hab : a < b) (v : ℝ × ℝ) (f : PressureStream.Lift MeanParameter → ℝ) : MeanField

Reconstructed mean pressure, given by PressureStream.torusAverage (PressureStream.meanPressure d a b M hab v f).

Equations

• NavierStokes.IntegratedMeanBalances.reconstructedMeanPressure d a b M hab v f = NavierStokes.PressureStream.torusAverage (NavierStokes.PressureStream.meanPressure d a b M hab v f)

noncomputable def NavierStokes.IntegratedMeanBalances.averagedRadialSource (f : PressureStream.Lift MeanParameter → ℝ) : MeanField

Averaged radial source, given by PressureStream.torusAverage f.

Equations

• NavierStokes.IntegratedMeanBalances.averagedRadialSource f = NavierStokes.PressureStream.torusAverage f

noncomputable def NavierStokes.IntegratedMeanBalances.normalizedMeanDensity (a b : ℝ) (hab : a < b) (x : MeanPoint) : ℝ

Normalized mean density, given by PressureStream.rho a b hab x.1.

Equations

• NavierStokes.IntegratedMeanBalances.normalizedMeanDensity a b hab x = NavierStokes.PressureStream.rho a b hab x.1

theorem NavierStokes.IntegratedMeanBalances.averagedRadialSource_shell {a b : ℝ} {f : PressureStream.Lift MeanParameter → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) : SmoothShell a b (averagedRadialSource f)

theorem NavierStokes.IntegratedMeanBalances.reconstructedMeanPressure_shell {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : ℝ × ℝ) {f : PressureStream.Lift MeanParameter → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) : SmoothShell a b (reconstructedMeanPressure d a b M hab v f)

theorem NavierStokes.IntegratedMeanBalances.normalizedMeanDensity_shell (a b : ℝ) (hab : a < b) : SmoothShell a b (normalizedMeanDensity a b hab)

theorem NavierStokes.IntegratedMeanBalances.constructed_pressure_deriv {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : ℝ × ℝ) {f : PressureStream.Lift MeanParameter → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (hper : PressureStream.TorusPeriodicLift f) (r : ℝ) (p : MeanParameter) : deriv (fun (s : ℝ) => reconstructedMeanPressure d a b M hab v f (s, p)) r = averagedRadialSource f (r, p) - normalizedMeanDensity a b hab (r, p) * pressureTotal (averagedRadialSource f) p

theorem NavierStokes.IntegratedMeanBalances.integrated_axial_constructed_pressure {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (ε : ℝ) (v : ℝ × ℝ) {f : PressureStream.Lift MeanParameter → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (hper : PressureStream.TorusPeriodicLift f) {γ radialFlux axialFlux virtualFlux : MeanField} (hγ : SmoothShell a b γ) (hr : SmoothShell a b radialFlux) (hz : SmoothShell a b axialFlux) (hT : SmoothShell a b virtualFlux) (hmass : radialMoment 1 γ = 0) (p : MeanParameter) : ∫ (r : ℝ) in Set.Ioi 0, r * axialBalance ε γ radialFlux axialFlux (reconstructedMeanPressure d a b M hab v f) virtualFlux (r, p) = ε * (fderiv ℝ (fun (q : MeanParameter) => axialDefect axialFlux (averagedRadialSource f) q + pressureCoefficient (normalizedMeanDensity a b hab) q * pressureTotal (averagedRadialSource f) q) p) (0, 1)

The second identity of (34) with pressure supplied by the actual compact primitive (33). No pressure moment or pressure derivative identity is assumed.