Measured debt changes for actual gauge updates

The debt is the three actual radial moments stored by CorrectionState. The change estimates use the actual velocity and covariance increments; no improved bound on the whole updated covariance or debt is assumed.

@[reducible, inline]

abbrev NavierStokes.GaugeDebtIncrement.Plane : Type

Plane: an abbreviation for PressureStream.Plane.

Equations

• NavierStokes.GaugeDebtIncrement.Plane = NavierStokes.PressureStream.Plane

@[reducible, inline]

abbrev NavierStokes.GaugeDebtIncrement.Point : Type

Point: an abbreviation for PressureStream.Lift Plane.

Equations

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

@[reducible, inline]

abbrev NavierStokes.GaugeDebtIncrement.Scalar : Type

Scalar: an abbreviation for MeanIncrementBounds.Field Point.

Equations

• NavierStokes.GaugeDebtIncrement.Scalar = NavierStokes.MeanIncrementBounds.Field NavierStokes.GaugeDebtIncrement.Point

@[reducible, inline]

abbrev NavierStokes.GaugeDebtIncrement.Tensor : Type

Tensor: an abbreviation for Fin 3 → Fin 3 → Scalar.

Equations

• NavierStokes.GaugeDebtIncrement.Tensor = (Fin 3 → Fin 3 → NavierStokes.GaugeDebtIncrement.Scalar)

structure NavierStokes.GaugeDebtIncrement.Regular {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (a b : ℝ) (f : Scalar) : Prop

Primitive local smoothness and actual support, without a class estimate.

• smooth : MeanIncrementBounds.SmoothOn (PhysicalMeanDomain.slowDomain U.carrier) f
• supported (n : ℕ) : VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) U.carrier (f n)

theorem NavierStokes.GaugeDebtIncrement.Regular.containing {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : Regular U a b f) {lo hi : ℝ} (hl : ∀ x ∈ U.carrier, lo ≤ VariableGaugeMean.qLength coord x * a) (hr : ∀ x ∈ U.carrier, VariableGaugeMean.qLength coord x * b ≤ hi) : LocalRankDefect.LocalShell lo hi U.carrier f

theorem NavierStokes.GaugeDebtIncrement.Regular.zero {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} : Regular U a b 0

theorem NavierStokes.GaugeDebtIncrement.Regular.add {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f g : Scalar} (hf : Regular U a b f) (hg : Regular U a b g) : Regular U a b (f + g)

theorem NavierStokes.GaugeDebtIncrement.Regular.neg {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : Regular U a b f) : Regular U a b (-f)

theorem NavierStokes.GaugeDebtIncrement.Regular.sub {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f g : Scalar} (hf : Regular U a b f) (hg : Regular U a b g) : Regular U a b (f - g)

theorem NavierStokes.GaugeDebtIncrement.Regular.mul {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f g : Scalar} (hf : Regular U a b f) (hg : Regular U a b g) : Regular U a b (f * g)

theorem NavierStokes.GaugeDebtIncrement.Regular.smul {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : Regular U a b f) (c : ℝ) : Regular U a b (c • f)

theorem NavierStokes.GaugeDebtIncrement.Regular.band_mul {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : Regular U a b f) (c : ℕ → ℝ) : Regular U a b fun (n : ℕ) (x : Point) => c n * f n x

theorem NavierStokes.GaugeDebtIncrement.Regular.directional {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : Regular U a b f) (v : Point) : Regular U a b fun (n : ℕ) (x : Point) => (fderiv ℝ (f n) x) v

theorem NavierStokes.GaugeDebtIncrement.Regular.coefficient_mul {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f g : Scalar} (hf : Regular U a b f) (ha : 0 < a) (hab : a < b) (hg : MeanIncrementBounds.SmoothOn (LocalRankDefect.positiveDomain U.carrier) g) : Regular U a b (g * f)

theorem NavierStokes.GaugeDebtIncrement.Regular.mul_coefficient {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f g : Scalar} (hf : Regular U a b f) (ha : 0 < a) (hab : a < b) (hg : MeanIncrementBounds.SmoothOn (LocalRankDefect.positiveDomain U.carrier) g) : Regular U a b (f * g)

