Exact angular averages of the lifted correction residual

Angular integration is over the actual circle variable. All differentiation uses Fréchet derivatives on an open lifted strip; the graph operators are instantiated from CorrectionState.Context.operators.

noncomputable def NavierStokes.LiftedMeanResidual.cylinder {D : Type} (U : Set D) : Set (D × ℝ)

Cylinder, given by U ×ˢ univ.

Equations

• NavierStokes.LiftedMeanResidual.cylinder U = U ×ˢ Set.univ

theorem NavierStokes.LiftedMeanResidual.cylinder_open {D : Type} [NormedAddCommGroup D] {U : Set D} (hU : IsOpen U) : IsOpen (cylinder U)

theorem NavierStokes.LiftedMeanResidual.continuous_slice {D E : Type} [NormedAddCommGroup D] [NormedAddCommGroup E] {U : Set D} (hU : IsOpen U) {f : D × ℝ → E} (hf : ContinuousOn f (cylinder U)) {x : D} (hx : x ∈ U) : Continuous fun (θ : ℝ) => f (x, θ)

theorem NavierStokes.LiftedMeanResidual.constant_mul_continuous (c : ℝ) {f : ℝ → ℝ} (hf : Continuous f) : Continuous fun (t : ℝ) => c * f t

theorem NavierStokes.LiftedMeanResidual.uniform_local_bound {D E : Type} [NormedAddCommGroup D] [NormedAddCommGroup E] {U : Set D} (hU : IsOpen U) {f : D × ℝ → E} (hf : ContinuousOn f (cylinder U)) {x : D} (hx : x ∈ U) (a b : ℝ) : ∃ η > 0, ∃ (C : ℝ), Metric.ball x η ⊆ U ∧ ∀ y ∈ Metric.ball x η, ∀ θ ∈ Set.uIcc a b, ‖f (y, θ)‖ ≤ C

theorem NavierStokes.LiftedMeanResidual.parameterDerivative_smooth {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} (hU : IsOpen U) {f : D × ℝ → E} (hf : ContDiffOn ℝ (↑⊤) f (cylinder U)) : ContDiffOn ℝ (↑⊤) (TransportPrimitive.parameterDerivative f) (cylinder U)

theorem NavierStokes.LiftedMeanResidual.parameter_hasFDerivAt {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} (hU : IsOpen U) {f : D × ℝ → E} (hf : ContDiffOn ℝ (↑⊤) f (cylinder U)) {x : D} (hx : x ∈ U) (θ : ℝ) : HasFDerivAt (fun (y : D) => f (y, θ)) (TransportPrimitive.parameterDerivative f (x, θ)) x

theorem NavierStokes.LiftedMeanResidual.parameterIntegral_hasFDerivAt {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} (hU : IsOpen U) {f : D × ℝ → E} (hf : ContDiffOn ℝ (↑⊤) f (cylinder U)) (a b : ℝ) {x : D} (hx : x ∈ U) : HasFDerivAt (fun (y : D) => ∫ (θ : ℝ) in a..b, f (y, θ)) (∫ (θ : ℝ) in a..b, TransportPrimitive.parameterDerivative f (x, θ)) x

