Exact angularly averaged Navier--Stokes balances

The average is a normalized actual interval integral. All coordinate derivatives are Fréchet derivatives on spacetime, and the Reynolds products include the entire oscillatory velocity.

@[reducible, inline]

abbrev NavierStokes.MeanResidual.Scalar : Type

Scalar: an abbreviation for SpaceTime → ℝ.

Equations

• NavierStokes.MeanResidual.Scalar = (NavierStokes.ProblemStatement.SpaceTime → ℝ)

@[reducible, inline]

abbrev NavierStokes.MeanResidual.Components : Type

Components: an abbreviation for Fin 3 → Scalar.

Equations

• NavierStokes.MeanResidual.Components = (Fin 3 → NavierStokes.MeanResidual.Scalar)

noncomputable def NavierStokes.MeanResidual.period : ℝ

Period, given by 2 * Real.pi.

Equations

• NavierStokes.MeanResidual.period = 2 * Real.pi

noncomputable def NavierStokes.MeanResidual.angularVector : ProblemStatement.SpaceTime

Angular vector, given by (0, coordinateVector 1).

Equations

• NavierStokes.MeanResidual.angularVector = (0, NavierStokes.ProblemStatement.coordinateVector 1)

noncomputable def NavierStokes.MeanResidual.angularShift (q : ProblemStatement.SpaceTime) (a : ℝ) : ProblemStatement.SpaceTime

Angular shift, given by q + a • angularVector.

Equations

• NavierStokes.MeanResidual.angularShift q a = q + a • NavierStokes.MeanResidual.angularVector

noncomputable def NavierStokes.MeanResidual.radius (q : ProblemStatement.SpaceTime) : ℝ

Radius, given by q.2 0.

Equations

• NavierStokes.MeanResidual.radius q = q.2.ofLp 0

theorem NavierStokes.MeanResidual.period_pos : 0 < period

theorem NavierStokes.MeanResidual.period_ne_zero : period ≠ 0

@[simp]

theorem NavierStokes.MeanResidual.angularShift_zero (q : ProblemStatement.SpaceTime) : angularShift q 0 = q

@[simp]

theorem NavierStokes.MeanResidual.radius_angularShift (q : ProblemStatement.SpaceTime) (a : ℝ) : radius (angularShift q a) = radius q