theorem NavierStokes.GaugeDebtIncrement.Regular.dr {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : Regular U a b f) (ha : 0 < a) (hab : a < b) {o : MeanIncrementBounds.Operators Point} (ho : LocalRankDefect.LocalOperators U.carrier o) : Regular U a b (o.dr f)

theorem NavierStokes.GaugeDebtIncrement.Regular.dz {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : Regular U a b f) (o : MeanIncrementBounds.Operators Point) : Regular U a b (o.dz f)

theorem NavierStokes.GaugeDebtIncrement.Regular.time {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : Regular U a b f) (o : MeanIncrementBounds.Operators Point) : Regular U a b (o.time f)

theorem NavierStokes.GaugeDebtIncrement.Regular.inv_mul {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : Regular U a b f) (ha : 0 < a) (hab : a < b) {o : MeanIncrementBounds.Operators Point} (ho : LocalRankDefect.LocalOperators U.carrier o) : Regular U a b (o.invRadius * f)

theorem NavierStokes.GaugeDebtIncrement.Regular.radialDiv {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : Regular U a b f) (ha : 0 < a) (hab : a < b) {o : MeanIncrementBounds.Operators Point} (ho : LocalRankDefect.LocalOperators U.carrier o) (c : ℝ) : Regular U a b (o.radialDiv c f)

theorem NavierStokes.GaugeDebtIncrement.Regular.viscosity {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : Regular U a b f) (ha : 0 < a) (hab : a < b) {o : MeanIncrementBounds.Operators Point} (ho : LocalRankDefect.LocalOperators U.carrier o) (c : ℝ) : Regular U a b (o.viscosity c f)