theorem NavierStokes.LiftedMeanResidual.parameterIntegral_smooth_nat {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (m : ℕ) {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : D × ℝ → E} : ContDiffOn ℝ (↑⊤) f (cylinder U) → ∀ (a b : ℝ), ContDiffOn ℝ (↑↑m) (fun (x : D) => ∫ (θ : ℝ) in a..b, f (x, θ)) U

theorem NavierStokes.LiftedMeanResidual.parameterIntegral_smooth {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {U : Set D} (hU : IsOpen U) {f : D × ℝ → E} (hf : ContDiffOn ℝ (↑⊤) f (cylinder U)) (a b : ℝ) : ContDiffOn ℝ (↑⊤) (fun (x : D) => ∫ (θ : ℝ) in a..b, f (x, θ)) U

noncomputable def NavierStokes.LiftedMeanResidual.period : ℝ

Period, given by 2 * Real.pi.

Equations

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

theorem NavierStokes.LiftedMeanResidual.period_ne : period ≠ 0

noncomputable def NavierStokes.LiftedMeanResidual.avg {D : Type} (f : D × ℝ → ℝ) (x : D) : ℝ

Avg, given by (∫ θ in (0 : ℝ)..period, f (x, θ)) / period.

Equations

• NavierStokes.LiftedMeanResidual.avg f x = (∫ (θ : ℝ) in 0..NavierStokes.LiftedMeanResidual.period, f (x, θ)) / NavierStokes.LiftedMeanResidual.period

noncomputable def NavierStokes.LiftedMeanResidual.liftDirection {D : Type} (V : D → D) (p : D × ℝ) : D × ℝ

Lift direction, given by (V p.1, 0).

Equations

• NavierStokes.LiftedMeanResidual.liftDirection V p = (V p.1, 0)

noncomputable def NavierStokes.LiftedMeanResidual.angularDirection {D : Type} [NormedAddCommGroup D] (_p : D × ℝ) : D × ℝ

Angular direction, given by (0, 1).

Equations

• NavierStokes.LiftedMeanResidual.angularDirection _p = (0, 1)

noncomputable def NavierStokes.LiftedMeanResidual.liftScalar {D : Type} (f : D → ℝ) (p : D × ℝ) : ℝ

Lift scalar, given by f p.1.

Equations

• NavierStokes.LiftedMeanResidual.liftScalar f p = f p.1

theorem NavierStokes.LiftedMeanResidual.liftDirection_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {V : D → D} (hV : ContDiffOn ℝ (↑⊤) V U) : ContDiffOn ℝ (↑⊤) (liftDirection V) (cylinder U)

theorem NavierStokes.LiftedMeanResidual.liftScalar_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {f : D → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) : ContDiffOn ℝ (↑⊤) (liftScalar f) (cylinder U)

theorem NavierStokes.LiftedMeanResidual.avg_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {f : D × ℝ → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (cylinder U)) : ContDiffOn ℝ (↑⊤) (avg f) U

theorem NavierStokes.LiftedMeanResidual.avg_lift {D : Type} (f : D → ℝ) : avg (liftScalar f) = f

theorem NavierStokes.LiftedMeanResidual.avg_add {D : Type} {f g : D × ℝ → ℝ} {x : D} (hf : Continuous fun (θ : ℝ) => f (x, θ)) (hg : Continuous fun (θ : ℝ) => g (x, θ)) : avg (fun (p : D × ℝ) => f p + g p) x = avg f x + avg g x

theorem NavierStokes.LiftedMeanResidual.avg_sub {D : Type} {f g : D × ℝ → ℝ} {x : D} (hf : Continuous fun (θ : ℝ) => f (x, θ)) (hg : Continuous fun (θ : ℝ) => g (x, θ)) : avg (fun (p : D × ℝ) => f p - g p) x = avg f x - avg g x

theorem NavierStokes.LiftedMeanResidual.avg_mul_left {D : Type} (a : D → ℝ) (f : D × ℝ → ℝ) (x : D) : avg (fun (p : D × ℝ) => a p.1 * f p) x = a x * avg f x

theorem NavierStokes.LiftedMeanResidual.avg_mul_right {D : Type} (f : D × ℝ → ℝ) (a : D → ℝ) (x : D) : avg (fun (p : D × ℝ) => f p * a p.1) x = avg f x * a x

theorem NavierStokes.LiftedMeanResidual.avg_congr {D : Type} {U : Set D} {f g : D × ℝ → ℝ} (hfg : Set.EqOn f g (cylinder U)) {x : D} (hx : x ∈ U) : avg f x = avg g x

theorem NavierStokes.LiftedMeanResidual.along_avg {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {f : D × ℝ → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (cylinder U)) (V : D → D) {x : D} (hx : x ∈ U) : HarmonicCalculus.along V (avg f) x = avg (HarmonicCalculus.along (liftDirection V) f) x

theorem NavierStokes.LiftedMeanResidual.avg_along_twice {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {f : D × ℝ → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (cylinder U)) {V : D → D} (hV : ContDiffOn ℝ (↑⊤) V U) {x : D} (hx : x ∈ U) : avg (HarmonicCalculus.along (liftDirection V) (HarmonicCalculus.along (liftDirection V) f)) x = HarmonicCalculus.along V (HarmonicCalculus.along V (avg f)) x

def NavierStokes.LiftedMeanResidual.PeriodicOn {D E : Type} (U : Set D) (f : D × ℝ → E) : Prop

Periodic on, given by ∀ x ∈ U, ∀ θ : ℝ, f (x, θ + period) = f (x, θ).

Equations

• NavierStokes.LiftedMeanResidual.PeriodicOn U f = ∀ x ∈ U, ∀ (θ : ℝ), f (x, θ + NavierStokes.LiftedMeanResidual.period) = f (x, θ)

theorem NavierStokes.LiftedMeanResidual.PeriodicOn.add {D E : Type} [NormedAddCommGroup E] {U : Set D} {f g : D × ℝ → E} (hf : PeriodicOn U f) (hg : PeriodicOn U g) : PeriodicOn U fun (p : D × ℝ) => f p + g p

theorem NavierStokes.LiftedMeanResidual.PeriodicOn.mul {D : Type} {U : Set D} {f g : D × ℝ → ℝ} (hf : PeriodicOn U f) (hg : PeriodicOn U g) : PeriodicOn U fun (p : D × ℝ) => f p * g p

theorem NavierStokes.LiftedMeanResidual.PeriodicOn.theta {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} (hU : IsOpen U) {f : D × ℝ → E} (hf : PeriodicOn U f) : PeriodicOn U (HarmonicCalculus.along angularDirection f)

theorem NavierStokes.LiftedMeanResidual.hasDerivAt_theta {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} (hU : IsOpen U) {f : D × ℝ → E} (hf : ContDiffOn ℝ (↑⊤) f (cylinder U)) {x : D} (hx : x ∈ U) (θ : ℝ) : HasDerivAt (fun (a : ℝ) => f (x, a)) (HarmonicCalculus.along angularDirection f (x, θ)) θ

theorem NavierStokes.LiftedMeanResidual.avg_theta_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {f : D × ℝ → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (cylinder U)) (hp : PeriodicOn U f) {x : D} (hx : x ∈ U) : avg (HarmonicCalculus.along angularDirection f) x = 0

theorem NavierStokes.LiftedMeanResidual.avg_theta_twice_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {f : D × ℝ → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (cylinder U)) (hp : PeriodicOn U f) {x : D} (hx : x ∈ U) : avg (HarmonicCalculus.along angularDirection (HarmonicCalculus.along angularDirection f)) x = 0

theorem NavierStokes.LiftedMeanResidual.along_lift {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {f : D → ℝ} {x : D} (hf : DifferentiableAt ℝ f x) (V : D → D) (θ : ℝ) : HarmonicCalculus.along (liftDirection V) (liftScalar f) (x, θ) = HarmonicCalculus.along V f x

theorem NavierStokes.LiftedMeanResidual.theta_lift_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {f : D → ℝ} {x : D} (hf : DifferentiableAt ℝ f x) (θ : ℝ) : HarmonicCalculus.along angularDirection (liftScalar f) (x, θ) = 0

noncomputable def NavierStokes.LiftedMeanResidual.radialVector {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : MeanIncrementBounds.Operators D) (n : ℕ) (x : D) : D

Radial vector, given by o.eR + (o.radialFrequency n * o.radialProfile x) • o.vR.

Equations

• NavierStokes.LiftedMeanResidual.radialVector o n x = o.eR + (o.radialFrequency n * o.radialProfile x) • o.vR

noncomputable def NavierStokes.LiftedMeanResidual.axialVector {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : MeanIncrementBounds.Operators D) (n : ℕ) (_x : D) : D

Axial vector, given by o.epsilon n • o.eZ.

Equations

• NavierStokes.LiftedMeanResidual.axialVector o n _x = o.epsilon n • o.eZ

noncomputable def NavierStokes.LiftedMeanResidual.temporalVector {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : MeanIncrementBounds.Operators D) (n : ℕ) (_x : D) : D

Temporal vector, given by o.fastCoefficient n • o.vT - o.epsilon n • o.eT.

Equations

• NavierStokes.LiftedMeanResidual.temporalVector o n _x = o.fastCoefficient n • o.vT - o.epsilon n • o.eT

noncomputable def NavierStokes.LiftedMeanResidual.radialDirection {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (n : ℕ) : D × ℝ → D × ℝ

Radial direction, given by liftDirection (radialVector c.operators n).

Equations

• NavierStokes.LiftedMeanResidual.radialDirection c n = NavierStokes.LiftedMeanResidual.liftDirection (NavierStokes.LiftedMeanResidual.radialVector c.operators n)

noncomputable def NavierStokes.LiftedMeanResidual.axialDirection {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (n : ℕ) : D × ℝ → D × ℝ

Axial direction, given by liftDirection (axialVector c.operators n).

Equations

• NavierStokes.LiftedMeanResidual.axialDirection c n = NavierStokes.LiftedMeanResidual.liftDirection (NavierStokes.LiftedMeanResidual.axialVector c.operators n)

noncomputable def NavierStokes.LiftedMeanResidual.timeDirection {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (n : ℕ) : D × ℝ → D × ℝ

Time direction, given by liftDirection (temporalVector c.operators n).

Equations

• NavierStokes.LiftedMeanResidual.timeDirection c n = NavierStokes.LiftedMeanResidual.liftDirection (NavierStokes.LiftedMeanResidual.temporalVector c.operators n)

noncomputable def NavierStokes.LiftedMeanResidual.complexBase {D : Type} (c : CorrectionState.Context D) (n : ℕ) (x : D × ℝ) : HarmonicCalculus.ComplexVector

Complex base, given by ![(c.base.radial n x.1 : ℂ), (c.base.angular n x.1 : ℂ), (c.base.axial n x.1 : ℂ)].

Equations

• NavierStokes.LiftedMeanResidual.complexBase c n x = ![↑(c.base.radial n x.1), ↑(c.base.angular n x.1), ↑(c.base.axial n x.1)]

noncomputable def NavierStokes.LiftedMeanResidual.complexPerturbation {D : Type} (u : CorrectionState.State D) (n : ℕ) (x : D × ℝ) : HarmonicCalculus.ComplexVector

Complex perturbation as an element of ComplexVector.

Equations

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

noncomputable def NavierStokes.LiftedMeanResidual.complexPressure {D : Type} (u : CorrectionState.State D) (n : ℕ) (x : D × ℝ) : ℂ

Complex pressure, given by (u.totalPressureIncrement n x : ℝ).

Equations

• NavierStokes.LiftedMeanResidual.complexPressure u n x = ↑(u.totalPressureIncrement n x)

noncomputable def NavierStokes.LiftedMeanResidual.virtualDivergence {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (n : ℕ) (x : D × ℝ) : Fin 3 → ℝ

Virtual divergence, given by ![0, -(c.operators.radialDiv 2 c.virtualTheta n x.1), -(c.operators.radialDiv 1 c.virtualAxial n x.1)].

Equations

• NavierStokes.LiftedMeanResidual.virtualDivergence c n x = ![0, -c.operators.radialDiv 2 c.virtualTheta n x.1, -c.operators.radialDiv 1 c.virtualAxial n x.1]

noncomputable def NavierStokes.LiftedMeanResidual.nonlinearResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (ε : ℝ) (R : D × ℝ → ℝ) (Vr Vθ Vz Vt : D × ℝ → D × ℝ) (B a : D × ℝ → HarmonicCalculus.ComplexVector) (p : D × ℝ → ℂ) (x : D × ℝ) : HarmonicCalculus.ComplexVector

Nonlinear residual, given by LinearWaveResidual.linearResidual ε R Vr Vθ Vz Vt B a p x + LinearWaveResidual.transport R Vr Vθ Vz a a x.

Equations

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

noncomputable def NavierStokes.LiftedMeanResidual.fullResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) : CorrectionState.Oscillation D

Full residual as an element of CorrectionState.Oscillation D.

Equations

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

noncomputable def NavierStokes.LiftedMeanResidual.fullGoodResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) : CorrectionState.Oscillation D

Full good residual, given by fullResidual c u - u.errors.total.

Equations

• NavierStokes.LiftedMeanResidual.fullGoodResidual c u = NavierStokes.LiftedMeanResidual.fullResidual c u - u.errors.total

noncomputable def NavierStokes.LiftedMeanResidual.angularMeanVector {D : Type} (f : CorrectionState.Oscillation D) : CorrectionState.MeanVector D

Angular mean vector, defined pointwise by CorrectionState.angularAverage (fun k p => f k p i) n x.

Equations

• NavierStokes.LiftedMeanResidual.angularMeanVector f n x i = NavierStokes.CorrectionState.angularAverage (fun (k : ℕ) (p : D × ℝ) => f k p i) n x

noncomputable def NavierStokes.LiftedMeanResidual.realDivergence {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D × ℝ → ℝ) (Vr Vθ Vz : D × ℝ → D × ℝ) (a : D × ℝ → Fin 3 → ℝ) (p : D × ℝ) : ℝ

Real divergence, given by along Vr (fun y => a y 0) p + a p 0 / R p + along Vθ (fun y => a y 1) p / R p + along Vz (fun y => a y 2) p.

Equations

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

noncomputable def NavierStokes.LiftedMeanResidual.quadraticFlux {D : Type} (B a : D × ℝ → Fin 3 → ℝ) (i j : Fin 3) (p : D × ℝ) : ℝ

Quadratic flux, given by B p i * a p j + a p i * B p j + a p i * a p j.

Equations

• NavierStokes.LiftedMeanResidual.quadraticFlux B a i j p = B p i * a p j + a p i * B p j + a p i * a p j

noncomputable def NavierStokes.LiftedMeanResidual.advectionIncrement {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D × ℝ → ℝ) (Vr Vθ Vz : D × ℝ → D × ℝ) (B a : D × ℝ → Fin 3 → ℝ) (p : D × ℝ) : Fin 3 → ℝ

Advection increment, constructed using LinearWaveResidual.realTransport.

Equations

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

noncomputable def NavierStokes.LiftedMeanResidual.conservativeFlux {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D × ℝ → ℝ) (Vr Vθ Vz : D × ℝ → D × ℝ) (J : Fin 3 → Fin 3 → D × ℝ → ℝ) (p : D × ℝ) : Fin 3 → ℝ

Conservative flux as an element of Fin 3 → ℝ.

Equations

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

theorem NavierStokes.LiftedMeanResidual.advectionIncrement_conservative {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D × ℝ → ℝ) (Vr Vθ Vz : D × ℝ → D × ℝ) {B a : D × ℝ → Fin 3 → ℝ} {p : D × ℝ} (hB : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D × ℝ) => B y i) p) (ha : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D × ℝ) => a y i) p) (i : Fin 3) : advectionIncrement R Vr Vθ Vz B a p i = conservativeFlux R Vr Vθ Vz (quadraticFlux B a) p i - realDivergence R Vr Vθ Vz B p * a p i - realDivergence R Vr Vθ Vz a p * (B p i + a p i)

The conservative quadratic identity is derived before taking an average. The two divergence errors display exactly which solenoidality is needed.

theorem NavierStokes.LiftedMeanResidual.advectionIncrement_eq_conservative {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D × ℝ → ℝ) (Vr Vθ Vz : D × ℝ → D × ℝ) {B a : D × ℝ → Fin 3 → ℝ} {p : D × ℝ} (hB : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D × ℝ) => B y i) p) (ha : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D × ℝ) => a y i) p) (hBd : realDivergence R Vr Vθ Vz B p = 0) (had : realDivergence R Vr Vθ Vz a p = 0) : advectionIncrement R Vr Vθ Vz B a p = conservativeFlux R Vr Vθ Vz (quadraticFlux B a) p