noncomputable def NavierStokes.MeanResidual.direction {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (v : ProblemStatement.SpaceTime) (f : ProblemStatement.SpaceTime → E) (q : ProblemStatement.SpaceTime) : E

Direction, given by fderiv ℝ f q v.

Equations

• NavierStokes.MeanResidual.direction v f q = (fderiv ℝ f q) v

noncomputable def NavierStokes.MeanResidual.dt {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ProblemStatement.SpaceTime → E) (q : ProblemStatement.SpaceTime) : E

Dt, given by direction (1, 0) f.

Equations

• NavierStokes.MeanResidual.dt f = NavierStokes.MeanResidual.direction (1, 0) f

noncomputable def NavierStokes.MeanResidual.dr {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ProblemStatement.SpaceTime → E) (q : ProblemStatement.SpaceTime) : E

Dr, given by direction (0, coordinateVector 0) f.

Equations

• NavierStokes.MeanResidual.dr f = NavierStokes.MeanResidual.direction (0, NavierStokes.ProblemStatement.coordinateVector 0) f

noncomputable def NavierStokes.MeanResidual.dtheta {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ProblemStatement.SpaceTime → E) (q : ProblemStatement.SpaceTime) : E

Dtheta, given by direction angularVector f.

Equations

• NavierStokes.MeanResidual.dtheta f = NavierStokes.MeanResidual.direction NavierStokes.MeanResidual.angularVector f

noncomputable def NavierStokes.MeanResidual.dz {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ProblemStatement.SpaceTime → E) (q : ProblemStatement.SpaceTime) : E

Dz, given by direction (0, coordinateVector 2) f.

Equations

• NavierStokes.MeanResidual.dz f = NavierStokes.MeanResidual.direction (0, NavierStokes.ProblemStatement.coordinateVector 2) f

noncomputable def NavierStokes.MeanResidual.average {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ProblemStatement.SpaceTime → E) (q : ProblemStatement.SpaceTime) : E

Average, given by period⁻¹ • ∫ a in (0 : ℝ)..period, f (angularShift q a).

Equations

• NavierStokes.MeanResidual.average f q = NavierStokes.MeanResidual.period⁻¹ • ∫ (a : ℝ) in 0..NavierStokes.MeanResidual.period, f (NavierStokes.MeanResidual.angularShift q a)

def NavierStokes.MeanResidual.AngularContinuous {E : Type} [NormedAddCommGroup E] (f : ProblemStatement.SpaceTime → E) : Prop

Angular continuous, given by ∀ q, Continuous (fun a => f (angularShift q a)).

Equations

• NavierStokes.MeanResidual.AngularContinuous f = ∀ (q : NavierStokes.ProblemStatement.SpaceTime), Continuous fun (a : ℝ) => f (NavierStokes.MeanResidual.angularShift q a)

def NavierStokes.MeanResidual.AngularPeriodic {E : Type} (f : ProblemStatement.SpaceTime → E) : Prop

Angular periodic, given by ∀ q, f (angularShift q period) = f q.

Equations

• NavierStokes.MeanResidual.AngularPeriodic f = ∀ (q : NavierStokes.ProblemStatement.SpaceTime), f (NavierStokes.MeanResidual.angularShift q NavierStokes.MeanResidual.period) = f q

def NavierStokes.MeanResidual.AngularInvariant {E : Type} (f : ProblemStatement.SpaceTime → E) : Prop

Angular invariant, given by ∀ q a, f (angularShift q a) = f q.

Equations

• NavierStokes.MeanResidual.AngularInvariant f = ∀ (q : NavierStokes.ProblemStatement.SpaceTime) (a : ℝ), f (NavierStokes.MeanResidual.angularShift q a) = f q

theorem NavierStokes.MeanResidual.contDiff_angularShift : ContDiff ℝ ↑⊤ fun (qa : ProblemStatement.SpaceTime × ℝ) => angularShift qa.1 qa.2

theorem NavierStokes.MeanResidual.direction_smooth {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (v : ProblemStatement.SpaceTime) {f : ProblemStatement.SpaceTime → E} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (direction v f)

theorem NavierStokes.MeanResidual.direction_continuous {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (v : ProblemStatement.SpaceTime) {f : ProblemStatement.SpaceTime → E} (hf : ContDiff ℝ (↑⊤) f) : Continuous (direction v f)

theorem NavierStokes.MeanResidual.continuous_angularShift (q : ProblemStatement.SpaceTime) : Continuous (angularShift q)

theorem NavierStokes.MeanResidual.angularContinuous_of_continuous {E : Type} [NormedAddCommGroup E] {f : ProblemStatement.SpaceTime → E} (hf : Continuous f) : AngularContinuous f

theorem NavierStokes.MeanResidual.AngularContinuous.add {E : Type} [NormedAddCommGroup E] {f g : ProblemStatement.SpaceTime → E} (hf : AngularContinuous f) (hg : AngularContinuous g) : AngularContinuous fun (q : ProblemStatement.SpaceTime) => f q + g q

theorem NavierStokes.MeanResidual.AngularContinuous.sub {E : Type} [NormedAddCommGroup E] {f g : ProblemStatement.SpaceTime → E} (hf : AngularContinuous f) (hg : AngularContinuous g) : AngularContinuous fun (q : ProblemStatement.SpaceTime) => f q - g q

theorem NavierStokes.MeanResidual.AngularContinuous.mul {f g : Scalar} (hf : AngularContinuous f) (hg : AngularContinuous g) : AngularContinuous fun (q : ProblemStatement.SpaceTime) => f q * g q

theorem NavierStokes.MeanResidual.AngularContinuous.div_radius {f : Scalar} (hf : AngularContinuous f) (n : ℕ) : AngularContinuous fun (q : ProblemStatement.SpaceTime) => f q / radius q ^ n

theorem NavierStokes.MeanResidual.AngularContinuous.const_mul {f : Scalar} (hf : AngularContinuous f) (c : ℝ) : AngularContinuous fun (q : ProblemStatement.SpaceTime) => c * f q

theorem NavierStokes.MeanResidual.AngularInvariant.angularContinuous {E : Type} [NormedAddCommGroup E] {f : ProblemStatement.SpaceTime → E} (hf : AngularInvariant f) : AngularContinuous f

theorem NavierStokes.MeanResidual.average_add {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ProblemStatement.SpaceTime → E} (hf : AngularContinuous f) (hg : AngularContinuous g) (q : ProblemStatement.SpaceTime) : average (fun (y : ProblemStatement.SpaceTime) => f y + g y) q = average f q + average g q

theorem NavierStokes.MeanResidual.average_sub {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ProblemStatement.SpaceTime → E} (hf : AngularContinuous f) (hg : AngularContinuous g) (q : ProblemStatement.SpaceTime) : average (fun (y : ProblemStatement.SpaceTime) => f y - g y) q = average f q - average g q

theorem NavierStokes.MeanResidual.average_invariant {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ProblemStatement.SpaceTime → E} (hf : AngularInvariant f) (q : ProblemStatement.SpaceTime) : average f q = f q

theorem NavierStokes.MeanResidual.average_const {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (c : E) (q : ProblemStatement.SpaceTime) : average (fun (x : ProblemStatement.SpaceTime) => c) q = c

theorem NavierStokes.MeanResidual.average_mul_invariant {a f : Scalar} (ha : AngularInvariant a) (q : ProblemStatement.SpaceTime) : average (fun (y : ProblemStatement.SpaceTime) => a y * f y) q = a q * average f q

theorem NavierStokes.MeanResidual.average_div_radius (f : Scalar) (q : ProblemStatement.SpaceTime) (n : ℕ) : average (fun (y : ProblemStatement.SpaceTime) => f y / radius y ^ n) q = average f q / radius q ^ n

theorem NavierStokes.MeanResidual.average_div_r (f : Scalar) (q : ProblemStatement.SpaceTime) : average (fun (y : ProblemStatement.SpaceTime) => f y / radius y) q = average f q / radius q

theorem NavierStokes.MeanResidual.average_const_mul (c : ℝ) (f : Scalar) (q : ProblemStatement.SpaceTime) : average (fun (y : ProblemStatement.SpaceTime) => c * f y) q = c * average f q

theorem NavierStokes.MeanResidual.average_congr {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ProblemStatement.SpaceTime → E} {q : ProblemStatement.SpaceTime} (h : ∀ a ∈ Set.uIcc 0 period, f (angularShift q a) = g (angularShift q a)) : average f q = average g q

theorem NavierStokes.MeanResidual.average_smooth {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ProblemStatement.SpaceTime → E} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (average f)

theorem NavierStokes.MeanResidual.direction_average {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ProblemStatement.SpaceTime → E} (hf : ContDiff ℝ (↑⊤) f) (v q : ProblemStatement.SpaceTime) : direction v (average f) q = average (direction v f) q

Differentiation under the actual compact angular integral.

theorem NavierStokes.MeanResidual.AngularPeriodic.direction {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ProblemStatement.SpaceTime → E} (hp : AngularPeriodic f) (v : ProblemStatement.SpaceTime) : AngularPeriodic (MeanResidual.direction v f)

theorem NavierStokes.MeanResidual.AngularInvariant.direction {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ProblemStatement.SpaceTime → E} (hp : AngularInvariant f) (v : ProblemStatement.SpaceTime) : AngularInvariant (MeanResidual.direction v f)

theorem NavierStokes.MeanResidual.AngularPeriodic.mul {f g : Scalar} (hf : AngularPeriodic f) (hg : AngularPeriodic g) : AngularPeriodic fun (q : ProblemStatement.SpaceTime) => f q * g q

theorem NavierStokes.MeanResidual.average_dtheta_zero {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ProblemStatement.SpaceTime → E} (hf : ContDiff ℝ (↑⊤) f) (hp : AngularPeriodic f) (q : ProblemStatement.SpaceTime) : average (dtheta f) q = 0

A full angular derivative has exactly zero average, by the fundamental theorem.

theorem NavierStokes.MeanResidual.dtheta_invariant_zero {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ProblemStatement.SpaceTime → E} (hf : ContDiff ℝ (↑⊤) f) (hp : AngularInvariant f) (q : ProblemStatement.SpaceTime) : dtheta f q = 0

theorem NavierStokes.MeanResidual.direction_add {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ProblemStatement.SpaceTime → E} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (v q : ProblemStatement.SpaceTime) : direction v (fun (y : ProblemStatement.SpaceTime) => f y + g y) q = direction v f q + direction v g q

theorem NavierStokes.MeanResidual.direction_sub {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ProblemStatement.SpaceTime → E} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (v q : ProblemStatement.SpaceTime) : direction v (fun (y : ProblemStatement.SpaceTime) => f y - g y) q = direction v f q - direction v g q

theorem NavierStokes.MeanResidual.direction_mul {f g : Scalar} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (v q : ProblemStatement.SpaceTime) : direction v (fun (y : ProblemStatement.SpaceTime) => f y * g y) q = direction v f q * g q + f q * direction v g q

theorem NavierStokes.MeanResidual.direction_map {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E →L[ℝ] F) {f : ProblemStatement.SpaceTime → E} (hf : ContDiff ℝ (↑⊤) f) (v q : ProblemStatement.SpaceTime) : direction v (fun (y : ProblemStatement.SpaceTime) => L (f y)) q = L (direction v f q)

theorem NavierStokes.MeanResidual.spatial_direction {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ProblemStatement.SpaceTime → E} (hf : ContDiff ℝ (↑⊤) f) (t : ℝ) (x : ProblemStatement.Space) (i : Fin 3) : CylindricalResidual.dCoord i (fun (y : ProblemStatement.Space) => f (t, y)) x = direction (0, ProblemStatement.coordinateVector i) f (t, x)

theorem NavierStokes.MeanResidual.spatial_second {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ProblemStatement.SpaceTime → E} (hf : ContDiff ℝ (↑⊤) f) (t : ℝ) (x : ProblemStatement.Space) (i : Fin 3) : CylindricalResidual.dCoord i (CylindricalResidual.dCoord i fun (y : ProblemStatement.Space) => f (t, y)) x = direction (0, ProblemStatement.coordinateVector i) (direction (0, ProblemStatement.coordinateVector i) f) (t, x)

theorem NavierStokes.MeanResidual.temporal_direction {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ProblemStatement.SpaceTime → E} (hf : ContDiff ℝ (↑⊤) f) (t : ℝ) (x : ProblemStatement.Space) : (fderiv ℝ (fun (s : ℝ) => f (s, x)) t) 1 = dt f (t, x)

noncomputable def NavierStokes.MeanResidual.velocity (w : Components) : ProblemStatement.VelocityField

Velocity, defined pointwise by pack (w 0 q) (w 1 q) (w 2 q).

Equations

• NavierStokes.MeanResidual.velocity w q = NavierStokes.AxisymmetricResidual.pack (w 0 q) (w 1 q) (w 2 q)

@[simp]

theorem NavierStokes.MeanResidual.velocity_apply (w : Components) (q : ProblemStatement.SpaceTime) (i : Fin 3) : (velocity w q).ofLp i = w i q

theorem NavierStokes.MeanResidual.velocity_smooth {w : Components} (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i)) : ContDiff ℝ (↑⊤) (velocity w)

theorem NavierStokes.MeanResidual.direction_velocity {w : Components} (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i)) (v q : ProblemStatement.SpaceTime) : direction v (velocity w) q = AxisymmetricResidual.pack (direction v (w 0) q) (direction v (w 1) q) (direction v (w 2) q)

theorem NavierStokes.MeanResidual.direction_velocity_component {w : Components} (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i)) (v q : ProblemStatement.SpaceTime) (i : Fin 3) : (direction v (velocity w) q).ofLp i = direction v (w i) q

noncomputable def NavierStokes.MeanResidual.laplacian (f : Scalar) (q : ProblemStatement.SpaceTime) : ℝ

Laplacian, given by dr (dr f) q + dr f q / radius q + dtheta (dtheta f) q / radius q ^ 2 + dz (dz f) q.

Equations

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

noncomputable def NavierStokes.MeanResidual.meanLaplacian (f : Scalar) (q : ProblemStatement.SpaceTime) : ℝ

Mean laplacian, given by dr (dr f) q + dr f q / radius q + dz (dz f) q.

Equations

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

noncomputable def NavierStokes.MeanResidual.radialDivergence (c : ℝ) (f : Scalar) (q : ProblemStatement.SpaceTime) : ℝ

Radial divergence, given by dr f q + c / radius q * f q.

Equations

• NavierStokes.MeanResidual.radialDivergence c f q = NavierStokes.MeanResidual.dr f q + c / NavierStokes.MeanResidual.radius q * f q

noncomputable def NavierStokes.MeanResidual.divergence (w : Components) (q : ProblemStatement.SpaceTime) : ℝ

Divergence, given by dr (w 0) q + w 0 q / radius q + dtheta (w 1) q / radius q + dz (w 2) q.

Equations

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

noncomputable def NavierStokes.MeanResidual.transport (w : Components) (f : Scalar) (q : ProblemStatement.SpaceTime) : ℝ

Transport, given by w 0 q * dr f q + w 1 q / radius q * dtheta f q + w 2 q * dz f q.

Equations

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

noncomputable def NavierStokes.MeanResidual.residualRadial (w : Components) (p : Scalar) (q : ProblemStatement.SpaceTime) : ℝ

Residual radial, constructed using dt.

Equations

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

noncomputable def NavierStokes.MeanResidual.residualAngular (w : Components) (p : Scalar) (q : ProblemStatement.SpaceTime) : ℝ

Residual angular, constructed using dt.

Equations

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

noncomputable def NavierStokes.MeanResidual.residualAxial (w : Components) (p : Scalar) (q : ProblemStatement.SpaceTime) : ℝ

Residual axial, given by dt (w 2) q + transport w (w 2) q - laplacian (w 2) q + dz p q.

Equations

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

theorem NavierStokes.MeanResidual.scalarLaplacian_eq {f : Scalar} (hf : ContDiff ℝ (↑⊤) f) (q : ProblemStatement.SpaceTime) : CylindricalResidual.scalarLaplacian (fun (y : ProblemStatement.Space) => f (q.1, y)) q.2 = laplacian f q

theorem NavierStokes.MeanResidual.scalarLaplacian_velocity {w : Components} (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i)) (q : ProblemStatement.SpaceTime) (i : Fin 3) : (CylindricalResidual.scalarLaplacian (fun (y : ProblemStatement.Space) => velocity w (q.1, y)) q.2).ofLp i = laplacian (w i) q