structure NavierStokes.GaugeDebtIncrement.RegularTriple {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (a b : ℝ) (m : MeanIncrementBounds.Triple Point) : Prop

Regular triple data, collecting radial, angular, axial.

• radial : Regular U a b m.radial
• angular : Regular U a b m.angular
• axial : Regular U a b m.axial

theorem NavierStokes.GaugeDebtIncrement.RegularTriple.smooth {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {m : MeanIncrementBounds.Triple Point} (hm : RegularTriple U a b m) : MeanIncrementBounds.SmoothTriple (PhysicalMeanDomain.slowDomain U.carrier) m

theorem NavierStokes.GaugeDebtIncrement.RegularTriple.updated {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {m h : MeanIncrementBounds.Triple Point} (hm : RegularTriple U a b m) (hh : RegularTriple U a b h) : RegularTriple U a b (MeanIncrementBounds.updated m h)

theorem NavierStokes.GaugeDebtIncrement.RegularTriple.thetaAxial {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {m base : MeanIncrementBounds.Triple Point} (hm : RegularTriple U a b m) (ha : 0 < a) (hab : a < b) (hb : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) base) : Regular U a b (MeanIncrementBounds.thetaAxial base m)

theorem NavierStokes.GaugeDebtIncrement.RegularTriple.axialAxial {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {m base : MeanIncrementBounds.Triple Point} (hm : RegularTriple U a b m) (ha : 0 < a) (hab : a < b) (hb : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) base) : Regular U a b (MeanIncrementBounds.axialAxial base m)

theorem NavierStokes.GaugeDebtIncrement.RegularTriple.axialRadial {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {m base : MeanIncrementBounds.Triple Point} (hm : RegularTriple U a b m) (ha : 0 < a) (hab : a < b) (hb : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) base) : Regular U a b (MeanIncrementBounds.axialRadial base m)

theorem NavierStokes.GaugeDebtIncrement.RegularTriple.radialRadial {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {m base : MeanIncrementBounds.Triple Point} (hm : RegularTriple U a b m) (ha : 0 < a) (hab : a < b) (hb : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) base) : Regular U a b (MeanIncrementBounds.radialRadial base m)

theorem NavierStokes.GaugeDebtIncrement.RegularTriple.radialAngular {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {m base : MeanIncrementBounds.Triple Point} (hm : RegularTriple U a b m) (ha : 0 < a) (hab : a < b) (hb : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) base) : Regular U a b (MeanIncrementBounds.radialAngular base m)

theorem NavierStokes.GaugeDebtIncrement.RegularTriple.gr {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {m base : MeanIncrementBounds.Triple Point} (hm : RegularTriple U a b m) (ha : 0 < a) (hab : a < b) (hb : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) base) {o : MeanIncrementBounds.Operators Point} (ho : LocalRankDefect.LocalOperators U.carrier o) (W : Tensor) (hW : ∀ (i j : Fin 3), Regular U a b (W i j)) : Regular U a b (MeanIncrementBounds.gr o base m W)

Exact moments and their class bounds

theorem NavierStokes.GaugeDebtIncrement.radialMoment_sub_on {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) {f g : Scalar} (hf : Regular U a b f) (hg : Regular U a b g) (k n : ℕ) {x : Plane} (hx : x ∈ U.carrier) : CorrectionState.radialMoment k (f - g) n x = CorrectionState.radialMoment k f n x - CorrectionState.radialMoment k g n x

theorem NavierStokes.GaugeDebtIncrement.radialMoment_add_on {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) {f g : Scalar} (hf : Regular U a b f) (hg : Regular U a b g) (k n : ℕ) {x : Plane} (hx : x ∈ U.carrier) : CorrectionState.radialMoment k (f + g) n x = CorrectionState.radialMoment k f n x + CorrectionState.radialMoment k g n x

noncomputable def NavierStokes.GaugeDebtIncrement.momentChange (G T Z : Scalar) : ℕ → Plane → Fin 3 → ℝ

Moment change, defined pointwise by ![radialMoment 0 G n x, radialMoment 2 T n x, radialMoment 1 Z n x - (1 / 2 : ℝ) * radialMoment 2 G n x].

Equations

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

theorem NavierStokes.GaugeDebtIncrement.debt_sub_eq {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (c : CorrectionState.Context Point) (u v : CorrectionState.State Point) (hgu : Regular U a b (u.gr c)) (hgv : Regular U a b (v.gr c)) (htu : Regular U a b (MeanIncrementBounds.thetaAxial c.base u.mean + u.covariance 2 1)) (htv : Regular U a b (MeanIncrementBounds.thetaAxial c.base v.mean + v.covariance 2 1)) (hzu : Regular U a b (MeanIncrementBounds.axialAxial c.base u.mean + u.covariance 2 2)) (hzv : Regular U a b (MeanIncrementBounds.axialAxial c.base v.mean + v.covariance 2 2)) (n : ℕ) {x : Plane} (hx : x ∈ U.carrier) : CorrectionState.debt c v n x - CorrectionState.debt c u n x = momentChange (v.gr c - u.gr c) (MeanIncrementBounds.thetaAxial c.base v.mean + v.covariance 2 1 - (MeanIncrementBounds.thetaAxial c.base u.mean + u.covariance 2 1)) (MeanIncrementBounds.axialAxial c.base v.mean + v.covariance 2 2 - (MeanIncrementBounds.axialAxial c.base u.mean + u.covariance 2 2)) n x

The actual State debt difference consists of the three actual moment changes, with the pressure-source contribution in the axial row retained.

theorem NavierStokes.GaugeDebtIncrement.momentChange_mem {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {H : ℝ} {G T Z : Scalar} (hG : Regular U a b G) (hT : Regular U a b T) (hZ : Regular U a b Z) (hcG : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) H G) (hcT : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) H T) (hcZ : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) H Z) (i : Fin 3) : WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) H fun (n : ℕ) (x : LocalSignedRequest.Plane) => momentChange G T Z n x i

theorem NavierStokes.GaugeDebtIncrement.debt_change_mem {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {H : ℝ} (c : CorrectionState.Context Point) (u v : CorrectionState.State Point) (hgu : Regular U a b (u.gr c)) (hgv : Regular U a b (v.gr c)) (htu : Regular U a b (MeanIncrementBounds.thetaAxial c.base u.mean + u.covariance 2 1)) (htv : Regular U a b (MeanIncrementBounds.thetaAxial c.base v.mean + v.covariance 2 1)) (hzu : Regular U a b (MeanIncrementBounds.axialAxial c.base u.mean + u.covariance 2 2)) (hzv : Regular U a b (MeanIncrementBounds.axialAxial c.base v.mean + v.covariance 2 2)) (hcG : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) H (v.gr c - u.gr c)) (hcT : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) H (MeanIncrementBounds.thetaAxial c.base v.mean + v.covariance 2 1 - (MeanIncrementBounds.thetaAxial c.base u.mean + u.covariance 2 1))) (hcZ : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) H (MeanIncrementBounds.axialAxial c.base v.mean + v.covariance 2 2 - (MeanIncrementBounds.axialAxial c.base u.mean + u.covariance 2 2))) (i : Fin 3) : WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) H fun (n : ℕ) (x : LocalSignedRequest.Plane) => CorrectionState.debt c v n x i - CorrectionState.debt c u n x i