structure NavierStokes.LiftedMeanResidual.Regular {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (U : Set D) (R : D → ℝ) (Vr Vz Vt : D → D) : Prop

Regular data, collecting isOpen, radius_smooth, radius_ne, radial_smooth, axial_smooth, time_smooth.

• isOpen : IsOpen U
• radius_smooth : ContDiffOn ℝ (↑⊤) R U
• radius_ne (x : D) : x ∈ U → R x ≠ 0
• radial_smooth : ContDiffOn ℝ (↑⊤) Vr U
• axial_smooth : ContDiffOn ℝ (↑⊤) Vz U
• time_smooth : ContDiffOn ℝ (↑⊤) Vt U

theorem NavierStokes.LiftedMeanResidual.quadraticFlux_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {B a : D × ℝ → Fin 3 → ℝ} (hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D × ℝ) => B y i) (cylinder U)) (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D × ℝ) => a y i) (cylinder U)) (i j : Fin 3) : ContDiffOn ℝ (↑⊤) (quadraticFlux B a i j) (cylinder U)

theorem NavierStokes.LiftedMeanResidual.quadraticFlux_periodic {D : Type} {U : Set D} {B a : D × ℝ → Fin 3 → ℝ} (hB : ∀ (i : Fin 3), PeriodicOn U fun (y : D × ℝ) => B y i) (ha : ∀ (i : Fin 3), PeriodicOn U fun (y : D × ℝ) => a y i) (i j : Fin 3) : PeriodicOn U (quadraticFlux B a i j)