theorem NavierStokes.MeanResidual.cylindricalResidual_radial {w : Components} {p : Scalar} (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i)) (hp : ContDiff ℝ (↑⊤) p) (q : ProblemStatement.SpaceTime) : (CylindricalResidual.cylindricalResidual (velocity w) p q.1 q.2).ofLp 0 = residualRadial w p q

theorem NavierStokes.MeanResidual.cylindricalResidual_angular {w : Components} {p : Scalar} (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i)) (hp : ContDiff ℝ (↑⊤) p) (q : ProblemStatement.SpaceTime) : (CylindricalResidual.cylindricalResidual (velocity w) p q.1 q.2).ofLp 1 = residualAngular w p q

theorem NavierStokes.MeanResidual.cylindricalResidual_axial {w : Components} {p : Scalar} (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i)) (hp : ContDiff ℝ (↑⊤) p) (q : ProblemStatement.SpaceTime) : (CylindricalResidual.cylindricalResidual (velocity w) p q.1 q.2).ofLp 2 = residualAxial w p q

noncomputable def NavierStokes.MeanResidual.conservativeRadial (w : Components) (p : Scalar) (q : ProblemStatement.SpaceTime) : ℝ

Conservative radial, constructed using dt.

Equations

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

noncomputable def NavierStokes.MeanResidual.conservativeAngular (w : Components) (p : Scalar) (q : ProblemStatement.SpaceTime) : ℝ

