Measured moment balances in the actual moving pressure gauge

The pressure coefficient is the measured second moment of the normalized physical density. It varies with the true similarity coordinate. All moment identities below use the actual state residual and the actual pressure recipe.

Actual state moment balances

Auxiliary torus averaging, radial integration, and the pressure constructor connect the literal state residual to its actual slow debt derivatives.

noncomputable def NavierStokes.StateMomentBalances.meanBar {S : Type} (f : CorrectionState.ScalarField (CorrectionState.Lift S)) : CorrectionState.ScalarField (CorrectionState.Lift S)

Mean bar, defined pointwise by MeanMomentBounds.liftedTorusAverage (f n).

Equations

• NavierStokes.StateMomentBalances.meanBar f n = NavierStokes.MeanMomentBounds.liftedTorusAverage (f n)

noncomputable def NavierStokes.StateMomentBalances.AuxiliaryAverage.unshuffle {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] : ((ℝ × S) × ℝ) × ℝ →L[ℝ] CorrectionState.Lift S

Coordinates ordered to match the two actual interval integrals.

Equations

• NavierStokes.StateMomentBalances.AuxiliaryAverage.unshuffle = { toFun := fun (x : ((ℝ × S) × ℝ) × ℝ) => (x.1.1.1, x.1.1.2, x.2, x.1.2), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

noncomputable def NavierStokes.StateMomentBalances.AuxiliaryAverage.slowProjection {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] : CorrectionState.Lift S →L[ℝ] ℝ × S

Slow projection, bundling toFun, map_add, map_smul, cont.

Equations

• NavierStokes.StateMomentBalances.AuxiliaryAverage.slowProjection = { toFun := fun (x : NavierStokes.CorrectionState.Lift S) => (x.1, x.2.1), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

theorem NavierStokes.StateMomentBalances.AuxiliaryAverage.pullback_derivative {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {f : CorrectionState.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (x v : ((ℝ × S) × ℝ) × ℝ) : (fderiv ℝ (f ∘ ⇑unshuffle) x) v = (fderiv ℝ f (unshuffle x)) (unshuffle v)

theorem NavierStokes.StateMomentBalances.AuxiliaryAverage.pullback_periodic {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {f : CorrectionState.Lift S → ℝ} (hp : PressureStream.TorusPeriodicLift f) : IntegratedMeanBalances.TorusPeriodic (f ∘ ⇑unshuffle)

theorem NavierStokes.StateMomentBalances.AuxiliaryAverage.average_slowDerivative {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {f : CorrectionState.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (v x : ℝ × S) : PressureStream.torusAverage (fun (y : PressureStream.Lift S) => (fderiv ℝ f y) (v.1, v.2, 0)) x = (fderiv ℝ (PressureStream.torusAverage f) x) v

theorem NavierStokes.StateMomentBalances.AuxiliaryAverage.average_torusDerivative {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {f : CorrectionState.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (v : PressureStream.Plane) (x : ℝ × S) : PressureStream.torusAverage (fun (y : PressureStream.Lift S) => (fderiv ℝ f y) (0, 0, v)) x = 0

theorem NavierStokes.StateMomentBalances.AuxiliaryAverage.average_add {S : Type} [NormedAddCommGroup S] {f g : CorrectionState.Lift S → ℝ} (hf : Continuous f) (hg : Continuous g) (x : ℝ × S) : PressureStream.torusAverage (fun (y : PressureStream.Lift S) => f y + g y) x = PressureStream.torusAverage f x + PressureStream.torusAverage g x

theorem NavierStokes.StateMomentBalances.AuxiliaryAverage.average_derivative {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {f : CorrectionState.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (v x : CorrectionState.Lift S) : PressureStream.torusAverage (fun (y : PressureStream.Lift S) => (fderiv ℝ f y) v) (x.1, x.2.1) = (fderiv ℝ (MeanMomentBounds.liftedTorusAverage f) x) v

The actual torus mean commutes with fixed slow derivatives and removes the periodic directions. This does not assume a commuting inverse.

theorem NavierStokes.StateMomentBalances.AuxiliaryAverage.average_const_mul {S : Type} (c : ℝ) (f : CorrectionState.Lift S → ℝ) (x : ℝ × S) : PressureStream.torusAverage (fun (y : PressureStream.Lift S) => c * f y) x = c * PressureStream.torusAverage f x

theorem NavierStokes.StateMomentBalances.AuxiliaryAverage.average_linear {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {f : CorrectionState.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (v w : CorrectionState.Lift S) (a b : ℝ × S → ℝ) (x : CorrectionState.Lift S) : PressureStream.torusAverage (fun (y : PressureStream.Lift S) => (fderiv ℝ f y) v + a (y.1, y.2.1) * (fderiv ℝ f y) w + b (y.1, y.2.1) * f y) (x.1, x.2.1) = (fderiv ℝ (MeanMomentBounds.liftedTorusAverage f) x) v + a (x.1, x.2.1) * (fderiv ℝ (MeanMomentBounds.liftedTorusAverage f) x) w + b (x.1, x.2.1) * MeanMomentBounds.liftedTorusAverage f x

theorem NavierStokes.StateMomentBalances.AuxiliaryAverage.meanBar_dz {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (o : MeanIncrementBounds.Operators (CorrectionState.Lift S)) (f : CorrectionState.ScalarField (CorrectionState.Lift S)) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (f n)) : meanBar (o.dz f) = o.dz (meanBar f)

theorem NavierStokes.StateMomentBalances.AuxiliaryAverage.meanBar_radialDiv {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (o : MeanIncrementBounds.Operators (CorrectionState.Lift S)) (hradius : o.radius = Prod.fst) (hprofile : ∀ (R : ℝ) (z : S) (Y : PressureStream.Plane), o.radialProfile (R, z, Y) = o.radialProfile (R, z, 0)) (f : CorrectionState.ScalarField (CorrectionState.Lift S)) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (f n)) (c : ℝ) : meanBar (o.radialDiv c f) = o.radialDiv c (meanBar f)

theorem NavierStokes.StateMomentBalances.AuxiliaryAverage.meanBar_add {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (f g : CorrectionState.ScalarField (CorrectionState.Lift S)) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hg : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (g n)) : meanBar (f + g) = meanBar f + meanBar g

theorem NavierStokes.StateMomentBalances.AuxiliaryAverage.meanBar_sub {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (f g : CorrectionState.ScalarField (CorrectionState.Lift S)) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hg : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (g n)) : meanBar (f - g) = meanBar f - meanBar g

theorem NavierStokes.StateMomentBalances.AuxiliaryAverage.radialDiv_sub {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (o : MeanIncrementBounds.Operators (CorrectionState.Lift S)) (c : ℝ) (f g : CorrectionState.ScalarField (CorrectionState.Lift S)) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hg : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (g n)) : o.radialDiv c (f - g) = o.radialDiv c f - o.radialDiv c g

theorem NavierStokes.StateMomentBalances.AuxiliaryAverage.meanBar_fluxBalance {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} (ha : 0 < a) (o : MeanIncrementBounds.Operators (CorrectionState.Lift S)) (ho : DefectIncrementBounds.PositiveOperators o) (hprofile : ∀ (R : ℝ) (z : S) (Y : PressureStream.Plane), o.radialProfile (R, z, Y) = o.radialProfile (R, z, 0)) (R A T : CorrectionState.ScalarField (CorrectionState.Lift S)) (c : ℝ) (hR : DefectIncrementBounds.Shell a b R) (hA : DefectIncrementBounds.Shell a b A) (hT : DefectIncrementBounds.Shell a b T) (hpR : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (R n)) (hpA : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (A n)) (hpT : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (T n)) : meanBar (o.radialDiv c R + o.dz A - o.radialDiv c T) = o.radialDiv c (meanBar R - meanBar T) + o.dz (meanBar A)

The torus-mean flux identity used for the initial improved bar estimate.

theorem NavierStokes.StateMomentBalances.AuxiliaryAverage.periodic_directional {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {f : CorrectionState.Lift S → ℝ} (hp : PressureStream.TorusPeriodicLift f) (v : CorrectionState.Lift S) : PressureStream.TorusPeriodicLift fun (x : PressureStream.Lift S) => (fderiv ℝ f x) v

theorem NavierStokes.StateMomentBalances.AuxiliaryAverage.periodic_dr {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (o : MeanIncrementBounds.Operators (CorrectionState.Lift S)) (hprofile : ∀ (R : ℝ) (z : S) (Y : PressureStream.Plane), o.radialProfile (R, z, Y) = o.radialProfile (R, z, 0)) {f : CorrectionState.ScalarField (CorrectionState.Lift S)} (hp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (f n)) (n : ℕ) : PressureStream.TorusPeriodicLift (o.dr f n)

theorem NavierStokes.StateMomentBalances.AuxiliaryAverage.periodic_dz {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (o : MeanIncrementBounds.Operators (CorrectionState.Lift S)) {f : CorrectionState.ScalarField (CorrectionState.Lift S)} (hp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (f n)) (n : ℕ) : PressureStream.TorusPeriodicLift (o.dz f n)

theorem NavierStokes.StateMomentBalances.AuxiliaryAverage.meanBar_dr {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (o : MeanIncrementBounds.Operators (CorrectionState.Lift S)) (hradius : o.radius = Prod.fst) (hprofile : ∀ (R : ℝ) (z : S) (Y : PressureStream.Plane), o.radialProfile (R, z, Y) = o.radialProfile (R, z, 0)) (f : CorrectionState.ScalarField (CorrectionState.Lift S)) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (f n)) : meanBar (o.dr f) = o.dr (meanBar f)

theorem NavierStokes.StateMomentBalances.AuxiliaryAverage.meanBar_band_mul {S : Type} (c : ℕ → ℝ) (f : CorrectionState.ScalarField (CorrectionState.Lift S)) : (meanBar fun (n : ℕ) (x : CorrectionState.Lift S) => c n * f n x) = fun (n : ℕ) (x : CorrectionState.Lift S) => c n * meanBar f n x

theorem NavierStokes.StateMomentBalances.AuxiliaryAverage.average_radial_mul {S : Type} (c : ℝ → ℝ) (f : CorrectionState.Lift S → ℝ) (x : ℝ × S) : PressureStream.torusAverage (fun (y : PressureStream.Lift S) => c y.1 * f y) x = c x.1 * PressureStream.torusAverage f x

theorem NavierStokes.StateMomentBalances.AuxiliaryAverage.meanBar_time {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (o : MeanIncrementBounds.Operators (CorrectionState.Lift S)) (f : CorrectionState.ScalarField (CorrectionState.Lift S)) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (f n)) : meanBar (o.time f) = o.time (meanBar f)

theorem NavierStokes.StateMomentBalances.AuxiliaryAverage.meanBar_viscosity {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} (ha : 0 < a) (o : MeanIncrementBounds.Operators (CorrectionState.Lift S)) (ho : DefectIncrementBounds.PositiveOperators o) (hprofile : ∀ (R : ℝ) (z : S) (Y : PressureStream.Plane), o.radialProfile (R, z, Y) = o.radialProfile (R, z, 0)) (f : CorrectionState.ScalarField (CorrectionState.Lift S)) (hf : DefectIncrementBounds.Shell a b f) (hp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (f n)) (c : ℝ) : meanBar (o.viscosity c f) = o.viscosity c (meanBar f)

Explicit graph operators acting on the actual torus means

noncomputable def NavierStokes.StateMomentBalances.averaged {S : Type} (f : CorrectionState.ScalarField (CorrectionState.Lift S)) : ℕ → ℝ × S → ℝ

Averaged, defined pointwise by PressureStream.torusAverage (f n).

Equations

• NavierStokes.StateMomentBalances.averaged f n = NavierStokes.PressureStream.torusAverage (f n)

noncomputable def NavierStokes.StateMomentBalances.liftSlow {S : Type} (f : ℕ → ℝ × S → ℝ) : CorrectionState.ScalarField (CorrectionState.Lift S)

Lift slow, defined pointwise by f n (x.1, x.2.1).

Equations

• NavierStokes.StateMomentBalances.liftSlow f n x = f n (x.1, x.2.1)

noncomputable def NavierStokes.StateMomentBalances.nativeOperators {S : Type} [NormedAddCommGroup S] (r : CorrectionState.ReconstructionData) (ε fast : ℕ → ℝ) (z t : S) (v : PressureStream.Plane) : MeanIncrementBounds.Operators (CorrectionState.Lift S)

Native operators, given by graphOperators r ε fast (z, 0) (t, 0) v.

Equations

• NavierStokes.StateMomentBalances.nativeOperators r ε fast z t v = NavierStokes.CorrectionState.graphOperators r ε fast (z, 0) (t, 0) v

theorem NavierStokes.StateMomentBalances.nativeOperators_positive {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : CorrectionState.ReconstructionData) (ε fast : ℕ → ℝ) (z t : S) (v : PressureStream.Plane) : DefectIncrementBounds.PositiveOperators (nativeOperators r ε fast z t v)

theorem NavierStokes.StateMomentBalances.nativeOperators_profile {S : Type} [NormedAddCommGroup S] (r : CorrectionState.ReconstructionData) (ε fast : ℕ → ℝ) (z t : S) (v : PressureStream.Plane) (R : ℝ) (s : S) (Y : PressureStream.Plane) : (nativeOperators r ε fast z t v).radialProfile (R, s, Y) = (nativeOperators r ε fast z t v).radialProfile (R, s, 0)

noncomputable def NavierStokes.StateMomentBalances.radialPartial {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (F : ℝ × S → ℝ) (x : ℝ × S) : ℝ

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

Equations

• NavierStokes.StateMomentBalances.radialPartial F x = (fderiv ℝ F x) (1, 0)

theorem NavierStokes.StateMomentBalances.radialPartial_smooth {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {F : ℝ × S → ℝ} (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (radialPartial F)

theorem NavierStokes.StateMomentBalances.radialPartial_eq_deriv {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {F : ℝ × S → ℝ} (hF : ContDiff ℝ (↑⊤) F) (R : ℝ) (s : S) : radialPartial F (R, s) = deriv (fun (q : ℝ) => F (q, s)) R

theorem NavierStokes.StateMomentBalances.radialPartial_twice_eq_deriv {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {F : ℝ × S → ℝ} (hF : ContDiff ℝ (↑⊤) F) (R : ℝ) (s : S) : radialPartial (radialPartial F) (R, s) = deriv (deriv fun (q : ℝ) => F (q, s)) R

theorem NavierStokes.StateMomentBalances.fderiv_liftSlow {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {F : ℕ → ℝ × S → ℝ} (hF : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (F n)) (n : ℕ) (x v : CorrectionState.Lift S) : (fderiv ℝ (liftSlow F n) x) v = (fderiv ℝ (F n) (x.1, x.2.1)) (v.1, v.2.1)

theorem NavierStokes.StateMomentBalances.native_dr_lift {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : CorrectionState.ReconstructionData) (ε fast : ℕ → ℝ) (z t : S) (v : PressureStream.Plane) {F : ℕ → ℝ × S → ℝ} (hF : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (F n)) : (nativeOperators r ε fast z t v).dr (liftSlow F) = liftSlow fun (n : ℕ) => radialPartial (F n)

theorem NavierStokes.StateMomentBalances.native_dz_lift {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : CorrectionState.ReconstructionData) (ε fast : ℕ → ℝ) (z t : S) (v : PressureStream.Plane) {F : ℕ → ℝ × S → ℝ} (hF : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (F n)) : (nativeOperators r ε fast z t v).dz (liftSlow F) = liftSlow fun (n : ℕ) (x : ℝ × S) => ε n * IntegratedMeanBalances.parameterPartial z (F n) x

theorem NavierStokes.StateMomentBalances.native_time_lift {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : CorrectionState.ReconstructionData) (ε fast : ℕ → ℝ) (z t : S) (v : PressureStream.Plane) {F : ℕ → ℝ × S → ℝ} (hF : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (F n)) : (nativeOperators r ε fast z t v).time (liftSlow F) = liftSlow fun (n : ℕ) (x : ℝ × S) => -ε n * IntegratedMeanBalances.parameterPartial t (F n) x

theorem NavierStokes.StateMomentBalances.parameterPartial_const_mul {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {F : ℝ × S → ℝ} (hF : ContDiff ℝ (↑⊤) F) (c : ℝ) (v : S) : (IntegratedMeanBalances.parameterPartial v fun (x : ℝ × S) => c * F x) = fun (x : ℝ × S) => c * IntegratedMeanBalances.parameterPartial v F x

theorem NavierStokes.StateMomentBalances.native_radialDiv_lift {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : CorrectionState.ReconstructionData) (ε fast : ℕ → ℝ) (z t : S) (v : PressureStream.Plane) {F : ℕ → ℝ × S → ℝ} (hF : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (F n)) (c : ℝ) (n : ℕ) (x : CorrectionState.Lift S) : (nativeOperators r ε fast z t v).radialDiv c (liftSlow F) n x = IntegratedMeanBalances.radialDivergence c (fun (q : ℝ) => F n (q, x.2.1)) x.1

theorem NavierStokes.StateMomentBalances.native_viscosity_lift {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : CorrectionState.ReconstructionData) (ε fast : ℕ → ℝ) (z t : S) (v : PressureStream.Plane) {F : ℕ → ℝ × S → ℝ} (hF : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (F n)) (c : ℝ) (n : ℕ) (x : CorrectionState.Lift S) : (nativeOperators r ε fast z t v).viscosity c (liftSlow F) n x = ε n * (deriv (deriv fun (q : ℝ) => F n (q, x.2.1)) x.1 + deriv (fun (q : ℝ) => F n (q, x.2.1)) x.1 / x.1 + ε n ^ 2 * IntegratedMeanBalances.parameterPartial z (IntegratedMeanBalances.parameterPartial z (F n)) (x.1, x.2.1) - c * F n (x.1, x.2.1) / x.1 ^ 2)

noncomputable def NavierStokes.StateMomentBalances.fluxResidual {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (o : MeanIncrementBounds.Operators (CorrectionState.Lift S)) (d k : ℝ) (u R Z T : CorrectionState.ScalarField (CorrectionState.Lift S)) : CorrectionState.ScalarField (CorrectionState.Lift S)

Flux residual, given by o.time u + o.radialDiv d R + o.dz Z - o.viscosity k u - o.radialDiv d T.

Equations

• NavierStokes.StateMomentBalances.fluxResidual o d k u R Z T = o.time u + o.radialDiv d R + o.dz Z - o.viscosity k u - o.radialDiv d T

theorem NavierStokes.StateMomentBalances.meanBar_fluxResidual {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} (ha : 0 < a) (o : MeanIncrementBounds.Operators (CorrectionState.Lift S)) (ho : DefectIncrementBounds.PositiveOperators o) (hprofile : ∀ (R : ℝ) (z : S) (Y : PressureStream.Plane), o.radialProfile (R, z, Y) = o.radialProfile (R, z, 0)) (d k : ℝ) {u R Z T : CorrectionState.ScalarField (CorrectionState.Lift S)} (hu : DefectIncrementBounds.Shell a b u) (hR : DefectIncrementBounds.Shell a b R) (hZ : DefectIncrementBounds.Shell a b Z) (hT : DefectIncrementBounds.Shell a b T) (pu : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (u n)) (pR : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (R n)) (pZ : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (Z n)) (pT : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (T n)) : meanBar (fluxResidual o d k u R Z T) = fluxResidual o d k (meanBar u) (meanBar R) (meanBar Z) (meanBar T)

noncomputable def NavierStokes.StateMomentBalances.balance {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (ε : ℝ) (z t : S) (d k : ℝ) (u R Z T : ℝ × S → ℝ) (x : ℝ × S) : ℝ

Balance as an element of ℝ.

Equations

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

theorem NavierStokes.StateMomentBalances.averaged_fluxResidual {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} (ha : 0 < a) (r : CorrectionState.ReconstructionData) (ε fast : ℕ → ℝ) (z t : S) (v : PressureStream.Plane) (d k : ℝ) {u R Z T : CorrectionState.ScalarField (CorrectionState.Lift S)} (hu : DefectIncrementBounds.Shell a b u) (hR : DefectIncrementBounds.Shell a b R) (hZ : DefectIncrementBounds.Shell a b Z) (hT : DefectIncrementBounds.Shell a b T) (pu : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (u n)) (pR : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (R n)) (pZ : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (Z n)) (pT : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (T n)) (n : ℕ) (x : ℝ × S) : averaged (fluxResidual (nativeOperators r ε fast z t v) d k u R Z T) n x = balance (ε n) z t d k (averaged u n) (averaged R n) (averaged Z n) (averaged T n) x

noncomputable def NavierStokes.StateMomentBalances.angularBalanceAlong {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (ε : ℝ) (z t : S) (u R Z T : ℝ × S → ℝ) (x : ℝ × S) : ℝ

Angular balance along as an element of ℝ.

Equations

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

noncomputable def NavierStokes.StateMomentBalances.axialBalanceAlong {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (ε : ℝ) (z t : S) (u R Z T : ℝ × S → ℝ) (x : ℝ × S) : ℝ

Axial balance along as an element of ℝ.

Equations

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

theorem NavierStokes.StateMomentBalances.balance_angular {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (ε : ℝ) (z t : S) (u R Z T : ℝ × S → ℝ) : balance ε z t 2 1 u R Z T = angularBalanceAlong ε z t u R Z T

theorem NavierStokes.StateMomentBalances.balance_axial {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (ε : ℝ) (z t : S) (u R Z T : ℝ × S → ℝ) : balance ε z t 1 0 u R Z T = axialBalanceAlong ε z t u R Z T

theorem NavierStokes.StateMomentBalances.angularBalanceAlong_eq_integrated (ε : ℝ) (u R Z T : IntegratedMeanBalances.MeanField) : angularBalanceAlong ε (0, 1) (1, 0) u R Z T = IntegratedMeanBalances.angularBalance ε u R Z T

theorem NavierStokes.StateMomentBalances.axialBalanceAlong_eq_integrated (ε : ℝ) (u R Z p T : IntegratedMeanBalances.MeanField) : axialBalanceAlong ε (0, 1) (1, 0) u R (fun (x : ℝ × ℝ × ℝ) => Z x + p x) T = IntegratedMeanBalances.axialBalance ε u R Z p T

structure NavierStokes.StateMomentBalances.RadialShell {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (a b : ℝ) (F : ℝ × S → ℝ) : Prop

Radial shell data, collecting smooth, supported.

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

theorem NavierStokes.StateMomentBalances.RadialShell.parameterDerivative {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} {F : ℝ × S → ℝ} (hF : RadialShell a b F) (v : S) : RadialShell a b (IntegratedMeanBalances.parameterPartial v F)

theorem NavierStokes.StateMomentBalances.RadialShell.add {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} {F G : ℝ × S → ℝ} (hF : RadialShell a b F) (hG : RadialShell a b G) : RadialShell a b fun (x : ℝ × S) => F x + G x

theorem NavierStokes.StateMomentBalances.RadialShell.slice_smooth {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} {F : ℝ × S → ℝ} (hF : RadialShell a b F) (p : S) : ContDiff ℝ ↑⊤ fun (r : ℝ) => F (r, p)

theorem NavierStokes.StateMomentBalances.RadialShell.slice_compact {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} {F : ℝ × S → ℝ} (hF : RadialShell a b F) (p : S) : HasCompactSupport fun (r : ℝ) => F (r, p)

theorem NavierStokes.StateMomentBalances.RadialShell.weighted_integrable {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} {F : ℝ × S → ℝ} (hF : RadialShell a b F) (n : ℕ) (p : S) : MeasureTheory.Integrable (fun (r : ℝ) => r ^ n * F (r, p)) MeasureTheory.volume

theorem NavierStokes.StateMomentBalances.integrated_angular_along {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} (ε : ℝ) (z t : S) {v radialFlux axialFlux virtualFlux : ℝ × S → ℝ} (hv : RadialShell a b v) (hr : RadialShell a b radialFlux) (hz : RadialShell a b axialFlux) (hT : RadialShell a b virtualFlux) (hmass : IntegratedMeanBalances.radialMoment 2 v = 0) (p : S) : IntegratedMeanBalances.radialMoment 2 (angularBalanceAlong ε z t v radialFlux axialFlux virtualFlux) p = ε * (fderiv ℝ (IntegratedMeanBalances.radialMoment 2 axialFlux) p) z

theorem NavierStokes.StateMomentBalances.integrated_axial_along {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} (ε : ℝ) (z t : S) {γ radialFlux axialFlux virtualFlux : ℝ × S → ℝ} (hγ : RadialShell a b γ) (hr : RadialShell a b radialFlux) (hz : RadialShell a b axialFlux) (hT : RadialShell a b virtualFlux) (hmass : IntegratedMeanBalances.radialMoment 1 γ = 0) (p : S) : IntegratedMeanBalances.radialMoment 1 (axialBalanceAlong ε z t γ radialFlux axialFlux virtualFlux) p = ε * (fderiv ℝ (IntegratedMeanBalances.radialMoment 1 axialFlux) p) z

theorem NavierStokes.StateMomentBalances.averaged_radialShell {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} {f : CorrectionState.ScalarField (CorrectionState.Lift S)} (hf : DefectIncrementBounds.Shell a b f) (n : ℕ) : RadialShell a b (averaged f n)

Literal state fluxes and actual debt identities

noncomputable def NavierStokes.StateMomentBalances.thetaRadialFlux {S : Type} (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) : CorrectionState.ScalarField (CorrectionState.Lift S)

Theta radial flux, given by MeanIncrementBounds.thetaRadial c.base u.mean + u.covariance 0 1.

Equations

• NavierStokes.StateMomentBalances.thetaRadialFlux c u = NavierStokes.MeanIncrementBounds.thetaRadial c.base u.mean + u.covariance 0 1

noncomputable def NavierStokes.StateMomentBalances.thetaAxialFlux {S : Type} (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) : CorrectionState.ScalarField (CorrectionState.Lift S)

Theta axial flux, given by MeanIncrementBounds.thetaAxial c.base u.mean + u.covariance 2 1.

Equations

• NavierStokes.StateMomentBalances.thetaAxialFlux c u = NavierStokes.MeanIncrementBounds.thetaAxial c.base u.mean + u.covariance 2 1

noncomputable def NavierStokes.StateMomentBalances.axialRadialFlux {S : Type} (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) : CorrectionState.ScalarField (CorrectionState.Lift S)

Axial radial flux, given by MeanIncrementBounds.axialRadial c.base u.mean + u.covariance 0 2.

Equations

• NavierStokes.StateMomentBalances.axialRadialFlux c u = NavierStokes.MeanIncrementBounds.axialRadial c.base u.mean + u.covariance 0 2

noncomputable def NavierStokes.StateMomentBalances.axialAxialFlux {S : Type} (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) : CorrectionState.ScalarField (CorrectionState.Lift S)

Axial axial flux, given by MeanIncrementBounds.axialAxial c.base u.mean + u.covariance 2 2.

Equations

• NavierStokes.StateMomentBalances.axialAxialFlux c u = NavierStokes.MeanIncrementBounds.axialAxial c.base u.mean + u.covariance 2 2

structure NavierStokes.StateMomentBalances.FluxInputs {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (a b : ℝ) (u R Z T : CorrectionState.ScalarField (CorrectionState.Lift S)) : Prop

Regularity of the actual pointwise fields; no averaged equation or moment identity is included among the premises.

• velocity : DefectIncrementBounds.Shell a b u
• radial : DefectIncrementBounds.Shell a b R
• axial : DefectIncrementBounds.Shell a b Z
• stress : DefectIncrementBounds.Shell a b T
• velocity_periodic (n : ℕ) : PressureStream.TorusPeriodicLift (u n)
• radial_periodic (n : ℕ) : PressureStream.TorusPeriodicLift (R n)
• axial_periodic (n : ℕ) : PressureStream.TorusPeriodicLift (Z n)
• stress_periodic (n : ℕ) : PressureStream.TorusPeriodicLift (T n)

@[reducible, inline]

abbrev NavierStokes.StateMomentBalances.AngularInputs {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (a b : ℝ) (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) : Prop

Angular inputs: an abbreviation for FluxInputs a b u.mean.angular (thetaRadialFlux c u) (thetaAxialFlux c u) c.virtualTheta.

Equations

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

@[reducible, inline]

abbrev NavierStokes.StateMomentBalances.AxialInputs {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (a b : ℝ) (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) : Prop

Axial inputs: an abbreviation for FluxInputs a b u.mean.axial (axialRadialFlux c u) (axialAxialFlux c u) c.virtualAxial.

Equations

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

theorem NavierStokes.StateMomentBalances.state_radialMoment_eq {S : Type} (k : ℕ) (f : CorrectionState.ScalarField (CorrectionState.Lift S)) (n : ℕ) (s : S) : CorrectionState.radialMoment k f n s = IntegratedMeanBalances.radialMoment k (averaged f n) s

theorem NavierStokes.StateMomentBalances.periodic_add {S : Type} {f g : CorrectionState.Lift S → ℝ} (hf : PressureStream.TorusPeriodicLift f) (hg : PressureStream.TorusPeriodicLift g) : PressureStream.TorusPeriodicLift fun (x : PressureStream.Lift S) => f x + g x

theorem NavierStokes.StateMomentBalances.averaged_thetaResidual {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} (ha : 0 < a) (r : CorrectionState.ReconstructionData) (ε fast : ℕ → ℝ) (z t : S) (v : PressureStream.Plane) (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) (ho : c.operators = nativeOperators r ε fast z t v) (H : AngularInputs a b c u) (n : ℕ) : averaged (u.thetaResidual c) n = angularBalanceAlong (ε n) z t (averaged u.mean.angular n) (averaged (thetaRadialFlux c u) n) (averaged (thetaAxialFlux c u) n) (averaged c.virtualTheta n)

theorem NavierStokes.StateMomentBalances.state_angular_moment {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} (ha : 0 < a) (r : CorrectionState.ReconstructionData) (ε fast : ℕ → ℝ) (z t : S) (v : PressureStream.Plane) (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) (ho : c.operators = nativeOperators r ε fast z t v) (H : AngularInputs a b c u) (hmass : CorrectionState.radialMoment 2 u.mean.angular = 0) (n : ℕ) (s : S) : CorrectionState.radialMoment 2 (u.thetaResidual c) n s = ε n * (fderiv ℝ (CorrectionState.thetaDefect c u n) s) z

noncomputable def NavierStokes.StateMomentBalances.pressureRecipe {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : CorrectionState.ReconstructionData) (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) : CorrectionState.ScalarField (CorrectionState.Lift S)

Pressure recipe, defined pointwise by PressureStream.meanPressure r.exponent r.inner r.outer (r.frequency n) r.inner_lt_outer r.radialDirection (u.gr c n).

Equations

• NavierStokes.StateMomentBalances.pressureRecipe r c u n = NavierStokes.PressureStream.meanPressure r.exponent r.inner r.outer (r.frequency n) ⋯ r.radialDirection (u.gr c n)

theorem NavierStokes.StateMomentBalances.pressure_recipe_of_fixed {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : CorrectionState.ReconstructionData) (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) (h : CorrectionState.reconstructPressure r c u = u) : u.pressure = pressureRecipe r c u

theorem NavierStokes.StateMomentBalances.pressureRecipe_shell {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : CorrectionState.ReconstructionData) (ha : 0 < r.inner) (hd : 0 < r.exponent) (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) (hg : DefectIncrementBounds.Shell r.inner r.outer (u.gr c)) : DefectIncrementBounds.Shell r.inner r.outer (pressureRecipe r c u)

noncomputable def NavierStokes.StateMomentBalances.pressureCoefficient (r : CorrectionState.ReconstructionData) : ℝ

Pressure coefficient, given by IntegratedMeanBalances.moment 2 (PressureStream.rho r.inner r.outer r.inner_lt_outer) / 2.

Equations

• NavierStokes.StateMomentBalances.pressureCoefficient r = NavierStokes.IntegratedMeanBalances.moment 2 (NavierStokes.PressureStream.rho r.inner r.outer ⋯) / 2

noncomputable def NavierStokes.StateMomentBalances.axialDebtPotential {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : CorrectionState.ReconstructionData) (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) : CorrectionState.ScalarField S

Axial debt potential, defined pointwise by CorrectionState.axialDefect c u n s + pressureCoefficient r * CorrectionState.pressureDefect c u n s.

Equations

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

theorem NavierStokes.StateMomentBalances.pressureRecipe_moment {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : CorrectionState.ReconstructionData) (ha : 0 < r.inner) (hd : 0 < r.exponent) (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) (hg : DefectIncrementBounds.Shell r.inner r.outer (u.gr c)) (pg : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (u.gr c n)) (n : ℕ) (s : S) : IntegratedMeanBalances.radialMoment 1 (averaged (pressureRecipe r c u) n) s = -(1 / 2) * CorrectionState.radialMoment 2 (u.gr c) n s + pressureCoefficient r * CorrectionState.pressureDefect c u n s

theorem NavierStokes.StateMomentBalances.pressureAlias_average_zero {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : CorrectionState.ReconstructionData) (ha : 0 < r.inner) (hd : 0 < r.exponent) (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) (hg : DefectIncrementBounds.Shell r.inner r.outer (u.gr c)) (pg : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (u.gr c n)) (n : ℕ) (x : ℝ × S) : PressureStream.torusAverage (PressureStream.pressureAlias r.exponent r.inner r.outer (r.frequency n) ⋯ r.radialDirection (u.gr c n)) x = 0

The exact pressure alias has zero auxiliary mean because the constructed pressure source has zero total mass.

theorem NavierStokes.StateMomentBalances.physicalCompact_periodic {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (v : PressureStream.Plane) {f : CorrectionState.Lift S → ℝ} (hp : PressureStream.TorusPeriodicLift f) : PressureStream.TorusPeriodicLift (RadialPullback.physicalCompact d a b M (0, v) f)

theorem NavierStokes.StateMomentBalances.physicalAlias_periodic {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (v : PressureStream.Plane) {f : CorrectionState.Lift S → ℝ} (hp : PressureStream.TorusPeriodicLift f) : PressureStream.TorusPeriodicLift (RadialPullback.physicalAlias d a b M (0, v) f)

theorem NavierStokes.StateMomentBalances.average_neg {S : Type} (f : CorrectionState.Lift S → ℝ) (x : ℝ × S) : PressureStream.torusAverage (fun (y : PressureStream.Lift S) => -f y) x = -PressureStream.torusAverage f x

theorem NavierStokes.StateMomentBalances.pressureAlias_state_average_zero {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : CorrectionState.ReconstructionData) (ha : 0 < r.inner) (hd : 0 < r.exponent) (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) (hg : DefectIncrementBounds.Shell r.inner r.outer (u.gr c)) (pg : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (u.gr c n)) (n : ℕ) (x : ℝ × S) (i : Fin 3) : PressureStream.torusAverage (fun (y : PressureStream.Lift S) => CorrectionState.pressureAlias r c u n (y, 0) i) x = 0

theorem NavierStokes.StateMomentBalances.axialAlias_periodic {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (v : PressureStream.Plane) (h : ℝ) (n : ℕ) (f : CorrectionState.Lift S → ℝ) : PressureStream.TorusPeriodicLift (TemporalMeanUpdate.axialAlias d a b M v h n f)

theorem NavierStokes.StateMomentBalances.temporalAlias_average_zero {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (r : CorrectionState.ReconstructionData) (ha : 0 < r.inner) (hd : 0 < r.exponent) (h : ℝ) (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) (hres : DefectIncrementBounds.Shell r.inner r.outer (u.axialResidual c)) (pres : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (u.axialResidual c n)) (n : ℕ) (x : ℝ × S) (i : Fin 3) : PressureStream.torusAverage (fun (y : PressureStream.Lift S) => CorrectionState.temporalAlias r h c u n (y, 0) i) x = 0

theorem NavierStokes.StateMomentBalances.pressureRecipe_periodic {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : CorrectionState.ReconstructionData) (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) (pg : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (u.gr c n)) (n : ℕ) : PressureStream.TorusPeriodicLift (pressureRecipe r c u n)

theorem NavierStokes.StateMomentBalances.averaged_axialResidual {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : CorrectionState.ReconstructionData) (ha : 0 < r.inner) (ε fast : ℕ → ℝ) (z t : S) (v : PressureStream.Plane) (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) (ho : c.operators = nativeOperators r ε fast z t v) (H : AxialInputs r.inner r.outer c u) (hp : DefectIncrementBounds.Shell r.inner r.outer u.pressure) (pp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (u.pressure n)) (n : ℕ) : averaged (u.axialResidual c) n = axialBalanceAlong (ε n) z t (averaged u.mean.axial n) (averaged (axialRadialFlux c u) n) (averaged (axialAxialFlux c u + u.pressure) n) (averaged c.virtualAxial n)

theorem NavierStokes.StateMomentBalances.axial_flux_pressure_moment {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : CorrectionState.ReconstructionData) (ha : 0 < r.inner) (hd : 0 < r.exponent) (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) (hZ : DefectIncrementBounds.Shell r.inner r.outer (axialAxialFlux c u)) (hg : DefectIncrementBounds.Shell r.inner r.outer (u.gr c)) (pg : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (u.gr c n)) (hrecipe : u.pressure = pressureRecipe r c u) : CorrectionState.radialMoment 1 (axialAxialFlux c u + u.pressure) = axialDebtPotential r c u

theorem NavierStokes.StateMomentBalances.state_axial_moment {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : CorrectionState.ReconstructionData) (ha : 0 < r.inner) (hd : 0 < r.exponent) (ε fast : ℕ → ℝ) (z t : S) (v : PressureStream.Plane) (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) (ho : c.operators = nativeOperators r ε fast z t v) (H : AxialInputs r.inner r.outer c u) (hg : DefectIncrementBounds.Shell r.inner r.outer (u.gr c)) (pg : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (u.gr c n)) (hrecipe : u.pressure = pressureRecipe r c u) (hmass : CorrectionState.radialMoment 1 u.mean.axial = 0) (n : ℕ) (s : S) : CorrectionState.radialMoment 1 (u.axialResidual c) n s = ε n * (fderiv ℝ (axialDebtPotential r c u n) s) z

Actual all-jet debt bounds yield the improved signed bump order

theorem NavierStokes.StateMomentBalances.slowClass_smooth {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {ε slow : ℕ → ℝ} {hε : ∀ (n : ℕ), 0 < ε n} {hε1 : ∀ (n : ℕ), ε n ≤ 1} {hslow : ∀ (n : ℕ), 1 ≤ slow n} {α : ℝ} {f : ℕ → S → ℝ} (hf : WeightedClasses.UnweightedClass (MeanMomentBounds.slowStripData ε slow hε hε1 hslow) α f) (n : ℕ) : ContDiff ℝ (↑⊤) (f n)

theorem NavierStokes.StateMomentBalances.slowClass_globalBandJets {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {ε slow : ℕ → ℝ} {hε : ∀ (n : ℕ), 0 < ε n} {hε1 : ∀ (n : ℕ), ε n ≤ 1} {hslow : ∀ (n : ℕ), 1 ≤ slow n} {α : ℝ} {f : ℕ → S → ℝ} (hf : WeightedClasses.UnweightedClass (MeanMomentBounds.slowStripData ε slow hε hε1 hslow) α f) : MeanMomentBounds.GlobalBandJets ε slow α f

noncomputable def NavierStokes.StateMomentBalances.slowProjection {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] : CorrectionState.Lift S →L[ℝ] S

Slow projection, given by (ContinuousLinearMap.fst ℝ S PressureStream.Plane).comp (ContinuousLinearMap.snd ℝ ℝ (S × PressureStream.Plane)).

Equations

• NavierStokes.StateMomentBalances.slowProjection = ContinuousLinearMap.fst ℝ S NavierStokes.PressureStream.Plane ∘SL ContinuousLinearMap.snd ℝ ℝ (S × NavierStokes.PressureStream.Plane)

theorem NavierStokes.StateMomentBalances.norm_slowProjection_le {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] : ‖slowProjection‖ ≤ 1

theorem NavierStokes.StateMomentBalances.slowClass_lift {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (P : SignedStressPrimitive.Patch) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) {ε slow : ℕ → ℝ} {hε : ∀ (n : ℕ), 0 < ε n} {hε1 : ∀ (n : ℕ), ε n ≤ 1} {hslow : ∀ (n : ℕ), 1 ≤ slow n} {α : ℝ} {f : ℕ → S → ℝ} (hf : WeightedClasses.UnweightedClass (MeanMomentBounds.slowStripData ε slow hε hε1 hslow) α f) : WeightedClasses.UnweightedClass (WeightedRadialPrimitive.logStripData P.a P.b cL cR ⋯ hcL hcR ε slow hε hε1 hslow) α fun (n : ℕ) (x : CorrectionState.Lift S) => f n x.2.1

theorem NavierStokes.StateMomentBalances.fderiv_parameterLift {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {f : S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (p : S × PressureStream.Plane) (z : S) : (fderiv ℝ (fun (y : S × PressureStream.Plane) => f y.1) p) (z, 0) = (fderiv ℝ f p.1) z

theorem NavierStokes.StateMomentBalances.bump_class_from_actual_debt {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (P : SignedStressPrimitive.Patch) (e : ℕ) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (ε slow : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hε1 : ∀ (n : ℕ), ε n ≤ 1) (hslow : ∀ (n : ℕ), 1 ≤ slow n) (α : ℝ) (F : CorrectionState.ScalarField (CorrectionState.Lift S)) (D : CorrectionState.ScalarField S) (z : S) (hD : WeightedClasses.UnweightedClass (MeanMomentBounds.slowStripData ε slow hε hε1 hslow) α D) (hidentity : ∀ (n : ℕ) (s : S), CorrectionState.radialMoment e F n s = ε n * (fderiv ℝ (D n) s) z) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData P.a P.b cL cR ⋯ hcL hcR ε slow hε hε1 hslow) (α + 1) fun (n : ℕ) => SignedStressPrimitive.bumpCorrection P e (meanBar F n)

The hypothesis is a bound on the actual slow debt. The residual moment identity is supplied by the state theorems below, rather than a bump estimate.

theorem NavierStokes.StateMomentBalances.state_angular_bump_improvedClass {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (P : SignedStressPrimitive.Patch) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (r : CorrectionState.ReconstructionData) (ha : 0 < r.inner) (ε fast slow : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hε1 : ∀ (n : ℕ), ε n ≤ 1) (hslow : ∀ (n : ℕ), 1 ≤ slow n) (z t : S) (v : PressureStream.Plane) (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) (α : ℝ) (ho : c.operators = nativeOperators r ε fast z t v) (H : AngularInputs r.inner r.outer c u) (hmass : CorrectionState.ZeroMasses u) (hD : WeightedClasses.UnweightedClass (MeanMomentBounds.slowStripData ε slow hε hε1 hslow) α (CorrectionState.thetaDefect c u)) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData P.a P.b cL cR ⋯ hcL hcR ε slow hε hε1 hslow) (α + 1) fun (n : ℕ) => SignedStressPrimitive.bumpCorrection P 2 (meanBar (u.thetaResidual c) n)

theorem NavierStokes.StateMomentBalances.state_axial_bump_improvedClass {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (P : SignedStressPrimitive.Patch) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (r : CorrectionState.ReconstructionData) (ha : 0 < r.inner) (hd : 0 < r.exponent) (ε fast slow : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hε1 : ∀ (n : ℕ), ε n ≤ 1) (hslow : ∀ (n : ℕ), 1 ≤ slow n) (z t : S) (v : PressureStream.Plane) (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) (α : ℝ) (ho : c.operators = nativeOperators r ε fast z t v) (H : AxialInputs r.inner r.outer c u) (hg : DefectIncrementBounds.Shell r.inner r.outer (u.gr c)) (pg : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (u.gr c n)) (hrecipe : u.pressure = pressureRecipe r c u) (hmass : CorrectionState.ZeroMasses u) (hP : WeightedClasses.UnweightedClass (MeanMomentBounds.slowStripData ε slow hε hε1 hslow) α (CorrectionState.pressureDefect c u)) (hZ : WeightedClasses.UnweightedClass (MeanMomentBounds.slowStripData ε slow hε hε1 hslow) α (CorrectionState.axialDefect c u)) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData P.a P.b cL cR ⋯ hcL hcR ε slow hε hε1 hslow) (α + 1) fun (n : ℕ) => SignedStressPrimitive.bumpCorrection P 1 (meanBar (u.axialResidual c) n)

theorem NavierStokes.StateMomentBalances.debt_component_pressure {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) : (fun (n : ℕ) (s : S) => CorrectionState.debt c u n s 0) = CorrectionState.pressureDefect c u

theorem NavierStokes.StateMomentBalances.debt_component_angular {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) : (fun (n : ℕ) (s : S) => CorrectionState.debt c u n s 1) = CorrectionState.thetaDefect c u

theorem NavierStokes.StateMomentBalances.debt_component_axial {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) : (fun (n : ℕ) (s : S) => CorrectionState.debt c u n s 2) = CorrectionState.axialDefect c u

theorem NavierStokes.StateMomentBalances.defectBounds_components {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {ε slow : ℕ → ℝ} {hε : ∀ (n : ℕ), 0 < ε n} {hε1 : ∀ (n : ℕ), ε n ≤ 1} {hslow : ∀ (n : ℕ), 1 ≤ slow n} {σ : ℝ} {c : CorrectionState.Context (CorrectionState.Lift S)} {u : CorrectionState.State (CorrectionState.Lift S)} (hD : CorrectionState.DefectBounds (MeanMomentBounds.slowStripData ε slow hε hε1 hslow) σ c u) : WeightedClasses.UnweightedClass (MeanMomentBounds.slowStripData ε slow hε hε1 hslow) (1 + σ) (CorrectionState.pressureDefect c u) ∧ WeightedClasses.UnweightedClass (MeanMomentBounds.slowStripData ε slow hε hε1 hslow) (1 + σ) (CorrectionState.thetaDefect c u) ∧ WeightedClasses.UnweightedClass (MeanMomentBounds.slowStripData ε slow hε hε1 hslow) (1 + σ) (CorrectionState.axialDefect c u)

@[reducible, inline]

abbrev NavierStokes.GaugeMomentBalances.Plane : Type

Plane: an abbreviation for PressureStream.Plane.

Equations

• NavierStokes.GaugeMomentBalances.Plane = NavierStokes.PressureStream.Plane

@[reducible, inline]

abbrev NavierStokes.GaugeMomentBalances.Point : Type

Point: an abbreviation for PressureStream.Lift Plane.

Equations

• NavierStokes.GaugeMomentBalances.Point = NavierStokes.PressureStream.Lift NavierStokes.GaugeMomentBalances.Plane

noncomputable def NavierStokes.GaugeMomentBalances.basePressureCoefficient (a b : ℝ) (hab : a < b) : ℝ

Base pressure coefficient, given by IntegratedMeanBalances.moment 2 (PressureStream.rho a b hab) / 2.

Equations

• NavierStokes.GaugeMomentBalances.basePressureCoefficient a b hab = NavierStokes.IntegratedMeanBalances.moment 2 (NavierStokes.PressureStream.rho a b hab) / 2

theorem NavierStokes.GaugeMomentBalances.basePressureCoefficient_lower {a b : ℝ} (ha : 0 < a) (hab : a < b) : a ^ 2 / 2 ≤ basePressureCoefficient a b hab

theorem NavierStokes.GaugeMomentBalances.basePressureCoefficient_pos {a b : ℝ} (ha : 0 < a) (hab : a < b) : 0 < basePressureCoefficient a b hab

noncomputable def NavierStokes.GaugeMomentBalances.pressureCoefficient {S : Type} (g : VariableGaugeMean.GaugeData S) (n : ℕ) (s : S) : ℝ

Pressure coefficient, given by basePressureCoefficient g.radial.inner g.radial.outer g.radial.inner_lt_outer * g.length n s ^ 2.

Equations

• NavierStokes.GaugeMomentBalances.pressureCoefficient g n s = NavierStokes.GaugeMomentBalances.basePressureCoefficient g.radial.inner g.radial.outer ⋯ * g.length n s ^ 2

theorem NavierStokes.GaugeMomentBalances.rho_second_moment_scale {l a b : ℝ} (hl : 0 < l) (hab : a < b) : IntegratedMeanBalances.moment 2 (PressureStream.rho (l * a) (l * b) ⋯) = l ^ 2 * IntegratedMeanBalances.moment 2 (PressureStream.rho a b hab)

Exact second moment of the scaled, normalized density.

theorem NavierStokes.GaugeMomentBalances.pressureCoefficient_measured {S : Type} (g : VariableGaugeMean.GaugeData S) (n : ℕ) (s : S) (hl : 0 < g.length n s) (Y : Plane) : (IntegratedMeanBalances.moment 2 fun (R : ℝ) => VariableGaugeMean.density g.radial.inner g.radial.outer ⋯ (g.length n) (R, s, Y)) / 2 = pressureCoefficient g n s

This is the coefficient of the pressure debt, measured in the moving physical radius, rather than in the normalized profile radius.

theorem NavierStokes.GaugeMomentBalances.moving_pressure_moment {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b d M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (ell : S → ℝ) (v : Plane) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hs : VariableGaugeMean.SupportedGauge a b ell U f) (hp : PhysicalMeanDomain.PeriodicOn U f) {s : S} (hsm : s ∈ U) (hl : 0 < ell s) : (IntegratedMeanBalances.moment 1 fun (R : ℝ) => PressureStream.torusAverage (VariableGaugeMean.meanPressure d a b M hab ell v f) (R, s)) = (-(1 / 2) * IntegratedMeanBalances.moment 2 fun (R : ℝ) => PressureStream.torusAverage f (R, s)) + basePressureCoefficient a b hab * ell s ^ 2 * PressureStream.pressureMass f s

The actual moving-gauge pressure moment. Freezing is used only to apply a radial integral theorem on one fiber; no slow derivative is frozen.

@[simp]

theorem NavierStokes.GaugeMomentBalances.reconstructState_gr {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : VariableGaugeMean.GaugeData S) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) : (VariableGaugeMean.reconstructState g c u).gr c = u.gr c

@[simp]

theorem NavierStokes.GaugeMomentBalances.reconstructState_idempotent {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : VariableGaugeMean.GaugeData S) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) : VariableGaugeMean.reconstructState g c (VariableGaugeMean.reconstructState g c u) = VariableGaugeMean.reconstructState g c u

theorem NavierStokes.GaugeMomentBalances.similarity_pressureCoefficient {h d a b M : ℝ} (hab : a < b) (index : ℕ → ℕ) (hc : 0 < 2 * h) (hc1 : 2 * h < 1) (n : ℕ) {s : Plane} (hs : 0 < s.1) : pressureCoefficient (VariableGaugeMean.similarityGauge h d a b M hab index) n s = basePressureCoefficient a b hab * SimilarityCoordinates.coordinateQ (2 * h) s

theorem NavierStokes.GaugeMomentBalances.similarity_pressureCoefficient_fderiv {h d a b M : ℝ} (hab : a < b) (index : ℕ → ℕ) (hc : 0 < 2 * h) (hc1 : 2 * h < 1) (n : ℕ) {s : Plane} (hs : 0 < s.1) (v : Plane) : (fderiv ℝ (pressureCoefficient (VariableGaugeMean.similarityGauge h d a b M hab index) n) s) v = basePressureCoefficient a b hab * ((v.1 + 2 * s.2 * SimilarityCoordinates.coordinateQ (2 * h) s ^ (2 * h) * v.2) / SimilarityCoordinates.scalarSlope (2 * h) s.2 (SimilarityCoordinates.coordinateQ (2 * h) s))

Local integration on a genuine open slow region

structure NavierStokes.GaugeMomentBalances.LocalField {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (a b : ℝ) (U : Set S) (f : CorrectionState.ScalarField (PressureStream.Lift S)) : Prop

Local smoothness, compact radial support, and true torus periodicity of a field. These are regularity hypotheses, not a moment equation.

• smooth (n : ℕ) : ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U)
• supported (n : ℕ) : PhysicalMeanDomain.SupportedOn a b U (f n)
• periodic (n : ℕ) : PhysicalMeanDomain.PeriodicOn U (f n)

theorem NavierStokes.GaugeMomentBalances.LocalField.add {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} {U : Set S} {f g : CorrectionState.ScalarField (PressureStream.Lift S)} (hf : LocalField a b U f) (hg : LocalField a b U g) : LocalField a b U (f + g)

noncomputable def NavierStokes.GaugeMomentBalances.localizeFamily {S : Type} (χ : S → ℝ) (f : CorrectionState.ScalarField (PressureStream.Lift S)) : CorrectionState.ScalarField (PressureStream.Lift S)

Localize family, defined pointwise by PhysicalMeanDomain.localize χ (f n).

Equations

• NavierStokes.GaugeMomentBalances.localizeFamily χ f n = NavierStokes.PhysicalMeanDomain.localize χ (f n)

theorem NavierStokes.GaugeMomentBalances.LocalField.localize {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} {U : Set S} (hU : IsOpen U) {f : CorrectionState.ScalarField (PressureStream.Lift S)} (hf : LocalField a b U f) {χ : S → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hs : tsupport χ ⊆ U) : DefectIncrementBounds.Shell a b (localizeFamily χ f)

theorem NavierStokes.GaugeMomentBalances.LocalField.localize_periodic {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} {U : Set S} {f : CorrectionState.ScalarField (PressureStream.Lift S)} (hf : LocalField a b U f) {χ : S → ℝ} (hs : tsupport χ ⊆ U) (n : ℕ) : PressureStream.TorusPeriodicLift (localizeFamily χ f n)

theorem NavierStokes.GaugeMomentBalances.radialMoment_fiber_congr {S : Type} (k : ℕ) {f g : CorrectionState.ScalarField (PressureStream.Lift S)} (n : ℕ) (s : S) (he : ∀ (R : ℝ) (Y : PressureStream.Plane), f n (R, s, Y) = g n (R, s, Y)) : CorrectionState.radialMoment k f n s = CorrectionState.radialMoment k g n s

theorem NavierStokes.GaugeMomentBalances.radialMoment_fiber_germ {S : Type} [NormedAddCommGroup S] (k : ℕ) {f g : CorrectionState.ScalarField (PressureStream.Lift S)} (n : ℕ) {s : S} (he : PhysicalMeanDomain.FiberGerm s (f n) (g n)) : CorrectionState.radialMoment k f n =ᶠ[nhds s] CorrectionState.radialMoment k g n

theorem NavierStokes.GaugeMomentBalances.radialMoment_localize {S : Type} (k : ℕ) (χ : S → ℝ) (f : CorrectionState.ScalarField (PressureStream.Lift S)) (n : ℕ) (s : S) : CorrectionState.radialMoment k (localizeFamily χ f) n s = χ s * CorrectionState.radialMoment k f n s

theorem NavierStokes.GaugeMomentBalances.dr_eventuallyEq {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (o : MeanIncrementBounds.Operators (PressureStream.Lift S)) {f g : CorrectionState.ScalarField (PressureStream.Lift S)} {n : ℕ} {x : PressureStream.Lift S} (he : f n =ᶠ[nhds x] g n) : o.dr f n =ᶠ[nhds x] o.dr g n

theorem NavierStokes.GaugeMomentBalances.dz_eventuallyEq {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (o : MeanIncrementBounds.Operators (PressureStream.Lift S)) {f g : CorrectionState.ScalarField (PressureStream.Lift S)} {n : ℕ} {x : PressureStream.Lift S} (he : f n =ᶠ[nhds x] g n) : o.dz f n =ᶠ[nhds x] o.dz g n

theorem NavierStokes.GaugeMomentBalances.fluxResidual_eventuallyEq {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (o : MeanIncrementBounds.Operators (PressureStream.Lift S)) (d k : ℝ) {u R Z T u' R' Z' T' : CorrectionState.ScalarField (PressureStream.Lift S)} {n : ℕ} {x : PressureStream.Lift S} (hu : u n =ᶠ[nhds x] u' n) (hR : R n =ᶠ[nhds x] R' n) (hZ : Z n =ᶠ[nhds x] Z' n) (hT : T n =ᶠ[nhds x] T' n) : StateMomentBalances.fluxResidual o d k u R Z T n =ᶠ[nhds x] StateMomentBalances.fluxResidual o d k u' R' Z' T' n

theorem NavierStokes.GaugeMomentBalances.global_angular_moment {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} (ha : 0 < a) (r : CorrectionState.ReconstructionData) (ε fast : ℕ → ℝ) (z t : S) (v : Plane) {u R Z T : CorrectionState.ScalarField (PressureStream.Lift S)} (H : StateMomentBalances.FluxInputs a b u R Z T) (hmass : CorrectionState.radialMoment 2 u = 0) (n : ℕ) (s : S) : CorrectionState.radialMoment 2 (StateMomentBalances.fluxResidual (StateMomentBalances.nativeOperators r ε fast z t v) 2 1 u R Z T) n s = ε n * (fderiv ℝ (CorrectionState.radialMoment 2 Z n) s) z

theorem NavierStokes.GaugeMomentBalances.global_axial_moment {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} (ha : 0 < a) (r : CorrectionState.ReconstructionData) (ε fast : ℕ → ℝ) (z t : S) (v : Plane) {u R Z T : CorrectionState.ScalarField (PressureStream.Lift S)} (H : StateMomentBalances.FluxInputs a b u R Z T) (hmass : CorrectionState.radialMoment 1 u = 0) (n : ℕ) (s : S) : CorrectionState.radialMoment 1 (StateMomentBalances.fluxResidual (StateMomentBalances.nativeOperators r ε fast z t v) 1 0 u R Z T) n s = ε n * (fderiv ℝ (CorrectionState.radialMoment 1 Z n) s) z

structure NavierStokes.GaugeMomentBalances.LocalFluxInputs {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (a b : ℝ) (U : Set S) (u R Z T : CorrectionState.ScalarField (PressureStream.Lift S)) : Prop

Local flux inputs data, collecting velocity, radial, axial, stress.

• velocity : LocalField a b U u
• radial : LocalField a b U R
• axial : LocalField a b U Z
• stress : LocalField a b U T

theorem NavierStokes.GaugeMomentBalances.localize_fiber_germ {S : Type} [NormedAddCommGroup S] {s : S} {χ : S → ℝ} (hχ : χ =ᶠ[nhds s] fun (x : S) => 1) (f : CorrectionState.ScalarField (PressureStream.Lift S)) (n : ℕ) : PhysicalMeanDomain.FiberGerm s (localizeFamily χ f n) (f n)

theorem NavierStokes.GaugeMomentBalances.localize_zero_moment {S : Type} [NormedAddCommGroup S] {U : Set S} {χ : S → ℝ} (hχ : tsupport χ ⊆ U) (e : ℕ) {u : CorrectionState.ScalarField (PressureStream.Lift S)} (hmass : ∀ (n : ℕ), ∀ s ∈ U, CorrectionState.radialMoment e u n s = 0) : CorrectionState.radialMoment e (localizeFamily χ u) = 0

theorem NavierStokes.GaugeMomentBalances.exists_slow_cutoff {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {U : Set S} (hU : IsOpen U) {s : S} (hs : s ∈ U) : ∃ (χ : S → ℝ), ContDiff ℝ (↑⊤) χ ∧ tsupport χ ⊆ U ∧ χ =ᶠ[nhds s] fun (x : S) => 1

theorem NavierStokes.GaugeMomentBalances.LocalFluxInputs.localize {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} {U : Set S} (hU : IsOpen U) {u R Z T : CorrectionState.ScalarField (PressureStream.Lift S)} (H : LocalFluxInputs a b U u R Z T) {χ : S → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hs : tsupport χ ⊆ U) : StateMomentBalances.FluxInputs a b (localizeFamily χ u) (localizeFamily χ R) (localizeFamily χ Z) (localizeFamily χ T)

theorem NavierStokes.GaugeMomentBalances.residual_moment_localize {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (o : MeanIncrementBounds.Operators (PressureStream.Lift S)) (e : ℕ) (d k : ℝ) {s : S} {χ : S → ℝ} (hχ : χ =ᶠ[nhds s] fun (x : S) => 1) (u R Z T : CorrectionState.ScalarField (PressureStream.Lift S)) (n : ℕ) : CorrectionState.radialMoment e (StateMomentBalances.fluxResidual o d k (localizeFamily χ u) (localizeFamily χ R) (localizeFamily χ Z) (localizeFamily χ T)) n s = CorrectionState.radialMoment e (StateMomentBalances.fluxResidual o d k u R Z T) n s

theorem NavierStokes.GaugeMomentBalances.local_angular_moment {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b : ℝ} (ha : 0 < a) {U : Set S} (hU : IsOpen U) (r : CorrectionState.ReconstructionData) (ε fast : ℕ → ℝ) (z t : S) (v : Plane) {u R Z T : CorrectionState.ScalarField (PressureStream.Lift S)} (H : LocalFluxInputs a b U u R Z T) (hmass : ∀ (n : ℕ), ∀ s ∈ U, CorrectionState.radialMoment 2 u n s = 0) (n : ℕ) {s : S} (hs : s ∈ U) : CorrectionState.radialMoment 2 (StateMomentBalances.fluxResidual (StateMomentBalances.nativeOperators r ε fast z t v) 2 1 u R Z T) n s = ε n * (fderiv ℝ (CorrectionState.radialMoment 2 Z n) s) z

All slow and radial derivatives are taken before integration. A compact slow cutoff equals one on a whole neighborhood, so no moving-boundary terms are omitted.

theorem NavierStokes.GaugeMomentBalances.local_axial_moment {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b : ℝ} (ha : 0 < a) {U : Set S} (hU : IsOpen U) (r : CorrectionState.ReconstructionData) (ε fast : ℕ → ℝ) (z t : S) (v : Plane) {u R Z T : CorrectionState.ScalarField (PressureStream.Lift S)} (H : LocalFluxInputs a b U u R Z T) (hmass : ∀ (n : ℕ), ∀ s ∈ U, CorrectionState.radialMoment 1 u n s = 0) (n : ℕ) {s : S} (hs : s ∈ U) : CorrectionState.radialMoment 1 (StateMomentBalances.fluxResidual (StateMomentBalances.nativeOperators r ε fast z t v) 1 0 u R Z T) n s = ε n * (fderiv ℝ (CorrectionState.radialMoment 1 Z n) s) z

theorem NavierStokes.GaugeMomentBalances.LocalField.radialMoment_smooth {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b : ℝ} {U : Set S} (hU : IsOpen U) {f : CorrectionState.ScalarField (PressureStream.Lift S)} (hf : LocalField a b U f) (e n : ℕ) : ContDiffOn ℝ (↑⊤) (CorrectionState.radialMoment e f n) U

theorem NavierStokes.GaugeMomentBalances.LocalField.radialMoment_add {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b : ℝ} {U : Set S} (hU : IsOpen U) {f g : CorrectionState.ScalarField (PressureStream.Lift S)} (hf : LocalField a b U f) (hg : LocalField a b U g) (e n : ℕ) {s : S} (hs : s ∈ U) : CorrectionState.radialMoment e (f + g) n s = CorrectionState.radialMoment e f n s + CorrectionState.radialMoment e g n s

The actual reconstructed state in a moving similarity shell

structure NavierStokes.GaugeMomentBalances.MovingField {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (a b : ℝ) (f : CorrectionState.ScalarField Point) : Prop

Regularity of an actual field on the moving physical shell.

• smooth (n : ℕ) : ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)
• supported (n : ℕ) : VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) U.carrier (f n)
• periodic (n : ℕ) : PhysicalMeanDomain.PeriodicOn U.carrier (f n)

theorem NavierStokes.GaugeMomentBalances.MovingField.containing {coord a b c e : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : CorrectionState.ScalarField Point} (hf : MovingField U a b f) (hl : ∀ s ∈ U.carrier, c ≤ VariableGaugeMean.qLength coord s * a) (hr : ∀ s ∈ U.carrier, VariableGaugeMean.qLength coord s * b ≤ e) : LocalField c e U.carrier f

theorem NavierStokes.GaugeMomentBalances.MovingField.radialMoment_smooth {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} (ha : 0 < a) (hab : a < b) {f : CorrectionState.ScalarField Point} (hf : MovingField U a b f) (e n : ℕ) : ContDiffOn ℝ (↑⊤) (CorrectionState.radialMoment e f n) U.carrier

structure NavierStokes.GaugeMomentBalances.MovingFluxInputs {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (a b : ℝ) (u R Z T : CorrectionState.ScalarField Point) : Prop

Moving flux inputs data, collecting velocity, radial, axial, stress.

• velocity : MovingField U a b u
• radial : MovingField U a b R
• axial : MovingField U a b Z
• stress : MovingField U a b T

@[reducible, inline]

abbrev NavierStokes.GaugeMomentBalances.MovingAngularInputs {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (a b : ℝ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) : Prop

Moving angular inputs: an abbreviation for MovingFluxInputs U a b u.mean.angular (thetaRadialFlux c u) (thetaAxialFlux c u) c.virtualTheta.

Equations

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

@[reducible, inline]

abbrev NavierStokes.GaugeMomentBalances.MovingAxialInputs {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (a b : ℝ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) : Prop

Moving axial inputs: an abbreviation for MovingFluxInputs U a b u.mean.axial (axialRadialFlux c u) (axialAxialFlux c u) c.virtualAxial.

Equations

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

noncomputable def NavierStokes.GaugeMomentBalances.pressureRecipe (g : VariableGaugeMean.GaugeData Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) : CorrectionState.ScalarField Point

Pressure recipe, given by (VariableGaugeMean.reconstructState g c u).pressure.

Equations

• NavierStokes.GaugeMomentBalances.pressureRecipe g c u = (NavierStokes.VariableGaugeMean.reconstructState g c u).pressure

noncomputable def NavierStokes.GaugeMomentBalances.axialDebtPotential (g : VariableGaugeMean.GaugeData Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) : CorrectionState.ScalarField Plane

Axial debt potential, defined pointwise by CorrectionState.axialDefect c u n s + pressureCoefficient g n s * CorrectionState.pressureDefect c u n s.

Equations

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

theorem NavierStokes.GaugeMomentBalances.pressureRecipe_movingField {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hg : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hf : MovingField U g.radial.inner g.radial.outer (u.gr c)) : MovingField U g.radial.inner g.radial.outer (pressureRecipe g c u)

theorem NavierStokes.GaugeMomentBalances.pressureRecipe_moment {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hg : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hf : MovingField U g.radial.inner g.radial.outer (u.gr c)) (n : ℕ) {s : Plane} (hs : s ∈ U.carrier) : CorrectionState.radialMoment 1 (pressureRecipe g c u) n s = -(1 / 2) * CorrectionState.radialMoment 2 (u.gr c) n s + pressureCoefficient g n s * CorrectionState.pressureDefect c u n s

theorem NavierStokes.GaugeMomentBalances.axial_flux_pressure_moment {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hg : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hZ : MovingField U g.radial.inner g.radial.outer (StateMomentBalances.axialAxialFlux c u)) (hf : MovingField U g.radial.inner g.radial.outer (u.gr c)) (n : ℕ) {s : Plane} (hs : s ∈ U.carrier) : CorrectionState.radialMoment 1 (StateMomentBalances.axialAxialFlux c u + pressureRecipe g c u) n s = axialDebtPotential g c u n s

theorem NavierStokes.GaugeMomentBalances.state_angular_moment {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (r : CorrectionState.ReconstructionData) (ε fast : ℕ → ℝ) (z t v : Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (ho : c.operators = StateMomentBalances.nativeOperators r ε fast z t v) (H : MovingAngularInputs U a b c u) (hmass : ∀ (n : ℕ), ∀ s ∈ U.carrier, CorrectionState.radialMoment 2 u.mean.angular n s = 0) (n : ℕ) {s : Plane} (hs : s ∈ U.carrier) : CorrectionState.radialMoment 2 (u.thetaResidual c) n s = ε n * (fderiv ℝ (CorrectionState.thetaDefect c u n) s) z

theorem NavierStokes.GaugeMomentBalances.reconstructed_state_axial_moment {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hg : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (ε fast : ℕ → ℝ) (z t v : Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (ho : c.operators = StateMomentBalances.nativeOperators g.radial ε fast z t v) (H : MovingAxialInputs U g.radial.inner g.radial.outer c u) (hf : MovingField U g.radial.inner g.radial.outer (u.gr c)) (hmass : ∀ (n : ℕ), ∀ s ∈ U.carrier, CorrectionState.radialMoment 1 u.mean.axial n s = 0) (n : ℕ) {s : Plane} (hs : s ∈ U.carrier) : CorrectionState.radialMoment 1 ((VariableGaugeMean.reconstructState g c u).axialResidual c) n s = ε n * (fderiv ℝ (axialDebtPotential g c u n) s) z

The residual is evaluated on the literal moving-gauge reconstruction. The differentiated potential contains the full variable measured coefficient.

theorem NavierStokes.GaugeMomentBalances.state_axial_moment {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hg : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (ε fast : ℕ → ℝ) (z t v : Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (ho : c.operators = StateMomentBalances.nativeOperators g.radial ε fast z t v) (H : MovingAxialInputs U g.radial.inner g.radial.outer c u) (hf : MovingField U g.radial.inner g.radial.outer (u.gr c)) (hfixed : VariableGaugeMean.reconstructState g c u = u) (hmass : ∀ (n : ℕ), ∀ s ∈ U.carrier, CorrectionState.radialMoment 1 u.mean.axial n s = 0) (n : ℕ) {s : Plane} (hs : s ∈ U.carrier) : CorrectionState.radialMoment 1 (u.axialResidual c) n s = ε n * (fderiv ℝ (axialDebtPotential g c u n) s) z

All variable-coefficient terms and the actual debt classes

theorem NavierStokes.GaugeMomentBalances.q_pressureCoefficient {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (hg : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (n : ℕ) {s : Plane} (hs : s ∈ U.carrier) : pressureCoefficient g n s = basePressureCoefficient g.radial.inner g.radial.outer ⋯ * SimilarityCoordinates.coordinateQ coord s

theorem NavierStokes.GaugeMomentBalances.pressureCoefficient_smooth {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (hg : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (n : ℕ) : ContDiffOn ℝ (↑⊤) (pressureCoefficient g n) U.carrier

theorem NavierStokes.GaugeMomentBalances.q_pressureCoefficient_fderiv {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (hg : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (n : ℕ) {s : Plane} (hs : s ∈ U.carrier) (v : Plane) : (fderiv ℝ (pressureCoefficient g n) s) v = basePressureCoefficient g.radial.inner g.radial.outer ⋯ * ((v.1 + 2 * s.2 * SimilarityCoordinates.coordinateQ coord s ^ coord * v.2) / SimilarityCoordinates.scalarSlope coord s.2 (SimilarityCoordinates.coordinateQ coord s))

theorem NavierStokes.GaugeMomentBalances.q_pressureCoefficient_axial_derivative_pos {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (ha : 0 < g.radial.inner) (hg : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (n : ℕ) {s : Plane} (hs : s ∈ U.carrier) (hz : 0 < s.2) : 0 < (fderiv ℝ (pressureCoefficient g n) s) (0, 1)

On the positive axial half-plane the coefficient has a strictly positive axial derivative, so replacing it by a constant would change the identity.

theorem NavierStokes.GaugeMomentBalances.axialDebtPotential_smooth {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (ha : 0 < g.radial.inner) (hg : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hZ : MovingField U g.radial.inner g.radial.outer (StateMomentBalances.axialAxialFlux c u)) (hf : MovingField U g.radial.inner g.radial.outer (u.gr c)) (n : ℕ) : ContDiffOn ℝ (↑⊤) (axialDebtPotential g c u n) U.carrier

theorem NavierStokes.GaugeMomentBalances.axialDebtPotential_fderiv {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (ha : 0 < g.radial.inner) (hg : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hZ : MovingField U g.radial.inner g.radial.outer (StateMomentBalances.axialAxialFlux c u)) (hf : MovingField U g.radial.inner g.radial.outer (u.gr c)) (n : ℕ) {s : Plane} (hs : s ∈ U.carrier) (v : Plane) : (fderiv ℝ (axialDebtPotential g c u n) s) v = (fderiv ℝ (CorrectionState.axialDefect c u n) s) v + pressureCoefficient g n s * (fderiv ℝ (CorrectionState.pressureDefect c u n) s) v + (fderiv ℝ (pressureCoefficient g n) s) v * CorrectionState.pressureDefect c u n s

The product rule is applied to the actual measured coefficient. In particular, the last summand is present even if the unweighted debts are known.

theorem NavierStokes.GaugeMomentBalances.state_axial_moment_expanded {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hg : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (ε fast : ℕ → ℝ) (v : Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (ho : c.operators = StateMomentBalances.nativeOperators g.radial ε fast (0, 1) (1, 0) v) (H : MovingAxialInputs U g.radial.inner g.radial.outer c u) (hf : MovingField U g.radial.inner g.radial.outer (u.gr c)) (hfixed : VariableGaugeMean.reconstructState g c u = u) (hmass : ∀ (n : ℕ), ∀ s ∈ U.carrier, CorrectionState.radialMoment 1 u.mean.axial n s = 0) (n : ℕ) {s : Plane} (hs : s ∈ U.carrier) : CorrectionState.radialMoment 1 (u.axialResidual c) n s = ε n * ((fderiv ℝ (CorrectionState.axialDefect c u n) s) (0, 1) + pressureCoefficient g n s * (fderiv ℝ (CorrectionState.pressureDefect c u n) s) (0, 1) + basePressureCoefficient g.radial.inner g.radial.outer ⋯ * (2 * s.2 * SimilarityCoordinates.coordinateQ coord s ^ coord / SimilarityCoordinates.scalarSlope coord s.2 (SimilarityCoordinates.coordinateQ coord s)) * CorrectionState.pressureDefect c u n s)

Explicit native Z balance, with the moving-density derivative retained.

theorem NavierStokes.GaugeMomentBalances.pressureCoefficient_unweighted {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (P : SignedStressPrimitive.Patch) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (g : VariableGaugeMean.GaugeData Plane) (hg : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) : WeightedClasses.UnweightedClass (LocalSignedRequest.movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) 0 fun (n : ℕ) (x : LocalSignedRequest.Point) => pressureCoefficient g n x.2.1

theorem NavierStokes.GaugeMomentBalances.axialDebtPotential_unweighted {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (P : SignedStressPrimitive.Patch) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (g : VariableGaugeMean.GaugeData Plane) (hg : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (α : ℝ) (hP : WeightedClasses.UnweightedClass (LocalSignedRequest.movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) α fun (n : ℕ) (x : LocalSignedRequest.Point) => CorrectionState.pressureDefect c u n x.2.1) (hZ : WeightedClasses.UnweightedClass (LocalSignedRequest.movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) α fun (n : ℕ) (x : LocalSignedRequest.Point) => CorrectionState.axialDefect c u n x.2.1) : WeightedClasses.UnweightedClass (LocalSignedRequest.movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) α fun (n : ℕ) (x : LocalSignedRequest.Point) => axialDebtPotential g c u n x.2.1

The combined potential has the same all-jet order as its actual two debt components. The coefficient estimate uses the same moving strip.

Removed physical bumps for the same actual residuals

theorem NavierStokes.GaugeMomentBalances.state_angular_bump_improvedClass {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) (P : SignedStressPrimitive.Patch) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (ha : 0 < a) (hab : a < b) (r : CorrectionState.ReconstructionData) (ε fast L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (z t v : Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (α : ℝ) (ho : c.operators = StateMomentBalances.nativeOperators r ε fast z t v) (H : MovingAngularInputs U a b c u) (hmass : ∀ (n : ℕ), ∀ s ∈ U.carrier, CorrectionState.radialMoment 2 u.mean.angular n s = 0) (hD : WeightedClasses.UnweightedClass (LocalSignedRequest.movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) α fun (n : ℕ) (x : LocalSignedRequest.Point) => CorrectionState.thetaDefect c u n x.2.1) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) (α + 1) fun (n : ℕ) (x : LocalSignedRequest.Point) => SignedStressPrimitive.physicalBump P 2 (SimilarityCoordinates.coordinateQ coord) (PressureStream.torusAverage (u.thetaResidual c n)) (x.1, x.2.1)

The literal angular residual, its measured mass, and the removed physical bump all refer to the same state and moving chart.

theorem NavierStokes.GaugeMomentBalances.reconstructed_state_axial_bump_improvedClass {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (P : SignedStressPrimitive.Patch) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (g : VariableGaugeMean.GaugeData Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hg : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (ε fast L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (z t v : Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (α : ℝ) (ho : c.operators = StateMomentBalances.nativeOperators g.radial ε fast z t v) (H : MovingAxialInputs U g.radial.inner g.radial.outer c u) (hf : MovingField U g.radial.inner g.radial.outer (u.gr c)) (hmass : ∀ (n : ℕ), ∀ s ∈ U.carrier, CorrectionState.radialMoment 1 u.mean.axial n s = 0) (hP : WeightedClasses.UnweightedClass (LocalSignedRequest.movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) α fun (n : ℕ) (x : LocalSignedRequest.Point) => CorrectionState.pressureDefect c u n x.2.1) (hZ : WeightedClasses.UnweightedClass (LocalSignedRequest.movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) α fun (n : ℕ) (x : LocalSignedRequest.Point) => CorrectionState.axialDefect c u n x.2.1) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) (α + 1) fun (n : ℕ) (x : LocalSignedRequest.Point) => SignedStressPrimitive.physicalBump P 1 (SimilarityCoordinates.coordinateQ coord) (PressureStream.torusAverage ((VariableGaugeMean.reconstructState g c u).axialResidual c n)) (x.1, x.2.1)

Direct reconstruction version: the source is the actual axial residual after applying the moving pressure recipe, with no moment identity as input.

theorem NavierStokes.GaugeMomentBalances.state_axial_bump_improvedClass {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (P : SignedStressPrimitive.Patch) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (g : VariableGaugeMean.GaugeData Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hg : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (ε fast L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (z t v : Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (α : ℝ) (ho : c.operators = StateMomentBalances.nativeOperators g.radial ε fast z t v) (H : MovingAxialInputs U g.radial.inner g.radial.outer c u) (hf : MovingField U g.radial.inner g.radial.outer (u.gr c)) (hfixed : VariableGaugeMean.reconstructState g c u = u) (hmass : ∀ (n : ℕ), ∀ s ∈ U.carrier, CorrectionState.radialMoment 1 u.mean.axial n s = 0) (hP : WeightedClasses.UnweightedClass (LocalSignedRequest.movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) α fun (n : ℕ) (x : LocalSignedRequest.Point) => CorrectionState.pressureDefect c u n x.2.1) (hZ : WeightedClasses.UnweightedClass (LocalSignedRequest.movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) α fun (n : ℕ) (x : LocalSignedRequest.Point) => CorrectionState.axialDefect c u n x.2.1) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) (α + 1) fun (n : ℕ) (x : LocalSignedRequest.Point) => SignedStressPrimitive.physicalBump P 1 (SimilarityCoordinates.coordinateQ coord) (PressureStream.torusAverage (u.axialResidual c n)) (x.1, x.2.1)

Fixed-point version for the actual output of a temporal or rank stage, whose constructor finishes with reconstructState.