Documentation

LeanPool.NavierStokesAndEuler.NavierStokes.ProfileHistories

Genuine smooth profile histories #

The histories are actual integrals of jointly smooth profiles. Their parameter derivatives and radial identities are derived from differentiation under the integral and the fundamental theorem of calculus, rather than supplied as independent history data.

Exact radial stress identities #

This file verifies the algebra and radial calculus in equations (6)--(9) of the candidate manuscript. Parameter derivatives are supplied as independent radial functions, with their requisite radial derivative identities stated explicitly. No existence of the candidate profiles or estimates for them is asserted.

noncomputable def NavierStokes.StressAlgebra.axialExponent (h : ℝ) :

The axial scaling exponent from the manuscript.

Equations

NavierStokes.StressAlgebra.axialExponent h = 1 / 2 - h

Instances For

noncomputable def NavierStokes.StressAlgebra.velocityExponent (h : ℝ) :

The velocity scaling exponent from the manuscript.

Equations

NavierStokes.StressAlgebra.velocityExponent h = 1 / 2 + h

Instances For

def NavierStokes.StressAlgebra.coordinateFactor (η : ℝ) :

The coordinate factor d = 1 - η².

Equations

NavierStokes.StressAlgebra.coordinateFactor η = 1 - η ^ 2

Instances For

noncomputable def NavierStokes.StressAlgebra.angularSource (h η x W U H Hx Hη : ℝ) :

H S_q, with radial derivatives written explicitly instead of logarithms.

Equations

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

Instances For

noncomputable def NavierStokes.StressAlgebra.axialSource (h η x W U Ux Uη P Px Pη : ℝ) :

S_n, with dot U = x U_x and dot P = x P_x.

Equations

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

Instances For

noncomputable def NavierStokes.StressAlgebra.angularPrimitive (h η : ℝ) (W H I Iη J Jη : ℝ → ℝ) (x : ℝ) :

The numerator of the angular integrated identity (9).

Equations

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

Instances For

noncomputable def NavierStokes.StressAlgebra.axialPrimitive (h η : ℝ) (W U M Mη S Sη P Pη : ℝ → ℝ) (x : ℝ) :

The numerator of the axial integrated identity (9).

Equations

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

Instances For

theorem NavierStokes.StressAlgebra.angular_derivative_algebra (h η x W Wx U Uη H Hx Hη : ℝ) (hW : W + x * Wx = 1 - 2 * axialExponent h * η * U - coordinateFactor η * Uη) :

-((W + x * Wx) * H + x * W * Hx) + (1 - h) * H - axialExponent h * η * Hη - coordinateFactor η * (Uη * H + U * Hη) + 2 * (h - axialExponent h) * η * (U * H) = angularSource h η x W U H Hx Hη

The angular integration-by-parts cancellation, as an exact polynomial identity.

theorem NavierStokes.StressAlgebra.axial_derivative_algebra (h η x W Wx U Ux Uη E Eη P Px Pη Pηx : ℝ) (hW : W + x * Wx = 1 - 2 * axialExponent h * η * U - coordinateFactor η * Uη) (hP : x * Px = E ^ 2 / 2) (hPη : x * Pηx = E * Eη) :

-((W + x * Wx) * U + x * W * Ux) + axialExponent h * (U - η * Uη) + 4 * h * η * (U ^ 2 - E ^ 2 / 2) - coordinateFactor η * (2 * U * Uη - E * Eη) + (4 * velocityExponent h * η * P - coordinateFactor η * Pη) + x * (4 * velocityExponent h * η * Px - coordinateFactor η * Pηx) = axialSource h η x W U Ux Uη P Px Pη

The axial integration-by-parts cancellation, including both pressure identities.

theorem NavierStokes.StressAlgebra.angularPrimitive_hasDerivAt (h η x : ℝ) (W H I Iη J Jη : ℝ → ℝ) (Wx Hx U Uη Hη : ℝ) (hWderiv : HasDerivAt W Wx x) (hH : HasDerivAt H Hx x) (hI : HasDerivAt I (H x) x) (hIη : HasDerivAt Iη Hη x) (hJ : HasDerivAt J (U * H x) x) (hJη : HasDerivAt Jη (Uη * H x + U * Hη) x) (hW : W x + x * Wx = 1 - 2 * axialExponent h * η * U - coordinateFactor η * Uη) :

HasDerivAt (angularPrimitive h η W H I Iη J Jη) (angularSource h η x (W x) U (H x) Hx Hη) x

Genuine radial differentiation of the angular primitive. The moment hypotheses are precisely I_x = H, (I_η)_x = H_η, J_x = UH, and (J_η)_x = U_ηH + UH_η.

theorem NavierStokes.StressAlgebra.axialPrimitive_hasDerivAt (h η x : ℝ) (W U M Mη S Sη P Pη : ℝ → ℝ) (Wx Ux Uη E Eη Px Pηx : ℝ) (hWderiv : HasDerivAt W Wx x) (hU : HasDerivAt U Ux x) (hM : HasDerivAt M (U x) x) (hMη : HasDerivAt Mη Uη x) (hS : HasDerivAt S (U x ^ 2 - E ^ 2 / 2) x) (hSη : HasDerivAt Sη (2 * U x * Uη - E * Eη) x) (hPderiv : HasDerivAt P Px x) (hPηderiv : HasDerivAt Pη Pηx x) (hW : W x + x * Wx = 1 - 2 * axialExponent h * η * U x - coordinateFactor η * Uη) (hP : x * Px = E ^ 2 / 2) (hPη : x * Pηx = E * Eη) :

HasDerivAt (axialPrimitive h η W U M Mη S Sη P Pη) (axialSource h η x (W x) (U x) Ux Uη (P x) Px (Pη x)) x

Genuine radial differentiation of the axial primitive. In addition to the moment identities this uses x P_x = E²/2 and its η derivative.

structure NavierStokes.StressAlgebra.AngularMomentData (h η X : ℝ) :

Data for the angular integrated identity on a specified closed radial interval. The fields are differential and initial conditions, not an assumed integral identity.