theorem NavierStokes.LiftedMeanResidual.avg_div {D : Type} (f : D × ℝ → ℝ) (a : D → ℝ) (x : D) : avg (fun (p : D × ℝ) => f p / a p.1) x = avg f x / a x

theorem NavierStokes.LiftedMeanResidual.avg_const_mul {D : Type} (c : ℝ) (f : D × ℝ → ℝ) (x : D) : avg (fun (p : D × ℝ) => c * f p) x = c * avg f x

noncomputable def NavierStokes.LiftedMeanResidual.meanConservativeFlux {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vz : D → D) (J : Fin 3 → Fin 3 → D → ℝ) (x : D) : Fin 3 → ℝ

Mean conservative flux as an element of Fin 3 → ℝ.

Equations

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

theorem NavierStokes.LiftedMeanResidual.avg_conservativeFlux {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {R : D → ℝ} {Vr Vz Vt : D → D} (G : Regular U R Vr Vz Vt) {J : Fin 3 → Fin 3 → D × ℝ → ℝ} (hJ : ∀ (i j : Fin 3), ContDiffOn ℝ (↑⊤) (J i j) (cylinder U)) (hp : ∀ (i j : Fin 3), PeriodicOn U (J i j)) {x : D} (hx : x ∈ U) (i : Fin 3) : avg (fun (p : D × ℝ) => conservativeFlux (liftScalar R) (liftDirection Vr) angularDirection (liftDirection Vz) J p i) x = meanConservativeFlux R Vr Vz (fun (i j : Fin 3) => avg (J i j)) x i

noncomputable def NavierStokes.LiftedMeanResidual.meanScalarLaplacian {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vz : D → D) (f : D → ℝ) (x : D) : ℝ

Mean scalar laplacian, given by along Vr (along Vr f) x + (R x)⁻¹ * along Vr f x + along Vz (along Vz f) x.

Equations

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

theorem NavierStokes.LiftedMeanResidual.avg_scalarLaplacian {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {R : D → ℝ} {Vr Vz Vt : D → D} (G : Regular U R Vr Vz Vt) {f : D × ℝ → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (cylinder U)) (hp : PeriodicOn U f) {x : D} (hx : x ∈ U) : avg (HarmonicCalculus.cylindricalLaplacian (liftScalar R) (liftDirection Vr) angularDirection (liftDirection Vz) f) x = meanScalarLaplacian R Vr Vz (avg f) x

theorem NavierStokes.LiftedMeanResidual.avg_neg {D : Type} (f : D × ℝ → ℝ) (x : D) : avg (fun (p : D × ℝ) => -f p) x = -avg f x

theorem NavierStokes.LiftedMeanResidual.avg_zero {D : Type} (x : D) : avg (fun (x : D × ℝ) => 0) x = 0

theorem NavierStokes.LiftedMeanResidual.Regular.scalarLaplacian_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {R : D → ℝ} {Vr Vz Vt : D → D} (G : Regular U R Vr Vz Vt) {f : D × ℝ → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (cylinder U)) : ContDiffOn ℝ (↑⊤) (HarmonicCalculus.cylindricalLaplacian (liftScalar R) (liftDirection Vr) angularDirection (liftDirection Vz) f) (cylinder U)

theorem NavierStokes.LiftedMeanResidual.Regular.frameLaplacian_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {R : D → ℝ} {Vr Vz Vt : D → D} (G : Regular U R Vr Vz Vt) {a : D × ℝ → Fin 3 → ℝ} (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (p : D × ℝ) => a p i) (cylinder U)) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (p : D × ℝ) => LinearWaveResidual.realFrameLaplacian (liftScalar R) (liftDirection Vr) angularDirection (liftDirection Vz) a p i) (cylinder U)

noncomputable def NavierStokes.LiftedMeanResidual.meanFrameLaplacian {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vz : D → D) (a : D → Fin 3 → ℝ) (x : D) (i : Fin 3) : ℝ

Mean frame laplacian, constructed using meanScalarLaplacian.

Equations

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

theorem NavierStokes.LiftedMeanResidual.avg_frameLaplacian {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {R : D → ℝ} {Vr Vz Vt : D → D} (G : Regular U R Vr Vz Vt) {a : D × ℝ → Fin 3 → ℝ} (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (p : D × ℝ) => a p i) (cylinder U)) (hp : ∀ (i : Fin 3), PeriodicOn U fun (p : D × ℝ) => a p i) {x : D} (hx : x ∈ U) (i : Fin 3) : avg (fun (p : D × ℝ) => LinearWaveResidual.realFrameLaplacian (liftScalar R) (liftDirection Vr) angularDirection (liftDirection Vz) a p i) x = meanFrameLaplacian R Vr Vz (fun (y : D) (j : Fin 3) => avg (fun (p : D × ℝ) => a p j) y) x i

theorem NavierStokes.LiftedMeanResidual.Regular.conservativeFlux_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {R : D → ℝ} {Vr Vz Vt : D → D} (G : Regular U R Vr Vz Vt) {J : Fin 3 → Fin 3 → D × ℝ → ℝ} (hJ : ∀ (i j : Fin 3), ContDiffOn ℝ (↑⊤) (J i j) (cylinder U)) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (p : D × ℝ) => conservativeFlux (liftScalar R) (liftDirection Vr) angularDirection (liftDirection Vz) J p i) (cylinder U)

noncomputable def NavierStokes.LiftedMeanResidual.realGradient {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D × ℝ → ℝ) (Vr Vθ Vz : D × ℝ → D × ℝ) (p : D × ℝ → ℝ) (x : D × ℝ) : Fin 3 → ℝ

Real gradient, given by ![along Vr p x, (R x)⁻¹ * along Vθ p x, along Vz p x].

Equations

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