Conservative angular, constructed using dt.

Equations

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

noncomputable def NavierStokes.MeanResidual.conservativeAxial (w : Components) (p : Scalar) (q : ProblemStatement.SpaceTime) : ℝ

Conservative axial, constructed using dt.

Equations

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

theorem NavierStokes.MeanResidual.conservativeRadial_eq {w : Components} (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i)) (p : Scalar) (q : ProblemStatement.SpaceTime) : conservativeRadial w p q = residualRadial w p q + w 0 q * divergence w q

theorem NavierStokes.MeanResidual.conservativeAngular_eq {w : Components} (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i)) (p : Scalar) (q : ProblemStatement.SpaceTime) : conservativeAngular w p q = residualAngular w p q + w 1 q * divergence w q

theorem NavierStokes.MeanResidual.conservativeAxial_eq {w : Components} (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i)) (p : Scalar) (q : ProblemStatement.SpaceTime) : conservativeAxial w p q = residualAxial w p q + w 2 q * divergence w q

theorem NavierStokes.MeanResidual.angularInvariant_radius {E : Type} (f : ℝ → E) : AngularInvariant fun (q : ProblemStatement.SpaceTime) => f (radius q)

theorem NavierStokes.MeanResidual.average_direction {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ProblemStatement.SpaceTime → E} (hf : ContDiff ℝ (↑⊤) f) (v q : ProblemStatement.SpaceTime) : average (direction v f) q = direction v (average f) q

theorem NavierStokes.MeanResidual.average_direction_twice {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ProblemStatement.SpaceTime → E} (hf : ContDiff ℝ (↑⊤) f) (v w q : ProblemStatement.SpaceTime) : average (direction v (direction w f)) q = direction v (direction w (average f)) q

theorem NavierStokes.MeanResidual.average_dt {f : Scalar} (hf : ContDiff ℝ (↑⊤) f) (q : ProblemStatement.SpaceTime) : average (dt f) q = dt (average f) q

theorem NavierStokes.MeanResidual.average_dr {f : Scalar} (hf : ContDiff ℝ (↑⊤) f) (q : ProblemStatement.SpaceTime) : average (dr f) q = dr (average f) q

theorem NavierStokes.MeanResidual.average_dz {f : Scalar} (hf : ContDiff ℝ (↑⊤) f) (q : ProblemStatement.SpaceTime) : average (dz f) q = dz (average f) q

theorem NavierStokes.MeanResidual.average_drdr {f : Scalar} (hf : ContDiff ℝ (↑⊤) f) (q : ProblemStatement.SpaceTime) : average (dr (dr f)) q = dr (dr (average f)) q

theorem NavierStokes.MeanResidual.average_dzdz {f : Scalar} (hf : ContDiff ℝ (↑⊤) f) (q : ProblemStatement.SpaceTime) : average (dz (dz f)) q = dz (dz (average f)) q

theorem NavierStokes.MeanResidual.angularContinuous_direction {f : Scalar} (hf : ContDiff ℝ (↑⊤) f) (v : ProblemStatement.SpaceTime) : AngularContinuous (direction v f)

theorem NavierStokes.MeanResidual.AngularContinuous.div_r {f : Scalar} (hf : AngularContinuous f) : AngularContinuous fun (q : ProblemStatement.SpaceTime) => f q / radius q

theorem NavierStokes.MeanResidual.angularContinuous_radialDivergence {f : Scalar} (hf : ContDiff ℝ (↑⊤) f) (c : ℝ) : AngularContinuous (radialDivergence c f)

theorem NavierStokes.MeanResidual.angularContinuous_laplacian {f : Scalar} (hf : ContDiff ℝ (↑⊤) f) : AngularContinuous (laplacian f)

theorem NavierStokes.MeanResidual.average_radialDivergence {f : Scalar} (hf : ContDiff ℝ (↑⊤) f) (c : ℝ) (q : ProblemStatement.SpaceTime) : average (radialDivergence c f) q = radialDivergence c (average f) q

theorem NavierStokes.MeanResidual.average_laplacian {f : Scalar} (hf : ContDiff ℝ (↑⊤) f) (hp : AngularPeriodic f) (q : ProblemStatement.SpaceTime) : average (laplacian f) q = meanLaplacian (average f) q

noncomputable def NavierStokes.MeanResidual.reynoldsRadial (w : Components) (p : Scalar) (q : ProblemStatement.SpaceTime) : ℝ

Reynolds radial, constructed using dt.

Equations

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

noncomputable def NavierStokes.MeanResidual.reynoldsAngular (w : Components) (q : ProblemStatement.SpaceTime) : ℝ

Reynolds angular, constructed using dt.

Equations

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

noncomputable def NavierStokes.MeanResidual.reynoldsAxial (w : Components) (p : Scalar) (q : ProblemStatement.SpaceTime) : ℝ

Reynolds axial, constructed using dt.

Equations

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

theorem NavierStokes.MeanResidual.average_conservativeAngular {w : Components} {p : Scalar} (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i)) (hp : ContDiff ℝ (↑⊤) p) (hwper : ∀ (i : Fin 3), AngularPeriodic (w i)) (hpper : AngularPeriodic p) (q : ProblemStatement.SpaceTime) : average (conservativeAngular w p) q = reynoldsAngular w q

theorem NavierStokes.MeanResidual.average_conservativeRadial {w : Components} {p : Scalar} (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i)) (hp : ContDiff ℝ (↑⊤) p) (hwper : ∀ (i : Fin 3), AngularPeriodic (w i)) (q : ProblemStatement.SpaceTime) : average (conservativeRadial w p) q = reynoldsRadial w p q

