Naturality of the actual common-index temporal state update #

All equalities are on full radial and free-torus fibers. The angular inverse, stream construction, retained alias and recomputed pressure are the literal operators used by VariableGaugeMean.temporalStageState.

source

@[reducible, inline]

abbrev NavierStokes.TemporalStateCoherence.Plane :

Type

Plane: an abbreviation for PressureStream.Plane.

Equations

NavierStokes.TemporalStateCoherence.Plane = NavierStokes.PressureStream.Plane

Instances For

Actual stream transport, reusable by the rank update #

source

theorem NavierStokes.TemporalStateCoherence.mul_rpow_pos_left {l : ℝ} (hl : 0 < l) (r d : ℝ) :

(l * r) ^ d = l ^ d * r ^ d

source

theorem NavierStokes.TemporalStateCoherence.physicalSpeed_vector_all {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {l : ℝ} (hl : 0 < l) (C : E →L[ℝ ] F) (d M N R : ℝ) (v : E) (w : F) (hshift : M • C v = (N * l ^ d) • w) :

C (PressureStream.physicalSpeed d M R • v) = l • PressureStream.physicalSpeed d N (l * R) • w

source

theorem NavierStokes.TemporalStateCoherence.streamPotential_fiberLocal {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (ell : S → ℝ) (v : Plane) :

PhysicalMeanDomain.FiberLocal (VariableGaugeMean.streamPotential d a b M ell v)

source

theorem NavierStokes.TemporalStateCoherence.streamPotential_congr_profile {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {d a b d' a' b' : ℝ} (hd : d = d') (ha : a = a') (hb : b = b') (M : ℝ) (ell : S → ℝ) (v : Plane) (f : PressureStream.Lift S → ℝ) :

VariableGaugeMean.streamPotential d a b M ell v f = VariableGaugeMean.streamPotential d' a' b' M ell v f

source

theorem NavierStokes.TemporalStateCoherence.streamPotential_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l : ℝ} (hl : 0 < l) (P : S ≃L[ℝ ] T) (k : ℕ) {a b d M N u : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v w : Plane) (hshift : M • (TemporalMeanUpdate.coverMap k) v = (N * l ^ d) • w) (ell : S → ℝ) (ell' : T → ℝ) {V : Set S} {U : Set T} (hU : IsOpen U) (hmap : Set.MapsTo (⇑P) V U) (hpos : ∀ s ∈ V, 0 < ell s) (hlen : ∀ s ∈ V, ell' (P s) = l * ell s) {f : PressureStream.Lift S → ℝ} {fr : PressureStream.Lift T → ℝ} (he : PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) u f fr) (hf : ContDiffOn ℝ (↑⊤) fr (PhysicalMeanDomain.slowDomain U)) (hs : VariableGaugeMean.SupportedGauge a b ell' U fr) :

PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) (u / l) (VariableGaugeMean.streamPotential d a b M ell v f) (VariableGaugeMean.streamPotential d a b N ell' w fr)

source

theorem NavierStokes.TemporalStateCoherence.graphDr_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l : ℝ} (hl : 0 < l) (P : S ≃L[ℝ ] T) (k : ℕ) {d M N u : ℝ} (v w : Plane) (hshift : M • (TemporalMeanUpdate.coverMap k) v = (N * l ^ d) • w) {V : Set S} (hV : IsOpen V) {f : PressureStream.Lift S → ℝ} {fr : PressureStream.Lift T → ℝ} (he : PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) u f fr) :

PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) (u * l) (PressureStream.graphDr (PressureStream.physicalSpeed d M) (0, v) f) (PressureStream.graphDr (PressureStream.physicalSpeed d N) (0, w) fr)

source

theorem NavierStokes.TemporalStateCoherence.divideRadius_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l : ℝ} (hl : 0 < l) (P : S ≃L[ℝ ] T) (k : ℕ) {u : ℝ} {V : Set S} {f : PressureStream.Lift S → ℝ} {fr : PressureStream.Lift T → ℝ} (he : PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) u f fr) :

PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) (u * l) (PressureStream.divideRadius f) (PressureStream.divideRadius fr)

source

theorem NavierStokes.TemporalStateCoherence.streamGamma_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l : ℝ} (hl : 0 < l) (P : S ≃L[ℝ ] T) (k : ℕ) {d M N u : ℝ} (v w : Plane) (hshift : M • (TemporalMeanUpdate.coverMap k) v = (N * l ^ d) • w) {V : Set S} (hV : IsOpen V) {f : PressureStream.Lift S → ℝ} {fr : PressureStream.Lift T → ℝ} (he : PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) u f fr) :

PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) (u * l) (PressureStream.streamGamma (PressureStream.physicalSpeed d M) (0, v) f) (PressureStream.streamGamma (PressureStream.physicalSpeed d N) (0, w) fr)

source

theorem NavierStokes.TemporalStateCoherence.streamBeta_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l : ℝ} (hl : 0 < l) (P : S ≃L[ℝ ] T) (k : ℕ) {u b : ℝ} (v : S × Plane) (w : T × Plane) (hvec : ((↑P).prodMap (TemporalMeanUpdate.coverMap k)) v = b • w) {V : Set S} (hV : IsOpen V) {f : PressureStream.Lift S → ℝ} {fr : PressureStream.Lift T → ℝ} (he : PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) u f fr) :

PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) (u * b) (PressureStream.streamBeta v f) (PressureStream.streamBeta w fr)

The actual common-index inverse and its normalization #

source

noncomputable def NavierStokes.TemporalStateCoherence.clock (h : ℝ) (n i : ℕ) :

ℝ

Clock, given by ChartScales.Tg ^ i * ChartScales.Q n ^ (1+h).

Equations

NavierStokes.TemporalStateCoherence.clock h n i = NavierStokes.ChartScales.Tg ^ i * NavierStokes.ChartScales.Q n ^ (1 + h)

Instances For

source

theorem NavierStokes.TemporalStateCoherence.clock_pos (h : ℝ) (n i : ℕ) :

0 < clock h n i

source

theorem NavierStokes.TemporalStateCoherence.clock_factor (h : ℝ) (n i nr ir k : ℕ) (c l : ℝ) (hclock : clock h n i * ChartScales.Tg ^ k = c * l * clock h nr ir) :

(clock h n i)⁻¹ * (ChartScales.Tg ^ k)⁻¹ * (c * c * l) = c * (clock h nr ir)⁻¹

source

theorem NavierStokes.TemporalStateCoherence.temporalAtIndex_coverPull {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (h : ℝ) (n i nr ir k : ℕ) (c l : ℝ) (P : S →L[ℝ ] T) (hclock : clock h n i * ChartScales.Tg ^ k = c * l * clock h nr ir) {f : PressureStream.Lift T → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (z : PressureStream.Lift S) :

MeanChartCompatibility.temporalAtIndex h n i (MeanChartCompatibility.coverPull l P k (c * c * l) f) z = c * MeanChartCompatibility.temporalAtIndex h nr ir f ((MeanChartCompatibility.chartLinear l (P.prodMap (TemporalMeanUpdate.coverMap k))) z)

source

theorem NavierStokes.TemporalStateCoherence.temporalAtIndex_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l c : ℝ} (hl : 0 < l) (P : S ≃L[ℝ ] T) (k : ℕ) (h : ℝ) (n i nr ir : ℕ) (hclock : clock h n i * ChartScales.Tg ^ k = c * l * clock h nr ir) {V : Set S} {U : Set T} (hU : IsOpen U) (hmap : Set.MapsTo (⇑P) V U) {f : PressureStream.Lift S → ℝ} {fr : PressureStream.Lift T → ℝ} (he : PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) (c * c * l) f fr) (hf : ContDiffOn ℝ (↑⊤) fr (PhysicalMeanDomain.slowDomain U)) (hp : PhysicalMeanDomain.PeriodicOn U fr) :

PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c (MeanChartCompatibility.temporalAtIndex h n i f) (MeanChartCompatibility.temporalAtIndex h nr ir fr)

source

theorem NavierStokes.TemporalStateCoherence.fastTime_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l : ℝ} (hl : 0 < l) (P : S ≃L[ℝ ] T) (k : ℕ) {u b : ℝ} {V : Set S} (hV : IsOpen V) (o : MeanIncrementBounds.Operators (PressureStream.Lift S)) (r : MeanIncrementBounds.Operators (PressureStream.Lift T)) (n nr : ℕ) (hv : (GaugeStateCoherence.chartEquiv l ⋯ P k) (o.fastCoefficient n • o.vT) = b • r.fastCoefficient nr • r.vT) {f : MeanIncrementBounds.Field (PressureStream.Lift S)} {fr : MeanIncrementBounds.Field (PressureStream.Lift T)} (he : PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) u (f n) (fr nr)) :

PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) (u * b) (o.fastTime f n) (r.fastTime fr nr)

Literal temporal fields and retained alias #

source

theorem NavierStokes.TemporalStateCoherence.temporalPotential_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] [FiniteDimensional ℝ T] {l c : ℝ} (hl : 0 < l) (P : S ≃L[ℝ ] T) (k : ℕ) {V : Set S} {U : Set T} (hV : IsOpen V) (hU : IsOpen U) (hmap : Set.MapsTo (⇑P) V U) (g : VariableGaugeMean.GaugeData S) (gr : VariableGaugeMean.GaugeData T) (C : CorrectionState.Context (PressureStream.Lift S)) (Cr : CorrectionState.Context (PressureStream.Lift T)) (s : CorrectionState.State (PressureStream.Lift S)) (r : CorrectionState.State (PressureStream.Lift T)) (h : ℝ) (index indexr : ℕ → ℕ) (n nr : ℕ) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hg : GaugeStateCoherence.GaugeOn V l (↑P) k g gr n nr) (H : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l s r n nr) (G : PhysicalResidualNaturality.ContextOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l C Cr n nr) (hclock : clock h n (index n) * ChartScales.Tg ^ k = c * l * clock h nr (indexr nr)) (hfz : ContDiffOn ℝ (↑⊤) (r.axialResidual Cr nr) (PhysicalMeanDomain.slowDomain U)) (hpz : PhysicalMeanDomain.PeriodicOn U (r.axialResidual Cr nr)) (hsz : VariableGaugeMean.SupportedGauge gr.radial.inner gr.radial.outer (gr.length nr) U (r.axialResidual Cr nr)) :

PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) (c / l) (VariableGaugeMean.temporalPotential g h index C s n) (VariableGaugeMean.temporalPotential gr h indexr Cr r nr)

source

theorem NavierStokes.TemporalStateCoherence.temporalIncrement_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] [FiniteDimensional ℝ T] {l c : ℝ} (hl : 0 < l) (P : S ≃L[ℝ ] T) (k : ℕ) {V : Set S} {U : Set T} (hV : IsOpen V) (hU : IsOpen U) (hmap : Set.MapsTo (⇑P) V U) (g : VariableGaugeMean.GaugeData S) (gr : VariableGaugeMean.GaugeData T) (C : CorrectionState.Context (PressureStream.Lift S)) (Cr : CorrectionState.Context (PressureStream.Lift T)) (s : CorrectionState.State (PressureStream.Lift S)) (r : CorrectionState.State (PressureStream.Lift T)) (h : ℝ) (index indexr : ℕ → ℕ) (n nr : ℕ) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hg : GaugeStateCoherence.GaugeOn V l (↑P) k g gr n nr) (H : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l s r n nr) (G : PhysicalResidualNaturality.ContextOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l C Cr n nr) (hclock : clock h n (index n) * ChartScales.Tg ^ k = c * l * clock h nr (indexr nr)) (hfz : ContDiffOn ℝ (↑⊤) (r.axialResidual Cr nr) (PhysicalMeanDomain.slowDomain U)) (hpz : PhysicalMeanDomain.PeriodicOn U (r.axialResidual Cr nr)) (hsz : VariableGaugeMean.SupportedGauge gr.radial.inner gr.radial.outer (gr.length nr) U (r.axialResidual Cr nr)) (axial : S × Plane) (axialr : T × Plane) (haxial : ((↑P).prodMap (TemporalMeanUpdate.coverMap k)) (C.operators.epsilon n • axial) = l • Cr.operators.epsilon nr • axialr) (hfθ : ContDiffOn ℝ (↑⊤) (r.thetaResidual Cr nr) (PhysicalMeanDomain.slowDomain U)) (hpθ : PhysicalMeanDomain.PeriodicOn U (r.thetaResidual Cr nr)) :

