The mean gain of the actual signed wave update

The state is updated with the same primary/signed native pulses and its pressure is recomputed by the moving-gauge operator. The removed physical bumps are controlled by actual moment identities; the complete covariance remainder retains the signed square and the curl terms.

@[reducible, inline]

abbrev NavierStokes.SignedMeanGain.ScalarField (D : Type) : Type

Scalar field: an abbreviation for MeanIncrementBounds.Field D.

Equations

• NavierStokes.SignedMeanGain.ScalarField D = NavierStokes.MeanIncrementBounds.Field D

@[reducible, inline]

abbrev NavierStokes.SignedMeanGain.Tensor (D : Type) : Type

Tensor: an abbreviation for Fin 3 → Fin 3 → ScalarField D.

Equations

• NavierStokes.SignedMeanGain.Tensor D = (Fin 3 → Fin 3 → NavierStokes.SignedMeanGain.ScalarField D)

noncomputable def NavierStokes.SignedMeanGain.thetaCovarianceChange {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : MeanIncrementBounds.Operators D) (X : Tensor D) : ScalarField D

These are changes of the literal covariance terms in (32).

Equations

• NavierStokes.SignedMeanGain.thetaCovarianceChange o X = o.radialDiv 2 (X 0 1) + o.dz (X 2 1)

noncomputable def NavierStokes.SignedMeanGain.axialCovarianceChange {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : MeanIncrementBounds.Operators D) (X : Tensor D) : ScalarField D

Axial covariance change, given by o.radialDiv 1 (X 0 2) + o.dz (X 2 2).

Equations

• NavierStokes.SignedMeanGain.axialCovarianceChange o X = o.radialDiv 1 (X 0 2) + o.dz (X 2 2)

noncomputable def NavierStokes.SignedMeanGain.radialCovarianceChange {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : MeanIncrementBounds.Operators D) (X : Tensor D) : ScalarField D

Radial covariance change, given by -o.radialDiv 1 (X 0 0) - o.dz (X 2 0) + o.invRadius * X 1 1.

Equations

• NavierStokes.SignedMeanGain.radialCovarianceChange o X = -o.radialDiv 1 (X 0 0) - o.dz (X 2 0) + o.invRadius * X 1 1

theorem NavierStokes.SignedMeanGain.smooth_updated {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {m h : MeanIncrementBounds.Triple D} (hm : MeanIncrementBounds.SmoothTriple U m) (hh : MeanIncrementBounds.SmoothTriple U h) : MeanIncrementBounds.SmoothTriple U (MeanIncrementBounds.updated m h)

theorem NavierStokes.SignedMeanGain.thetaResidual_covariance_change {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (o : MeanIncrementBounds.Operators D) {b m : MeanIncrementBounds.Triple D} (hb : MeanIncrementBounds.SmoothTriple U b) (hm : MeanIncrementBounds.SmoothTriple U m) (W X : Tensor D) (hW : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn U (W i j)) (hX : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn U (X i j)) (T : ScalarField D) : MeanIncrementBounds.Agree U (MeanIncrementBounds.thetaResidual o b m (W + X) T - MeanIncrementBounds.thetaResidual o b m W T) (thetaCovarianceChange o X)

theorem NavierStokes.SignedMeanGain.axialResidual_covariance_change {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (o : MeanIncrementBounds.Operators D) {b m : MeanIncrementBounds.Triple D} (hb : MeanIncrementBounds.SmoothTriple U b) (hm : MeanIncrementBounds.SmoothTriple U m) (W X : Tensor D) (hW : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn U (W i j)) (hX : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn U (X i j)) (p T : ScalarField D) (hp : MeanIncrementBounds.SmoothOn U p) : MeanIncrementBounds.Agree U (MeanIncrementBounds.axialResidual o b m (W + X) p T - MeanIncrementBounds.axialResidual o b m W p T) (axialCovarianceChange o X)

theorem NavierStokes.SignedMeanGain.gr_covariance_change {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (o : MeanIncrementBounds.Operators D) {b m : MeanIncrementBounds.Triple D} (hb : MeanIncrementBounds.SmoothTriple U b) (hm : MeanIncrementBounds.SmoothTriple U m) (W X : Tensor D) (hW : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn U (W i j)) (hX : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn U (X i j)) : MeanIncrementBounds.Agree U (MeanIncrementBounds.gr o b m (W + X) - MeanIncrementBounds.gr o b m W) (radialCovarianceChange o X)

def NavierStokes.SignedMeanGain.TensorClass {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (α : ℝ) (X : Tensor D) : Prop

A bound on each actual tensor entry. It is not a bound on the resulting residual and contains no update-preservation assertion.

Equations

• NavierStokes.SignedMeanGain.TensorClass s α X = ∀ (i j : Fin 3), NavierStokes.WeightedClasses.MeanClass s α (X i j)

theorem NavierStokes.SignedMeanGain.thetaCovarianceChange_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : MeanIncrementBounds.Operators D} {κ α : ℝ} (ho : MeanIncrementBounds.OperatorBounds s o κ) {X : Tensor D} (hX : TensorClass s α X) : WeightedClasses.MeanClass s (α - κ) (thetaCovarianceChange o X)

theorem NavierStokes.SignedMeanGain.axialCovarianceChange_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : MeanIncrementBounds.Operators D} {κ α : ℝ} (ho : MeanIncrementBounds.OperatorBounds s o κ) {X : Tensor D} (hX : TensorClass s α X) : WeightedClasses.MeanClass s (α - κ) (axialCovarianceChange o X)

theorem NavierStokes.SignedMeanGain.radialCovarianceChange_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : MeanIncrementBounds.Operators D} {κ α : ℝ} (ho : MeanIncrementBounds.OperatorBounds s o κ) {X : Tensor D} (hX : TensorClass s α X) : WeightedClasses.MeanClass s (α - κ) (radialCovarianceChange o X)

Literal state and covariance increments

noncomputable def NavierStokes.SignedMeanGain.zeroTriple {D : Type} : MeanIncrementBounds.Triple D

Zero triple, given by ⟨0, 0, 0⟩.

Equations

• NavierStokes.SignedMeanGain.zeroTriple = { radial := 0, angular := 0, axial := 0 }

theorem NavierStokes.SignedMeanGain.updated_zeroTriple {D : Type} (m : MeanIncrementBounds.Triple D) : MeanIncrementBounds.updated m zeroTriple = m

noncomputable def NavierStokes.SignedMeanGain.covarianceIncrement {D : Type} (u w : CorrectionState.Oscillation D) : Tensor D

Covariance increment, given by bilinearCovariance (u + w) (u + w) - bilinearCovariance u u.

Equations

• NavierStokes.SignedMeanGain.covarianceIncrement u w = NavierStokes.CorrectionState.bilinearCovariance (u + w) (u + w) - NavierStokes.CorrectionState.bilinearCovariance u u

theorem NavierStokes.SignedMeanGain.covariance_increment_split {D : Type} (p u t k : CorrectionState.Oscillation D) (hu : LabelSumBounds.AngularContinuous u) (ht : LabelSumBounds.AngularContinuous t) (hk : LabelSumBounds.AngularContinuous k) : covarianceIncrement u (t + k) = LabelSumBounds.symmetricCovariance p t + LabelSumBounds.signedRemainder p u t k

noncomputable def NavierStokes.SignedMeanGain.waveStage {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : VariableGaugeMean.GaugeData S) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) (w : CorrectionState.Oscillation (PressureStream.Lift S)) (q : CorrectionState.OscillatoryScalar (PressureStream.Lift S)) (gaussian : CorrectionState.Oscillation (PressureStream.Lift S)) : CorrectionState.State (PressureStream.Lift S)

Wave stage, given by VariableGaugeMean.reconstructState g c (u.addIncrement zeroTriple 0 w q ⟨0, gaussian, 0⟩).

Equations

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

noncomputable def NavierStokes.SignedMeanGain.pressureChange {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : VariableGaugeMean.GaugeData S) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) (w : CorrectionState.Oscillation (PressureStream.Lift S)) (q : CorrectionState.OscillatoryScalar (PressureStream.Lift S)) (gaussian : CorrectionState.Oscillation (PressureStream.Lift S)) : ScalarField (PressureStream.Lift S)