theorem NavierStokes.MeanResidual.average_conservativeAxial {w : Components} {p : Scalar} (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i)) (hp : ContDiff ℝ (↑⊤) p) (hwper : ∀ (i : Fin 3), AngularPeriodic (w i)) (q : ProblemStatement.SpaceTime) : average (conservativeAxial w p) q = reynoldsAxial w p q

theorem NavierStokes.MeanResidual.average_residualRadial {w : Components} {p : Scalar} (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i)) (hp : ContDiff ℝ (↑⊤) p) (hwper : ∀ (i : Fin 3), AngularPeriodic (w i)) (hdiv : ∀ (y : ProblemStatement.SpaceTime), 0 < radius y → divergence w y = 0) (q : ProblemStatement.SpaceTime) (hr : 0 < radius q) : average (residualRadial w p) q = reynoldsRadial w p q

theorem NavierStokes.MeanResidual.average_residualAngular {w : Components} {p : Scalar} (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i)) (hp : ContDiff ℝ (↑⊤) p) (hwper : ∀ (i : Fin 3), AngularPeriodic (w i)) (hpper : AngularPeriodic p) (hdiv : ∀ (y : ProblemStatement.SpaceTime), 0 < radius y → divergence w y = 0) (q : ProblemStatement.SpaceTime) (hr : 0 < radius q) : average (residualAngular w p) q = reynoldsAngular w q

theorem NavierStokes.MeanResidual.average_residualAxial {w : Components} {p : Scalar} (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i)) (hp : ContDiff ℝ (↑⊤) p) (hwper : ∀ (i : Fin 3), AngularPeriodic (w i)) (hdiv : ∀ (y : ProblemStatement.SpaceTime), 0 < radius y → divergence w y = 0) (q : ProblemStatement.SpaceTime) (hr : 0 < radius q) : average (residualAxial w p) q = reynoldsAxial w p q

theorem NavierStokes.MeanResidual.AngularInvariant.add {E : Type} [NormedAddCommGroup E] {f g : ProblemStatement.SpaceTime → E} (hf : AngularInvariant f) (hg : AngularInvariant g) : AngularInvariant fun (q : ProblemStatement.SpaceTime) => f q + g q

theorem NavierStokes.MeanResidual.AngularInvariant.mul {f g : Scalar} (hf : AngularInvariant f) (hg : AngularInvariant g) : AngularInvariant fun (q : ProblemStatement.SpaceTime) => f q * g q

theorem NavierStokes.MeanResidual.AngularPeriodic.add {E : Type} [NormedAddCommGroup E] {f g : ProblemStatement.SpaceTime → E} (hf : AngularPeriodic f) (hg : AngularPeriodic g) : AngularPeriodic fun (q : ProblemStatement.SpaceTime) => f q + g q

noncomputable def NavierStokes.MeanResidual.total (base mean osc : Components) : Components

The complete velocity split, with no omission of any part of osc.

Equations

• NavierStokes.MeanResidual.total base mean osc i q = base i q + mean i q + osc i q

noncomputable def NavierStokes.MeanResidual.covariance (osc : Components) (i j : Fin 3) : Scalar

The exact Reynolds product of the full oscillatory fields.

Equations

• NavierStokes.MeanResidual.covariance osc i j = NavierStokes.MeanResidual.average fun (q : NavierStokes.ProblemStatement.SpaceTime) => osc i q * osc j q

noncomputable def NavierStokes.MeanResidual.fluxDifference (base mean osc : Components) (i j : Fin 3) : Scalar

Flux difference, defined pointwise by `base i q * mean j q + mean i q * base j q + mean i q

• mean j q + covariance osc i j q`.

Equations

• NavierStokes.MeanResidual.fluxDifference base mean osc i j q = base i q * mean j q + mean i q * base j q + mean i q * mean j q + NavierStokes.MeanResidual.covariance osc i j q

theorem NavierStokes.MeanResidual.covariance_smooth {osc : Components} (ho : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (osc i)) (i j : Fin 3) : ContDiff ℝ (↑⊤) (covariance osc i j)

theorem NavierStokes.MeanResidual.covariance_symm (osc : Components) (i j : Fin 3) : covariance osc i j = covariance osc j i

theorem NavierStokes.MeanResidual.total_smooth {base mean osc : Components} (hb : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (base i)) (hm : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (mean i)) (ho : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (osc i)) (i : Fin 3) : ContDiff ℝ (↑⊤) (total base mean osc i)

theorem NavierStokes.MeanResidual.fluxDifference_smooth {base mean osc : Components} (hb : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (base i)) (hm : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (mean i)) (ho : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (osc i)) (i j : Fin 3) : ContDiff ℝ (↑⊤) (fluxDifference base mean osc i j)

theorem NavierStokes.MeanResidual.total_periodic {base mean osc : Components} (hb : ∀ (i : Fin 3), AngularInvariant (base i)) (hm : ∀ (i : Fin 3), AngularInvariant (mean i)) (ho : ∀ (i : Fin 3), AngularPeriodic (osc i)) (i : Fin 3) : AngularPeriodic (total base mean osc i)

theorem NavierStokes.MeanResidual.average_affine_product {a b f g : Scalar} (ha : AngularInvariant a) (hb : AngularInvariant b) (hf : AngularContinuous f) (hg : AngularContinuous g) (q : ProblemStatement.SpaceTime) (hf0 : average f q = 0) (hg0 : average g q = 0) : average (fun (y : ProblemStatement.SpaceTime) => (a y + f y) * (b y + g y)) q = a q * b q + average (fun (y : ProblemStatement.SpaceTime) => f y * g y) q

theorem NavierStokes.MeanResidual.average_total {base mean osc : Components} (hb : ∀ (i : Fin 3), AngularInvariant (base i)) (hm : ∀ (i : Fin 3), AngularInvariant (mean i)) (ho : ∀ (i : Fin 3), AngularContinuous (osc i)) (hz : ∀ (i : Fin 3) (q : ProblemStatement.SpaceTime), average (osc i) q = 0) (i : Fin 3) : average (total base mean osc i) = fun (q : ProblemStatement.SpaceTime) => base i q + mean i q