noncomputable def NavierStokes.LiftedMeanResidual.meanGradient {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (Vr Vz : D → D) (p : D → ℝ) (x : D) : Fin 3 → ℝ

Mean gradient, given by ![along Vr p x, 0, along Vz p x].

Equations

• NavierStokes.LiftedMeanResidual.meanGradient Vr Vz p x = ![NavierStokes.HarmonicCalculus.along Vr p x, 0, NavierStokes.HarmonicCalculus.along Vz p x]

theorem NavierStokes.LiftedMeanResidual.Regular.gradient_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {R : D → ℝ} {Vr Vz Vt : D → D} (G : Regular U R Vr Vz Vt) {p : D × ℝ → ℝ} (hp : ContDiffOn ℝ (↑⊤) p (cylinder U)) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (x : D × ℝ) => realGradient (liftScalar R) (liftDirection Vr) angularDirection (liftDirection Vz) p x i) (cylinder U)

theorem NavierStokes.LiftedMeanResidual.avg_gradient {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {R : D → ℝ} {Vr Vz Vt : D → D} (G : Regular U R Vr Vz Vt) {p : D × ℝ → ℝ} (hp : ContDiffOn ℝ (↑⊤) p (cylinder U)) (hper : PeriodicOn U p) {x : D} (hx : x ∈ U) (i : Fin 3) : avg (fun (y : D × ℝ) => realGradient (liftScalar R) (liftDirection Vr) angularDirection (liftDirection Vz) p y i) x = meanGradient Vr Vz (avg p) x i

noncomputable def NavierStokes.LiftedMeanResidual.realNonlinearResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (ε : ℝ) (R : D × ℝ → ℝ) (Vr Vθ Vz Vt : D × ℝ → D × ℝ) (B a : D × ℝ → Fin 3 → ℝ) (p : D × ℝ → ℝ) (x : D × ℝ) : Fin 3 → ℝ

Real nonlinear residual, given by LinearWaveResidual.realComponentLinearResidual ε R Vr Vθ Vz Vt B a p x + LinearWaveResidual.realTransport R Vr Vθ Vz a a x.

Equations

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

theorem NavierStokes.LiftedMeanResidual.nonlinearResidual_realLift {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {R : D → ℝ} {Vr Vz Vt : D → D} (G : Regular U R Vr Vz Vt) (ε : ℝ) {B a : D × ℝ → Fin 3 → ℝ} {p : D × ℝ → ℝ} (hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D × ℝ) => B y i) (cylinder U)) (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D × ℝ) => a y i) (cylinder U)) (hp : ContDiffOn ℝ (↑⊤) p (cylinder U)) {x : D × ℝ} (hx : x ∈ cylinder U) (i : Fin 3) : (nonlinearResidual ε (liftScalar R) (liftDirection Vr) angularDirection (liftDirection Vz) (liftDirection Vt) (LinearWaveResidual.realLift B) (LinearWaveResidual.realLift a) (fun (y : D × ℝ) => ↑(p y)) x i).re = realNonlinearResidual ε (liftScalar R) (liftDirection Vr) angularDirection (liftDirection Vz) (liftDirection Vt) B a p x i

theorem NavierStokes.LiftedMeanResidual.realNonlinearResidual_conservative {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (ε : ℝ) (R : D × ℝ → ℝ) (Vr Vθ Vz Vt : D × ℝ → D × ℝ) {B a : D × ℝ → Fin 3 → ℝ} (p : D × ℝ → ℝ) {x : D × ℝ} (hB : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D × ℝ) => B y i) x) (ha : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D × ℝ) => a y i) x) (hBd : realDivergence R Vr Vθ Vz B x = 0) (had : realDivergence R Vr Vθ Vz a x = 0) (i : Fin 3) : realNonlinearResidual ε R Vr Vθ Vz Vt B a p x i = HarmonicCalculus.along Vt (fun (y : D × ℝ) => a y i) x + conservativeFlux R Vr Vθ Vz (quadraticFlux B a) x i + realGradient R Vr Vθ Vz p x i - ε * LinearWaveResidual.realFrameLaplacian R Vr Vθ Vz a x i

noncomputable def NavierStokes.LiftedMeanResidual.meanExpression {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (ε : ℝ) (R : D → ℝ) (Vr Vz Vt : D → D) (a : D → Fin 3 → ℝ) (p : D → ℝ) (J : Fin 3 → Fin 3 → D → ℝ) (x : D) (i : Fin 3) : ℝ

Mean expression, given by `along Vt (fun y => a y i) x + meanConservativeFlux R Vr Vz J x i

• meanGradient Vr Vz p x i - ε * meanFrameLaplacian R Vr Vz a x i`.

Equations

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

theorem NavierStokes.LiftedMeanResidual.avg_realNonlinearResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {R : D → ℝ} {Vr Vz Vt : D → D} (G : Regular U R Vr Vz Vt) (ε : ℝ) {B a : D × ℝ → Fin 3 → ℝ} {p : D × ℝ → ℝ} (hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D × ℝ) => B y i) (cylinder U)) (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D × ℝ) => a y i) (cylinder U)) (hp : ContDiffOn ℝ (↑⊤) p (cylinder U)) (hBper : ∀ (i : Fin 3), PeriodicOn U fun (y : D × ℝ) => B y i) (haper : ∀ (i : Fin 3), PeriodicOn U fun (y : D × ℝ) => a y i) (hpper : PeriodicOn U p) (hBd : ∀ y ∈ cylinder U, realDivergence (liftScalar R) (liftDirection Vr) angularDirection (liftDirection Vz) B y = 0) (had : ∀ y ∈ cylinder U, realDivergence (liftScalar R) (liftDirection Vr) angularDirection (liftDirection Vz) a y = 0) {x : D} (hx : x ∈ U) (i : Fin 3) : avg (fun (y : D × ℝ) => realNonlinearResidual ε (liftScalar R) (liftDirection Vr) angularDirection (liftDirection Vz) (liftDirection Vt) B a p y i) x = meanExpression ε R Vr Vz Vt (fun (y : D) (j : Fin 3) => avg (fun (p : D × ℝ) => a p j) y) (avg p) (fun (j k : Fin 3) => avg (quadraticFlux B a j k)) x i

Reynolds averaging for the full real lifted nonlinear residual.

theorem NavierStokes.LiftedMeanResidual.dr_eq_along {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : MeanIncrementBounds.Operators D) (f : MeanIncrementBounds.Field D) (n : ℕ) (x : D) : o.dr f n x = HarmonicCalculus.along (radialVector o n) (f n) x

theorem NavierStokes.LiftedMeanResidual.dz_eq_along {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : MeanIncrementBounds.Operators D) (f : MeanIncrementBounds.Field D) (n : ℕ) (x : D) : o.dz f n x = HarmonicCalculus.along (axialVector o n) (f n) x

theorem NavierStokes.LiftedMeanResidual.time_eq_along {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : MeanIncrementBounds.Operators D) (f : MeanIncrementBounds.Field D) (n : ℕ) (x : D) : o.time f n x = HarmonicCalculus.along (temporalVector o n) (f n) x