W : ℝ → ℝ
W of AngularMomentData, of type ℝ → ℝ.
Wx : ℝ → ℝ
Wx of AngularMomentData, of type ℝ → ℝ.
H : ℝ → ℝ
H of AngularMomentData, of type ℝ → ℝ.
Hx : ℝ → ℝ
Hx of AngularMomentData, of type ℝ → ℝ.
Hη : ℝ → ℝ
Hη of AngularMomentData, of type ℝ → ℝ.
U : ℝ → ℝ
U of AngularMomentData, of type ℝ → ℝ.
Uη : ℝ → ℝ
Uη of AngularMomentData, of type ℝ → ℝ.
I : ℝ → ℝ
I of AngularMomentData, of type ℝ → ℝ.
Iη : ℝ → ℝ
Iη of AngularMomentData, of type ℝ → ℝ.
J : ℝ → ℝ
J of AngularMomentData, of type ℝ → ℝ.
Jη : ℝ → ℝ
Jη of AngularMomentData, of type ℝ → ℝ.
W_deriv (x : ℝ) : x ∈ Set.uIcc 0 X → HasDerivAt self.W (self.Wx x) x
H_deriv (x : ℝ) : x ∈ Set.uIcc 0 X → HasDerivAt self.H (self.Hx x) x
I_deriv (x : ℝ) : x ∈ Set.uIcc 0 X → HasDerivAt self.I (self.H x) x
Iη_deriv (x : ℝ) : x ∈ Set.uIcc 0 X → HasDerivAt self.Iη (self.Hη x) x
J_deriv (x : ℝ) : x ∈ Set.uIcc 0 X → HasDerivAt self.J (self.U x * self.H x) x
Jη_deriv (x : ℝ) : x ∈ Set.uIcc 0 X → HasDerivAt self.Jη (self.Uη x * self.H x + self.U x * self.Hη x) x
W_balance (x : ℝ) : x ∈ Set.uIcc 0 X → self.W x + x * self.Wx x = 1 - 2 * axialExponent h * η * self.U x - coordinateFactor η * self.Uη x
I_zero : self.I 0 = 0
Iη_zero : self.Iη 0 = 0
J_zero : self.J 0 = 0
Jη_zero : self.Jη 0 = 0

Instances For

theorem NavierStokes.StressAlgebra.angular_integrated_identity {h η X : ℝ} (p : AngularMomentData h η X) (hint : IntervalIntegrable (fun (x : ℝ) => angularSource h η x (p.W x) (p.U x) (p.H x) (p.Hx x) (p.Hη x)) MeasureTheory.volume 0 X) :

∫ (x : ℝ) in 0..X, angularSource h η x (p.W x) (p.U x) (p.H x) (p.Hx x) (p.Hη x) = angularPrimitive h η p.W p.H p.I p.Iη p.J p.Jη X

The first integral formula in the proof of Lemma 3.3, derived by the fundamental theorem of calculus from explicit differential moment conditions.

structure NavierStokes.StressAlgebra.AxialMomentData (h η X : ℝ) :

Differential and initial data required for the axial integrated identity.

W : ℝ → ℝ
W of AxialMomentData, of type ℝ → ℝ.
Wx : ℝ → ℝ
Wx of AxialMomentData, of type ℝ → ℝ.
U : ℝ → ℝ
U of AxialMomentData, of type ℝ → ℝ.
Ux : ℝ → ℝ
Ux of AxialMomentData, of type ℝ → ℝ.
Uη : ℝ → ℝ
Uη of AxialMomentData, of type ℝ → ℝ.
E : ℝ → ℝ
E of AxialMomentData, of type ℝ → ℝ.
Eη : ℝ → ℝ
Eη of AxialMomentData, of type ℝ → ℝ.
P : ℝ → ℝ
P of AxialMomentData, of type ℝ → ℝ.
Px : ℝ → ℝ
Px of AxialMomentData, of type ℝ → ℝ.
Pη : ℝ → ℝ
Pη of AxialMomentData, of type ℝ → ℝ.
Pηx : ℝ → ℝ
Pηx of AxialMomentData, of type ℝ → ℝ.
M : ℝ → ℝ
M of AxialMomentData, of type ℝ → ℝ.
Mη : ℝ → ℝ
Mη of AxialMomentData, of type ℝ → ℝ.
S : ℝ → ℝ
Parameter S of AxialMomentData, of type ℝ → ℝ.
Sη : ℝ → ℝ
Sη of AxialMomentData, of type ℝ → ℝ.
W_deriv (x : ℝ) : x ∈ Set.uIcc 0 X → HasDerivAt self.W (self.Wx x) x
U_deriv (x : ℝ) : x ∈ Set.uIcc 0 X → HasDerivAt self.U (self.Ux x) x
M_deriv (x : ℝ) : x ∈ Set.uIcc 0 X → HasDerivAt self.M (self.U x) x
Mη_deriv (x : ℝ) : x ∈ Set.uIcc 0 X → HasDerivAt self.Mη (self.Uη x) x
S_deriv (x : ℝ) : x ∈ Set.uIcc 0 X → HasDerivAt self.S (self.U x ^ 2 - self.E x ^ 2 / 2) x
Sη_deriv (x : ℝ) : x ∈ Set.uIcc 0 X → HasDerivAt self.Sη (2 * self.U x * self.Uη x - self.E x * self.Eη x) x
P_deriv (x : ℝ) : x ∈ Set.uIcc 0 X → HasDerivAt self.P (self.Px x) x
Pη_deriv (x : ℝ) : x ∈ Set.uIcc 0 X → HasDerivAt self.Pη (self.Pηx x) x
W_balance (x : ℝ) : x ∈ Set.uIcc 0 X → self.W x + x * self.Wx x = 1 - 2 * axialExponent h * η * self.U x - coordinateFactor η * self.Uη x
pressure_balance (x : ℝ) : x ∈ Set.uIcc 0 X → x * self.Px x = self.E x ^ 2 / 2
pressure_η_balance (x : ℝ) : x ∈ Set.uIcc 0 X → x * self.Pηx x = self.E x * self.Eη x
M_zero : self.M 0 = 0
Mη_zero : self.Mη 0 = 0
S_zero : self.S 0 = 0
Sη_zero : self.Sη 0 = 0

Instances For

theorem NavierStokes.StressAlgebra.axial_integrated_identity {h η X : ℝ} (p : AxialMomentData h η X) (hint : IntervalIntegrable (fun (x : ℝ) => axialSource h η x (p.W x) (p.U x) (p.Ux x) (p.Uη x) (p.P x) (p.Px x) (p.Pη x)) MeasureTheory.volume 0 X) :

