Coherence of the actual moving-gauge pressure reconstruction

The hypotheses transport the primitive gauge data and the incoming state on whole radial/torus fibers. The recomputed pressure and retained cutoff alias are obtained from their genuine integral definitions.

@[reducible, inline]

abbrev NavierStokes.GaugeStateCoherence.Plane : Type

Plane: an abbreviation for PressureStream.Plane.

Equations

• NavierStokes.GaugeStateCoherence.Plane = NavierStokes.PressureStream.Plane

noncomputable def NavierStokes.GaugeStateCoherence.chartEquiv {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (l : ℝ) (hl : l ≠ 0) (P : S ≃L[ℝ] T) (k : ℕ) : PressureStream.Lift S ≃L[ℝ] PressureStream.Lift T

The actual invertible map on the universal cover.

Equations

• NavierStokes.GaugeStateCoherence.chartEquiv l hl P k = (NavierStokes.PhysicalResidualNaturality.scalarEquiv ℝ l hl).prodCongr (P.prodCongr (NavierStokes.CommonCoverSolve.coverPower k))

@[simp]

theorem NavierStokes.GaugeStateCoherence.chartEquiv_apply {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (l : ℝ) (hl : l ≠ 0) (P : S ≃L[ℝ] T) (k : ℕ) (z : PressureStream.Lift S) : (chartEquiv l hl P k) z = (l * z.1, P z.2.1, (TemporalMeanUpdate.coverMap k) z.2.2)

theorem NavierStokes.GaugeStateCoherence.chartEquiv_toContinuousLinearMap {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (l : ℝ) (hl : l ≠ 0) (P : S ≃L[ℝ] T) (k : ℕ) : ↑(chartEquiv l hl P k) = MeanChartCompatibility.chartLinear l ((↑P).prodMap (TemporalMeanUpdate.coverMap k))

theorem NavierStokes.GaugeStateCoherence.coverPull_eq {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (l : ℝ) (hl : l ≠ 0) (P : S ≃L[ℝ] T) (k : ℕ) (u : ℝ) (f : PressureStream.Lift T → ℝ) (z : PressureStream.Lift S) : MeanChartCompatibility.coverPull l (↑P) k u f z = u * f ((chartEquiv l hl P k) z)

Whole-fiber locality of the actual gauge operators

theorem NavierStokes.GaugeStateCoherence.pressureSource_fiberLocal {S : Type} (a b : ℝ) (hab : a < b) (ell : S → ℝ) : PhysicalMeanDomain.FiberLocal (VariableGaugeMean.pressureSource a b hab ell)

theorem NavierStokes.GaugeStateCoherence.meanPressure_fiberLocal {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (hab : a < b) (ell : S → ℝ) (v : Plane) : PhysicalMeanDomain.FiberLocal (VariableGaugeMean.meanPressure d a b M hab ell v)

theorem NavierStokes.GaugeStateCoherence.meanPressure_congr_profile {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {d a b d' a' b' : ℝ} {hab : a < b} {hab' : a' < b'} (hd : d = d') (ha : a = a') (hb : b = b') (M : ℝ) (ell : S → ℝ) (v : Plane) (f : PressureStream.Lift S → ℝ) : VariableGaugeMean.meanPressure d a b M hab ell v f = VariableGaugeMean.meanPressure d' a' b' M hab' ell v f

noncomputable def NavierStokes.GaugeStateCoherence.pressureAlias {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (hab : a < b) (ell : S → ℝ) (v : Plane) (f : PressureStream.Lift S → ℝ) : PressureStream.Lift S → ℝ

The scalar whose negative is the radial component of pressureAliasState.

Equations

• NavierStokes.GaugeStateCoherence.pressureAlias d a b M hab ell v f = NavierStokes.VariableGaugeMean.compactAlias d a b M ell v (NavierStokes.VariableGaugeMean.pressureSource a b hab ell f)

theorem NavierStokes.GaugeStateCoherence.pressureAlias_fiberLocal {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (hab : a < b) (ell : S → ℝ) (v : Plane) : PhysicalMeanDomain.FiberLocal (pressureAlias d a b M hab ell v)

theorem NavierStokes.GaugeStateCoherence.pressureAlias_eq_fixed {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} (hab : a < b) (d M : ℝ) (ell : S → ℝ) (v : Plane) (f : PressureStream.Lift S → ℝ) (z : PressureStream.Lift S) (hl : 0 < ell z.2.1) : pressureAlias d a b M hab ell v f z = PressureStream.pressureAlias d (ell z.2.1 * a) (ell z.2.1 * b) M ⋯ v f z

theorem NavierStokes.GaugeStateCoherence.pressureAlias_congr_endpoints {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b a' b' : ℝ} {hab : a < b} {hab' : a' < b'} (ha : a = a') (hb : b = b') (d M : ℝ) (v : Plane) (f : PressureStream.Lift S → ℝ) (z : PressureStream.Lift S) : PressureStream.pressureAlias d a b M hab v f z = PressureStream.pressureAlias d a' b' M hab' v f z

Recomputed pressure from transported primitive data

structure NavierStokes.GaugeStateCoherence.GaugeOn {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (V : Set S) (l : ℝ) (P : S →L[ℝ] T) (k : ℕ) (g : VariableGaugeMean.GaugeData S) (r : VariableGaugeMean.GaugeData T) (n nr : ℕ) : Prop

Only primitive gauge data are compared: profile endpoints, exponent, length and actual radial transport vector.

• exponent : r.radial.exponent = g.radial.exponent
• inner : r.radial.inner = g.radial.inner
• outer : r.radial.outer = g.radial.outer
• positive (s : S) : s ∈ V → 0 < g.length n s
• length (s : S) : s ∈ V → r.length nr (P s) = l * g.length n s
• frequency : g.radial.frequency n • (TemporalMeanUpdate.coverMap k) g.radial.radialDirection = (r.radial.frequency nr * l ^ g.radial.exponent) • r.radial.radialDirection

theorem NavierStokes.GaugeStateCoherence.meanPressure_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) (chartEquiv l ⋯ P k) u f fr) (hf : ContDiffOn ℝ (↑⊤) fr (PhysicalMeanDomain.slowDomain U)) (hp : PhysicalMeanDomain.PeriodicOn U fr) (hs : VariableGaugeMean.SupportedGauge a b ell' U fr) : PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (chartEquiv l ⋯ P k) (u / l) (VariableGaugeMean.meanPressure d a b M hab ell v f) (VariableGaugeMean.meanPressure d a b N hab ell' w fr)

theorem NavierStokes.GaugeStateCoherence.reconstructState_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ 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)) (n nr : ℕ) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hg : GaugeOn V l (↑P) k g gr n nr) (H : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (chartEquiv l ⋯ P k) c l s r n nr) (G : PhysicalResidualNaturality.ContextOn (PhysicalMeanDomain.slowDomain V) (chartEquiv l ⋯ P k) c l C Cr n nr) (hf : ContDiffOn ℝ (↑⊤) (r.gr Cr nr) (PhysicalMeanDomain.slowDomain U)) (hp : PhysicalMeanDomain.PeriodicOn U (r.gr Cr nr)) (hs : VariableGaugeMean.SupportedGauge gr.radial.inner gr.radial.outer (gr.length nr) U (r.gr Cr nr)) : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (chartEquiv l ⋯ P k) c l (VariableGaugeMean.reconstructState g C s) (VariableGaugeMean.reconstructState gr Cr r) n nr

The retained pressure alias has the residual units

theorem NavierStokes.GaugeStateCoherence.fixedPressureAlias_fiberLocal {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (hab : a < b) (v : Plane) : PhysicalMeanDomain.FiberLocal (PressureStream.pressureAlias d a b M hab v)

theorem NavierStokes.GaugeStateCoherence.pressureAlias_zero_of_nonpositive {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (M : ℝ) (ell : S → ℝ) (v : Plane) (f : PressureStream.Lift S → ℝ) (z : PressureStream.Lift S) (hl : 0 < ell z.2.1) (hz : z.1 ≤ 0) : pressureAlias d a b M hab ell v f z = 0

theorem NavierStokes.GaugeStateCoherence.pressureAlias_supported {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (M : ℝ) (ell : S → ℝ) (v : Plane) (f : PressureStream.Lift S → ℝ) (V : Set S) (hl : ∀ s ∈ V, 0 < ell s) : VariableGaugeMean.SupportedGauge a b ell V (pressureAlias d a b M hab ell v f)

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

theorem NavierStokes.GaugeStateCoherence.pressureAlias_coverPull {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l a b d : ℝ} (hl : 0 < l) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (P : S →L[ℝ] T) (k : ℕ) (M N u : ℝ) (v w : Plane) (hshift : M • (TemporalMeanUpdate.coverMap k) v = (N * l ^ d) • w) (ell : S → ℝ) (ell' : T → ℝ) {U : Set T} (hU : IsOpen U) {f : PressureStream.Lift T → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hp : PhysicalMeanDomain.PeriodicOn U f) (hs : VariableGaugeMean.SupportedGauge a b ell' U f) (z : PressureStream.Lift S) (hz : P z.2.1 ∈ U) (hzl : 0 < ell z.2.1) (hell : ell' (P z.2.1) = l * ell z.2.1) : pressureAlias d a b M hab ell v (MeanChartCompatibility.coverPull l P k u f) z = u * pressureAlias d a b N hab ell' w f ((MeanChartCompatibility.chartLinear l (P.prodMap (TemporalMeanUpdate.coverMap k))) z)

Naturality of the actual variable-gauge alias, including all nonpositive radii where the cutoff makes both sides vanish.

theorem NavierStokes.GaugeStateCoherence.pressureAlias_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) (chartEquiv l ⋯ P k) u f fr) (hf : ContDiffOn ℝ (↑⊤) fr (PhysicalMeanDomain.slowDomain U)) (hp : PhysicalMeanDomain.PeriodicOn U fr) (hs : VariableGaugeMean.SupportedGauge a b ell' U fr) : PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (chartEquiv l ⋯ P k) u (pressureAlias d a b M hab ell v f) (pressureAlias d a b N hab ell' w fr)

theorem NavierStokes.GaugeStateCoherence.pressureAliasState_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ 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)) (n nr : ℕ) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hg : GaugeOn V l (↑P) k g gr n nr) (H : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (chartEquiv l ⋯ P k) c l s r n nr) (G : PhysicalResidualNaturality.ContextOn (PhysicalMeanDomain.slowDomain V) (chartEquiv l ⋯ P k) c l C Cr n nr) (hf : ContDiffOn ℝ (↑⊤) (r.gr Cr nr) (PhysicalMeanDomain.slowDomain U)) (hp : PhysicalMeanDomain.PeriodicOn U (r.gr Cr nr)) (hs : VariableGaugeMean.SupportedGauge gr.radial.inner gr.radial.outer (gr.length nr) U (r.gr Cr nr)) (z : PressureStream.Lift S) : z ∈ PhysicalMeanDomain.slowDomain V → ∀ (theta : ℝ) (i : Fin 3), VariableGaugeMean.pressureAliasState g C s n (z, theta) i = c * c * l * VariableGaugeMean.pressureAliasState gr Cr r nr ((chartEquiv l ⋯ P k) z, theta) i

The actual similarity gauge in two bands

noncomputable def NavierStokes.GaugeStateCoherence.bandScale (n m : ℕ) : ℝ

Band scale, given by (ChartScales.Q n / ChartScales.Q m) ^ (1 / 2 : ℝ).

Equations

• NavierStokes.GaugeStateCoherence.bandScale n m = (NavierStokes.ChartScales.Q n / NavierStokes.ChartScales.Q m) ^ (1 / 2)

theorem NavierStokes.GaugeStateCoherence.bandScale_pos (n m : ℕ) : 0 < bandScale n m

noncomputable def NavierStokes.GaugeStateCoherence.bandVelocityScale (h : ℝ) (n m : ℕ) : ℝ

Band velocity scale, given by (ChartScales.Q n / ChartScales.Q m) ^ CoordinateAlgebra.A h.

Equations

• NavierStokes.GaugeStateCoherence.bandVelocityScale h n m = (NavierStokes.ChartScales.Q n / NavierStokes.ChartScales.Q m) ^ NavierStokes.CoordinateAlgebra.A h

noncomputable def NavierStokes.GaugeStateCoherence.bandSlowEquiv (h : ℝ) (n m : ℕ) : Plane ≃L[ℝ] Plane

The slow coordinates are ordered (T,Z), as in the moving mean gauge.

Equations

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

@[simp]

theorem NavierStokes.GaugeStateCoherence.bandSlowEquiv_apply (h : ℝ) (n m : ℕ) (s : Plane) : (bandSlowEquiv h n m) s = (ChartScales.Q n / ChartScales.Q m * s.1, (ChartScales.Q n / ChartScales.Q m) ^ CoordinateAlgebra.D h * s.2)

noncomputable def NavierStokes.GaugeStateCoherence.bandChartEquiv (h : ℝ) (n m k : ℕ) : PressureStream.Lift Plane ≃L[ℝ] PressureStream.Lift Plane

Band chart equiv, given by chartEquiv (bandScale n m) (bandScale_pos n m).ne' (bandSlowEquiv h n m) k.

Equations

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

@[simp]

theorem NavierStokes.GaugeStateCoherence.bandChartEquiv_apply (h : ℝ) (n m k : ℕ) (z : PressureStream.Lift Plane) : (bandChartEquiv h n m k) z = (bandScale n m * z.1, (bandSlowEquiv h n m) z.2.1, (TemporalMeanUpdate.coverMap k) z.2.2)

theorem NavierStokes.GaugeStateCoherence.qLength_bandSlowEquiv {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (n m : ℕ) {s : Plane} (hs : 0 < s.1) : VariableGaugeMean.qLength (2 * h) ((bandSlowEquiv h n m) s) = bandScale n m * VariableGaugeMean.qLength (2 * h) s

theorem NavierStokes.GaugeStateCoherence.radialFrequency_band_transport (h d M : ℝ) (n m k i ir : ℕ) (hi : i + k = ir) : MeanChartCompatibility.radialFrequency h n i d M * ChartScales.Lambda ^ k = MeanChartCompatibility.radialFrequency h m ir d M * bandScale n m ^ d

theorem NavierStokes.GaugeStateCoherence.similarityGaugeOn {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (d a b M : ℝ) (hab : a < b) (index : ℕ → ℕ) (n m k : ℕ) (hi : index n + k = index m) {V : Set Plane} (hV : ∀ s ∈ V, 0 < s.1) : GaugeOn V (bandScale n m) (↑(bandSlowEquiv h n m)) k (VariableGaugeMean.similarityGauge h d a b M hab index) (VariableGaugeMean.similarityGauge h d a b M hab index) n m

The similarity gauge satisfies all primitive transport laws with the actual band scales and actual common-index gap.

theorem NavierStokes.GaugeStateCoherence.bandScale_eq_ratioPower (n m : ℕ) : bandScale n m = PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q m) (1 / 2)

theorem NavierStokes.GaugeStateCoherence.bandVelocityScale_eq_ratioPower (h : ℝ) (n m : ℕ) : bandVelocityScale h n m = PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q m) (CoordinateAlgebra.A h)

theorem NavierStokes.GaugeStateCoherence.similarity_reconstruction_on {h d a b M : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (index : ℕ → ℕ) (n m k : ℕ) (hi : index n + k = index m) {V U : Set Plane} (hV : IsOpen V) (hU : IsOpen U) (htime : ∀ s ∈ V, 0 < s.1) (hmap : Set.MapsTo (⇑(bandSlowEquiv h n m)) V U) (C Cr : CorrectionState.Context (PressureStream.Lift Plane)) (s r : CorrectionState.State (PressureStream.Lift Plane)) (H : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (bandChartEquiv h n m k) (bandVelocityScale h n m) (bandScale n m) s r n m) (G : PhysicalResidualNaturality.ContextOn (PhysicalMeanDomain.slowDomain V) (bandChartEquiv h n m k) (bandVelocityScale h n m) (bandScale n m) C Cr n m) (hf : ContDiffOn ℝ (↑⊤) (r.gr Cr m) (PhysicalMeanDomain.slowDomain U)) (hp : PhysicalMeanDomain.PeriodicOn U (r.gr Cr m)) (hs : VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength (2 * h)) U (r.gr Cr m)) : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (bandChartEquiv h n m k) (bandVelocityScale h n m) (bandScale n m) (VariableGaugeMean.reconstructState (VariableGaugeMean.similarityGauge h d a b M hab index) C s) (VariableGaugeMean.reconstructState (VariableGaugeMean.similarityGauge h d a b M hab index) Cr r) n m ∧ ∀ z ∈ PhysicalMeanDomain.slowDomain V, ∀ (theta : ℝ) (i : Fin 3), VariableGaugeMean.pressureAliasState (VariableGaugeMean.similarityGauge h d a b M hab index) C s n (z, theta) i = bandVelocityScale h n m * bandVelocityScale h n m * bandScale n m * VariableGaugeMean.pressureAliasState (VariableGaugeMean.similarityGauge h d a b M hab index) Cr r m ((bandChartEquiv h n m k) z, theta) i

Concrete band/common-cover reconstruction, with the length and frequency transport laws derived from similarityGauge itself.

Actual support, on the same moving shell

theorem NavierStokes.GaugeStateCoherence.supportedGauge_of_scalarOn {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l u a b : ℝ} (hl : 0 < l) (P : S ≃L[ℝ] T) (k : ℕ) (ell : S → ℝ) (ell' : T → ℝ) {V : Set S} {U : Set T} (hmap : Set.MapsTo (⇑P) V U) (hlen : ∀ s ∈ V, ell' (P s) = l * ell s) {f : PressureStream.Lift S → ℝ} {fr : PressureStream.Lift T → ℝ} (he : PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (chartEquiv l ⋯ P k) u f fr) (hs : VariableGaugeMean.SupportedGauge a b ell' U fr) : VariableGaugeMean.SupportedGauge a b ell V f

theorem NavierStokes.GaugeStateCoherence.meanPressure_supported {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (M : ℝ) (ell : S → ℝ) (v : Plane) {U : Set S} (hU : IsOpen U) (hl : ∀ s ∈ U, 0 < ell s) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hs : VariableGaugeMean.SupportedGauge a b ell U f) : VariableGaugeMean.SupportedGauge a b ell U (VariableGaugeMean.meanPressure d a b M hab ell v f)

theorem NavierStokes.GaugeStateCoherence.reconstructState_pressure_supported {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : VariableGaugeMean.GaugeData S) (C : CorrectionState.Context (PressureStream.Lift S)) (s : CorrectionState.State (PressureStream.Lift S)) (n : ℕ) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) {U : Set S} (hU : IsOpen U) (hl : ∀ t ∈ U, 0 < g.length n t) (hf : ContDiffOn ℝ (↑⊤) (s.gr C n) (PhysicalMeanDomain.slowDomain U)) (hs : VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (g.length n) U (s.gr C n)) : VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (g.length n) U ((VariableGaugeMean.reconstructState g C s).pressure n)

theorem NavierStokes.GaugeStateCoherence.pressureAliasState_supported {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : VariableGaugeMean.GaugeData S) (C : CorrectionState.Context (PressureStream.Lift S)) (s : CorrectionState.State (PressureStream.Lift S)) (n : ℕ) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) {U : Set S} (hl : ∀ t ∈ U, 0 < g.length n t) (theta : ℝ) (i : Fin 3) : VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (g.length n) U fun (z : PressureStream.Lift S) => VariableGaugeMean.pressureAliasState g C s n (z, theta) i