Local mass preservation for the actual moving-gauge temporal update

All conclusions are restricted to the valid open slow region. The common torus index and the moving radial support are retained throughout.

@[reducible, inline]

abbrev NavierStokes.GaugeMassPreservation.Plane : Type

Plane: an abbreviation for PressureStream.Plane.

Equations

• NavierStokes.GaugeMassPreservation.Plane = NavierStokes.PressureStream.Plane

@[reducible, inline]

abbrev NavierStokes.GaugeMassPreservation.Point : Type

Point: an abbreviation for PressureStream.Lift Plane.

Equations

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

theorem NavierStokes.GaugeMassPreservation.streamGamma_frozen_on {coord a b d M : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : Plane) {f : Point → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) (hs : VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) U.carrier f) {s : Plane} (hsm : s ∈ U.carrier) (R : ℝ) (Y : Plane) : PressureStream.streamGamma (PressureStream.physicalSpeed d M) (0, v) (VariableGaugeMean.streamPotential d a b M (VariableGaugeMean.qLength coord) v f) (R, s, Y) = PressureStream.streamGamma (PressureStream.physicalSpeed d M) (0, v) (PressureStream.streamPotential d (VariableGaugeMean.qLength coord s * a) (VariableGaugeMean.qLength coord s * b) M (0, v) (PhysicalMeanDomain.freezeSlow s f)) (R, s, Y)

Equality of the moving and frozen stream realizations on one complete radial/torus fiber. Radial differentiation, including at zero, is retained.

theorem NavierStokes.GaugeMassPreservation.streamGamma_slice_continuous_on {coord a b d M : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : Plane) {f : Point → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) (hs : VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) U.carrier f) {s : Plane} (hsm : s ∈ U.carrier) (R : ℝ) : Continuous fun (Y : Plane) => PressureStream.streamGamma (PressureStream.physicalSpeed d M) (0, v) (VariableGaugeMean.streamPotential d a b M (VariableGaugeMean.qLength coord) v f) (R, s, Y)

theorem NavierStokes.GaugeMassPreservation.streamGamma_bar_eq_desired_on {coord a b d M : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : Plane) {f : Point → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) (hs : VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) U.carrier f) (hp : PhysicalMeanDomain.PeriodicOn U.carrier f) {s : Plane} (hsm : s ∈ U.carrier) (hm : ∫ (r : ℝ), r * PressureStream.torusAverage f (r, s) = 0) (R : ℝ) : PressureStream.torusAverage (PressureStream.streamGamma (PressureStream.physicalSpeed d M) (0, v) (VariableGaugeMean.streamPotential d a b M (VariableGaugeMean.qLength coord) v f)) (R, s) = PressureStream.torusAverage f (R, s)

Zero weighted bar mass gives the prescribed axial bar in the moving gauge. The conclusion covers every real radius, including zero.

theorem NavierStokes.GaugeMassPreservation.continuous_torus_slice {U : Set Plane} {f : Point → ℝ} (hf : ContinuousOn f (PhysicalMeanDomain.slowDomain U)) {s : Plane} (hs : s ∈ U) (R : ℝ) : Continuous fun (Y : Plane) => f (R, s, Y)

theorem NavierStokes.GaugeMassPreservation.torusAverage_add_slice (f g : Point → ℝ) (R : ℝ) (s : Plane) (hf : Continuous fun (Y : PressureStream.Plane) => f (R, s, Y)) (hg : Continuous fun (Y : PressureStream.Plane) => g (R, s, Y)) : PressureStream.torusAverage (fun (z : PressureStream.Lift Plane) => f z + g z) (R, s) = PressureStream.torusAverage f (R, s) + PressureStream.torusAverage g (R, s)

theorem NavierStokes.GaugeMassPreservation.radialMoment_congr_torusAverage (k : ℕ) (f g : CorrectionState.ScalarField Point) (n : ℕ) (s : Plane) (he : ∀ (R : ℝ), PressureStream.torusAverage (f n) (R, s) = PressureStream.torusAverage (g n) (R, s)) : CorrectionState.radialMoment k f n s = CorrectionState.radialMoment k g n s

theorem NavierStokes.GaugeMassPreservation.radialMoment_zero_of_torusAverage (k : ℕ) (f : CorrectionState.ScalarField Point) (n : ℕ) (s : Plane) (he : ∀ (R : ℝ), PressureStream.torusAverage (f n) (R, s) = 0) : CorrectionState.radialMoment k f n s = 0

noncomputable def NavierStokes.GaugeMassPreservation.ZeroMassesOn (U : Set Plane) (u : CorrectionState.State Point) : Prop

The two conserved mean masses, restricted to a specified slow set.

Equations

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

theorem NavierStokes.GaugeMassPreservation.ZeroMassesOn.of_global {U : Set Plane} {u : CorrectionState.State Point} (hu : CorrectionState.ZeroMasses u) : ZeroMassesOn U u

theorem NavierStokes.GaugeMassPreservation.temporalIncrement_torusMean_on {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (h : ℝ) (index : ℕ → ℕ) (axial : Plane × Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hθ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.thetaResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hz : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.axialResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hpθ : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.thetaResidual c n)) (hpz : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.axialResidual c n)) (hsz : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (u.axialResidual c n)) (n : ℕ) (R : ℝ) {s : Plane} (hs : s ∈ U.carrier) : PressureStream.torusAverage ((VariableGaugeMean.temporalIncrementState g h index axial c u).angular n) (R, s) = 0 ∧ PressureStream.torusAverage ((VariableGaugeMean.temporalIncrementState g h index axial c u).axial n) (R, s) = 0