∫ (x : ℝ) in 0..X, axialSource h η x (p.W x) (p.U x) (p.Ux x) (p.Uη x) (p.P x) (p.Px x) (p.Pη x) = axialPrimitive h η p.W p.U p.M p.Mη p.S p.Sη p.P p.Pη X

The second integral formula in Lemma 3.3, including its pressure terms.

theorem NavierStokes.StressAlgebra.angular_integrated_lag {h η X : ℝ} (p : AngularMomentData h η X) (hX : X ≠ 0) (hH : p.H X ≠ 0) (hint : IntervalIntegrable (fun (x : ℝ) => angularSource h η x (p.W x) (p.U x) (p.H x) (p.Hx x) (p.Hη x)) MeasureTheory.volume 0 X) :

(∫ (x : ℝ) in 0..X, angularSource h η x (p.W x) (p.U x) (p.H x) (p.Hx x) (p.Hη x)) / (X * p.H X) = -p.W X + ((1 - h) * p.I X - axialExponent h * η * p.Iη X - coordinateFactor η * p.Jη X + 2 * (h - axialExponent h) * η * p.J X) / (X * p.H X)

The angular formula (9) after division by the regular integrating factor. The left side is the regular primitive definition of Q_s.

theorem NavierStokes.StressAlgebra.axial_integrated_lag {h η X : ℝ} (p : AxialMomentData h η X) (hX : X ≠ 0) (hint : IntervalIntegrable (fun (x : ℝ) => axialSource h η x (p.W x) (p.U x) (p.Ux x) (p.Uη x) (p.P x) (p.Px x) (p.Pη x)) MeasureTheory.volume 0 X) :

(∫ (x : ℝ) in 0..X, axialSource h η x (p.W x) (p.U x) (p.Ux x) (p.Uη x) (p.P x) (p.Px x) (p.Pη x)) / X = -p.W X * p.U X + axialExponent h * (p.M X - η * p.Mη X) / X + (4 * h * η * p.S X - coordinateFactor η * p.Sη X) / X + 4 * velocityExponent h * η * p.P X - coordinateFactor η * p.Pη X

The axial formula (9) after division by its regular integrating factor. The left side is the regular primitive definition of N_s.

theorem NavierStokes.StressAlgebra.angular_source_logarithmic_form (h η x W U H Hx Hη : ℝ) (hH : H ≠ 0) :

H * (-W * (x * Hx / H) - h * (1 - 2 * η * U) - (axialExponent h * η + coordinateFactor η * U) * (Hη / H)) = angularSource h η x W U H Hx Hη

The source written with logarithmic derivatives agrees with H S_q. Its use for actual logarithms requires the usual nonvanishing profile conditions.

theorem NavierStokes.StressAlgebra.angular_lag_primitive_iff (H Q : ℝ → ℝ) (x Hx Qx Sq : ℝ) (hH : HasDerivAt H Hx x) (hQ : HasDerivAt Q Qx x) (hHne : H x ≠ 0) :

HasDerivAt (fun (y : ℝ) => y * H y * Q y) (H x * Sq) x ↔ x * Qx + (1 + x * Hx / H x) * Q x = Sq

Multiplying (6)'s angular lag equation by its integrating factor gives the primitive equation. This equivalence uses genuine derivatives of H and Q.

theorem NavierStokes.StressAlgebra.axial_lag_primitive_iff (N : ℝ → ℝ) (x Nx Sn : ℝ) (hN : HasDerivAt N Nx x) :

HasDerivAt (fun (y : ℝ) => y * N y) Sn x ↔ x * Nx + N x = Sn

The axial lag equation's integrating factor is x.

theorem NavierStokes.StressAlgebra.stressFree_angular_lag_algebra (x L φ φx φxx : ℝ) (hφ : φ ≠ 0) :

x * (-2 * L * (φxx * φ - φx ^ 2) / φ ^ 2) + (2 + x * φx / φ) * (-2 * L * φx / φ) = -2 * L * (x * φxx + 2 * φx) / φ

The angular stress-free substitution from (7) yields exactly the radial second-order expression in (8). Here φx and φxx denote radial derivatives.

theorem NavierStokes.StressAlgebra.stressFree_axial_lag_algebra (x L Ux Uxx : ℝ) :

x * (-2 * L * Uxx) + -2 * L * Ux = -2 * L * (x * Uxx + Ux)

The axial stress-free substitution from (7) yields its expression in (8).

theorem NavierStokes.StressAlgebra.axial_stress_coefficient (x R E L Ns Ux : ℝ) (hR : R ≠ 0) (hE : E ≠ 0) (hL : L ≠ 0) :

E / R * (x * Ns / (L * E) + 2 * x * Ux / E) = x / R * (Ns / L + 2 * Ux)

The axial coefficient of F (p_s - s) in (7), with the positive viscous primitive 2 x U_x / R made explicit. Here R is the radial factor sqrt(2x).

theorem NavierStokes.StressAlgebra.angular_stress_coefficient (x R E L Qs Ex : ℝ) (hR : R ≠ 0) (hE : E ≠ 0) (hL : L ≠ 0) :

E / R * (x * Qs / L - (1 - 2 * x * Ex / E)) = E / R * (x * Qs / L) + (2 * x * Ex - E) / R

The angular coefficient of (7), with its radial viscous primitive exposed. This verifies the sign of the subtraction of a = 1 - 2 dot(E)/E.

@[reducible, inline]

abbrev NavierStokes.ProfileHistories.Point :

Point: an abbreviation for ℝ × ℝ.

Equations

NavierStokes.ProfileHistories.Point = (ℝ × ℝ)

Instances For

@[reducible, inline]

abbrev NavierStokes.ProfileHistories.Field :

Field: an abbreviation for Point → ℝ.

Equations

NavierStokes.ProfileHistories.Field = (NavierStokes.ProfileHistories.Point → ℝ)

Instances For

structure NavierStokes.ProfileHistories.RadialDomain :

An open profile domain containing every radial segment from the axis to one of its points. Open rectangles centered radially at zero are examples.

carrier : Set Point
Carrier of RadialDomain, of type Set Point.
isOpen : IsOpen self.carrier
scale_mem (p : Point) : p ∈ self.carrier → ∀ t ∈ Set.Icc 0 1, (t * p.1, p.2) ∈ self.carrier