theorem NavierStokes.LiftedMeanResidual.radialDiv_eq {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : MeanIncrementBounds.Operators D) (c : ℝ) (f : MeanIncrementBounds.Field D) (n : ℕ) (x : D) : o.radialDiv c f n x = HarmonicCalculus.along (radialVector o n) (f n) x + c * f n x / o.radius x

theorem NavierStokes.LiftedMeanResidual.viscosity_eq {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : MeanIncrementBounds.Operators D) (c : ℝ) (f : MeanIncrementBounds.Field D) (n : ℕ) (x : D) : o.viscosity c f n x = o.epsilon n * (meanScalarLaplacian o.radius (radialVector o n) (axialVector o n) (f n) x - c * (o.radius x ^ 2)⁻¹ * f n x)

noncomputable def NavierStokes.LiftedMeanResidual.tripleVector {D : Type} (m : MeanIncrementBounds.Triple D) (n : ℕ) (x : D) : Fin 3 → ℝ

Triple vector, given by ![m.radial n x, m.angular n x, m.axial n x].

Equations

• NavierStokes.LiftedMeanResidual.tripleVector m n x = ![m.radial n x, m.angular n x, m.axial n x]

noncomputable def NavierStokes.LiftedMeanResidual.baseLift {D : Type} (c : CorrectionState.Context D) (n : ℕ) (p : D × ℝ) : Fin 3 → ℝ

Base lift, given by tripleVector c.base n p.1.

Equations

• NavierStokes.LiftedMeanResidual.baseLift c n p = NavierStokes.LiftedMeanResidual.tripleVector c.base n p.1

noncomputable def NavierStokes.LiftedMeanResidual.perturbation {D : Type} (u : CorrectionState.State D) (n : ℕ) (p : D × ℝ) : Fin 3 → ℝ

Perturbation, given by tripleVector u.mean n p.1 + u.oscillation n p.

Equations

• NavierStokes.LiftedMeanResidual.perturbation u n p = NavierStokes.LiftedMeanResidual.tripleVector u.mean n p.1 + u.oscillation n p

theorem NavierStokes.LiftedMeanResidual.complexBase_eq {D : Type} (c : CorrectionState.Context D) (n : ℕ) : complexBase c n = LinearWaveResidual.realLift (baseLift c n)

theorem NavierStokes.LiftedMeanResidual.complexPerturbation_eq {D : Type} (u : CorrectionState.State D) (n : ℕ) : complexPerturbation u n = LinearWaveResidual.realLift (perturbation u n)

theorem NavierStokes.LiftedMeanResidual.totalVelocity_eq {D : Type} (c : CorrectionState.Context D) (u : CorrectionState.State D) (n : ℕ) : u.totalVelocity c n = fun (p : D × ℝ) => baseLift c n p + perturbation u n p

theorem NavierStokes.LiftedMeanResidual.tripleVector_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {m : MeanIncrementBounds.Triple D} (hm : MeanIncrementBounds.SmoothTriple U m) (n : ℕ) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (x : D) => tripleVector m n x i) U

structure NavierStokes.LiftedMeanResidual.MeanHypotheses {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (U : Set D) (c : CorrectionState.Context D) (u : CorrectionState.State D) : Prop

Primitive hypotheses on the actual state. The mean-PDE identity is a conclusion, and is not a field of this structure.

• isOpen : IsOpen U
• radius_smooth : ContDiffOn ℝ (↑⊤) c.operators.radius U
• radius_ne (x : D) : x ∈ U → c.operators.radius x ≠ 0
• profile_smooth : ContDiffOn ℝ (↑⊤) c.operators.radialProfile U
• base_smooth : MeanIncrementBounds.SmoothTriple U c.base
• mean_smooth : MeanIncrementBounds.SmoothTriple U u.mean
• pressure_smooth : MeanIncrementBounds.SmoothOn U u.pressure
• oscillation_smooth (n : ℕ) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (p : D × ℝ) => u.oscillation n p i) (cylinder U)
• oscillatoryPressure_smooth (n : ℕ) : ContDiffOn ℝ (↑⊤) (u.oscillatoryPressure n) (cylinder U)
• oscillation_periodic (n : ℕ) (i : Fin 3) : PeriodicOn U fun (p : D × ℝ) => u.oscillation n p i
• oscillatoryPressure_periodic (n : ℕ) : PeriodicOn U (u.oscillatoryPressure n)
• oscillation_mean_zero (n : ℕ) (x : D) : x ∈ U → ∀ (i : Fin 3), CorrectionState.angularAverage (fun (k : ℕ) (p : D × ℝ) => u.oscillation k p i) n x = 0
• oscillatoryPressure_mean_zero (n : ℕ) (x : D) : x ∈ U → CorrectionState.angularAverage u.oscillatoryPressure n x = 0
• base_divergence (n : ℕ) (p : D × ℝ) : p ∈ cylinder U → realDivergence (liftScalar c.operators.radius) (radialDirection c n) angularDirection (axialDirection c n) (baseLift c n) p = 0
• total_divergence (n : ℕ) (p : D × ℝ) : p ∈ cylinder U → realDivergence (liftScalar c.operators.radius) (radialDirection c n) angularDirection (axialDirection c n) (u.totalVelocity c n) p = 0
• base_error_continuous (n : ℕ) (x : D) : x ∈ U → ∀ (i : Fin 3), Continuous fun (θ : ℝ) => u.errors.base n (x, θ) i
• excluded_continuous (n : ℕ) (x : D) : x ∈ U → ∀ (i : Fin 3), Continuous fun (θ : ℝ) => u.errors.total n (x, θ) i

theorem NavierStokes.LiftedMeanResidual.MeanHypotheses.regular {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : CorrectionState.Context D} {u : CorrectionState.State D} (H : MeanHypotheses U c u) (n : ℕ) : Regular U c.operators.radius (radialVector c.operators n) (axialVector c.operators n) (temporalVector c.operators n)

theorem NavierStokes.LiftedMeanResidual.MeanHypotheses.baseLift_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : CorrectionState.Context D} {u : CorrectionState.State D} (H : MeanHypotheses U c u) (n : ℕ) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (p : D × ℝ) => baseLift c n p i) (cylinder U)

theorem NavierStokes.LiftedMeanResidual.MeanHypotheses.perturbation_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : CorrectionState.Context D} {u : CorrectionState.State D} (H : MeanHypotheses U c u) (n : ℕ) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (p : D × ℝ) => perturbation u n p i) (cylinder U)

theorem NavierStokes.LiftedMeanResidual.MeanHypotheses.pressureIncrement_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : CorrectionState.Context D} {u : CorrectionState.State D} (H : MeanHypotheses U c u) (n : ℕ) : ContDiffOn ℝ (↑⊤) (u.totalPressureIncrement n) (cylinder U)