theorem NavierStokes.GaugeDebtIncrement.smoothTriple_mono {V W : Set Point} {m : MeanIncrementBounds.Triple Point} (hm : MeanIncrementBounds.SmoothTriple W m) (hVW : V ⊆ W) : MeanIncrementBounds.SmoothTriple V m

theorem NavierStokes.GaugeDebtIncrement.Regular.zero_of_nonpositive {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : Regular U a b f) (ha : 0 < a) (n : ℕ) {z : Point} (hz : z.2.1 ∈ U.carrier) (hR : z.1 ≤ 0) : f n z = 0

theorem NavierStokes.GaugeDebtIncrement.agree_slow_of_positive {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f g : Scalar} (ha : 0 < a) (hf : Regular U a b f) (hg : Regular U a b g) (he : MeanIncrementBounds.Agree (LocalRankDefect.positiveDomain U.carrier) f g) : MeanIncrementBounds.Agree (PhysicalMeanDomain.slowDomain U.carrier) f g

theorem NavierStokes.GaugeDebtIncrement.moving_subset_positive {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) : (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL).domain ⊆ LocalRankDefect.positiveDomain U.carrier

theorem NavierStokes.GaugeDebtIncrement.radialMoment_congr_on {U : Set Plane} {f g : Scalar} (he : MeanIncrementBounds.Agree (PhysicalMeanDomain.slowDomain U) f g) (k n : ℕ) {x : Plane} (hx : x ∈ U) : CorrectionState.radialMoment k f n x = CorrectionState.radialMoment k g n x