Instances For

def NavierStokes.ProfileHistories.RadialDomain.rectangle (R a b : ℝ) :

A concrete open rectangle meeting the axis. Positivity of R is needed only to make it nonempty, not for the radial stability proof.

Equations

NavierStokes.ProfileHistories.RadialDomain.rectangle R a b = { carrier := Set.Ioo (-R) R ×ˢ Set.Ioo a b, isOpen := ⋯, scale_mem := ⋯ }

Instances For

noncomputable def NavierStokes.ProfileHistories.radialPartial (F : Field) (p : Point) :

Radial partial, given by fderiv ℝ F p (1, 0).

Equations

NavierStokes.ProfileHistories.radialPartial F p = (fderiv ℝ F p) (1, 0)

Instances For

noncomputable def NavierStokes.ProfileHistories.parameterPartial (F : Field) (p : Point) :

Parameter partial, given by fderiv ℝ F p (0, 1).

Equations

NavierStokes.ProfileHistories.parameterPartial F p = (fderiv ℝ F p) (0, 1)

Instances For

theorem NavierStokes.ProfileHistories.radialPartial_hasDerivAt (D : RadialDomain) {F : Field} (hF : ContDiffOn ℝ (↑⊤) F D.carrier) {p : Point} (hp : p ∈ D.carrier) :

HasDerivAt (fun (x : ℝ) => F (x, p.2)) (radialPartial F p) p.1

theorem NavierStokes.ProfileHistories.parameterPartial_hasDerivAt (D : RadialDomain) {F : Field} (hF : ContDiffOn ℝ (↑⊤) F D.carrier) {p : Point} (hp : p ∈ D.carrier) :

HasDerivAt (fun (η : ℝ) => F (p.1, η)) (parameterPartial F p) p.2

theorem NavierStokes.ProfileHistories.radialPartial_smooth (D : RadialDomain) {F : Field} (hF : ContDiffOn ℝ (↑⊤) F D.carrier) :

ContDiffOn ℝ (↑⊤) (radialPartial F) D.carrier

theorem NavierStokes.ProfileHistories.parameterPartial_smooth (D : RadialDomain) {F : Field} (hF : ContDiffOn ℝ (↑⊤) F D.carrier) :

ContDiffOn ℝ (↑⊤) (parameterPartial F) D.carrier

theorem NavierStokes.ProfileHistories.compact_parameter_jet_continuous {s : Set Point} {G : Point → ℝ → ℝ} (hG : ∀ p ∈ s, ∀ t ∈ Set.Icc 0 1, ContDiffAt ℝ (↑⊤) (fun (z : Point × ℝ) => G z.1 z.2) (p, t)) (k : ℕ) :

ContinuousOn (fun (z : Point × ℝ) => SmoothParameterIntegral.jet G k z.1 z.2) (s ×ˢ Set.Icc 0 1)

theorem NavierStokes.ProfileHistories.compact_parameter_integral_smooth {s : Set Point} {G : Point → ℝ → ℝ} (hs : IsOpen s) (hG : ∀ p ∈ s, ∀ t ∈ Set.Icc 0 1, ContDiffAt ℝ (↑⊤) (fun (z : Point × ℝ) => G z.1 z.2) (p, t)) :

ContDiffOn ℝ (↑⊤) (fun (p : Point) => ∫ (t : ℝ) in 0..1, G p t) s

theorem NavierStokes.ProfileHistories.compact_parameter_fderiv_continuous {s : Set Point} {G : Point → ℝ → ℝ} (hG : ∀ p ∈ s, ∀ t ∈ Set.Icc 0 1, ContDiffAt ℝ (↑⊤) (fun (z : Point × ℝ) => G z.1 z.2) (p, t)) :

ContinuousOn (fun (z : Point × ℝ) => fderiv ℝ (fun (p : Point) => G p z.2) z.1) (s ×ˢ Set.Icc 0 1)

theorem NavierStokes.ProfileHistories.compact_parameter_integral_hasFDerivAt {s : Set Point} {G : Point → ℝ → ℝ} (hs : IsOpen s) (hG : ∀ p ∈ s, ∀ t ∈ Set.Icc 0 1, ContDiffAt ℝ (↑⊤) (fun (z : Point × ℝ) => G z.1 z.2) (p, t)) {p : Point} (hp : p ∈ s) :

HasFDerivAt (fun (q : Point) => ∫ (t : ℝ) in 0..1, G q t) (∫ (t : ℝ) in 0..1, fderiv ℝ (fun (q : Point) => G q t) p) p

The derivative of the compact parameter integral is the integral of the genuine parameter derivative. Joint smoothness supplies the local majorant.

noncomputable def NavierStokes.ProfileHistories.average (F : Field) (p : Point) :

Regular radial average, including its value at the axis.

Equations

NavierStokes.ProfileHistories.average F p = ∫ (t : ℝ) in 0..1, F (t * p.1, p.2)

Instances For

noncomputable def NavierStokes.ProfileHistories.primitive (F : Field) (p : Point) :

Actual radial history from the axis.

Equations

NavierStokes.ProfileHistories.primitive F p = ∫ (x : ℝ) in 0..p.1, F (x, p.2)

Instances For

theorem NavierStokes.ProfileHistories.primitive_eq_mul_average (F : Field) (p : Point) :

primitive F p = p.1 * average F p

theorem NavierStokes.ProfileHistories.average_at_axis (F : Field) (η : ℝ) :

average F (0, η) = F (0, η)

theorem NavierStokes.ProfileHistories.primitive_at_axis (F : Field) (η : ℝ) :

primitive F (0, η) = 0

theorem NavierStokes.ProfileHistories.average_integrand_smooth (D : RadialDomain) {F : Field} (hF : ContDiffOn ℝ (↑⊤) F D.carrier) (p : Point) (hp : p ∈ D.carrier) (t : ℝ) (ht : t ∈ Set.Icc 0 1) :

ContDiffAt ℝ (↑⊤) (fun (z : Point × ℝ) => F (z.2 * z.1.1, z.1.2)) (p, t)

theorem NavierStokes.ProfileHistories.average_smooth (D : RadialDomain) {F : Field} (hF : ContDiffOn ℝ (↑⊤) F D.carrier) :

ContDiffOn ℝ (↑⊤) (average F) D.carrier