Pressure change, given by (waveStage g c u w q gaussian).pressure - u.pressure.

Equations

• NavierStokes.SignedMeanGain.pressureChange g c u w q gaussian = (NavierStokes.SignedMeanGain.waveStage g c u w q gaussian).pressure - u.pressure

theorem NavierStokes.SignedMeanGain.waveStage_mean {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : VariableGaugeMean.GaugeData S) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) (w : CorrectionState.Oscillation (PressureStream.Lift S)) (q : CorrectionState.OscillatoryScalar (PressureStream.Lift S)) (gaussian : CorrectionState.Oscillation (PressureStream.Lift S)) : (waveStage g c u w q gaussian).mean = u.mean

theorem NavierStokes.SignedMeanGain.waveStage_covariance {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : VariableGaugeMean.GaugeData S) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) (w : CorrectionState.Oscillation (PressureStream.Lift S)) (q : CorrectionState.OscillatoryScalar (PressureStream.Lift S)) (gaussian : CorrectionState.Oscillation (PressureStream.Lift S)) : (waveStage g c u w q gaussian).covariance = u.covariance + covarianceIncrement u.oscillation w

theorem NavierStokes.SignedMeanGain.waveStage_gaussian {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : VariableGaugeMean.GaugeData S) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) (w : CorrectionState.Oscillation (PressureStream.Lift S)) (q : CorrectionState.OscillatoryScalar (PressureStream.Lift S)) (gaussian : CorrectionState.Oscillation (PressureStream.Lift S)) : (waveStage g c u w q gaussian).errors.gaussian = u.errors.gaussian + gaussian

theorem NavierStokes.SignedMeanGain.waveStage_theta_change {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {U : Set (PressureStream.Lift S)} (hU : IsOpen U) (g : VariableGaugeMean.GaugeData S) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) (w : CorrectionState.Oscillation (PressureStream.Lift S)) (q : CorrectionState.OscillatoryScalar (PressureStream.Lift S)) (gaussian : CorrectionState.Oscillation (PressureStream.Lift S)) (hb : MeanIncrementBounds.SmoothTriple U c.base) (hm : MeanIncrementBounds.SmoothTriple U u.mean) (hW : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn U (u.covariance i j)) (hX : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn U (covarianceIncrement u.oscillation w i j)) : MeanIncrementBounds.Agree U ((waveStage g c u w q gaussian).thetaResidual c - u.thetaResidual c) (thetaCovarianceChange c.operators (covarianceIncrement u.oscillation w))

theorem NavierStokes.SignedMeanGain.waveStage_gr_change {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {U : Set (PressureStream.Lift S)} (hU : IsOpen U) (g : VariableGaugeMean.GaugeData S) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) (w : CorrectionState.Oscillation (PressureStream.Lift S)) (q : CorrectionState.OscillatoryScalar (PressureStream.Lift S)) (gaussian : CorrectionState.Oscillation (PressureStream.Lift S)) (hb : MeanIncrementBounds.SmoothTriple U c.base) (hm : MeanIncrementBounds.SmoothTriple U u.mean) (hW : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn U (u.covariance i j)) (hX : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn U (covarianceIncrement u.oscillation w i j)) : MeanIncrementBounds.Agree U ((waveStage g c u w q gaussian).gr c - u.gr c) (radialCovarianceChange c.operators (covarianceIncrement u.oscillation w))