theorem NavierStokes.MeanResidual.average_total_product {base mean osc : Components} (hb : ∀ (i : Fin 3), AngularInvariant (base i)) (hm : ∀ (i : Fin 3), AngularInvariant (mean i)) (ho : ∀ (i : Fin 3), AngularContinuous (osc i)) (hz : ∀ (i : Fin 3) (q : ProblemStatement.SpaceTime), average (osc i) q = 0) (i j : Fin 3) : (average fun (q : ProblemStatement.SpaceTime) => total base mean osc i q * total base mean osc j q) = fun (q : ProblemStatement.SpaceTime) => base i q * base j q + fluxDifference base mean osc i j q

theorem NavierStokes.MeanResidual.fluxDifference_diagonal (base mean osc : Components) (i : Fin 3) (q : ProblemStatement.SpaceTime) : fluxDifference base mean osc i i q = 2 * base i q * mean i q + mean i q ^ 2 + covariance osc i i q

theorem NavierStokes.MeanResidual.direction_twice_add {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ProblemStatement.SpaceTime → E} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (v w q : ProblemStatement.SpaceTime) : direction v (direction w fun (y : ProblemStatement.SpaceTime) => f y + g y) q = direction v (direction w f) q + direction v (direction w g) q

theorem NavierStokes.MeanResidual.meanLaplacian_add {f g : Scalar} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (q : ProblemStatement.SpaceTime) : meanLaplacian (fun (y : ProblemStatement.SpaceTime) => f y + g y) q = meanLaplacian f q + meanLaplacian g q

theorem NavierStokes.MeanResidual.radialDivergence_add {f g : Scalar} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (c : ℝ) (q : ProblemStatement.SpaceTime) : radialDivergence c (fun (y : ProblemStatement.SpaceTime) => f y + g y) q = radialDivergence c f q + radialDivergence c g q

noncomputable def NavierStokes.MeanResidual.baseRadial (b : Components) (p : Scalar) (q : ProblemStatement.SpaceTime) : ℝ

Base radial, constructed using dt.

Equations

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

noncomputable def NavierStokes.MeanResidual.baseAngular (b : Components) (q : ProblemStatement.SpaceTime) : ℝ

Base angular, constructed using dt.

Equations

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

noncomputable def NavierStokes.MeanResidual.baseAxial (b : Components) (p : Scalar) (q : ProblemStatement.SpaceTime) : ℝ

Base axial, given by dt (b 2) q + radialDivergence 1 (fun y => b 0 y * b 2 y) q + dz (fun y => b 2 y * b 2 y) q - meanLaplacian (b 2) q + dz p q.

Equations

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

noncomputable def NavierStokes.MeanResidual.Etheta (b m o : Components) (Ttheta : Scalar) (q : ProblemStatement.SpaceTime) : ℝ

Physical version of E_theta in (32), with viscosity one.

Equations

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

noncomputable def NavierStokes.MeanResidual.Ez (b m o : Components) (pm Tz : Scalar) (q : ProblemStatement.SpaceTime) : ℝ

Physical version of E_z in (32), with viscosity one.

Equations

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

noncomputable def NavierStokes.MeanResidual.gr (b m o : Components) (q : ProblemStatement.SpaceTime) : ℝ

Required physical radial pressure derivative in (32).

Equations

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

theorem NavierStokes.MeanResidual.reynoldsAngular_total_sub {b m o : Components} (hb : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (b i)) (hm : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (m i)) (ho : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (o i)) (hbi : ∀ (i : Fin 3), AngularInvariant (b i)) (hmi : ∀ (i : Fin 3), AngularInvariant (m i)) (hz : ∀ (i : Fin 3) (q : ProblemStatement.SpaceTime), average (o i) q = 0) (Ttheta : Scalar) (q : ProblemStatement.SpaceTime) : reynoldsAngular (total b m o) q - baseAngular b q - radialDivergence 2 Ttheta q = Etheta b m o Ttheta q

theorem NavierStokes.MeanResidual.reynoldsRadial_total_sub {b m o : Components} {p pb pm : Scalar} (hb : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (b i)) (hm : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (m i)) (ho : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (o i)) (hpb : ContDiff ℝ (↑⊤) pb) (hpm : ContDiff ℝ (↑⊤) pm) (hbi : ∀ (i : Fin 3), AngularInvariant (b i)) (hmi : ∀ (i : Fin 3), AngularInvariant (m i)) (hz : ∀ (i : Fin 3) (q : ProblemStatement.SpaceTime), average (o i) q = 0) (hpavg : average p = fun (q : ProblemStatement.SpaceTime) => pb q + pm q) (q : ProblemStatement.SpaceTime) : reynoldsRadial (total b m o) p q - baseRadial b pb q = dr pm q - gr b m o q

theorem NavierStokes.MeanResidual.reynoldsAxial_total_sub {b m o : Components} {p pb pm : Scalar} (hb : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (b i)) (hm : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (m i)) (ho : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (o i)) (hpb : ContDiff ℝ (↑⊤) pb) (hpm : ContDiff ℝ (↑⊤) pm) (hbi : ∀ (i : Fin 3), AngularInvariant (b i)) (hmi : ∀ (i : Fin 3), AngularInvariant (m i)) (hz : ∀ (i : Fin 3) (q : ProblemStatement.SpaceTime), average (o i) q = 0) (hpavg : average p = fun (q : ProblemStatement.SpaceTime) => pb q + pm q) (Tz : Scalar) (q : ProblemStatement.SpaceTime) : reynoldsAxial (total b m o) p q - baseAxial b pb q - radialDivergence 1 Tz q = Ez b m o pm Tz q

theorem NavierStokes.MeanResidual.reynoldsAngular_invariant {b : Components} (hbi : ∀ (i : Fin 3), AngularInvariant (b i)) (q : ProblemStatement.SpaceTime) : reynoldsAngular b q = baseAngular b q

theorem NavierStokes.MeanResidual.reynoldsRadial_invariant {b : Components} {p : Scalar} (hbi : ∀ (i : Fin 3), AngularInvariant (b i)) (hpi : AngularInvariant p) (q : ProblemStatement.SpaceTime) : reynoldsRadial b p q = baseRadial b p q

theorem NavierStokes.MeanResidual.reynoldsAxial_invariant {b : Components} {p : Scalar} (hbi : ∀ (i : Fin 3), AngularInvariant (b i)) (hpi : AngularInvariant p) (q : ProblemStatement.SpaceTime) : reynoldsAxial b p q = baseAxial b p q

theorem NavierStokes.MeanResidual.residuals_invariant {b : Components} {p : Scalar} (hbi : ∀ (i : Fin 3), AngularInvariant (b i)) (hpi : AngularInvariant p) : AngularInvariant (residualRadial b p) ∧ AngularInvariant (residualAngular b p) ∧ AngularInvariant (residualAxial b p)