theorem NavierStokes.ProfileHistories.primitive_smooth (D : RadialDomain) {F : Field} (hF : ContDiffOn ℝ (↑⊤) F D.carrier) :

ContDiffOn ℝ (↑⊤) (primitive F) D.carrier

theorem NavierStokes.ProfileHistories.RadialDomain.segment_mem (D : RadialDomain) {p : Point} (hp : p ∈ D.carrier) {x : ℝ} (hx : x ∈ Set.uIcc 0 p.1) :

(x, p.2) ∈ D.carrier

theorem NavierStokes.ProfileHistories.radial_slice_continuous (D : RadialDomain) {F : Field} (hF : ContDiffOn ℝ (↑⊤) F D.carrier) (η : ℝ) :

ContinuousOn (fun (x : ℝ) => F (x, η)) {x : ℝ | (x, η) ∈ D.carrier}

theorem NavierStokes.ProfileHistories.radial_slice_intervalIntegrable (D : RadialDomain) {F : Field} (hF : ContDiffOn ℝ (↑⊤) F D.carrier) {p : Point} (hp : p ∈ D.carrier) :

IntervalIntegrable (fun (x : ℝ) => F (x, p.2)) MeasureTheory.volume 0 p.1

theorem NavierStokes.ProfileHistories.primitive_hasDerivAt (D : RadialDomain) {F : Field} (hF : ContDiffOn ℝ (↑⊤) F D.carrier) {p : Point} (hp : p ∈ D.carrier) :

HasDerivAt (fun (x : ℝ) => primitive F (x, p.2)) (F p) p.1

The history has its defining integrand as genuine radial derivative.

theorem NavierStokes.ProfileHistories.radialPartial_primitive (D : RadialDomain) {F : Field} (hF : ContDiffOn ℝ (↑⊤) F D.carrier) {p : Point} (hp : p ∈ D.carrier) :

radialPartial (primitive F) p = F p

theorem NavierStokes.ProfileHistories.compact_parameter_integral_parameterPartial {s : Set Point} {G : Point → ℝ → ℝ} (hs : IsOpen s) (hG : ∀ p ∈ s, ∀ t ∈ Set.Icc 0 1, ContDiffAt ℝ (↑⊤) (fun (z : Point × ℝ) => G z.1 z.2) (p, t)) {p : Point} (hp : p ∈ s) :

parameterPartial (fun (q : Point) => ∫ (t : ℝ) in 0..1, G q t) p = ∫ (t : ℝ) in 0..1, parameterPartial (fun (q : Point) => G q t) p

theorem NavierStokes.ProfileHistories.parameterPartial_average (D : RadialDomain) {F : Field} (hF : ContDiffOn ℝ (↑⊤) F D.carrier) {p : Point} (hp : p ∈ D.carrier) :

parameterPartial (average F) p = average (parameterPartial F) p

Parameter differentiation commutes with the regular average, including at X=0.

theorem NavierStokes.ProfileHistories.parameterPartial_primitive (D : RadialDomain) {F : Field} (hF : ContDiffOn ℝ (↑⊤) F D.carrier) {p : Point} (hp : p ∈ D.carrier) :

parameterPartial (primitive F) p = primitive (parameterPartial F) p

The parameter derivative of a history is the actual history of the parameter derivative; no history derivative is assumed.

theorem NavierStokes.ProfileHistories.parameterPartial_primitive_hasDerivAt (D : RadialDomain) {F : Field} (hF : ContDiffOn ℝ (↑⊤) F D.carrier) {p : Point} (hp : p ∈ D.carrier) :

HasDerivAt (fun (x : ℝ) => parameterPartial (primitive F) (x, p.2)) (parameterPartial F p) p.1

Mixed radial/parameter differentiation of an actual history.

theorem NavierStokes.ProfileHistories.parameterPartial_primitive_at_axis (D : RadialDomain) {F : Field} (hF : ContDiffOn ℝ (↑⊤) F D.carrier) {η : ℝ} (hη : (0, η) ∈ D.carrier) :

parameterPartial (primitive F) (0, η) = 0

theorem NavierStokes.ProfileHistories.average_eq_quotient (F : Field) {p : Point} (hX : p.1 ≠ 0) :

average F p = primitive F p / p.1

structure NavierStokes.ProfileHistories.Profiles (D : RadialDomain) :

Smooth profiles and an arbitrary smooth axial pressure normalization. Only local smoothness at the relevant parameter values is required.

f : Field
F of Profiles, of type Field.
U : Field
U of Profiles, of type Field.
f_smooth : ContDiffOn ℝ (↑⊤) self.f D.carrier
U_smooth : ContDiffOn ℝ (↑⊤) self.U D.carrier
pressure0 : ℝ → ℝ
Pressure0 of Profiles, of type ℝ → ℝ.
pressure0_smooth (p : Point) : p ∈ D.carrier → ContDiffAt ℝ (↑⊤) self.pressure0 p.2

Instances For

def NavierStokes.ProfileHistories.Profiles.H {D : RadialDomain} (P : Profiles D) :

H, defined pointwise by 2 * p.1 * P.f p.

Equations

P.H p = 2 * p.1 * P.f p

Instances For

noncomputable def NavierStokes.ProfileHistories.Profiles.E {D : RadialDomain} (P : Profiles D) :

E, defined pointwise by Real.sqrt (2 * p.1) * P.f p.

Equations

P.E p = √(2 * p.1) * P.f p

Instances For

noncomputable def NavierStokes.ProfileHistories.Profiles.Eη {D : RadialDomain} (P : Profiles D) :

Eη, defined pointwise by Real.sqrt (2 * p.1) * parameterPartial P.f p.

Equations

P.Eη p = √(2 * p.1) * NavierStokes.ProfileHistories.parameterPartial P.f p

Instances For

def NavierStokes.ProfileHistories.Profiles.transportDensity {D : RadialDomain} (P : Profiles D) :

Transport density, defined pointwise by P.U p * P.H p.

Equations

P.transportDensity p = P.U p * P.H p

Instances For

def NavierStokes.ProfileHistories.Profiles.energyDensity {D : RadialDomain} (P : Profiles D) :

Energy density, defined pointwise by P.U p ^ 2 - p.1 * P.f p ^ 2.

Equations

P.energyDensity p = P.U p ^ 2 - p.1 * P.f p ^ 2

Instances For