PhysicalResidualNaturality.TripleOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c (VariableGaugeMean.temporalIncrementState g h index axial C s) (VariableGaugeMean.temporalIncrementState gr h indexr axialr Cr r) n nr

source

theorem NavierStokes.TemporalStateCoherence.temporalAxialDifference_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] [FiniteDimensional ℝ T] {l c : ℝ} (hl : 0 < l) (P : S ≃L[ℝ ] T) (k : ℕ) {V : Set S} {U : Set T} (hV : IsOpen V) (hU : IsOpen U) (hmap : Set.MapsTo (⇑P) V U) (g : VariableGaugeMean.GaugeData S) (gr : VariableGaugeMean.GaugeData T) (C : CorrectionState.Context (PressureStream.Lift S)) (Cr : CorrectionState.Context (PressureStream.Lift T)) (s : CorrectionState.State (PressureStream.Lift S)) (r : CorrectionState.State (PressureStream.Lift T)) (h : ℝ) (index indexr : ℕ → ℕ) (n nr : ℕ) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hg : GaugeStateCoherence.GaugeOn V l (↑P) k g gr n nr) (H : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l s r n nr) (G : PhysicalResidualNaturality.ContextOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l C Cr n nr) (hclock : clock h n (index n) * ChartScales.Tg ^ k = c * l * clock h nr (indexr nr)) (hfz : ContDiffOn ℝ (↑⊤) (r.axialResidual Cr nr) (PhysicalMeanDomain.slowDomain U)) (hpz : PhysicalMeanDomain.PeriodicOn U (r.axialResidual Cr nr)) (hsz : VariableGaugeMean.SupportedGauge gr.radial.inner gr.radial.outer (gr.length nr) U (r.axialResidual Cr nr)) (axial : S × Plane) (axialr : T × Plane) (haxial : ((↑P).prodMap (TemporalMeanUpdate.coverMap k)) (C.operators.epsilon n • axial) = l • Cr.operators.epsilon nr • axialr) (hfθ : ContDiffOn ℝ (↑⊤) (r.thetaResidual Cr nr) (PhysicalMeanDomain.slowDomain U)) (hpθ : PhysicalMeanDomain.PeriodicOn U (r.thetaResidual Cr nr)) :

PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c (VariableGaugeMean.temporalAxialDifference g h index C s n) (VariableGaugeMean.temporalAxialDifference gr h indexr Cr r nr)

source