theorem NavierStokes.GaugeDebtIncrement.wave_thetaFlux_change (g : VariableGaugeMean.GaugeData Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (w : CorrectionState.Oscillation Point) (q : CorrectionState.OscillatoryScalar Point) (gaussian : CorrectionState.Oscillation Point) : MeanIncrementBounds.thetaAxial c.base (SignedMeanGain.waveStage g c u w q gaussian).mean + (SignedMeanGain.waveStage g c u w q gaussian).covariance 2 1 - (MeanIncrementBounds.thetaAxial c.base u.mean + u.covariance 2 1) = SignedMeanGain.covarianceIncrement u.oscillation w 2 1

theorem NavierStokes.GaugeDebtIncrement.wave_axialFlux_change (g : VariableGaugeMean.GaugeData Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (w : CorrectionState.Oscillation Point) (q : CorrectionState.OscillatoryScalar Point) (gaussian : CorrectionState.Oscillation Point) : MeanIncrementBounds.axialAxial c.base (SignedMeanGain.waveStage g c u w q gaussian).mean + (SignedMeanGain.waveStage g c u w q gaussian).covariance 2 2 - (MeanIncrementBounds.axialAxial c.base u.mean + u.covariance 2 2) = SignedMeanGain.covarianceIncrement u.oscillation w 2 2

theorem NavierStokes.GaugeDebtIncrement.waveStage_mean_regular {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (w : CorrectionState.Oscillation Point) (q : CorrectionState.OscillatoryScalar Point) (gaussian : CorrectionState.Oscillation Point) (hm : RegularTriple U a b u.mean) : RegularTriple U a b (SignedMeanGain.waveStage g c u w q gaussian).mean

theorem NavierStokes.GaugeDebtIncrement.waveStage_covariance_regular {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (w : CorrectionState.Oscillation Point) (q : CorrectionState.OscillatoryScalar Point) (gaussian : CorrectionState.Oscillation Point) (hW : ∀ (i j : Fin 3), Regular U a b (u.covariance i j)) (hX : ∀ (i j : Fin 3), Regular U a b (SignedMeanGain.covarianceIncrement u.oscillation w i j)) (i j : Fin 3) : Regular U a b ((SignedMeanGain.waveStage g c u w q gaussian).covariance i j)

theorem NavierStokes.GaugeDebtIncrement.waveStage_gr_agree {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (g : VariableGaugeMean.GaugeData Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (w : CorrectionState.Oscillation Point) (q : CorrectionState.OscillatoryScalar Point) (gaussian : CorrectionState.Oscillation Point) (hop : LocalRankDefect.LocalOperators U.carrier c.operators) (hb : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) c.base) (hm : RegularTriple U a b u.mean) (hW : ∀ (i j : Fin 3), Regular U a b (u.covariance i j)) (hX : ∀ (i j : Fin 3), Regular U a b (SignedMeanGain.covarianceIncrement u.oscillation w i j)) : MeanIncrementBounds.Agree (PhysicalMeanDomain.slowDomain U.carrier) ((SignedMeanGain.waveStage g c u w q gaussian).gr c - u.gr c) (SignedMeanGain.radialCovarianceChange c.operators (SignedMeanGain.covarianceIncrement u.oscillation w))

theorem NavierStokes.GaugeDebtIncrement.waveStage_debt_change_formula {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (g : VariableGaugeMean.GaugeData Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (w : CorrectionState.Oscillation Point) (q : CorrectionState.OscillatoryScalar Point) (gaussian : CorrectionState.Oscillation Point) (hop : LocalRankDefect.LocalOperators U.carrier c.operators) (hb : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) c.base) (hm : RegularTriple U a b u.mean) (hW : ∀ (i j : Fin 3), Regular U a b (u.covariance i j)) (hX : ∀ (i j : Fin 3), Regular U a b (SignedMeanGain.covarianceIncrement u.oscillation w i j)) (n : ℕ) {x : Plane} (hx : x ∈ U.carrier) : CorrectionState.debt c (SignedMeanGain.waveStage g c u w q gaussian) n x - CorrectionState.debt c u n x = momentChange (SignedMeanGain.radialCovarianceChange c.operators (SignedMeanGain.covarianceIncrement u.oscillation w)) (SignedMeanGain.covarianceIncrement u.oscillation w 2 1) (SignedMeanGain.covarianceIncrement u.oscillation w 2 2) n x

The wave adds exactly the covariance moments; pressure recomputation adds no term to the definition of measured debt.

theorem NavierStokes.GaugeDebtIncrement.waveStage_debt_change_mem {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (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) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (w : CorrectionState.Oscillation Point) (q : CorrectionState.OscillatoryScalar Point) (gaussian : CorrectionState.Oscillation Point) (hop : LocalRankDefect.LocalOperators U.carrier c.operators) (hb : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) c.base) (hm : RegularTriple U a b u.mean) (hW : ∀ (i j : Fin 3), Regular U a b (u.covariance i j)) (hX : ∀ (i j : Fin 3), Regular U a b (SignedMeanGain.covarianceIncrement u.oscillation w i j)) {κ α : ℝ} (ho : MeanIncrementBounds.OperatorBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) c.operators κ) (hcX : SignedMeanGain.TensorClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α (SignedMeanGain.covarianceIncrement u.oscillation w)) (i : Fin 3) : WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) (α - κ) fun (n : ℕ) (x : LocalSignedRequest.Plane) => CorrectionState.debt c (SignedMeanGain.waveStage g c u w q gaussian) n x i - CorrectionState.debt c u n x i

theorem NavierStokes.GaugeDebtIncrement.temporalStage_mean (g : VariableGaugeMean.GaugeData Plane) (h : ℝ) (index : ℕ → ℕ) (axial : Plane × Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) : (VariableGaugeMean.temporalStageState g h index axial c u).mean = MeanIncrementBounds.updated u.mean (VariableGaugeMean.temporalIncrementState g h index axial c u)

theorem NavierStokes.GaugeDebtIncrement.temporalStage_covariance (g : VariableGaugeMean.GaugeData Plane) (h : ℝ) (index : ℕ → ℕ) (axial : Plane × Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) : (VariableGaugeMean.temporalStageState g h index axial c u).covariance = u.covariance

theorem NavierStokes.GaugeDebtIncrement.temporal_thetaFlux_change (g : VariableGaugeMean.GaugeData Plane) (h : ℝ) (index : ℕ → ℕ) (axial : Plane × Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) : MeanIncrementBounds.thetaAxial c.base (VariableGaugeMean.temporalStageState g h index axial c u).mean + (VariableGaugeMean.temporalStageState g h index axial c u).covariance 2 1 - (MeanIncrementBounds.thetaAxial c.base u.mean + u.covariance 2 1) = MeanIncrementBounds.deltaThetaAxial c.base u.mean (VariableGaugeMean.temporalIncrementState g h index axial c u)

theorem NavierStokes.GaugeDebtIncrement.temporal_axialFlux_change (g : VariableGaugeMean.GaugeData Plane) (h : ℝ) (index : ℕ → ℕ) (axial : Plane × Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) : MeanIncrementBounds.axialAxial c.base (VariableGaugeMean.temporalStageState g h index axial c u).mean + (VariableGaugeMean.temporalStageState g h index axial c u).covariance 2 2 - (MeanIncrementBounds.axialAxial c.base u.mean + u.covariance 2 2) = MeanIncrementBounds.deltaAxialAxial c.base u.mean (VariableGaugeMean.temporalIncrementState g h index axial c u)

theorem NavierStokes.GaugeDebtIncrement.temporalStage_mean_regular {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (h : ℝ) (index : ℕ → ℕ) (axial : Plane × Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hm : RegularTriple U a b u.mean) (hi : RegularTriple U a b (VariableGaugeMean.temporalIncrementState g h index axial c u)) : RegularTriple U a b (VariableGaugeMean.temporalStageState g h index axial c u).mean

theorem NavierStokes.GaugeDebtIncrement.temporalStage_covariance_regular {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (h : ℝ) (index : ℕ → ℕ) (axial : Plane × Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hW : ∀ (i j : Fin 3), Regular U a b (u.covariance i j)) (i j : Fin 3) : Regular U a b ((VariableGaugeMean.temporalStageState g h index axial c u).covariance i j)

theorem NavierStokes.GaugeDebtIncrement.temporalStage_debt_change_formula {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (g : VariableGaugeMean.GaugeData Plane) (h : ℝ) (index : ℕ → ℕ) (axial : Plane × Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hop : LocalRankDefect.LocalOperators U.carrier c.operators) (hb : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) c.base) (hm : RegularTriple U a b u.mean) (hi : RegularTriple U a b (VariableGaugeMean.temporalIncrementState g h index axial c u)) (hW : ∀ (i j : Fin 3), Regular U a b (u.covariance i j)) (n : ℕ) {x : Plane} (hx : x ∈ U.carrier) : CorrectionState.debt c (VariableGaugeMean.temporalStageState g h index axial c u) n x - CorrectionState.debt c u n x = momentChange ((VariableGaugeMean.temporalStageState g h index axial c u).gr c - u.gr c) (MeanIncrementBounds.deltaThetaAxial c.base u.mean (VariableGaugeMean.temporalIncrementState g h index axial c u)) (MeanIncrementBounds.deltaAxialAxial c.base u.mean (VariableGaugeMean.temporalIncrementState g h index axial c u)) n x

Only the actual mean increment contributes to the temporal flux change; the covariance remains the same actual angular integral.

theorem NavierStokes.GaugeDebtIncrement.temporalStage_debt_change_mem {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (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) (h : ℝ) (index : ℕ → ℕ) (axial : Plane × Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hop : LocalRankDefect.LocalOperators U.carrier c.operators) (hb : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) c.base) (hm : RegularTriple U a b u.mean) (hi : RegularTriple U a b (VariableGaugeMean.temporalIncrementState g h index axial c u)) (hW : ∀ (i j : Fin 3), Regular U a b (u.covariance i j)) {κ H : ℝ} (ho : MeanIncrementBounds.OperatorBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) c.operators κ) (hbC : MeanIncrementBounds.BaseBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) c.base) (hmC : MeanIncrementBounds.CumulativeBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) u.mean) (hiC : MeanIncrementBounds.IncrementBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) H (VariableGaugeMean.temporalIncrementState g h index axial c u)) (hH : 9 / 10 ≤ H) (hκ : 2 * κ ≤ 9 / 10) (i : Fin 3) : WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) H fun (n : ℕ) (x : LocalSignedRequest.Plane) => CorrectionState.debt c (VariableGaugeMean.temporalStageState g h index axial c u) n x i - CorrectionState.debt c u n x i

theorem NavierStokes.GaugeDebtIncrement.debt_mem_after_change (s : WeightedClasses.StripData Plane) (c : CorrectionState.Context Point) (u v : CorrectionState.State Point) {α β H : ℝ} (hα : H ≤ α) (hβ : H ≤ β) (hold : ∀ (i : Fin 3), WeightedClasses.UnweightedClass s α fun (n : ℕ) (x : Plane) => CorrectionState.debt c u n x i) (hchange : ∀ (i : Fin 3), WeightedClasses.UnweightedClass s β fun (n : ℕ) (x : Plane) => CorrectionState.debt c v n x i - CorrectionState.debt c u n x i) (i : Fin 3) : WeightedClasses.UnweightedClass s H fun (n : ℕ) (x : Plane) => CorrectionState.debt c v n x i

Old measured debt plus the proved actual change controls the next debt. The two input exponents may be weakened to a common requested exponent.

theorem NavierStokes.GaugeDebtIncrement.defectBounds_after_change (s : WeightedClasses.StripData Plane) (c : CorrectionState.Context Point) (u v : CorrectionState.State Point) {σ τ β : ℝ} (hσ : τ ≤ σ) (hβ : 1 + τ ≤ β) (hold : CorrectionState.DefectBounds s σ c u) (hchange : ∀ (i : Fin 3), WeightedClasses.UnweightedClass s β fun (n : ℕ) (x : Plane) => CorrectionState.debt c v n x i - CorrectionState.debt c u n x i) : CorrectionState.DefectBounds s τ c v

theorem NavierStokes.GaugeDebtIncrement.waveStage_debt_mem {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (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) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (w : CorrectionState.Oscillation Point) (q : CorrectionState.OscillatoryScalar Point) (gaussian : CorrectionState.Oscillation Point) (hop : LocalRankDefect.LocalOperators U.carrier c.operators) (hb : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) c.base) (hm : RegularTriple U a b u.mean) (hW : ∀ (i j : Fin 3), Regular U a b (u.covariance i j)) (hX : ∀ (i j : Fin 3), Regular U a b (SignedMeanGain.covarianceIncrement u.oscillation w i j)) {κ α : ℝ} (ho : MeanIncrementBounds.OperatorBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) c.operators κ) (hcX : SignedMeanGain.TensorClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α (SignedMeanGain.covarianceIncrement u.oscillation w)) {β : ℝ} (hβ : α - κ ≤ β) (hold : ∀ (i : Fin 3), WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) β fun (n : ℕ) (x : LocalSignedRequest.Plane) => CorrectionState.debt c u n x i) (i : Fin 3) : WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) (α - κ) fun (n : ℕ) (x : LocalSignedRequest.Plane) => CorrectionState.debt c (SignedMeanGain.waveStage g c u w q gaussian) n x i