theorem NavierStokes.MeanResidual.base_residuals {b : Components} {p : Scalar} (hb : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (b i)) (hp : ContDiff ℝ (↑⊤) p) (hbi : ∀ (i : Fin 3), AngularInvariant (b i)) (hpi : AngularInvariant p) (hdiv : ∀ (y : ProblemStatement.SpaceTime), 0 < radius y → divergence b y = 0) (q : ProblemStatement.SpaceTime) (hr : 0 < radius q) : residualRadial b p q = baseRadial b p q ∧ residualAngular b p q = baseAngular b q ∧ residualAxial b p q = baseAxial b p q

theorem NavierStokes.MeanResidual.exact_mean_balances {b m o : Components} {p pb pm : Scalar} (hb : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (b i)) (hm : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (m i)) (ho : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (o i)) (hp : ContDiff ℝ (↑⊤) p) (hpb : ContDiff ℝ (↑⊤) pb) (hpm : ContDiff ℝ (↑⊤) pm) (hbi : ∀ (i : Fin 3), AngularInvariant (b i)) (hmi : ∀ (i : Fin 3), AngularInvariant (m i)) (hop : ∀ (i : Fin 3), AngularPeriodic (o i)) (hpp : AngularPeriodic p) (hpbi : AngularInvariant pb) (hz : ∀ (i : Fin 3) (q : ProblemStatement.SpaceTime), average (o i) q = 0) (hpavg : average p = fun (q : ProblemStatement.SpaceTime) => pb q + pm q) (hdiv : ∀ (y : ProblemStatement.SpaceTime), 0 < radius y → divergence (total b m o) y = 0) (hbdiv : ∀ (y : ProblemStatement.SpaceTime), 0 < radius y → divergence b y = 0) (Ttheta Tz : Scalar) (q : ProblemStatement.SpaceTime) (hr : 0 < radius q) : average (fun (y : ProblemStatement.SpaceTime) => (CylindricalResidual.cylindricalResidual (velocity (total b m o)) p y.1 y.2).ofLp 1) q - (CylindricalResidual.cylindricalResidual (velocity b) pb q.1 q.2).ofLp 1 - radialDivergence 2 Ttheta q = Etheta b m o Ttheta q ∧ average (fun (y : ProblemStatement.SpaceTime) => (CylindricalResidual.cylindricalResidual (velocity (total b m o)) p y.1 y.2).ofLp 2) q - (CylindricalResidual.cylindricalResidual (velocity b) pb q.1 q.2).ofLp 2 - radialDivergence 1 Tz q = Ez b m o pm Tz q ∧ average (fun (y : ProblemStatement.SpaceTime) => (CylindricalResidual.cylindricalResidual (velocity (total b m o)) p y.1 y.2).ofLp 0) q - (CylindricalResidual.cylindricalResidual (velocity b) pb q.1 q.2).ofLp 0 = dr pm q - gr b m o q

Exact physical mean balances (32) for the actual cylindrical residual. The tensor entries are the prescribed physical radial flux entries; covariance is the integral of the entire oscillatory field, including any curl corrections.

theorem NavierStokes.MeanResidual.Etheta_expanded (b m o : Components) (T : Scalar) (q : ProblemStatement.SpaceTime) : Etheta b m o T q = dt (m 1) q + radialDivergence 2 (fun (y : ProblemStatement.SpaceTime) => b 0 y * m 1 y + m 0 y * b 1 y + m 0 y * m 1 y + covariance o 0 1 y) q + dz (fun (y : ProblemStatement.SpaceTime) => b 2 y * m 1 y + b 1 y * m 2 y + m 2 y * m 1 y + covariance o 2 1 y) q - (meanLaplacian (m 1) q - m 1 q / radius q ^ 2) - radialDivergence 2 T q

theorem NavierStokes.MeanResidual.Ez_expanded (b m o : Components) (pm T : Scalar) (q : ProblemStatement.SpaceTime) : Ez b m o pm T q = dt (m 2) q + radialDivergence 1 (fun (y : ProblemStatement.SpaceTime) => b 0 y * m 2 y + m 0 y * b 2 y + m 0 y * m 2 y + covariance o 0 2 y) q + dz (fun (y : ProblemStatement.SpaceTime) => 2 * b 2 y * m 2 y + m 2 y ^ 2 + covariance o 2 2 y + pm y) q - meanLaplacian (m 2) q - radialDivergence 1 T q

theorem NavierStokes.MeanResidual.gr_expanded (b m o : Components) (q : ProblemStatement.SpaceTime) : gr b m o q = -(dt (m 0) q + radialDivergence 1 (fun (y : ProblemStatement.SpaceTime) => 2 * b 0 y * m 0 y + m 0 y ^ 2 + covariance o 0 0 y) q + dz (fun (y : ProblemStatement.SpaceTime) => b 0 y * m 2 y + b 2 y * m 0 y + m 0 y * m 2 y + covariance o 2 0 y) q - (2 * b 1 q * m 1 q + m 1 q ^ 2 + covariance o 1 1 q) / radius q - (meanLaplacian (m 0) q - m 0 q / radius q ^ 2))

noncomputable def NavierStokes.MeanResidual.meanPressure (p pb : Scalar) : Scalar

The perturbation pressure is defined from its actual angular mean.

Equations

• NavierStokes.MeanResidual.meanPressure p pb q = NavierStokes.MeanResidual.average p q - pb q

theorem NavierStokes.MeanResidual.meanPressure_smooth {p pb : Scalar} (hp : ContDiff ℝ (↑⊤) p) (hpb : ContDiff ℝ (↑⊤) pb) : ContDiff ℝ (↑⊤) (meanPressure p pb)

theorem NavierStokes.MeanResidual.meanPressure_reconstruction (p pb : Scalar) : average p = fun (q : ProblemStatement.SpaceTime) => pb q + meanPressure p pb q

theorem NavierStokes.MeanResidual.cylindricalDivergence_eq {w : Components} (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i)) (q : ProblemStatement.SpaceTime) : CylindricalResidual.vectorDivergence (fun (y : ProblemStatement.Space) => velocity w (q.1, y)) q.2 = divergence w q

def NavierStokes.MeanResidual.Represents (u : ProblemStatement.VelocityField) (w : Components) : Prop

Represents, given by ∀ q : SpaceTime, u (q.1, CylindricalResidual.chart q.2) = CylindricalResidual.frame (q.2 1) (velocity w q).