theorem NavierStokes.TemporalStateCoherence.temporalAliasState_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] [FiniteDimensional ℝ T] {l c : ℝ} (hl : 0 < l) (P : S ≃L[ℝ ] T) (k : ℕ) {V : Set S} {U : Set T} (hV : IsOpen V) (hU : IsOpen U) (hmap : Set.MapsTo (⇑P) V U) (g : VariableGaugeMean.GaugeData S) (gr : VariableGaugeMean.GaugeData T) (C : CorrectionState.Context (PressureStream.Lift S)) (Cr : CorrectionState.Context (PressureStream.Lift T)) (s : CorrectionState.State (PressureStream.Lift S)) (r : CorrectionState.State (PressureStream.Lift T)) (h : ℝ) (index indexr : ℕ → ℕ) (n nr : ℕ) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hg : GaugeStateCoherence.GaugeOn V l (↑P) k g gr n nr) (H : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l s r n nr) (G : PhysicalResidualNaturality.ContextOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l C Cr n nr) (hclock : clock h n (index n) * ChartScales.Tg ^ k = c * l * clock h nr (indexr nr)) (hfz : ContDiffOn ℝ (↑⊤) (r.axialResidual Cr nr) (PhysicalMeanDomain.slowDomain U)) (hpz : PhysicalMeanDomain.PeriodicOn U (r.axialResidual Cr nr)) (hsz : VariableGaugeMean.SupportedGauge gr.radial.inner gr.radial.outer (gr.length nr) U (r.axialResidual Cr nr)) (axial : S × Plane) (axialr : T × Plane) (haxial : ((↑P).prodMap (TemporalMeanUpdate.coverMap k)) (C.operators.epsilon n • axial) = l • Cr.operators.epsilon nr • axialr) (hfθ : ContDiffOn ℝ (↑⊤) (r.thetaResidual Cr nr) (PhysicalMeanDomain.slowDomain U)) (hpθ : PhysicalMeanDomain.PeriodicOn U (r.thetaResidual Cr nr)) (hfast : (GaugeStateCoherence.chartEquiv l ⋯ P k) (C.operators.fastCoefficient n • C.operators.vT) = (c * l) • Cr.operators.fastCoefficient nr • Cr.operators.vT) (z : PressureStream.Lift S) :

z ∈ PhysicalMeanDomain.slowDomain V → ∀ (theta : ℝ) (i : Fin 3), VariableGaugeMean.temporalAliasState g h index C s n (z, theta) i = c * c * l * VariableGaugeMean.temporalAliasState gr h indexr Cr r nr ((GaugeStateCoherence.chartEquiv l ⋯ P k) z, theta) i

source

theorem NavierStokes.TemporalStateCoherence.temporalBeforePressure_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] [FiniteDimensional ℝ T] {l c : ℝ} (hl : 0 < l) (P : S ≃L[ℝ ] T) (k : ℕ) {V : Set S} {U : Set T} (hV : IsOpen V) (hU : IsOpen U) (hmap : Set.MapsTo (⇑P) V U) (g : VariableGaugeMean.GaugeData S) (gr : VariableGaugeMean.GaugeData T) (C : CorrectionState.Context (PressureStream.Lift S)) (Cr : CorrectionState.Context (PressureStream.Lift T)) (s : CorrectionState.State (PressureStream.Lift S)) (r : CorrectionState.State (PressureStream.Lift T)) (h : ℝ) (index indexr : ℕ → ℕ) (n nr : ℕ) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hg : GaugeStateCoherence.GaugeOn V l (↑P) k g gr n nr) (H : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l s r n nr) (G : PhysicalResidualNaturality.ContextOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l C Cr n nr) (hclock : clock h n (index n) * ChartScales.Tg ^ k = c * l * clock h nr (indexr nr)) (hfz : ContDiffOn ℝ (↑⊤) (r.axialResidual Cr nr) (PhysicalMeanDomain.slowDomain U)) (hpz : PhysicalMeanDomain.PeriodicOn U (r.axialResidual Cr nr)) (hsz : VariableGaugeMean.SupportedGauge gr.radial.inner gr.radial.outer (gr.length nr) U (r.axialResidual Cr nr)) (axial : S × Plane) (axialr : T × Plane) (haxial : ((↑P).prodMap (TemporalMeanUpdate.coverMap k)) (C.operators.epsilon n • axial) = l • Cr.operators.epsilon nr • axialr) (hfθ : ContDiffOn ℝ (↑⊤) (r.thetaResidual Cr nr) (PhysicalMeanDomain.slowDomain U)) (hpθ : PhysicalMeanDomain.PeriodicOn U (r.thetaResidual Cr nr)) (hfast : (GaugeStateCoherence.chartEquiv l ⋯ P k) (C.operators.fastCoefficient n • C.operators.vT) = (c * l) • Cr.operators.fastCoefficient nr • Cr.operators.vT) :

PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l (s.addIncrement (VariableGaugeMean.temporalIncrementState g h index axial C s) 0 0 0 { base := 0, gaussian := 0, aliasError := VariableGaugeMean.temporalAliasState g h index C s }) (r.addIncrement (VariableGaugeMean.temporalIncrementState gr h indexr axialr Cr r) 0 0 0 { base := 0, gaussian := 0, aliasError := VariableGaugeMean.temporalAliasState gr h indexr Cr r }) n nr

source

theorem NavierStokes.TemporalStateCoherence.temporalStage_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] [FiniteDimensional ℝ T] {l c : ℝ} (hl : 0 < l) (P : S ≃L[ℝ ] T) (k : ℕ) {V : Set S} {U : Set T} (hV : IsOpen V) (hU : IsOpen U) (hmap : Set.MapsTo (⇑P) V U) (g : VariableGaugeMean.GaugeData S) (gr : VariableGaugeMean.GaugeData T) (C : CorrectionState.Context (PressureStream.Lift S)) (Cr : CorrectionState.Context (PressureStream.Lift T)) (s : CorrectionState.State (PressureStream.Lift S)) (r : CorrectionState.State (PressureStream.Lift T)) (h : ℝ) (index indexr : ℕ → ℕ) (n nr : ℕ) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hg : GaugeStateCoherence.GaugeOn V l (↑P) k g gr n nr) (H : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l s r n nr) (G : PhysicalResidualNaturality.ContextOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l C Cr n nr) (hclock : clock h n (index n) * ChartScales.Tg ^ k = c * l * clock h nr (indexr nr)) (hfz : ContDiffOn ℝ (↑⊤) (r.axialResidual Cr nr) (PhysicalMeanDomain.slowDomain U)) (hpz : PhysicalMeanDomain.PeriodicOn U (r.axialResidual Cr nr)) (hsz : VariableGaugeMean.SupportedGauge gr.radial.inner gr.radial.outer (gr.length nr) U (r.axialResidual Cr nr)) (axial : S × Plane) (axialr : T × Plane) (haxial : ((↑P).prodMap (TemporalMeanUpdate.coverMap k)) (C.operators.epsilon n • axial) = l • Cr.operators.epsilon nr • axialr) (hfθ : ContDiffOn ℝ (↑⊤) (r.thetaResidual Cr nr) (PhysicalMeanDomain.slowDomain U)) (hpθ : PhysicalMeanDomain.PeriodicOn U (r.thetaResidual Cr nr)) (hfast : (GaugeStateCoherence.chartEquiv l ⋯ P k) (C.operators.fastCoefficient n • C.operators.vT) = (c * l) • Cr.operators.fastCoefficient nr • Cr.operators.vT) (hfpost : ContDiffOn ℝ (↑⊤) ((VariableGaugeMean.temporalStageState gr h indexr axialr Cr r).gr Cr nr) (PhysicalMeanDomain.slowDomain U)) (hppost : PhysicalMeanDomain.PeriodicOn U ((VariableGaugeMean.temporalStageState gr h indexr axialr Cr r).gr Cr nr)) (hspost : VariableGaugeMean.SupportedGauge gr.radial.inner gr.radial.outer (gr.length nr) U ((VariableGaugeMean.temporalStageState gr h indexr axialr Cr r).gr Cr nr)) :

PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l (VariableGaugeMean.temporalStageState g h index axial C s) (VariableGaugeMean.temporalStageState gr h indexr axialr Cr r) n nr

Full coherence of the literal temporal stage, including recomputed pressure. The analytic conditions concern the source supplied to that pressure integral; output coherence is derived.

source