noncomputable def NavierStokes.ProfileHistories.Profiles.M {D : RadialDomain} (P : Profiles D) :

M, given by primitive P.U.

Equations

P.M = NavierStokes.ProfileHistories.primitive P.U

Instances For

noncomputable def NavierStokes.ProfileHistories.Profiles.I {D : RadialDomain} (P : Profiles D) :

I, given by primitive P.H.

Equations

P.I = NavierStokes.ProfileHistories.primitive P.H

Instances For

noncomputable def NavierStokes.ProfileHistories.Profiles.J {D : RadialDomain} (P : Profiles D) :

J, given by primitive P.transportDensity.

Equations

P.J = NavierStokes.ProfileHistories.primitive P.transportDensity

Instances For

noncomputable def NavierStokes.ProfileHistories.Profiles.S {D : RadialDomain} (P : Profiles D) :

S, given by primitive P.energyDensity.

Equations

P.S = NavierStokes.ProfileHistories.primitive P.energyDensity

Instances For

noncomputable def NavierStokes.ProfileHistories.Profiles.Ubar {D : RadialDomain} (P : Profiles D) :

Ubar, given by average P.U.

Equations

P.Ubar = NavierStokes.ProfileHistories.average P.U

Instances For

noncomputable def NavierStokes.ProfileHistories.Profiles.pressure {D : RadialDomain} (P : Profiles D) :

Pressure, defined pointwise by P.pressure0 p.2 + primitive (fun q => P.f q ^ 2) p.

Equations

P.pressure p = P.pressure0 p.2 + NavierStokes.ProfileHistories.primitive (fun (q : NavierStokes.ProfileHistories.Point) => P.f q ^ 2) p

Instances For

noncomputable def NavierStokes.ProfileHistories.Profiles.W {D : RadialDomain} (P : Profiles D) (h : ℝ) :

W, defined pointwise by 1 - 2 * axialExponent h * p.2 * P.Ubar p - coordinateFactor p.2 * average (parameterPartial P.U) p.

Equations

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

Instances For

theorem NavierStokes.ProfileHistories.Profiles.H_smooth {D : RadialDomain} (P : Profiles D) :

ContDiffOn ℝ (↑⊤) P.H D.carrier

theorem NavierStokes.ProfileHistories.Profiles.transportDensity_smooth {D : RadialDomain} (P : Profiles D) :

ContDiffOn ℝ (↑⊤) P.transportDensity D.carrier

theorem NavierStokes.ProfileHistories.Profiles.energyDensity_smooth {D : RadialDomain} (P : Profiles D) :

ContDiffOn ℝ (↑⊤) P.energyDensity D.carrier

theorem NavierStokes.ProfileHistories.Profiles.M_smooth {D : RadialDomain} (P : Profiles D) :

ContDiffOn ℝ (↑⊤) P.M D.carrier

theorem NavierStokes.ProfileHistories.Profiles.I_smooth {D : RadialDomain} (P : Profiles D) :

ContDiffOn ℝ (↑⊤) P.I D.carrier

theorem NavierStokes.ProfileHistories.Profiles.J_smooth {D : RadialDomain} (P : Profiles D) :

ContDiffOn ℝ (↑⊤) P.J D.carrier

theorem NavierStokes.ProfileHistories.Profiles.S_smooth {D : RadialDomain} (P : Profiles D) :

ContDiffOn ℝ (↑⊤) P.S D.carrier

theorem NavierStokes.ProfileHistories.Profiles.Ubar_smooth {D : RadialDomain} (P : Profiles D) :

ContDiffOn ℝ (↑⊤) P.Ubar D.carrier

theorem NavierStokes.ProfileHistories.Profiles.pressure_smooth {D : RadialDomain} (P : Profiles D) :

ContDiffOn ℝ (↑⊤) P.pressure D.carrier

theorem NavierStokes.ProfileHistories.Profiles.W_smooth {D : RadialDomain} (P : Profiles D) (h : ℝ) :

ContDiffOn ℝ (↑⊤) (P.W h) D.carrier

theorem NavierStokes.ProfileHistories.Profiles.Ubar_at_axis {D : RadialDomain} (P : Profiles D) (η : ℝ) :

P.Ubar (0, η) = P.U (0, η)

theorem NavierStokes.ProfileHistories.Profiles.Ubar_eq_mass_quotient {D : RadialDomain} (P : Profiles D) {p : Point} (hX : p.1 ≠ 0) :

P.Ubar p = P.M p / p.1

theorem NavierStokes.ProfileHistories.Profiles.W_formula {D : RadialDomain} (P : Profiles D) (h : ℝ) {p : Point} (hp : p ∈ D.carrier) :

P.W h p = 1 - 2 * StressAlgebra.axialExponent h * p.2 * P.Ubar p - StressAlgebra.coordinateFactor p.2 * parameterPartial P.Ubar p

theorem NavierStokes.ProfileHistories.Profiles.XW_eq_histories {D : RadialDomain} (P : Profiles D) (h : ℝ) (p : Point) :

p.1 * P.W h p = p.1 - 2 * StressAlgebra.axialExponent h * p.2 * P.M p - StressAlgebra.coordinateFactor p.2 * primitive (parameterPartial P.U) p

theorem NavierStokes.ProfileHistories.Profiles.XW_hasDerivAt {D : RadialDomain} (P : Profiles D) (h : ℝ) {p : Point} (hp : p ∈ D.carrier) :

HasDerivAt (fun (x : ℝ) => x * P.W h (x, p.2)) (1 - 2 * StressAlgebra.axialExponent h * p.2 * P.U p - StressAlgebra.coordinateFactor p.2 * parameterPartial P.U p) p.1

The key identity used in both integrations by parts is derived from FTC.

theorem NavierStokes.ProfileHistories.Profiles.W_balance {D : RadialDomain} (P : Profiles D) (h : ℝ) {p : Point} (hp : p ∈ D.carrier) :

P.W h p + p.1 * radialPartial (P.W h) p = 1 - 2 * StressAlgebra.axialExponent h * p.2 * P.U p - StressAlgebra.coordinateFactor p.2 * parameterPartial P.U p

theorem NavierStokes.ProfileHistories.Profiles.parameterPartial_H {D : RadialDomain} (P : Profiles D) {p : Point} (hp : p ∈ D.carrier) :

parameterPartial P.H p = 2 * p.1 * parameterPartial P.f p