theorem NavierStokes.GaugeDebtIncrement.waveStage_defectBounds {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (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) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (w : CorrectionState.Oscillation Point) (q : CorrectionState.OscillatoryScalar Point) (gaussian : CorrectionState.Oscillation Point) (hop : LocalRankDefect.LocalOperators U.carrier c.operators) (hb : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) c.base) (hm : RegularTriple U a b u.mean) (hW : ∀ (i j : Fin 3), Regular U a b (u.covariance i j)) (hX : ∀ (i j : Fin 3), Regular U a b (SignedMeanGain.covarianceIncrement u.oscillation w i j)) {κ α : ℝ} (ho : MeanIncrementBounds.OperatorBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) c.operators κ) (hcX : SignedMeanGain.TensorClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α (SignedMeanGain.covarianceIncrement u.oscillation w)) {σ τ : ℝ} (hσ : τ ≤ σ) (hτ : 1 + τ ≤ α - κ) (hold : CorrectionState.DefectBounds (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) σ c u) : CorrectionState.DefectBounds (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) τ c (SignedMeanGain.waveStage g c u w q gaussian)

theorem NavierStokes.GaugeDebtIncrement.temporalStage_debt_mem {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (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) (h : ℝ) (index : ℕ → ℕ) (axial : Plane × Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hop : LocalRankDefect.LocalOperators U.carrier c.operators) (hb : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) c.base) (hm : RegularTriple U a b u.mean) (hi : RegularTriple U a b (VariableGaugeMean.temporalIncrementState g h index axial c u)) (hW : ∀ (i j : Fin 3), Regular U a b (u.covariance i j)) {κ H : ℝ} (ho : MeanIncrementBounds.OperatorBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) c.operators κ) (hbC : MeanIncrementBounds.BaseBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) c.base) (hmC : MeanIncrementBounds.CumulativeBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) u.mean) (hiC : MeanIncrementBounds.IncrementBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) H (VariableGaugeMean.temporalIncrementState g h index axial c u)) (hH : 9 / 10 ≤ H) (hκ : 2 * κ ≤ 9 / 10) {β : ℝ} (hβ : H ≤ β) (hold : ∀ (i : Fin 3), WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) β fun (n : ℕ) (x : LocalSignedRequest.Plane) => CorrectionState.debt c u n x i) (i : Fin 3) : WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) H fun (n : ℕ) (x : LocalSignedRequest.Plane) => CorrectionState.debt c (VariableGaugeMean.temporalStageState g h index axial c u) n x i

theorem NavierStokes.GaugeDebtIncrement.temporalStage_defectBounds {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (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) (h : ℝ) (index : ℕ → ℕ) (axial : Plane × Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hop : LocalRankDefect.LocalOperators U.carrier c.operators) (hb : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) c.base) (hm : RegularTriple U a b u.mean) (hi : RegularTriple U a b (VariableGaugeMean.temporalIncrementState g h index axial c u)) (hW : ∀ (i j : Fin 3), Regular U a b (u.covariance i j)) {κ H : ℝ} (ho : MeanIncrementBounds.OperatorBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) c.operators κ) (hbC : MeanIncrementBounds.BaseBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) c.base) (hmC : MeanIncrementBounds.CumulativeBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) u.mean) (hiC : MeanIncrementBounds.IncrementBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) H (VariableGaugeMean.temporalIncrementState g h index axial c u)) (hH : 9 / 10 ≤ H) (hκ : 2 * κ ≤ 9 / 10) {σ τ : ℝ} (hσ : τ ≤ σ) (hτ : 1 + τ ≤ H) (hold : CorrectionState.DefectBounds (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) σ c u) : CorrectionState.DefectBounds (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) τ c (VariableGaugeMean.temporalStageState g h index axial c u)