theorem NavierStokes.LiftedMeanResidual.realDivergence_add {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D × ℝ → ℝ) (Vr Vθ Vz : D × ℝ → D × ℝ) {a b : D × ℝ → Fin 3 → ℝ} {p : D × ℝ} (ha : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D × ℝ) => a y i) p) (hb : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D × ℝ) => b y i) p) : realDivergence R Vr Vθ Vz (fun (y : D × ℝ) => a y + b y) p = realDivergence R Vr Vθ Vz a p + realDivergence R Vr Vθ Vz b p

theorem NavierStokes.LiftedMeanResidual.MeanHypotheses.perturbation_divergence {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : CorrectionState.Context D} {u : CorrectionState.State D} (H : MeanHypotheses U c u) (n : ℕ) {p : D × ℝ} (hp : p ∈ cylinder U) : realDivergence (liftScalar c.operators.radius) (radialDirection c n) angularDirection (axialDirection c n) (perturbation u n) p = 0

theorem NavierStokes.LiftedMeanResidual.periodic_lift {D : Type} (U : Set D) (f : D → ℝ) : PeriodicOn U (liftScalar f)

theorem NavierStokes.LiftedMeanResidual.MeanHypotheses.baseLift_periodic {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : CorrectionState.Context D} {u : CorrectionState.State D} (_H : MeanHypotheses U c u) (n : ℕ) (i : Fin 3) : PeriodicOn U fun (p : D × ℝ) => baseLift c n p i

theorem NavierStokes.LiftedMeanResidual.MeanHypotheses.perturbation_periodic {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : CorrectionState.Context D} {u : CorrectionState.State D} (H : MeanHypotheses U c u) (n : ℕ) (i : Fin 3) : PeriodicOn U fun (p : D × ℝ) => perturbation u n p i

theorem NavierStokes.LiftedMeanResidual.MeanHypotheses.pressureIncrement_periodic {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : CorrectionState.Context D} {u : CorrectionState.State D} (H : MeanHypotheses U c u) (n : ℕ) : PeriodicOn U (u.totalPressureIncrement n)

theorem NavierStokes.LiftedMeanResidual.avg_affine {D : Type} (a : D → ℝ) {f : D × ℝ → ℝ} {x : D} (hf : Continuous fun (θ : ℝ) => f (x, θ)) (hz : avg f x = 0) : avg (fun (p : D × ℝ) => a p.1 + f p) x = a x

theorem NavierStokes.LiftedMeanResidual.avg_affine_product {D : Type} (a b : D → ℝ) {f g : D × ℝ → ℝ} {x : D} (hf : Continuous fun (θ : ℝ) => f (x, θ)) (hg : Continuous fun (θ : ℝ) => g (x, θ)) (hf0 : avg f x = 0) (hg0 : avg g x = 0) : avg (fun (p : D × ℝ) => (a p.1 + f p) * (b p.1 + g p)) x = a x * b x + avg (fun (p : D × ℝ) => f p * g p) x

theorem NavierStokes.LiftedMeanResidual.MeanHypotheses.avg_perturbation {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : CorrectionState.Context D} {u : CorrectionState.State D} (H : MeanHypotheses U c u) (n : ℕ) {x : D} (hx : x ∈ U) (i : Fin 3) : avg (fun (p : D × ℝ) => perturbation u n p i) x = tripleVector u.mean n x i

theorem NavierStokes.LiftedMeanResidual.MeanHypotheses.avg_pressureIncrement {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : CorrectionState.Context D} {u : CorrectionState.State D} (H : MeanHypotheses U c u) (n : ℕ) {x : D} (hx : x ∈ U) : avg (u.totalPressureIncrement n) x = u.pressure n x

noncomputable def NavierStokes.LiftedMeanResidual.stateFlux {D : Type} (c : CorrectionState.Context D) (u : CorrectionState.State D) (i j : Fin 3) (n : ℕ) (x : D) : ℝ

State flux, constructed using tripleVector.

Equations

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

theorem NavierStokes.LiftedMeanResidual.MeanHypotheses.avg_quadraticFlux {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : CorrectionState.Context D} {u : CorrectionState.State D} (H : MeanHypotheses U c u) (n : ℕ) {x : D} (hx : x ∈ U) (i j : Fin 3) : avg (quadraticFlux (baseLift c n) (perturbation u n) i j) x = stateFlux c u i j n x

theorem NavierStokes.LiftedMeanResidual.MeanHypotheses.covariance_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : CorrectionState.Context D} {u : CorrectionState.State D} (H : MeanHypotheses U c u) (i j : Fin 3) : MeanIncrementBounds.SmoothOn U (u.covariance i j)

theorem NavierStokes.LiftedMeanResidual.MeanHypotheses.stateFlux_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : CorrectionState.Context D} {u : CorrectionState.State D} (H : MeanHypotheses U c u) (i j : Fin 3) : MeanIncrementBounds.SmoothOn U (stateFlux c u i j)