theorem NavierStokes.ProfileHistories.Profiles.parameterPartial_transportDensity {D : RadialDomain} (P : Profiles D) {p : Point} (hp : p ∈ D.carrier) :

parameterPartial P.transportDensity p = parameterPartial P.U p * P.H p + P.U p * parameterPartial P.H p

theorem NavierStokes.ProfileHistories.Profiles.parameterPartial_energyDensity {D : RadialDomain} (P : Profiles D) {p : Point} (hp : p ∈ D.carrier) :

parameterPartial P.energyDensity p = 2 * P.U p * parameterPartial P.U p - 2 * p.1 * P.f p * parameterPartial P.f p

theorem NavierStokes.ProfileHistories.Profiles.E_sq {D : RadialDomain} (P : Profiles D) {p : Point} (hX : 0 ≤ p.1) :

P.E p ^ 2 / 2 = p.1 * P.f p ^ 2

theorem NavierStokes.ProfileHistories.Profiles.E_mul_Eη {D : RadialDomain} (P : Profiles D) {p : Point} (hX : 0 ≤ p.1) :

P.E p * P.Eη p = 2 * p.1 * P.f p * parameterPartial P.f p

theorem NavierStokes.ProfileHistories.Profiles.Eη_hasDerivAt {D : RadialDomain} (P : Profiles D) {p : Point} (hp : p ∈ D.carrier) :

HasDerivAt (fun (η : ℝ) => P.E (p.1, η)) (P.Eη p) p.2

theorem NavierStokes.ProfileHistories.Profiles.pressure_hasDerivAt {D : RadialDomain} (P : Profiles D) {p : Point} (hp : p ∈ D.carrier) :

HasDerivAt (fun (x : ℝ) => P.pressure (x, p.2)) (P.f p ^ 2) p.1

theorem NavierStokes.ProfileHistories.Profiles.radialPartial_pressure {D : RadialDomain} (P : Profiles D) {p : Point} (hp : p ∈ D.carrier) :

radialPartial P.pressure p = P.f p ^ 2

theorem NavierStokes.ProfileHistories.Profiles.parameterPartial_pressure {D : RadialDomain} (P : Profiles D) {p : Point} (hp : p ∈ D.carrier) :

parameterPartial P.pressure p = deriv P.pressure0 p.2 + parameterPartial (primitive fun (q : Point) => P.f q ^ 2) p

theorem NavierStokes.ProfileHistories.Profiles.parameterPartial_pressure_hasDerivAt {D : RadialDomain} (P : Profiles D) {p : Point} (hp : p ∈ D.carrier) :

HasDerivAt (fun (x : ℝ) => parameterPartial P.pressure (x, p.2)) (2 * P.f p * parameterPartial P.f p) p.1

theorem NavierStokes.ProfileHistories.Profiles.axis_mem {D : RadialDomain} {p : Point} (hp : p ∈ D.carrier) :

(0, p.2) ∈ D.carrier

noncomputable def NavierStokes.ProfileHistories.Profiles.angularData {D : RadialDomain} (P : Profiles D) (h : ℝ) (p : Point) (hp : p ∈ D.carrier) :

StressAlgebra.AngularMomentData h p.2 p.1

Every field and every derivative in the angular stress data is obtained from the actual profiles and the actual integral histories.

Equations

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

Instances For

noncomputable def NavierStokes.ProfileHistories.Profiles.axialData {D : RadialDomain} (P : Profiles D) (h : ℝ) (p : Point) (hp : p ∈ D.carrier) (hX : 0 ≤ p.1) :

StressAlgebra.AxialMomentData h p.2 p.1

The axial data also use the pressure constructed by integrating f².

Equations

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

Instances For

noncomputable def NavierStokes.ProfileHistories.Profiles.angularSource {D : RadialDomain} (P : Profiles D) (h : ℝ) :

Angular source, defined pointwise by StressAlgebra.angularSource h p.2 p.1 (P.W h p) (P.U p) (P.H p) (radialPartial P.H p) (parameterPartial P.H p).

Equations

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

Instances For

noncomputable def NavierStokes.ProfileHistories.Profiles.axialSource {D : RadialDomain} (P : Profiles D) (h : ℝ) :

Axial source as an element of Field.

Equations

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

Instances For

theorem NavierStokes.ProfileHistories.Profiles.angularSource_smooth {D : RadialDomain} (P : Profiles D) (h : ℝ) :

ContDiffOn ℝ (↑⊤) (P.angularSource h) D.carrier

theorem NavierStokes.ProfileHistories.Profiles.axialSource_smooth {D : RadialDomain} (P : Profiles D) (h : ℝ) :

ContDiffOn ℝ (↑⊤) (P.axialSource h) D.carrier

noncomputable def NavierStokes.ProfileHistories.Profiles.angularLag {D : RadialDomain} (P : Profiles D) (h : ℝ) :

The printed Q_s is the regular primitive divided by its integrating factor.

Equations

P.angularLag h p = NavierStokes.ProfileHistories.primitive (P.angularSource h) p / (p.1 * P.H p)

Instances For

noncomputable def NavierStokes.ProfileHistories.Profiles.axialLag {D : RadialDomain} (P : Profiles D) (h : ℝ) :

The printed N_s is the regular primitive divided by X.

Equations

P.axialLag h p = NavierStokes.ProfileHistories.primitive (P.axialSource h) p / p.1

Instances For

theorem NavierStokes.ProfileHistories.Profiles.angularLag_integrated {D : RadialDomain} (P : Profiles D) (h : ℝ) {p : Point} (hp : p ∈ D.carrier) (hX : p.1 ≠ 0) (hH : P.H p ≠ 0) :

P.angularLag h p = -P.W h p + ((1 - h) * P.I p - StressAlgebra.axialExponent h * p.2 * parameterPartial P.I p - StressAlgebra.coordinateFactor p.2 * parameterPartial P.J p + 2 * (h - StressAlgebra.axialExponent h) * p.2 * P.J p) / (p.1 * P.H p)

Equation (9), angular row, for actual smooth profile histories.

theorem NavierStokes.ProfileHistories.Profiles.axialLag_integrated {D : RadialDomain} (P : Profiles D) (h : ℝ) {p : Point} (hp : p ∈ D.carrier) (hX : 0 < p.1) :