Equations

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

theorem NavierStokes.MeanResidual.Represents.components {u : ProblemStatement.VelocityField} {w : Components} (h : Represents u w) : CylindricalResidual.velocityComponents u = velocity w

noncomputable def NavierStokes.MeanResidual.cartesianResidual (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (i : Fin 3) (q : ProblemStatement.SpaceTime) : ℝ

Exact physical Cartesian residual resolved in the cylindrical frame.

Equations

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

theorem NavierStokes.MeanResidual.cartesianResidual_eq {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {w : Components} {P : Scalar} (hrep : Represents u w) (hpull : CylindricalResidual.pressurePullback p = P) (q : ProblemStatement.SpaceTime) (hr : 0 < radius q) (hu : ContDiffAt ℝ 2 u (q.1, CylindricalResidual.chart q.2)) (hp : DifferentiableAt ℝ p (q.1, CylindricalResidual.chart q.2)) (i : Fin 3) : cartesianResidual u p i q = (CylindricalResidual.cylindricalResidual (velocity w) P q.1 q.2).ofLp i

theorem NavierStokes.MeanResidual.cartesianDivergence_eq {u : ProblemStatement.VelocityField} {w : Components} (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i)) (hrep : Represents u w) (q : ProblemStatement.SpaceTime) (hr : 0 < radius q) (hu : ContDiffAt ℝ 2 u (q.1, CylindricalResidual.chart q.2)) : ProblemStatement.spatialDivergence u q.1 (CylindricalResidual.chart q.2) = divergence w q

theorem NavierStokes.MeanResidual.average_cartesianResidual_eq {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {w : Components} {P : Scalar} (hrep : Represents u w) (hpull : CylindricalResidual.pressurePullback p = P) (hu : ∀ (y : ProblemStatement.SpaceTime), 0 < radius y → ContDiffAt ℝ 2 u (y.1, CylindricalResidual.chart y.2)) (hp : ∀ (y : ProblemStatement.SpaceTime), 0 < radius y → DifferentiableAt ℝ p (y.1, CylindricalResidual.chart y.2)) (q : ProblemStatement.SpaceTime) (hr : 0 < radius q) (i : Fin 3) : average (cartesianResidual u p i) q = average (fun (y : ProblemStatement.SpaceTime) => (CylindricalResidual.cylindricalResidual (velocity w) P y.1 y.2).ofLp i) q

theorem NavierStokes.MeanResidual.exact_cartesian_mean_balances {u ub : ProblemStatement.VelocityField} {P Pb : ProblemStatement.PressureField} {b m o : Components} {p pb pm : Scalar} (hb : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (b i)) (hm : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (m i)) (ho : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (o i)) (hp : ContDiff ℝ (↑⊤) p) (hpb : ContDiff ℝ (↑⊤) pb) (hpm : ContDiff ℝ (↑⊤) pm) (hbi : ∀ (i : Fin 3), AngularInvariant (b i)) (hmi : ∀ (i : Fin 3), AngularInvariant (m i)) (hop : ∀ (i : Fin 3), AngularPeriodic (o i)) (hpp : AngularPeriodic p) (hpbi : AngularInvariant pb) (hz : ∀ (i : Fin 3) (q : ProblemStatement.SpaceTime), average (o i) q = 0) (hpavg : average p = fun (q : ProblemStatement.SpaceTime) => pb q + pm q) (hrep : Represents u (total b m o)) (hbrep : Represents ub b) (hpull : CylindricalResidual.pressurePullback P = p) (hbpull : CylindricalResidual.pressurePullback Pb = pb) (hu : ∀ (y : ProblemStatement.SpaceTime), 0 < radius y → ContDiffAt ℝ 2 u (y.1, CylindricalResidual.chart y.2)) (hub : ∀ (y : ProblemStatement.SpaceTime), 0 < radius y → ContDiffAt ℝ 2 ub (y.1, CylindricalResidual.chart y.2)) (hP : ∀ (y : ProblemStatement.SpaceTime), 0 < radius y → DifferentiableAt ℝ P (y.1, CylindricalResidual.chart y.2)) (hPb : ∀ (y : ProblemStatement.SpaceTime), 0 < radius y → DifferentiableAt ℝ Pb (y.1, CylindricalResidual.chart y.2)) (hdiv : ∀ (y : ProblemStatement.SpaceTime), 0 < radius y → ProblemStatement.spatialDivergence u y.1 (CylindricalResidual.chart y.2) = 0) (hbdiv : ∀ (y : ProblemStatement.SpaceTime), 0 < radius y → ProblemStatement.spatialDivergence ub y.1 (CylindricalResidual.chart y.2) = 0) (Ttheta Tz : Scalar) (q : ProblemStatement.SpaceTime) (hr : 0 < radius q) : average (cartesianResidual u P 1) q - cartesianResidual ub Pb 1 q - radialDivergence 2 Ttheta q = Etheta b m o Ttheta q ∧ average (cartesianResidual u P 2) q - cartesianResidual ub Pb 2 q - radialDivergence 1 Tz q = Ez b m o pm Tz q ∧ average (cartesianResidual u P 0) q - cartesianResidual ub Pb 0 q = dr pm q - gr b m o q

End-to-end mean balances for the actual Cartesian operators. Cartesian regularity is required only at positive-radius chart points.

theorem NavierStokes.MeanResidual.average_invariant_of_periodic {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ProblemStatement.SpaceTime → E} (hf : ContDiff ℝ (↑⊤) f) (hp : AngularPeriodic f) : AngularInvariant (average f)

theorem NavierStokes.MeanResidual.covariance_invariant {o : Components} (ho : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (o i)) (hop : ∀ (i : Fin 3), AngularPeriodic (o i)) (i j : Fin 3) : AngularInvariant (covariance o i j)

theorem NavierStokes.MeanResidual.retain_base_error {Rtheta Rz Rr Btheta Bz Br Ttheta Tz Etheta Ez Drp gr ftheta fz fr : ℝ} (hθ : Rtheta - Btheta - Ttheta = Etheta) (hz : Rz - Bz - Tz = Ez) (hr : Rr - Br = Drp - gr) (hbθ : Btheta = -Ttheta + ftheta) (hbz : Bz = -Tz + fz) (hbr : Br = fr) : Rtheta = Etheta + ftheta ∧ Rz = Ez + fz ∧ Rr = Drp - gr + fr

Substitution of (24) retains, rather than discards, its full base error.