theorem NavierStokes.LiftedMeanResidual.meanExpression_congr {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (ε : ℝ) (R : D → ℝ) (Vr Vz Vt : D → D) {a b : D → Fin 3 → ℝ} {p q : D → ℝ} {J K : Fin 3 → Fin 3 → D → ℝ} (hab : ∀ (i : Fin 3), Set.EqOn (fun (x : D) => a x i) (fun (x : D) => b x i) U) (hpq : Set.EqOn p q U) (hJK : ∀ (i j : Fin 3), Set.EqOn (J i j) (K i j) U) {x : D} (hx : x ∈ U) (i : Fin 3) : meanExpression ε R Vr Vz Vt a p J x i = meanExpression ε R Vr Vz Vt b q K x i

theorem NavierStokes.LiftedMeanResidual.stateFlux_00 {D : Type} (c : CorrectionState.Context D) (u : CorrectionState.State D) : stateFlux c u 0 0 = MeanIncrementBounds.radialRadial c.base u.mean + u.covariance 0 0

theorem NavierStokes.LiftedMeanResidual.stateFlux_01 {D : Type} (c : CorrectionState.Context D) (u : CorrectionState.State D) : stateFlux c u 0 1 = MeanIncrementBounds.thetaRadial c.base u.mean + u.covariance 0 1

theorem NavierStokes.LiftedMeanResidual.stateFlux_02 {D : Type} (c : CorrectionState.Context D) (u : CorrectionState.State D) : stateFlux c u 0 2 = MeanIncrementBounds.axialRadial c.base u.mean + u.covariance 0 2

theorem NavierStokes.LiftedMeanResidual.stateFlux_11 {D : Type} (c : CorrectionState.Context D) (u : CorrectionState.State D) : stateFlux c u 1 1 = MeanIncrementBounds.radialAngular c.base u.mean + u.covariance 1 1

theorem NavierStokes.LiftedMeanResidual.stateFlux_20 {D : Type} (c : CorrectionState.Context D) (u : CorrectionState.State D) : stateFlux c u 2 0 = MeanIncrementBounds.axialRadial c.base u.mean + u.covariance 2 0

theorem NavierStokes.LiftedMeanResidual.stateFlux_21 {D : Type} (c : CorrectionState.Context D) (u : CorrectionState.State D) : stateFlux c u 2 1 = MeanIncrementBounds.thetaAxial c.base u.mean + u.covariance 2 1

theorem NavierStokes.LiftedMeanResidual.stateFlux_22 {D : Type} (c : CorrectionState.Context D) (u : CorrectionState.State D) : stateFlux c u 2 2 = MeanIncrementBounds.axialAxial c.base u.mean + u.covariance 2 2

theorem NavierStokes.LiftedMeanResidual.meanExpression_state {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : CorrectionState.Context D} {u : CorrectionState.State D} (H : MeanHypotheses U c u) (n : ℕ) {x : D} (hx : x ∈ U) (i : Fin 3) : meanExpression (c.operators.epsilon n) c.operators.radius (radialVector c.operators n) (axialVector c.operators n) (temporalVector c.operators n) (tripleVector u.mean n) (u.pressure n) (fun (j k : Fin 3) => stateFlux c u j k n) x i + virtualDivergence c n (x, 0) i = u.reducedMeanResidual c n x i

noncomputable def NavierStokes.LiftedMeanResidual.nonlinearField {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) : CorrectionState.Oscillation D

Nonlinear field as an element of CorrectionState.Oscillation D.

Equations

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

theorem NavierStokes.LiftedMeanResidual.MeanHypotheses.nonlinearField_eq_real {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : CorrectionState.Context D} {u : CorrectionState.State D} (H : MeanHypotheses U c u) (n : ℕ) {p : D × ℝ} (hp : p ∈ cylinder U) (i : Fin 3) : nonlinearField c u n p i = realNonlinearResidual (c.operators.epsilon n) (liftScalar c.operators.radius) (radialDirection c n) angularDirection (axialDirection c n) (timeDirection c n) (baseLift c n) (perturbation u n) (u.totalPressureIncrement n) p i

theorem NavierStokes.LiftedMeanResidual.MeanHypotheses.nonlinearField_continuous {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : CorrectionState.Context D} {u : CorrectionState.State D} (H : MeanHypotheses U c u) (n : ℕ) {x : D} (hx : x ∈ U) (i : Fin 3) : Continuous fun (θ : ℝ) => nonlinearField c u n (x, θ) i

theorem NavierStokes.LiftedMeanResidual.MeanHypotheses.avg_nonlinearField {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : CorrectionState.Context D} {u : CorrectionState.State D} (H : MeanHypotheses U c u) (n : ℕ) {x : D} (hx : x ∈ U) (i : Fin 3) : avg (fun (p : D × ℝ) => nonlinearField c u n p i) x = meanExpression (c.operators.epsilon n) c.operators.radius (radialVector c.operators n) (axialVector c.operators n) (temporalVector c.operators n) (tripleVector u.mean n) (u.pressure n) (fun (j k : Fin 3) => stateFlux c u j k n) x i

theorem NavierStokes.LiftedMeanResidual.avg_virtualDivergence {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (n : ℕ) (x : D) (i : Fin 3) : avg (fun (p : D × ℝ) => virtualDivergence c n p i) x = virtualDivergence c n (x, 0) i

theorem NavierStokes.LiftedMeanResidual.angularMean_fullResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : CorrectionState.Context D} {u : CorrectionState.State D} (H : MeanHypotheses U c u) (n : ℕ) {x : D} (hx : x ∈ U) (i : Fin 3) : angularMeanVector (fullResidual c u) n x i = u.meanResidual c n x i

The actual full residual averages to equation (32) plus exactly the stored base error.

theorem NavierStokes.LiftedMeanResidual.angularMean_fullGoodResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : CorrectionState.Context D} {u : CorrectionState.State D} (H : MeanHypotheses U c u) (n : ℕ) {x : D} (hx : x ∈ U) (i : Fin 3) : angularMeanVector (fullGoodResidual c u) n x i = u.meanGoodResidual c n x i

No Gaussian or alias term is silently discarded: the exact angular mean of the explicitly subtracted total is removed on both sides.

theorem NavierStokes.LiftedMeanResidual.meanGoodResidual_errors {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (n : ℕ) (x : D) (i : Fin 3) (hb : Continuous fun (θ : ℝ) => u.errors.base n (x, θ) i) (hg : Continuous fun (θ : ℝ) => u.errors.gaussian n (x, θ) i) (ha : Continuous fun (θ : ℝ) => u.errors.aliasError n (x, θ) i) : u.meanGoodResidual c n x i = u.reducedMeanResidual c n x i - CorrectionState.angularAverage (fun (k : ℕ) (p : D × ℝ) => u.errors.gaussian k p i) n x - CorrectionState.angularAverage (fun (k : ℕ) (p : D × ℝ) => u.errors.aliasError k p i) n x

theorem NavierStokes.LiftedMeanResidual.angularMean_fullGoodResidual_errors {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : CorrectionState.Context D} {u : CorrectionState.State D} (H : MeanHypotheses U c u) (n : ℕ) {x : D} (hx : x ∈ U) (i : Fin 3) (hg : Continuous fun (θ : ℝ) => u.errors.gaussian n (x, θ) i) (ha : Continuous fun (θ : ℝ) => u.errors.aliasError n (x, θ) i) : angularMeanVector (fullGoodResidual c u) n x i = u.reducedMeanResidual c n x i - CorrectionState.angularAverage (fun (k : ℕ) (p : D × ℝ) => u.errors.gaussian k p i) n x - CorrectionState.angularAverage (fun (k : ℕ) (p : D × ℝ) => u.errors.aliasError k p i) n x

theorem NavierStokes.LiftedMeanResidual.graphOperators_profile_smooth {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : CorrectionState.ReconstructionData) (epsilon fast : ℕ → ℝ) (axial slowTime : S × PressureStream.Plane) (temporal : PressureStream.Plane) {U : Set (PressureStream.Lift S)} (hpos : ∀ x ∈ U, 0 < x.1) : ContDiffOn ℝ (↑⊤) (CorrectionState.graphOperators r epsilon fast axial slowTime temporal).radialProfile U

The actual power-graph profile is smooth on every positive radial strip.

theorem NavierStokes.LiftedMeanResidual.graphOperators_regular {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : CorrectionState.ReconstructionData) (epsilon fast : ℕ → ℝ) (axial slowTime : S × PressureStream.Plane) (temporal : PressureStream.Plane) {U : Set (PressureStream.Lift S)} (hU : IsOpen U) (hpos : ∀ x ∈ U, 0 < x.1) (n : ℕ) : have o := CorrectionState.graphOperators r epsilon fast axial slowTime temporal; Regular U o.radius (radialVector o n) (axialVector o n) (temporalVector o n)

Direct instantiation by the genuine graph operators used by the state.