P.axialLag h p = -P.W h p * P.U p + StressAlgebra.axialExponent h * (P.M p - p.2 * parameterPartial P.M p) / p.1 + (4 * h * p.2 * P.S p - StressAlgebra.coordinateFactor p.2 * parameterPartial P.S p) / p.1 + 4 * StressAlgebra.velocityExponent h * p.2 * P.pressure p - StressAlgebra.coordinateFactor p.2 * parameterPartial P.pressure p

Equation (9), axial row, with constructed pressure and actual histories.

theorem NavierStokes.ProfileHistories.Profiles.angularLag_smoothAt {D : RadialDomain} (P : Profiles D) (h : ℝ) {p : Point} (hp : p ∈ D.carrier) (hX : p.1 ≠ 0) (hH : P.H p ≠ 0) :

ContDiffAt ℝ (↑⊤) (P.angularLag h) p

theorem NavierStokes.ProfileHistories.Profiles.axialLag_smoothAt {D : RadialDomain} (P : Profiles D) (h : ℝ) {p : Point} (hp : p ∈ D.carrier) (hX : p.1 ≠ 0) :

ContDiffAt ℝ (↑⊤) (P.axialLag h) p

theorem NavierStokes.ProfileHistories.Profiles.angularLag_hasDerivAt {D : RadialDomain} (P : Profiles D) (h : ℝ) {p : Point} (hp : p ∈ D.carrier) (hX : p.1 ≠ 0) (hH : P.H p ≠ 0) :

HasDerivAt (fun (x : ℝ) => P.angularLag h (x, p.2)) ((P.angularSource h p * (p.1 * P.H p) - primitive (P.angularSource h) p * (P.H p + p.1 * radialPartial P.H p)) / (p.1 * P.H p) ^ 2) p.1

theorem NavierStokes.ProfileHistories.Profiles.axialLag_hasDerivAt {D : RadialDomain} (P : Profiles D) (h : ℝ) {p : Point} (hp : p ∈ D.carrier) (hX : p.1 ≠ 0) :

HasDerivAt (fun (x : ℝ) => P.axialLag h (x, p.2)) ((P.axialSource h p * p.1 - primitive (P.axialSource h) p) / p.1 ^ 2) p.1

theorem NavierStokes.ProfileHistories.Profiles.angularLag_equation {D : RadialDomain} (P : Profiles D) (h : ℝ) {p : Point} (hp : p ∈ D.carrier) (hX : p.1 ≠ 0) (hH : P.H p ≠ 0) :

p.1 * deriv (fun (x : ℝ) => P.angularLag h (x, p.2)) p.1 + (1 + p.1 * radialPartial P.H p / P.H p) * P.angularLag h p = P.angularSource h p / P.H p

The angular differential equation (6), with logarithmic slopes as ratios of genuine derivatives.

theorem NavierStokes.ProfileHistories.Profiles.axialLag_equation {D : RadialDomain} (P : Profiles D) (h : ℝ) {p : Point} (hp : p ∈ D.carrier) (hX : p.1 ≠ 0) :

p.1 * deriv (fun (x : ℝ) => P.axialLag h (x, p.2)) p.1 + P.axialLag h p = P.axialSource h p

The axial differential equation (6), with the actual primitive-defined N_s.

theorem NavierStokes.ProfileHistories.Profiles.H_ne_zero {D : RadialDomain} (P : Profiles D) {p : Point} (hX : p.1 ≠ 0) (hf : P.f p ≠ 0) :

P.H p ≠ 0

theorem NavierStokes.ProfileHistories.Profiles.E_ne_zero {D : RadialDomain} (P : Profiles D) {p : Point} (hX : 0 < p.1) (hf : P.f p ≠ 0) :

P.E p ≠ 0

theorem NavierStokes.ProfileHistories.Profiles.logH_radial_deriv {D : RadialDomain} (P : Profiles D) {p : Point} (hp : p ∈ D.carrier) (hH : P.H p ≠ 0) :

deriv (fun (x : ℝ) => Real.log (P.H (x, p.2))) p.1 = radialPartial P.H p / P.H p

theorem NavierStokes.ProfileHistories.Profiles.logE_parameter_deriv {D : RadialDomain} (P : Profiles D) {p : Point} (hp : p ∈ D.carrier) (hX : 0 < p.1) (hf : P.f p ≠ 0) :

deriv (fun (η : ℝ) => Real.log (P.E (p.1, η))) p.2 = parameterPartial P.H p / P.H p

theorem NavierStokes.ProfileHistories.Profiles.angularLag_equation_logarithmic {D : RadialDomain} (P : Profiles D) (h : ℝ) {p : Point} (hp : p ∈ D.carrier) (hX : 0 < p.1) (hf : P.f p ≠ 0) :

p.1 * deriv (fun (x : ℝ) => P.angularLag h (x, p.2)) p.1 + (1 + p.1 * deriv (fun (x : ℝ) => Real.log (P.H (x, p.2))) p.1) * P.angularLag h p = -P.W h p * (p.1 * deriv (fun (x : ℝ) => Real.log (P.H (x, p.2))) p.1) - h * (1 - 2 * p.2 * P.U p) - (StressAlgebra.axialExponent h * p.2 + StressAlgebra.coordinateFactor p.2 * P.U p) * deriv (fun (η : ℝ) => Real.log (P.E (p.1, η))) p.2

The angular row of (6) with actual logarithms, not surrogate slope data.

theorem NavierStokes.ProfileHistories.Profiles.axialLag_equation_explicit {D : RadialDomain} (P : Profiles D) (h : ℝ) {p : Point} (hp : p ∈ D.carrier) (hX : 0 < p.1) :

p.1 * deriv (fun (x : ℝ) => P.axialLag h (x, p.2)) p.1 + P.axialLag h p = -P.W h p * (p.1 * radialPartial P.U p) - StressAlgebra.velocityExponent h * (1 - 2 * p.2 * P.U p) * P.U p - (StressAlgebra.axialExponent h * p.2 + StressAlgebra.coordinateFactor p.2 * P.U p) * parameterPartial P.U p - StressAlgebra.coordinateFactor p.2 * parameterPartial P.pressure p + 4 * StressAlgebra.velocityExponent h * p.2 * P.pressure p + 2 * p.2 * (p.1 * radialPartial P.pressure p)

The axial row of (6), with the pressure derivative proved from its integral.