theorem NavierStokes.SignedMeanGain.axialResidual_pressure_change {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (o : MeanIncrementBounds.Operators D) {b m : MeanIncrementBounds.Triple D} (hb : MeanIncrementBounds.SmoothTriple U b) (hm : MeanIncrementBounds.SmoothTriple U m) (W : Tensor D) (hW : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn U (W i j)) (p q T : ScalarField D) (hp : MeanIncrementBounds.SmoothOn U p) (hq : MeanIncrementBounds.SmoothOn U q) : MeanIncrementBounds.Agree U (MeanIncrementBounds.axialResidual o b m W (p + q) T - MeanIncrementBounds.axialResidual o b m W p T) (o.dz q)

theorem NavierStokes.SignedMeanGain.waveStage_axial_change {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {U : Set (PressureStream.Lift S)} (hU : IsOpen U) (g : VariableGaugeMean.GaugeData S) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) (w : CorrectionState.Oscillation (PressureStream.Lift S)) (q : CorrectionState.OscillatoryScalar (PressureStream.Lift S)) (e : CorrectionState.Oscillation (PressureStream.Lift S)) (hb : MeanIncrementBounds.SmoothTriple U c.base) (hm : MeanIncrementBounds.SmoothTriple U u.mean) (hW : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn U (u.covariance i j)) (hX : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn U (covarianceIncrement u.oscillation w i j)) (hp : MeanIncrementBounds.SmoothOn U u.pressure) (hδp : MeanIncrementBounds.SmoothOn U (pressureChange g c u w q e)) : MeanIncrementBounds.Agree U ((waveStage g c u w q e).axialResidual c - u.axialResidual c) (axialCovarianceChange c.operators (covarianceIncrement u.oscillation w) + c.operators.dz (pressureChange g c u w q e))

Averaging on the actual open slow domain

theorem NavierStokes.SignedMeanGain.torus_slice_continuous {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {U : Set S} {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) {x : ℝ × S} (hx : x.2 ∈ U) : Continuous fun (Y : PressureStream.Plane) => f (x.1, x.2, Y)

theorem NavierStokes.SignedMeanGain.meanBar_add_on {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {U : Set S} {f g : ScalarField (PressureStream.Lift S)} (hf : MeanIncrementBounds.SmoothOn (PhysicalMeanDomain.slowDomain U) f) (hg : MeanIncrementBounds.SmoothOn (PhysicalMeanDomain.slowDomain U) g) (n : ℕ) {x : PressureStream.Lift S} (hx : x.2.1 ∈ U) : StateMomentBalances.meanBar (f + g) n x = StateMomentBalances.meanBar f n x + StateMomentBalances.meanBar g n x

theorem NavierStokes.SignedMeanGain.meanBar_sub_on {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {U : Set S} {f g : ScalarField (PressureStream.Lift S)} (hf : MeanIncrementBounds.SmoothOn (PhysicalMeanDomain.slowDomain U) f) (hg : MeanIncrementBounds.SmoothOn (PhysicalMeanDomain.slowDomain U) g) (n : ℕ) {x : PressureStream.Lift S} (hx : x.2.1 ∈ U) : StateMomentBalances.meanBar (f - g) n x = StateMomentBalances.meanBar f n x - StateMomentBalances.meanBar g n x

theorem NavierStokes.SignedMeanGain.meanBar_radialDiv_on {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {U : Set S} (hU : IsOpen U) (o : MeanIncrementBounds.Operators (PressureStream.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 : ScalarField (PressureStream.Lift S)} (hf : MeanIncrementBounds.SmoothOn (PhysicalMeanDomain.slowDomain U) f) (hp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U (f n)) (e : ℝ) (n : ℕ) {x : PressureStream.Lift S} (hx : x.2.1 ∈ U) : StateMomentBalances.meanBar (o.radialDiv e f) n x = o.radialDiv e (StateMomentBalances.meanBar f) n x

theorem NavierStokes.SignedMeanGain.native_radialDiv_slow_on {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : CorrectionState.ReconstructionData) (ε fast : ℕ → ℝ) (z t : S) (v : PressureStream.Plane) {U : Set S} (hU : IsOpen U) {F : ℕ → ℝ × S → ℝ} (hF : MeanIncrementBounds.SmoothOn (PhysicalMeanDomain.slowDomain U) (StateMomentBalances.liftSlow F)) (e : ℝ) (n : ℕ) {x : PressureStream.Lift S} (hx : x.2.1 ∈ U) : (StateMomentBalances.nativeOperators r ε fast z t v).radialDiv e (StateMomentBalances.liftSlow F) n x = IntegratedMeanBalances.radialDivergence e (fun (q : ℝ) => F n (q, x.2.1)) x.1

Only a germ near the positive radius is used; no global extension of the physical stress or the slow domain is assumed.

Uniform estimates for the actual finite label sums

structure NavierStokes.SignedMeanGain.Assembly {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type} {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {α δ β η : ℝ} (f : LabelSumBounds.SignedFamily s P α δ β η) : Type

Primitive geometry of the active label assembly; the overlap estimate is derived by LabelSumBounds independently of the size of labels n.

• width : ℝ

  Width of Assembly, of type ℝ.

• exponent : ℝ

  Exponent of Assembly, of type ℝ.

• vr : TorusInverse.Plane

  Vr of Assembly, of type TorusInverse.Plane.

• vt : TorusInverse.Plane

  Vt of Assembly, of type TorusInverse.Plane.

• slots : PartitionedCovariance.SlotSystem self.width self.exponent self.vr self.vt

  Slots of Assembly, of type PartitionedCovariance.SlotSystem width exponent vr vt.

• labels : ℕ → Finset ι

  Label type of Assembly, of type ℕ → Finset ι.

• label : ℕ → ι → SlotColoring.Label

  Label of Assembly, of type ℕ → ι → SlotColoring.Label.

• injective (n : ℕ) : Set.InjOn (self.label n) ↑(self.labels n)
• level (n : ℕ) (l : ι) : l ∈ self.labels n → 1 ≤ (self.label n l).1
• window : ℕ → D → LabelSumBounds.WindowPoint

  Window of Assembly, of type ℕ → D → WindowPoint.

• window_continuous (n : ℕ) : ContinuousOn (self.window n) s.domain
• auxiliary : ℕ → D → TorusInverse.Plane

  Auxiliary of Assembly, of type ℕ → D → TorusInverse.Plane.

• primary_support : LabelSumBounds.SupportedOscillations self.slots self.label self.window self.auxiliary s.domain fun (l : ι) => (f.primary l).oscillation
• old_support : LabelSumBounds.SupportedOscillations self.slots self.label self.window self.auxiliary s.domain fun (l : ι) => (f.old l).oscillation
• tangent_support : LabelSumBounds.SupportedOscillations self.slots self.label self.window self.auxiliary s.domain fun (l : ι) => (f.tangent l).oscillation
• curl_support : LabelSumBounds.SupportedOscillations self.slots self.label self.window self.auxiliary s.domain fun (l : ι) => (f.curl l).oscillation

noncomputable def NavierStokes.SignedMeanGain.primaryField {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type} {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {α δ β η : ℝ} (f : LabelSumBounds.SignedFamily s P α δ β η) (a : Assembly f) : CorrectionState.Oscillation D

Primary field, given by fieldSum a.labels (fun l => (f.primary l).oscillation).

Equations

• NavierStokes.SignedMeanGain.primaryField f a = NavierStokes.LabelSumBounds.fieldSum a.labels fun (l : ι) => (f.primary l).oscillation

noncomputable def NavierStokes.SignedMeanGain.oldField {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type} {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {α δ β η : ℝ} (f : LabelSumBounds.SignedFamily s P α δ β η) (a : Assembly f) : CorrectionState.Oscillation D

Old field, given by fieldSum a.labels (fun l => (f.old l).oscillation).

Equations

• NavierStokes.SignedMeanGain.oldField f a = NavierStokes.LabelSumBounds.fieldSum a.labels fun (l : ι) => (f.old l).oscillation

noncomputable def NavierStokes.SignedMeanGain.tangentField {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type} {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {α δ β η : ℝ} (f : LabelSumBounds.SignedFamily s P α δ β η) (a : Assembly f) : CorrectionState.Oscillation D

Tangent field, given by fieldSum a.labels (fun l => (f.tangent l).oscillation).

Equations

• NavierStokes.SignedMeanGain.tangentField f a = NavierStokes.LabelSumBounds.fieldSum a.labels fun (l : ι) => (f.tangent l).oscillation

noncomputable def NavierStokes.SignedMeanGain.curlField {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type} {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {α δ β η : ℝ} (f : LabelSumBounds.SignedFamily s P α δ β η) (a : Assembly f) : CorrectionState.Oscillation D

Curl field, given by fieldSum a.labels (fun l => (f.curl l).oscillation).

Equations

• NavierStokes.SignedMeanGain.curlField f a = NavierStokes.LabelSumBounds.fieldSum a.labels fun (l : ι) => (f.curl l).oscillation

noncomputable def NavierStokes.SignedMeanGain.remainderTensor {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type} {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {α δ β η : ℝ} (f : LabelSumBounds.SignedFamily s P α δ β η) (a : Assembly f) : Tensor D

Remainder tensor, given by signedRemainder (primaryField f a) (oldField f a) (tangentField f a) (curlField f a).

Equations

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

noncomputable def NavierStokes.SignedMeanGain.crossTensor {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type} {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {α δ β η : ℝ} (f : LabelSumBounds.SignedFamily s P α δ β η) (a : Assembly f) : Tensor D

Cross tensor, given by symmetricCovariance (primaryField f a) (tangentField f a).

Equations

• NavierStokes.SignedMeanGain.crossTensor f a = NavierStokes.LabelSumBounds.symmetricCovariance (NavierStokes.SignedMeanGain.primaryField f a) (NavierStokes.SignedMeanGain.tangentField f a)

noncomputable def NavierStokes.SignedMeanGain.incrementTensor {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type} {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {α δ β η : ℝ} (f : LabelSumBounds.SignedFamily s P α δ β η) (a : Assembly f) : Tensor D

Increment tensor, given by covarianceIncrement (oldField f a) (tangentField f a + curlField f a).

Equations

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

theorem NavierStokes.SignedMeanGain.incrementTensor_split {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type} {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {α δ β η : ℝ} (f : LabelSumBounds.SignedFamily s P α δ β η) (a : Assembly f) : incrementTensor f a = crossTensor f a + remainderTensor f a

theorem NavierStokes.SignedMeanGain.remainderTensor_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type} {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {α δ β η : ℝ} (f : LabelSumBounds.SignedFamily s P α δ β η) (a : Assembly f) {γ : ℝ} (hβη : β ≤ η) (hγd : γ ≤ δ + β) (hγc : γ ≤ α + η) (hγs : γ ≤ 2 * β) : TensorClass s γ (remainderTensor f a)

theorem NavierStokes.SignedMeanGain.incrementTensor_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type} {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {α δ β η : ℝ} (f : LabelSumBounds.SignedFamily s P α δ β η) (a : Assembly f) (hαβ : α ≤ β) (hβη : β ≤ η) : TensorClass s (α + β) (incrementTensor f a)

theorem NavierStokes.SignedMeanGain.signed_tensor_bounds {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type} {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {σ κ : ℝ} (hσ : 1 / 5 ≤ σ) (hκsmall : κ ≤ 1 / 100000) (f : LabelSumBounds.SignedFamily s P (1 / 2) (17 / 25) (1 / 2 + σ - κ) (1 + σ - 2 * κ)) (a : Assembly f) : TensorClass s (1 + σ - κ) (incrementTensor f a) ∧ TensorClass s (1 + σ + 17 / 100 + κ) (remainderTensor f a)

The exact native cross, for the physical moving-gauge request

theorem NavierStokes.SignedMeanGain.nativeTangentBlock_zero {d h : ℝ} {vr vt : TorusInverse.Plane} {sys : PartitionedCovariance.SlotSystem d h vr vt} {l : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys l) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (a : SignedWaveUpdate.Vec2) (q : ℝ) (x : SlotColoring.Position) (j : Fin 2) (hm : PartitionedCovariance.mask d l q x = 0) (Y : TorusInverse.Plane) (θ : ℝ) (i : Fin 3) : (SignedWaveUpdate.nativeTangentBlock P hdet outer ε a q x j).oscillation 0 (Y, θ) i = 0

theorem NavierStokes.SignedMeanGain.nativeAssembly_eq_finite {d h : ℝ} {vr vt : TorusInverse.Plane} {sys : PartitionedCovariance.SlotSystem d h vr vt} {N : ℕ} (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (a : PartitionedCovariance.UnsignedLabel → SignedWaveUpdate.Vec2) (q : ℝ) (x : SlotColoring.Position) (F : Finset (PartitionedCovariance.UnsignedLabel × Fin 2)) (hF : ∀ l ∉ F, PartitionedCovariance.mask d (PartitionedCovariance.tailLabel N l.1) q x = 0) (Y : TorusInverse.Plane) (θ : ℝ) (i : Fin 3) : SignedWaveUpdate.nativeAssembly P hdet outer ε a q x Y θ i = ∑ l ∈ F, (SignedWaveUpdate.nativeTangentBlock (P l.1) hdet (outer l.1) (ε l.1) (a l.1) q x l.2).oscillation 0 (Y, θ) i

theorem NavierStokes.SignedMeanGain.native_physical_cross {d h : ℝ} {vr vt : TorusInverse.Plane} {sys : PartitionedCovariance.SlotSystem d h vr vt} (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (N : ℕ) (hN : 1 ≤ N) (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) {q : ℝ} (hq : 0 < q) (hqN : q ≤ ChartScales.Q N) (x : SlotColoring.Position) (T σ : SignedWaveUpdate.Vec2) (hcone : ∀ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask d (PartitionedCovariance.tailLabel N U) q x ≠ 0 → SmoothCovariance.StrictCone (P U).matrix (PartitionedCovariance.chartTarget h q N T U)) (i : Fin 2) : have primary := SignedWaveUpdate.nativeAssembly P hdet (PartitionedCovariance.physicalOuter h N) (PartitionedCovariance.physicalViscosity h N) (fun (U : PartitionedCovariance.UnsignedLabel) => SmoothCovariance.amplitudes (P U).matrix (PartitionedCovariance.chartTarget h q N T U)) q x; have signed := SignedWaveUpdate.nativeAssembly P hdet (PartitionedCovariance.physicalOuter h N) (PartitionedCovariance.physicalViscosity h N) (fun (U : PartitionedCovariance.UnsignedLabel) => SignedCovariance.increment (P U).matrix (PartitionedCovariance.chartTarget h q N T U) (SignedCovariance.chartStress h N σ U)) q x; (PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (θ : ℝ) => primary Y θ 0 * signed Y θ i.succ + signed Y θ 0 * primary Y θ i.succ) = σ i

One moving chart and its measured debts

@[reducible, inline]

abbrev NavierStokes.SignedMeanGain.Point : Type

Point: an abbreviation for LocalSignedRequest.Point.

Equations

• NavierStokes.SignedMeanGain.Point = NavierStokes.LocalSignedRequest.Point

@[reducible, inline]

abbrev NavierStokes.SignedMeanGain.Plane : Type

Plane: an abbreviation for PressureStream.Plane.

Equations

• NavierStokes.SignedMeanGain.Plane = NavierStokes.PressureStream.Plane

structure NavierStokes.SignedMeanGain.Geometry : Type

Geometry data, collecting coord, region, patch, leftWeight, rightWeight, left_pos and their compatibility conditions.

• coord : ℝ

  Coord of Geometry, of type ℝ.

• region : LocalSignedRequest.SlowRegion self.coord

  Region of Geometry, of type LocalSignedRequest.SlowRegion coord.

• patch : SignedStressPrimitive.Patch

  Patch of Geometry, of type SignedStressPrimitive.Patch.

• leftWeight : ℝ

  Left weight of Geometry, of type ℝ.

• rightWeight : ℝ

  Right weight of Geometry, of type ℝ.

• left_pos : 0 < self.leftWeight
• right_pos : 0 < self.rightWeight
• epsilon : ℕ → ℝ

  Epsilon of Geometry, of type ℕ → ℝ.

• slow : ℕ → ℝ

  Slow of Geometry, of type ℕ → ℝ.

• epsilon_pos (n : ℕ) : 0 < self.epsilon n
• epsilon_le_one (n : ℕ) : self.epsilon n ≤ 1
• slow_ge_one (n : ℕ) : 1 ≤ self.slow n
• gauge : VariableGaugeMean.GaugeData Plane

  Gauge of Geometry, of type VariableGaugeMean.GaugeData Plane.

• inner_eq : self.gauge.radial.inner = self.patch.a
• outer_eq : self.gauge.radial.outer = self.patch.b
• exponent_pos : 0 < self.gauge.radial.exponent
• length_eq (n : ℕ) : self.gauge.length n = VariableGaugeMean.qLength self.coord
• fast : ℕ → ℝ

  Fast of Geometry, of type ℕ → ℝ.

• axial : Plane

  Axial of Geometry, of type Plane.

• time : Plane

  Time of Geometry, of type Plane.

• temporal : Plane

  Temporal of Geometry, of type Plane.

noncomputable def NavierStokes.SignedMeanGain.Geometry.strip (G : Geometry) : WeightedClasses.StripData Point

Strip, constructed using LocalSignedRequest.movingStripData.

Equations

• G.strip = NavierStokes.LocalSignedRequest.movingStripData G.region G.patch.a G.patch.b G.leftWeight G.rightWeight ⋯ ⋯ ⋯ G.epsilon G.slow ⋯ ⋯ ⋯

noncomputable def NavierStokes.SignedMeanGain.Geometry.slowStrip (G : Geometry) : WeightedClasses.StripData Plane

Slow strip, constructed using PhysicalMeanDomain.localSlowStripData.

Equations

• G.slowStrip = NavierStokes.PhysicalMeanDomain.localSlowStripData G.region.carrier ⋯ G.epsilon G.slow ⋯ ⋯ ⋯

noncomputable def NavierStokes.SignedMeanGain.Geometry.domain (G : Geometry) : Set Point

Domain, given by PhysicalMeanDomain.slowDomain G.region.carrier.

Equations

• G.domain = NavierStokes.PhysicalMeanDomain.slowDomain G.region.carrier

noncomputable def NavierStokes.SignedMeanGain.Geometry.operators (G : Geometry) : MeanIncrementBounds.Operators Point

Operators, given by StateMomentBalances.nativeOperators G.gauge.radial G.epsilon G.fast G.axial G.time G.temporal.

Equations

• G.operators = NavierStokes.StateMomentBalances.nativeOperators G.gauge.radial G.epsilon G.fast G.axial G.time G.temporal

theorem NavierStokes.SignedMeanGain.Geometry.inner_pos (G : Geometry) : 0 < G.gauge.radial.inner

theorem NavierStokes.SignedMeanGain.Geometry.domain_open (G : Geometry) : IsOpen G.domain

theorem NavierStokes.SignedMeanGain.Geometry.strip_subset (G : Geometry) : G.strip.domain ⊆ G.domain

theorem NavierStokes.SignedMeanGain.Geometry.strip_fiber (G : Geometry) {x : Point} (hx : x ∈ G.strip.domain) (Y : Plane) : (x.1, x.2.1, Y) ∈ G.strip.domain

theorem NavierStokes.SignedMeanGain.Geometry.strip_radius_pos (G : Geometry) {x : Point} (hx : x ∈ G.strip.domain) : 0 < x.1

theorem NavierStokes.SignedMeanGain.Geometry.local_operators (G : Geometry) : LocalRankDefect.LocalOperators G.region.carrier G.operators

theorem NavierStokes.SignedMeanGain.Geometry.average_mem (G : Geometry) {α : ℝ} {f : ScalarField Point} (hf : MeanIncrementBounds.SmoothOn G.domain f) (hclass : WeightedClasses.MeanClass G.strip α f) : WeightedClasses.MeanClass G.strip α (StateMomentBalances.meanBar f)

theorem NavierStokes.SignedMeanGain.Geometry.average_congr (G : Geometry) {f g : ScalarField Point} (he : MeanIncrementBounds.Agree G.strip.domain f g) : MeanIncrementBounds.Agree G.strip.domain (StateMomentBalances.meanBar f) (StateMomentBalances.meanBar g)

theorem NavierStokes.SignedMeanGain.Geometry.slowClass_lift (G : Geometry) {α : ℝ} {f : ℕ → Plane → ℝ} (hf : WeightedClasses.UnweightedClass G.slowStrip α f) : WeightedClasses.UnweightedClass G.strip α fun (n : ℕ) (x : Point) => f n x.2.1

The actual slow jet bound lifts through the norm-one slow projection.

def NavierStokes.SignedMeanGain.MovingField (G : Geometry) (f : ScalarField Point) : Prop

Regularity is imposed on actual fluxes, before any class estimate on their derivatives is derived.

Equations

• NavierStokes.SignedMeanGain.MovingField G f = NavierStokes.GaugeMomentBalances.MovingField G.region G.patch.a G.patch.b f

theorem NavierStokes.SignedMeanGain.MovingField.sub {G : Geometry} {f g : ScalarField Point} (hf : MovingField G f) (hg : MovingField G g) : MovingField G (f - g)

theorem NavierStokes.SignedMeanGain.MovingField.covariance_flux_smooth {G : Geometry} {X : Tensor Point} (hX : ∀ (i j : Fin 3), MovingField G (X i j)) : MeanIncrementBounds.SmoothOn G.domain (thetaCovarianceChange G.operators X) ∧ MeanIncrementBounds.SmoothOn G.domain (axialCovarianceChange G.operators X) ∧ MeanIncrementBounds.SmoothOn G.domain (radialCovarianceChange G.operators X)

Actual pressure recomputation and the physical cancellation

noncomputable def NavierStokes.SignedMeanGain.physicalSigma (G : Geometry) (e : ℕ) (f : ScalarField Point) : ScalarField Point

Physical sigma, defined pointwise by SignedStressPrimitive.physicalBarSigma G.patch e (SimilarityCoordinates.coordinateQ G.coord) (f n) (x.1, x.2.1).

Equations

• NavierStokes.SignedMeanGain.physicalSigma G e f n x = NavierStokes.SignedStressPrimitive.physicalBarSigma G.patch e (NavierStokes.SimilarityCoordinates.coordinateQ G.coord) (f n) (x.1, x.2.1)

noncomputable def NavierStokes.SignedMeanGain.removedBump (G : Geometry) (e : ℕ) (f : ScalarField Point) : ScalarField Point

Removed bump as an element of ScalarField Point.

Equations

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

theorem NavierStokes.SignedMeanGain.radialDiv_congr {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (o : MeanIncrementBounds.Operators D) (e : ℝ) {f g : ScalarField D} (he : MeanIncrementBounds.Agree U f g) : MeanIncrementBounds.Agree U (o.radialDiv e f) (o.radialDiv e g)

theorem NavierStokes.SignedMeanGain.pressureChange_mem (G : Geometry) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (w : CorrectionState.Oscillation Point) (q : CorrectionState.OscillatoryScalar Point) (gaussian : CorrectionState.Oscillation Point) (hfixed : VariableGaugeMean.reconstructState G.gauge c u = u) (h0 : MovingField G (u.gr c)) (h1 : MovingField G ((waveStage G.gauge c u w q gaussian).gr c)) {α : ℝ} (hclass : WeightedClasses.MeanClass G.strip α ((waveStage G.gauge c u w q gaussian).gr c - u.gr c)) : WeightedClasses.MeanClass G.strip α (pressureChange G.gauge c u w q gaussian)

theorem NavierStokes.SignedMeanGain.physicalSigma_smooth (G : Geometry) (e : ℕ) {f : ScalarField Point} (hf : MeanIncrementBounds.SmoothOn G.domain f) (hs : ∀ (n : ℕ), LocalSignedRequest.MovingSupport G.patch.a G.patch.b G.coord G.region.carrier (f n)) : MeanIncrementBounds.SmoothOn G.domain (physicalSigma G e f)

theorem NavierStokes.SignedMeanGain.physicalSigma_cancels (G : Geometry) (e : ℕ) (he : e = 2 ∨ e = 1) {f : ScalarField Point} (hf : MeanIncrementBounds.SmoothOn G.domain f) (hs : ∀ (n : ℕ), LocalSignedRequest.MovingSupport G.patch.a G.patch.b G.coord G.region.carrier (f n)) (n : ℕ) {x : Point} (hx : x ∈ G.strip.domain) : StateMomentBalances.meanBar f n x + G.operators.radialDiv (↑e) (physicalSigma G e f) n x = removedBump G e f n x

theorem NavierStokes.SignedMeanGain.cross_cancels (G : Geometry) (e : ℕ) (he : e = 2 ∨ e = 1) {f X : ScalarField Point} (hf : MeanIncrementBounds.SmoothOn G.domain f) (hs : ∀ (n : ℕ), LocalSignedRequest.MovingSupport G.patch.a G.patch.b G.coord G.region.carrier (f n)) (hX : MovingField G X) (hcross : MeanIncrementBounds.Agree G.strip.domain (StateMomentBalances.meanBar X) (physicalSigma G e f)) (n : ℕ) {x : Point} (hx : x ∈ G.strip.domain) : StateMomentBalances.meanBar f n x + StateMomentBalances.meanBar (G.operators.radialDiv (↑e) X) n x = removedBump G e f n x

theorem NavierStokes.SignedMeanGain.Geometry.removed_bumps_mem (G : Geometry) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) {α : ℝ} (ho : c.operators = G.operators) (Hθ : GaugeMomentBalances.MovingAngularInputs G.region G.patch.a G.patch.b c u) (Hz : GaugeMomentBalances.MovingAxialInputs G.region G.patch.a G.patch.b c u) (hr : MovingField G (u.gr c)) (hfixed : VariableGaugeMean.reconstructState G.gauge c u = u) (hmθ : ∀ (n : ℕ), ∀ z ∈ G.region.carrier, CorrectionState.radialMoment 2 u.mean.angular n z = 0) (hmz : ∀ (n : ℕ), ∀ z ∈ G.region.carrier, CorrectionState.radialMoment 1 u.mean.axial n z = 0) (hD : ∀ (i : Fin 3), WeightedClasses.UnweightedClass G.slowStrip α fun (n : ℕ) (z : Plane) => CorrectionState.debt c u n z i) : WeightedClasses.MeanClass G.strip (α + 1) (removedBump G 2 (u.thetaResidual c)) ∧ WeightedClasses.MeanClass G.strip (α + 1) (removedBump G 1 (u.axialResidual c))

The literal averaged residual after the update

noncomputable def NavierStokes.SignedMeanGain.thetaRemainderField (G : Geometry) (S E : Tensor Point) : ScalarField Point

Theta remainder field, given by thetaCovarianceChange G.operators E + G.operators.dz (S 2 1).

Equations

• NavierStokes.SignedMeanGain.thetaRemainderField G S E = NavierStokes.SignedMeanGain.thetaCovarianceChange G.operators E + G.operators.dz (S 2 1)

noncomputable def NavierStokes.SignedMeanGain.axialRemainderField (G : Geometry) (S E : Tensor Point) (p : ScalarField Point) : ScalarField Point

Axial remainder field, given by axialCovarianceChange G.operators E + G.operators.dz (S 2 2) + G.operators.dz p.

Equations

• NavierStokes.SignedMeanGain.axialRemainderField G S E p = NavierStokes.SignedMeanGain.axialCovarianceChange G.operators E + G.operators.dz (S 2 2) + G.operators.dz p

structure NavierStokes.SignedMeanGain.LocalData (G : Geometry) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (w : CorrectionState.Oscillation Point) (q : CorrectionState.OscillatoryScalar Point) (gaussian : CorrectionState.Oscillation Point) : Prop

These hypotheses concern local regularity and the actual incoming state. None is a bound or a cancellation assertion about the updated residual.

• operators_eq : c.operators = G.operators
• base : MeanIncrementBounds.SmoothTriple G.strip.domain c.base
• mean : MeanIncrementBounds.SmoothTriple G.strip.domain u.mean
• covariance (i j : Fin 3) : MeanIncrementBounds.SmoothOn G.strip.domain (u.covariance i j)
• theta : MeanIncrementBounds.SmoothOn G.domain (u.thetaResidual c)
• axial : MeanIncrementBounds.SmoothOn G.domain (u.axialResidual c)
• theta_support (n : ℕ) : LocalSignedRequest.MovingSupport G.patch.a G.patch.b G.coord G.region.carrier (u.thetaResidual c n)
• axial_support (n : ℕ) : LocalSignedRequest.MovingSupport G.patch.a G.patch.b G.coord G.region.carrier (u.axialResidual c n)
• angular_flux : GaugeMomentBalances.MovingAngularInputs G.region G.patch.a G.patch.b c u
• axial_flux : GaugeMomentBalances.MovingAxialInputs G.region G.patch.a G.patch.b c u
• source : MovingField G (u.gr c)
• updated_source : MovingField G ((waveStage G.gauge c u w q gaussian).gr c)
• reconstructed : VariableGaugeMean.reconstructState G.gauge c u = u
• angular_mass (n : ℕ) (z : LocalSignedRequest.Plane) : z ∈ G.region.carrier → CorrectionState.radialMoment 2 u.mean.angular n z = 0
• axial_mass (n : ℕ) (z : LocalSignedRequest.Plane) : z ∈ G.region.carrier → CorrectionState.radialMoment 1 u.mean.axial n z = 0

theorem NavierStokes.SignedMeanGain.LocalData.pressure_smooth {G : Geometry} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} {w : CorrectionState.Oscillation Point} {q : CorrectionState.OscillatoryScalar Point} {gaussian : CorrectionState.Oscillation Point} (H : LocalData G c u w q gaussian) : MeanIncrementBounds.SmoothOn G.domain u.pressure

theorem NavierStokes.SignedMeanGain.LocalData.pressureChange_smooth {G : Geometry} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} {w : CorrectionState.Oscillation Point} {q : CorrectionState.OscillatoryScalar Point} {gaussian : CorrectionState.Oscillation Point} (H : LocalData G c u w q gaussian) : MeanIncrementBounds.SmoothOn G.domain (pressureChange G.gauge c u w q gaussian)

theorem NavierStokes.SignedMeanGain.LocalData.pressureChange_mem {G : Geometry} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} {w : CorrectionState.Oscillation Point} {q : CorrectionState.OscillatoryScalar Point} {gaussian : CorrectionState.Oscillation Point} (H : LocalData G c u w q gaussian) {α κ : ℝ} (ho : MeanIncrementBounds.OperatorBounds G.strip G.operators κ) (hX : TensorClass G.strip α (covarianceIncrement u.oscillation w)) : WeightedClasses.MeanClass G.strip (α - κ) (pressureChange G.gauge c u w q gaussian)

theorem NavierStokes.SignedMeanGain.LocalData.theta_split {G : Geometry} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} {w : CorrectionState.Oscillation Point} {q : CorrectionState.OscillatoryScalar Point} {gaussian : CorrectionState.Oscillation Point} (H : LocalData G c u w q gaussian) {S E : Tensor Point} (hS : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn G.strip.domain (S i j)) (hE : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn G.strip.domain (E i j)) (hX : covarianceIncrement u.oscillation w = S + E) : MeanIncrementBounds.Agree G.strip.domain ((waveStage G.gauge c u w q gaussian).thetaResidual c) (u.thetaResidual c + G.operators.radialDiv 2 (S 0 1) + thetaRemainderField G S E)

theorem NavierStokes.SignedMeanGain.LocalData.axial_split {G : Geometry} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} {w : CorrectionState.Oscillation Point} {q : CorrectionState.OscillatoryScalar Point} {gaussian : CorrectionState.Oscillation Point} (H : LocalData G c u w q gaussian) {S E : Tensor Point} (hS : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn G.strip.domain (S i j)) (hE : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn G.strip.domain (E i j)) (hX : covarianceIncrement u.oscillation w = S + E) : MeanIncrementBounds.Agree G.strip.domain ((waveStage G.gauge c u w q gaussian).axialResidual c) (u.axialResidual c + G.operators.radialDiv 1 (S 0 2) + axialRemainderField G S E (pressureChange G.gauge c u w q gaussian))

theorem NavierStokes.SignedMeanGain.averaged_residual_decomposition (G : Geometry) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (w : CorrectionState.Oscillation Point) (q : CorrectionState.OscillatoryScalar Point) (gaussian : CorrectionState.Oscillation Point) (H : LocalData G c u w q gaussian) (S E : Tensor Point) (hS : ∀ (i j : Fin 3), MovingField G (S i j)) (hE : ∀ (i j : Fin 3), MovingField G (E i j)) (hX : covarianceIncrement u.oscillation w = S + E) (hcrossθ : MeanIncrementBounds.Agree G.strip.domain (StateMomentBalances.meanBar (S 0 1)) (physicalSigma G 2 (u.thetaResidual c))) (hcrossz : MeanIncrementBounds.Agree G.strip.domain (StateMomentBalances.meanBar (S 0 2)) (physicalSigma G 1 (u.axialResidual c))) : MeanIncrementBounds.Agree G.strip.domain (StateMomentBalances.meanBar ((waveStage G.gauge c u w q gaussian).thetaResidual c)) (removedBump G 2 (u.thetaResidual c) + StateMomentBalances.meanBar (thetaRemainderField G S E)) ∧ MeanIncrementBounds.Agree G.strip.domain (StateMomentBalances.meanBar ((waveStage G.gauge c u w q gaussian).axialResidual c)) (removedBump G 1 (u.axialResidual c) + StateMomentBalances.meanBar (axialRemainderField G S E (pressureChange G.gauge c u w q gaussian)))

A direct identity for the torus average: the radial primary cross cancels the adjusted old residual. The axial cross flux and pressure change are displayed explicitly in the remaining term.

Quantitative mean gain

theorem NavierStokes.SignedMeanGain.signed_mean_gain_of_cross (G : Geometry) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) {ι : Type} {P : ι → ℕ → Point → ℝ} {σ κ : ℝ} (hσ : 1 / 5 ≤ σ) (hκ : 0 ≤ κ) (hκsmall : κ ≤ 1 / 100000) (f : LabelSumBounds.SignedFamily G.strip P (1 / 2) (17 / 25) (1 / 2 + σ - κ) (1 + σ - 2 * κ)) (a : Assembly f) (q : CorrectionState.OscillatoryScalar Point) (gaussian : CorrectionState.Oscillation Point) (hold : u.oscillation = oldField f a) (H : LocalData G c u (tangentField f a + curlField f a) q gaussian) (ho : MeanIncrementBounds.OperatorBounds G.strip G.operators κ) (hX : ∀ (i j : Fin 3), MovingField G (incrementTensor f a i j)) (hS : ∀ (i j : Fin 3), MovingField G (crossTensor f a i j)) (hθ : WeightedClasses.MeanClass G.strip (1 + σ - κ) (u.thetaResidual c)) (hz : WeightedClasses.MeanClass G.strip (1 + σ - κ) (u.axialResidual c)) (hd : CorrectionState.DefectBounds G.slowStrip (σ - κ) c u) (hcrossθ : MeanIncrementBounds.Agree G.strip.domain (StateMomentBalances.meanBar (crossTensor f a 0 1)) (physicalSigma G 2 (u.thetaResidual c))) (hcrossz : MeanIncrementBounds.Agree G.strip.domain (StateMomentBalances.meanBar (crossTensor f a 0 2)) (physicalSigma G 1 (u.axialResidual c))) : have v := waveStage G.gauge c u (tangentField f a + curlField f a) q gaussian; WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ) (v.thetaResidual c) ∧ WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ) (v.axialResidual c) ∧ WeightedClasses.MeanClass G.strip (1 + σ + 17 / 100) (StateMomentBalances.meanBar (v.thetaResidual c)) ∧ WeightedClasses.MeanClass G.strip (1 + σ + 17 / 100) (StateMomentBalances.meanBar (v.axialResidual c))

This intermediate estimate isolates the two exact cross identities. The native theorem below discharges them by the signed inverse construction.

A shared native construction, before any signed output is known

@[reducible, inline]

abbrev NavierStokes.SignedMeanGain.NativeIndex : Type

Native index: an abbreviation for PartitionedCovariance.UnsignedLabel × Fin 2.

Equations

• NavierStokes.SignedMeanGain.NativeIndex = (NavierStokes.PartitionedCovariance.UnsignedLabel × Fin 2)

structure NavierStokes.SignedMeanGain.NativeData (G : Geometry) : Type

All matches concern the common matrix, unit fundamental, mask and carrier. The signed coefficient is constructed below from the measured physical request, not included as a realization hypothesis.

• width : ℝ

  Width of NativeData, of type ℝ.

• exponent : ℝ

  Exponent of NativeData, of type ℝ.

• vr : Plane

  Vr of NativeData, of type Plane.

• vt : Plane

  Vt of NativeData, of type Plane.

• slots : PartitionedCovariance.SlotSystem self.width self.exponent self.vr self.vt

  Slots of NativeData, of type PartitionedCovariance.SlotSystem width exponent vr vt.

• determinant : self.vr.1 * self.vt.2 - self.vr.2 * self.vt.1 ≠ 0
• index : ℕ → ℕ

  Index of NativeData, of type ℕ → ℕ.

• index_pos (n : ℕ) : 1 ≤ self.index n
• pairs (n : ℕ) : ℝ × Plane → (l : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData self.slots (PartitionedCovariance.tailLabel (self.index n) l)

  Pairs supplied by NativeData.

• position : ℕ → ℝ × Plane → SlotColoring.Position

  Position of NativeData, of type ℕ → (ℝ × Plane) → SlotColoring.Position.

• modelTarget : ℕ → ℝ × Plane → SignedWaveUpdate.Vec2

  Model target of NativeData, of type ℕ → (ℝ × Plane) → SignedWaveUpdate.Vec2.

• matrix : PartitionedCovariance.UnsignedLabel → ℕ → Point → SignedWaveUpdate.Mat2

  Matrix of NativeData, of type PartitionedCovariance.UnsignedLabel → ℕ → Point → SignedWaveUpdate.Mat2.

• target : PartitionedCovariance.UnsignedLabel → ℕ → Point → SignedWaveUpdate.Vec2

  Target of NativeData, of type PartitionedCovariance.UnsignedLabel → ℕ → Point → SignedWaveUpdate.Vec2.

• mask : PartitionedCovariance.UnsignedLabel → ℕ → Point → ℝ

  Mask of NativeData, of type PartitionedCovariance.UnsignedLabel → ℕ → Point → ℝ.

• unit : NativeIndex → ℕ → Point → SignedWaveUpdate.Space

  Unit of NativeData, of type NativeIndex → ℕ → Point → SignedWaveUpdate.Space.

• frequency : NativeIndex → ℕ → ℝ

  Frequency of NativeData, of type NativeIndex → ℕ → ℝ.

• phase : NativeIndex → ℕ → Point → ℝ

  Phase of NativeData, of type NativeIndex → ℕ → Point → ℝ.

• angular : NativeIndex → ℕ → ℤ

  Angular of NativeData, of type NativeIndex → ℕ → ℤ.

• matrix_match (l : PartitionedCovariance.UnsignedLabel) (n : ℕ) (x : Point) : x ∈ G.strip.domain → self.matrix l n x = (self.pairs n (x.1, x.2.1) l).matrix
• target_match (l : PartitionedCovariance.UnsignedLabel) (n : ℕ) (x : Point) : x ∈ G.strip.domain → self.target l n x = PartitionedCovariance.chartTarget self.exponent (SimilarityCoordinates.coordinateQ G.coord x.2.1) (self.index n) (self.modelTarget n (x.1, x.2.1)) l
• mask_match (l : PartitionedCovariance.UnsignedLabel) (n : ℕ) (x : Point) : x ∈ G.strip.domain → self.mask l n x = PartitionedCovariance.mask self.width (PartitionedCovariance.tailLabel (self.index n) l) (SimilarityCoordinates.coordinateQ G.coord x.2.1) (self.position n (x.1, x.2.1))
• unit_match (l : NativeIndex) (n : ℕ) (x : Point) : x ∈ G.strip.domain → self.unit l n x = SignedWaveUpdate.nativeUnit (self.pairs n (x.1, x.2.1) l.1) ⋯ l.2 x.2.2
• phase_match (l : NativeIndex) (n : ℕ) (x : Point) : x ∈ G.strip.domain → self.frequency l n * self.phase l n x = (self.pairs n (x.1, x.2.1) l.1).phases l.2 x.2.2
• angular_match (l : NativeIndex) (n : ℕ) (x : Point) : x ∈ G.strip.domain → self.angular l n = (self.pairs n (x.1, x.2.1) l.1).modes l.2
• tail_bound (n : ℕ) (x : Point) : x ∈ G.strip.domain → SimilarityCoordinates.coordinateQ G.coord x.2.1 ≤ ChartScales.Q (self.index n)
• cone (n : ℕ) (x : Point) : x ∈ G.strip.domain → ∀ (l : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask self.width (PartitionedCovariance.tailLabel (self.index n) l) (SimilarityCoordinates.coordinateQ G.coord x.2.1) (self.position n (x.1, x.2.1)) ≠ 0 → SmoothCovariance.StrictCone (self.pairs n (x.1, x.2.1) l).matrix (PartitionedCovariance.chartTarget self.exponent (SimilarityCoordinates.coordinateQ G.coord x.2.1) (self.index n) (self.modelTarget n (x.1, x.2.1)) l)
• labels : ℕ → Finset NativeIndex

  Label type of NativeData, of type ℕ → Finset NativeIndex.

• coverage (n : ℕ) (x : Point) : x ∈ G.strip.domain → ∀ l ∉ self.labels n, PartitionedCovariance.mask self.width (PartitionedCovariance.tailLabel (self.index n) l.1) (SimilarityCoordinates.coordinateQ G.coord x.2.1) (self.position n (x.1, x.2.1)) = 0

noncomputable def NavierStokes.SignedMeanGain.NativeData.block {G : Geometry} (B : NativeData G) (A : PartitionedCovariance.UnsignedLabel → ℕ → Point → SignedWaveUpdate.Vec2) (l : NativeIndex) : CorrectionState.HarmonicBlock Point

Block, constructed using SignedWaveUpdate.coefficientBlock.

Equations

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

noncomputable def NavierStokes.SignedMeanGain.NativeData.primaryBlocks {G : Geometry} (B : NativeData G) : NativeIndex → CorrectionState.HarmonicBlock Point

Primary blocks, given by B.block (fun l n x => SmoothCovariance.amplitudes (B.matrix l n x) (B.target l n x)).

Equations

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

noncomputable def NavierStokes.SignedMeanGain.NativeData.signedBlocks {G : Geometry} (B : NativeData G) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) : NativeIndex → CorrectionState.HarmonicBlock Point

Signed blocks, constructed using B.block.

Equations

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

theorem NavierStokes.SignedMeanGain.NativeData.block_realization {G : Geometry} (B : NativeData G) (A : PartitionedCovariance.UnsignedLabel → ℕ → Point → SignedWaveUpdate.Vec2) (l : NativeIndex) (n : ℕ) {x : Point} (hx : x ∈ G.strip.domain) (θ : ℝ) (i : Fin 3) : (B.block A l).oscillation n (x, θ) i = (SignedWaveUpdate.nativeTangentBlock (B.pairs n (x.1, x.2.1) l.1) ⋯ (PartitionedCovariance.physicalOuter B.exponent (B.index n) l.1) (PartitionedCovariance.physicalViscosity B.exponent (B.index n) l.1) (A l.1 n x) (SimilarityCoordinates.coordinateQ G.coord x.2.1) (B.position n (x.1, x.2.1)) l.2).oscillation 0 (x.2.2, θ) i

theorem NavierStokes.SignedMeanGain.NativeData.primary_realization {G : Geometry} (B : NativeData G) (l : NativeIndex) (n : ℕ) {x : Point} (hx : x ∈ G.strip.domain) (θ : ℝ) (i : Fin 3) : (B.primaryBlocks l).oscillation n (x, θ) i = (SignedWaveUpdate.nativeTangentBlock (B.pairs n (x.1, x.2.1) l.1) ⋯ (PartitionedCovariance.physicalOuter B.exponent (B.index n) l.1) (PartitionedCovariance.physicalViscosity B.exponent (B.index n) l.1) (SmoothCovariance.amplitudes (B.pairs n (x.1, x.2.1) l.1).matrix (PartitionedCovariance.chartTarget B.exponent (SimilarityCoordinates.coordinateQ G.coord x.2.1) (B.index n) (B.modelTarget n (x.1, x.2.1)) l.1)) (SimilarityCoordinates.coordinateQ G.coord x.2.1) (B.position n (x.1, x.2.1)) l.2).oscillation 0 (x.2.2, θ) i

theorem NavierStokes.SignedMeanGain.NativeData.signed_realization {G : Geometry} (B : NativeData G) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (l : NativeIndex) (n : ℕ) {x : Point} (hx : x ∈ G.strip.domain) (θ : ℝ) (i : Fin 3) : (B.signedBlocks c u l).oscillation n (x, θ) i = (SignedWaveUpdate.nativeTangentBlock (B.pairs n (x.1, x.2.1) l.1) ⋯ (PartitionedCovariance.physicalOuter B.exponent (B.index n) l.1) (PartitionedCovariance.physicalViscosity B.exponent (B.index n) l.1) (SignedCovariance.increment (B.pairs n (x.1, x.2.1) l.1).matrix (PartitionedCovariance.chartTarget B.exponent (SimilarityCoordinates.coordinateQ G.coord x.2.1) (B.index n) (B.modelTarget n (x.1, x.2.1)) l.1) (SignedCovariance.chartStress B.exponent (B.index n) (LocalSignedRequest.requestedStress G.patch G.coord c u n x) l.1)) (SimilarityCoordinates.coordinateQ G.coord x.2.1) (B.position n (x.1, x.2.1)) l.2).oscillation 0 (x.2.2, θ) i

theorem NavierStokes.SignedMeanGain.meanBar_symmetricCovariance (p t : CorrectionState.Oscillation Point) (hp : LabelSumBounds.AngularContinuous p) (ht : LabelSumBounds.AngularContinuous t) (i j : Fin 3) (n : ℕ) (x : Point) : StateMomentBalances.meanBar (LabelSumBounds.symmetricCovariance p t i j) n x = PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (θ : ℝ) => p n ((x.1, x.2.1, Y), θ) i * t n ((x.1, x.2.1, Y), θ) j + t n ((x.1, x.2.1, Y), θ) i * p n ((x.1, x.2.1, Y), θ) j

theorem NavierStokes.SignedMeanGain.NativeData.requested_cross {G : Geometry} (B : NativeData G) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (i : Fin 2) : MeanIncrementBounds.Agree G.strip.domain (StateMomentBalances.meanBar (LabelSumBounds.symmetricCovariance (LabelSumBounds.fieldSum B.labels fun (l : NativeIndex) => (B.primaryBlocks l).oscillation) (LabelSumBounds.fieldSum B.labels fun (l : NativeIndex) => (B.signedBlocks c u l).oscillation) 0 i.succ)) fun (n : ℕ) (x : Point) => LocalSignedRequest.requestedStress G.patch G.coord c u n x i

theorem NavierStokes.SignedMeanGain.oscillation_eq_of_coefficients {D : Type} (a b : CorrectionState.HarmonicBlock D) (hv : a.velocity = b.velocity) (hc : LabelSumBounds.SameCarrier a b) : a.oscillation = b.oscillation

Equality of the stored harmonic coefficients and carrier metadata identifies the actual oscillations; the pressure coefficients need not agree.

theorem NavierStokes.SignedMeanGain.native_family_cross (G : Geometry) (B : NativeData G) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) {P : NativeIndex → ℕ → Point → ℝ} {α δ β η : ℝ} (f : LabelSumBounds.SignedFamily G.strip P α δ β η) (a : Assembly f) (hl : a.labels = B.labels) (hp : ∀ (l : NativeIndex), (f.primary l).velocity = (B.primaryBlocks l).velocity) (hcp : ∀ (l : NativeIndex), LabelSumBounds.SameCarrier (f.primary l) (B.primaryBlocks l)) (ht : ∀ (l : NativeIndex), (f.tangent l).velocity = (B.signedBlocks c u l).velocity) (hct : ∀ (l : NativeIndex), LabelSumBounds.SameCarrier (f.tangent l) (B.signedBlocks c u l)) : MeanIncrementBounds.Agree G.strip.domain (StateMomentBalances.meanBar (crossTensor f a 0 1)) (physicalSigma G 2 (u.thetaResidual c)) ∧ MeanIncrementBounds.Agree G.strip.domain (StateMomentBalances.meanBar (crossTensor f a 0 2)) (physicalSigma G 1 (u.axialResidual c))

This binds the abstract label-estimate package to the explicit common native construction by its coefficient definitions. The physical cross is a conclusion, with no signed-output realization as a hypothesis.

theorem NavierStokes.SignedMeanGain.native_signed_mean_gain (G : Geometry) (B : NativeData G) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) {P : NativeIndex → ℕ → Point → ℝ} {σ κ : ℝ} (hσ : 1 / 5 ≤ σ) (hκ : 0 ≤ κ) (hκsmall : κ ≤ 1 / 100000) (f : LabelSumBounds.SignedFamily G.strip P (1 / 2) (17 / 25) (1 / 2 + σ - κ) (1 + σ - 2 * κ)) (a : Assembly f) (hl : a.labels = B.labels) (hp : ∀ (l : NativeIndex), (f.primary l).velocity = (B.primaryBlocks l).velocity) (hcp : ∀ (l : NativeIndex), LabelSumBounds.SameCarrier (f.primary l) (B.primaryBlocks l)) (ht : ∀ (l : NativeIndex), (f.tangent l).velocity = (B.signedBlocks c u l).velocity) (hct : ∀ (l : NativeIndex), LabelSumBounds.SameCarrier (f.tangent l) (B.signedBlocks c u l)) (q : CorrectionState.OscillatoryScalar Point) (gaussian : CorrectionState.Oscillation Point) (hold : u.oscillation = oldField f a) (H : LocalData G c u (tangentField f a + curlField f a) q gaussian) (ho : MeanIncrementBounds.OperatorBounds G.strip G.operators κ) (hX : ∀ (i j : Fin 3), MovingField G (incrementTensor f a i j)) (hS : ∀ (i j : Fin 3), MovingField G (crossTensor f a i j)) (hθ : WeightedClasses.MeanClass G.strip (1 + σ - κ) (u.thetaResidual c)) (hz : WeightedClasses.MeanClass G.strip (1 + σ - κ) (u.axialResidual c)) (hd : CorrectionState.DefectBounds G.slowStrip (σ - κ) c u) : have v := waveStage G.gauge c u (tangentField f a + curlField f a) q gaussian; WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ) (v.thetaResidual c) ∧ WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ) (v.axialResidual c) ∧ WeightedClasses.MeanClass G.strip (1 + σ + 17 / 100) (StateMomentBalances.meanBar (v.thetaResidual c)) ∧ WeightedClasses.MeanClass G.strip (1 + σ + 17 / 100) (StateMomentBalances.meanBar (v.axialResidual c))

The signed-wave mean gain for the actual reconstructed state. Incoming raw residuals and measured defects have exponent 1+σ-κ; the output raw residuals have exponent 1+σ-2κ, and their actual torus means gain 17/100. The same native primary, masks, matrix, quotient, and fundamental supply the cross cancellation. All remaining covariance terms are estimated literally.

theorem NavierStokes.SignedMeanGain.native_stage_gaussian_retained (G : Geometry) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) {ι : Type} {P : ι → ℕ → Point → ℝ} {α δ β η : ℝ} (f : LabelSumBounds.SignedFamily G.strip P α δ β η) (a : Assembly f) (q : CorrectionState.OscillatoryScalar Point) (gaussian : CorrectionState.Oscillation Point) : (waveStage G.gauge c u (tangentField f a + curlField f a) q gaussian).errors.gaussian = u.errors.gaussian + gaussian

The excluded Gaussian field is carried by the very same output state. The raw mean estimate does not set this field or its average to zero.