theorem NavierStokes.GaugeMassPreservation.temporalIncrement_slice_continuous_on {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (h : ℝ) (index : ℕ → ℕ) (axial : Plane × Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hθ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.thetaResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hz : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.axialResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hpθ : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.thetaResidual c n)) (hpz : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.axialResidual c n)) (hsz : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (u.axialResidual c n)) (n : ℕ) (R : ℝ) {s : Plane} (hs : s ∈ U.carrier) : (Continuous fun (Y : PressureStream.Plane) => (VariableGaugeMean.temporalIncrementState g h index axial c u).angular n (R, s, Y)) ∧ Continuous fun (Y : PressureStream.Plane) => (VariableGaugeMean.temporalIncrementState g h index axial c u).axial n (R, s, Y)

theorem NavierStokes.GaugeMassPreservation.temporalIncrement_radialMoments_zero_on {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (h : ℝ) (index : ℕ → ℕ) (axial : Plane × Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hθ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.thetaResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hz : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.axialResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hpθ : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.thetaResidual c n)) (hpz : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.axialResidual c n)) (hsz : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (u.axialResidual c n)) (k n : ℕ) {s : Plane} (hs : s ∈ U.carrier) : CorrectionState.radialMoment k (VariableGaugeMean.temporalIncrementState g h index axial c u).angular n s = 0 ∧ CorrectionState.radialMoment k (VariableGaugeMean.temporalIncrementState g h index axial c u).axial n s = 0

Every radial moment of either conserved increment vanishes on the valid slow set, since its full torus average is identically zero there.

theorem NavierStokes.GaugeMassPreservation.temporalStage_torusMean_on {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (h : ℝ) (index : ℕ → ℕ) (axial : Plane × Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hmθ : ∀ (n : ℕ), ContinuousOn (u.mean.angular n) (PhysicalMeanDomain.slowDomain U.carrier)) (hmz : ∀ (n : ℕ), ContinuousOn (u.mean.axial n) (PhysicalMeanDomain.slowDomain U.carrier)) (hθ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.thetaResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hz : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.axialResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hpθ : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.thetaResidual c n)) (hpz : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.axialResidual c n)) (hsz : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (u.axialResidual c n)) (n : ℕ) (R : ℝ) {s : Plane} (hs : s ∈ U.carrier) : PressureStream.torusAverage ((VariableGaugeMean.temporalStageState g h index axial c u).mean.angular n) (R, s) = PressureStream.torusAverage (u.mean.angular n) (R, s) ∧ PressureStream.torusAverage ((VariableGaugeMean.temporalStageState g h index axial c u).mean.axial n) (R, s) = PressureStream.torusAverage (u.mean.axial n) (R, s)

Pressure reconstruction and the stored temporal alias leave the actual angular/axial torus means unchanged after the common-index increment.

theorem NavierStokes.GaugeMassPreservation.temporalStage_preserve_masses_on {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (h : ℝ) (index : ℕ → ℕ) (axial : Plane × Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hmθ : ∀ (n : ℕ), ContinuousOn (u.mean.angular n) (PhysicalMeanDomain.slowDomain U.carrier)) (hmz : ∀ (n : ℕ), ContinuousOn (u.mean.axial n) (PhysicalMeanDomain.slowDomain U.carrier)) (hθ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.thetaResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hz : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.axialResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hpθ : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.thetaResidual c n)) (hpz : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.axialResidual c n)) (hsz : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (u.axialResidual c n)) (n : ℕ) {s : Plane} (hs : s ∈ U.carrier) : CorrectionState.radialMoment 2 (VariableGaugeMean.temporalStageState g h index axial c u).mean.angular n s = CorrectionState.radialMoment 2 u.mean.angular n s ∧ CorrectionState.radialMoment 1 (VariableGaugeMean.temporalStageState g h index axial c u).mean.axial n s = CorrectionState.radialMoment 1 u.mean.axial n s

The literal reconstructed temporal state preserves both physical mean masses on the valid slow region. No statement is made outside that region.

theorem NavierStokes.GaugeMassPreservation.temporalStage_zeroMassesOn {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (h : ℝ) (index : ℕ → ℕ) (axial : Plane × Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hmθ : ∀ (n : ℕ), ContinuousOn (u.mean.angular n) (PhysicalMeanDomain.slowDomain U.carrier)) (hmz : ∀ (n : ℕ), ContinuousOn (u.mean.axial n) (PhysicalMeanDomain.slowDomain U.carrier)) (hθ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.thetaResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hz : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.axialResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hpθ : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.thetaResidual c n)) (hpz : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.axialResidual c n)) (hsz : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (u.axialResidual c n)) (hu : ZeroMassesOn U.carrier u) : ZeroMassesOn U.carrier (VariableGaugeMean.temporalStageState g h index axial c u)

theorem NavierStokes.GaugeMassPreservation.temporalStage_zeroMassesOn_of_global {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (h : ℝ) (index : ℕ → ℕ) (axial : Plane × Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hmθ : ∀ (n : ℕ), ContinuousOn (u.mean.angular n) (PhysicalMeanDomain.slowDomain U.carrier)) (hmz : ∀ (n : ℕ), ContinuousOn (u.mean.axial n) (PhysicalMeanDomain.slowDomain U.carrier)) (hθ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.thetaResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hz : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.axialResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hpθ : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.thetaResidual c n)) (hpz : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.axialResidual c n)) (hsz : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (u.axialResidual c n)) (hu : CorrectionState.ZeroMasses u) : ZeroMassesOn U.carrier (VariableGaugeMean.temporalStageState g h index axial c u)