The actual similarity-dependent mean gauge

The endpoints are multiplied by the actual sqrt(q). The cutoff and normalized density are defined explicitly, and the primitive is the existing integral operator evaluated with those endpoints on each slow fiber.

The estimates use the moving profile R / sqrt(q) and the full ordinary Fréchet derivatives. Their constants are uniform in the source family and the radial transport frequency. The exact cutoff alias is retained.

The final State theorems derive pressure, pressure-change and temporal increment classes from the actual input fields on the valid slow domain. The common torus index and its bounded gap from the native index remain explicit. This module does not assert arbitrary-power alias decay.

theorem NavierStokes.VariableGaugeMean.positiveRadius_scale {l : ℝ} (hl : l ≠ 0) (a r : ℝ) : RadialPullback.positiveRadius (l * a) (l * r) = l * RadialPullback.positiveRadius a r

theorem NavierStokes.VariableGaugeMean.powerChart_scale {l a : ℝ} (hl : 0 < l) (ha : 0 < a) (d r : ℝ) : RadialPullback.powerChart d (l * a) (l * r) = l ^ d * RadialPullback.powerChart d a r

theorem NavierStokes.VariableGaugeMean.physicalCutoff_scale {l a b : ℝ} (hl : 0 < l) (ha : 0 < a) (hab : a < b) (d r : ℝ) : RadialPullback.physicalCutoff d (l * a) (l * b) (l * r) = RadialPullback.physicalCutoff d a b r

noncomputable def NavierStokes.VariableGaugeMean.radialRatio {S : Type} (ell : S → ℝ) (z : PressureStream.Lift S) : ℝ

Radial ratio, given by z.1 / ell z.2.1.

Equations

• NavierStokes.VariableGaugeMean.radialRatio ell z = z.1 / ell z.2.1

noncomputable def NavierStokes.VariableGaugeMean.cutoff {S : Type} (d a b : ℝ) (ell : S → ℝ) (z : PressureStream.Lift S) : ℝ

Cutoff, given by RadialPullback.physicalCutoff d a b (radialRatio ell z).

Equations

• NavierStokes.VariableGaugeMean.cutoff d a b ell z = NavierStokes.RadialPullback.physicalCutoff d a b (NavierStokes.VariableGaugeMean.radialRatio ell z)

noncomputable def NavierStokes.VariableGaugeMean.density {S : Type} (a b : ℝ) (hab : a < b) (ell : S → ℝ) (z : PressureStream.Lift S) : ℝ

Density, given by (ell z.2.1)⁻¹ * PressureStream.rho a b hab (radialRatio ell z).

Equations

• NavierStokes.VariableGaugeMean.density a b hab ell z = (ell z.2.1)⁻¹ * NavierStokes.PressureStream.rho a b hab (NavierStokes.VariableGaugeMean.radialRatio ell z)

noncomputable def NavierStokes.VariableGaugeMean.SupportedGauge {S : Type} (a b : ℝ) (ell : S → ℝ) (U : Set S) (f : PressureStream.Lift S → ℝ) : Prop

Supported gauge, given by ∀ z, z.2.1 ∈ U → f z ≠ 0 → z.1 ∈ Icc (ell z.2.1 * a) (ell z.2.1 * b).

Equations

• NavierStokes.VariableGaugeMean.SupportedGauge a b ell U f = ∀ (z : NavierStokes.PressureStream.Lift S), z.2.1 ∈ U → f z ≠ 0 → z.1 ∈ Set.Icc (ell z.2.1 * a) (ell z.2.1 * b)

noncomputable def NavierStokes.VariableGaugeMean.compactPrimitive {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (ell : S → ℝ) (v : PressureStream.Plane) (f : PressureStream.Lift S → ℝ) (z : PressureStream.Lift S) : ℝ

Genuine integral with the actual endpoints on this slow fiber.

Equations

• NavierStokes.VariableGaugeMean.compactPrimitive d a b M ell v f z = NavierStokes.RadialPullback.physicalCompact d (ell z.2.1 * a) (ell z.2.1 * b) M (0, v) f z

noncomputable def NavierStokes.VariableGaugeMean.pressureSource {S : Type} (a b : ℝ) (hab : a < b) (ell : S → ℝ) (f : PressureStream.Lift S → ℝ) (z : PressureStream.Lift S) : ℝ

Pressure source, given by f z - density a b hab ell z * PressureStream.pressureMass f z.2.1.

Equations

• NavierStokes.VariableGaugeMean.pressureSource a b hab ell f z = f z - NavierStokes.VariableGaugeMean.density a b hab ell z * NavierStokes.PressureStream.pressureMass f z.2.1

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

Mean pressure, given by compactPrimitive d a b M ell v (pressureSource a b hab ell f).

Equations

• NavierStokes.VariableGaugeMean.meanPressure d a b M hab ell v f = NavierStokes.VariableGaugeMean.compactPrimitive d a b M ell v (NavierStokes.VariableGaugeMean.pressureSource a b hab ell f)

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

Stream potential, given by PressureStream.divideRadius (compactPrimitive d a b M ell v (PressureStream.weightedSource f)).

Equations

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

noncomputable def NavierStokes.VariableGaugeMean.compactAlias {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (ell : S → ℝ) (v : PressureStream.Plane) (f : PressureStream.Lift S → ℝ) (z : PressureStream.Lift S) : ℝ

Compact alias, given by RadialPullback.physicalAlias d (ell z.2.1 * a) (ell z.2.1 * b) M ((0 : S), v) f z.

Equations

• NavierStokes.VariableGaugeMean.compactAlias d a b M ell v f z = NavierStokes.RadialPullback.physicalAlias d (ell z.2.1 * a) (ell z.2.1 * b) M (0, v) f z

theorem NavierStokes.VariableGaugeMean.cutoff_eq_scaled {S : Type} {a b : ℝ} (ha : 0 < a) (hab : a < b) (d : ℝ) (ell : S → ℝ) (z : PressureStream.Lift S) (hl : 0 < ell z.2.1) : cutoff d a b ell z = RadialPullback.physicalCutoff d (ell z.2.1 * a) (ell z.2.1 * b) z.1

theorem NavierStokes.VariableGaugeMean.density_eq_scaled {S : Type} {a b : ℝ} (hab : a < b) (ell : S → ℝ) (z : PressureStream.Lift S) (hl : 0 < ell z.2.1) : density a b hab ell z = PressureStream.rho (ell z.2.1 * a) (ell z.2.1 * b) ⋯ z.1

theorem NavierStokes.VariableGaugeMean.density_integral {S : Type} {a b : ℝ} (hab : a < b) (ell : S → ℝ) (s : S) (hl : 0 < ell s) (Y : PressureStream.Plane) : ∫ (r : ℝ), density a b hab ell (r, s, Y) = 1

theorem NavierStokes.VariableGaugeMean.radialRatio_contDiffOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {ell : S → ℝ} {U : Set S} (hl : ContDiffOn ℝ (↑⊤) ell U) (hp : ∀ s ∈ U, 0 < ell s) : ContDiffOn ℝ (↑⊤) (radialRatio ell) (PhysicalMeanDomain.slowDomain U)

theorem NavierStokes.VariableGaugeMean.cutoff_contDiffOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a : ℝ} (ha : 0 < a) (d b : ℝ) {ell : S → ℝ} {U : Set S} (hl : ContDiffOn ℝ (↑⊤) ell U) (hp : ∀ s ∈ U, 0 < ell s) : ContDiffOn ℝ (↑⊤) (cutoff d a b ell) (PhysicalMeanDomain.slowDomain U)

theorem NavierStokes.VariableGaugeMean.density_contDiffOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} (hab : a < b) {ell : S → ℝ} {U : Set S} (hl : ContDiffOn ℝ (↑⊤) ell U) (hp : ∀ s ∈ U, 0 < ell s) : ContDiffOn ℝ (↑⊤) (density a b hab ell) (PhysicalMeanDomain.slowDomain U)

theorem NavierStokes.VariableGaugeMean.density_supported {S : Type} {a b : ℝ} (hab : a < b) (ell : S → ℝ) (U : Set S) (hl : ∀ s ∈ U, 0 < ell s) : SupportedGauge a b ell U (density a b hab ell)

theorem NavierStokes.VariableGaugeMean.pressureSource_supported {S : Type} {a b : ℝ} (hab : a < b) {ell : S → ℝ} {U : Set S} (hl : ∀ s ∈ U, 0 < ell s) {f : PressureStream.Lift S → ℝ} (hf : SupportedGauge a b ell U f) : SupportedGauge a b ell U (pressureSource a b hab ell f)

theorem NavierStokes.VariableGaugeMean.supportedGauge_containing {S : Type} {a b c e l L : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hleft : c ≤ l * a) (hright : L * b ≤ e) {ell : S → ℝ} {U : Set S} (hl : ∀ s ∈ U, ell s ∈ Set.Icc l L) {f : PressureStream.Lift S → ℝ} (hf : SupportedGauge a b ell U f) : PhysicalMeanDomain.SupportedOn c e U f

noncomputable def NavierStokes.VariableGaugeMean.qLength (coord : ℝ) (s : TorusInverse.Plane) : ℝ

Slow variables in this module follow the rank/domain convention (T,Z).

Equations

• NavierStokes.VariableGaugeMean.qLength coord s = √(NavierStokes.SimilarityCoordinates.coordinateQ coord s)

theorem NavierStokes.VariableGaugeMean.qLength_pos {coord : ℝ} (hc : 0 < coord) (hc1 : coord < 1) {s : TorusInverse.Plane} (hs : 0 < s.1) : 0 < qLength coord s

theorem NavierStokes.VariableGaugeMean.qLength_contDiffOn {coord : ℝ} (hc : 0 < coord) (hc1 : coord < 1) : ContDiffOn ℝ (↑⊤) (qLength coord) {s : TorusInverse.Plane | 0 < s.1}

noncomputable def NavierStokes.VariableGaugeMean.cutoffModel (d a b : ℝ) (y : MeanRankUpdate.ModelPoint) : ℝ

Cutoff model, given by RadialPullback.physicalCutoff d a b (y.2.1 / Real.sqrt y.1).

Equations

• NavierStokes.VariableGaugeMean.cutoffModel d a b y = NavierStokes.RadialPullback.physicalCutoff d a b (y.2.1 / √y.1)

noncomputable def NavierStokes.VariableGaugeMean.densityModel (a b : ℝ) (hab : a < b) (y : MeanRankUpdate.ModelPoint) : ℝ

Density model, given by (Real.sqrt y.1)⁻¹ * PressureStream.rho a b hab (y.2.1 / Real.sqrt y.1).

Equations

• NavierStokes.VariableGaugeMean.densityModel a b hab y = (√y.1)⁻¹ * NavierStokes.PressureStream.rho a b hab (y.2.1 / √y.1)

theorem NavierStokes.VariableGaugeMean.cutoffModel_contDiffOn {a : ℝ} (ha : 0 < a) (d b : ℝ) : ContDiffOn ℝ (↑⊤) (cutoffModel d a b) PhysicalCoordinateBounds.positiveTime

theorem NavierStokes.VariableGaugeMean.densityModel_contDiffOn {a b : ℝ} (hab : a < b) : ContDiffOn ℝ (↑⊤) (densityModel a b hab) PhysicalCoordinateBounds.positiveTime

theorem NavierStokes.VariableGaugeMean.cutoff_q_eq_kernel (coord d a b : ℝ) : cutoff d a b (qLength coord) = MeanRankUpdate.chartKernel coord (cutoffModel d a b)

theorem NavierStokes.VariableGaugeMean.density_q_eq_kernel (coord a b : ℝ) (hab : a < b) : density a b hab (qLength coord) = MeanRankUpdate.chartKernel coord (densityModel a b hab)

theorem NavierStokes.VariableGaugeMean.cutoff_q_finiteJets {coord qlo qhi rlo rhi a : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (hqlo : 0 < qlo) (ha : 0 < a) (d b : ℝ) {U : Set MeanRankUpdate.ChartPoint} (hT : ∀ p ∈ U, MeanRankUpdate.chartInput p ∈ PhysicalCoordinateBounds.positiveTime) (hq : ∀ p ∈ U, MeanRankUpdate.chartQ coord p ∈ Set.Icc qlo qhi) (hR : ∀ p ∈ U, p.1 ∈ Set.Icc rlo rhi) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ JetBounds.FiniteJetBound m (cutoff d a b (qLength coord)) U C

All joint cutoff jets, including actual derivatives of q, are derived from the inverse-coordinate jet theorem on its compact model box.

theorem NavierStokes.VariableGaugeMean.density_q_finiteJets {coord qlo qhi rlo rhi a b : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (hqlo : 0 < qlo) (hab : a < b) {U : Set MeanRankUpdate.ChartPoint} (hT : ∀ p ∈ U, MeanRankUpdate.chartInput p ∈ PhysicalCoordinateBounds.positiveTime) (hq : ∀ p ∈ U, MeanRankUpdate.chartQ coord p ∈ Set.Icc qlo qhi) (hR : ∀ p ∈ U, p.1 ∈ Set.Icc rlo rhi) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ JetBounds.FiniteJetBound m (density a b hab (qLength coord)) U C

noncomputable def NavierStokes.VariableGaugeMean.physicalPast {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (d c M : ℝ) (v : E) (f : ℝ × E → ℝ) (z : ℝ × E) : ℝ

Physical past, constructed using TransportPrimitive.pastIntegral.

Equations

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

theorem NavierStokes.VariableGaugeMean.normalizeSource_anchor_eq {E : Type} {c a b d : ℝ} (hc : 0 < c) (hca : c ≤ a) (hab : a < b) (hd : 0 < d) {f : ℝ × E → ℝ} (hs : RadialAlias.RadiallySupported a b f) : RadialPullback.normalizeSource d c f = RadialPullback.normalizeSource d a f

theorem NavierStokes.VariableGaugeMean.powerChart_anchor_lt {c a d R : ℝ} (hc : 0 < c) (hca : c ≤ a) (hd : 0 < d) (hR : R < a) : RadialPullback.powerChart d c R < a ^ d

theorem NavierStokes.VariableGaugeMean.physicalCompact_reference {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {c a b d M : ℝ} (hc : 0 < c) (hca : c ≤ a) (hab : a < b) (hd : 0 < d) (v : E) {f : ℝ × E → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) : RadialPullback.physicalCompact d a b M v f z = physicalPast d c M v f z - RadialPullback.physicalCutoff d a b z.1 * PressureStream.physicalTotal d c M v f z

Changing the auxiliary regularization radius leaves the actual primitive unchanged; only the compactification cutoff remains.

theorem NavierStokes.VariableGaugeMean.physicalPast_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {c e d M : ℝ} (hc : 0 < c) (hce : c < e) (hd : 0 < d) (v : E) {f : ℝ × E → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported c e f) : ContDiff ℝ (↑⊤) (physicalPast d c M v f)

theorem NavierStokes.VariableGaugeMean.physicalTotal_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {c e d M : ℝ} (hc : 0 < c) (hce : c < e) (hd : 0 < d) (v : E) {f : ℝ × E → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported c e f) : ContDiff ℝ (↑⊤) (PressureStream.physicalTotal d c M v f)

theorem NavierStokes.VariableGaugeMean.compactPrimitive_fiberLocal {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (ell : S → ℝ) (v : PressureStream.Plane) : PhysicalMeanDomain.FiberLocal (compactPrimitive d a b M ell v)

theorem NavierStokes.VariableGaugeMean.physicalPast_fiberLocal {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d c M : ℝ) (v : PressureStream.Plane) : PhysicalMeanDomain.FiberLocal (physicalPast d c M (0, v))

theorem NavierStokes.VariableGaugeMean.physicalTotal_fiberLocal {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d c M : ℝ) (v : PressureStream.Plane) : PhysicalMeanDomain.FiberLocal (PressureStream.physicalTotal d c M (0, v))

theorem NavierStokes.VariableGaugeMean.freezeSlow_contDiff {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {U : Set S} (hU : IsOpen U) {s : S} (hs : s ∈ U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) : ContDiff ℝ (↑⊤) (PhysicalMeanDomain.freezeSlow s f)

theorem NavierStokes.VariableGaugeMean.compactPrimitive_reference {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {c a b d M : ℝ} (hc : 0 < c) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (ell : S → ℝ) (v : PressureStream.Plane) {U : Set S} (hU : IsOpen U) (hl : ∀ s ∈ U, 0 < ell s) (hleft : ∀ s ∈ U, c ≤ ell s * a) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hs : SupportedGauge a b ell U f) (z : PressureStream.Lift S) (hz : z.2.1 ∈ U) : compactPrimitive d a b M ell v f z = physicalPast d c M (0, v) f z - cutoff d a b ell z * PressureStream.physicalTotal d c M (0, v) f z

theorem NavierStokes.VariableGaugeMean.physicalPast_contDiffOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {c e d M : ℝ} (hc : 0 < c) (hce : c < e) (hd : 0 < d) (v : PressureStream.Plane) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanDomain.SupportedOn c e U f) : ContDiffOn ℝ (↑⊤) (physicalPast d c M (0, v) f) (PhysicalMeanDomain.slowDomain U)

theorem NavierStokes.VariableGaugeMean.physicalTotal_contDiffOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {c e d M : ℝ} (hc : 0 < c) (hce : c < e) (hd : 0 < d) (v : PressureStream.Plane) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanDomain.SupportedOn c e U f) : ContDiffOn ℝ (↑⊤) (PressureStream.physicalTotal d c M (0, v) f) (PhysicalMeanDomain.slowDomain U)

theorem NavierStokes.VariableGaugeMean.compactPrimitive_contDiffOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {c e a b d M : ℝ} (hc : 0 < c) (hce : c < e) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : PressureStream.Plane) {ell : S → ℝ} {U : Set S} (hU : IsOpen U) (hell : ContDiffOn ℝ (↑⊤) ell U) (hl : ∀ s ∈ U, 0 < ell s) (hleft : ∀ s ∈ U, c ≤ ell s * a) (hright : ∀ s ∈ U, ell s * b ≤ e) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hs : SupportedGauge a b ell U f) : ContDiffOn ℝ (↑⊤) (compactPrimitive d a b M ell v f) (PhysicalMeanDomain.slowDomain U)

theorem NavierStokes.VariableGaugeMean.logWeight_zero_zero {a b R : ℝ} (ha : 0 < a) (hR : R ∈ Set.Ioo a b) : WeightedRadialPrimitive.logWeight 0 0 a b 0 R = 1

theorem NavierStokes.VariableGaugeMean.normalizeSource_unweighted_fiber {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {c e d : ℝ} (hc : 0 < c) (hce : c < e) (hd : 0 < d) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : PressureStream.Lift S → ℝ), ContDiff ℝ (↑⊤) f → RadialAlias.RadiallySupported c e f → ∀ (A : ℝ), 0 ≤ A → ∀ (s : S), (∀ j ≤ m, ∀ R ∈ Set.Ioo c e, ∀ (Y : PressureStream.Plane), ‖iteratedFDeriv ℝ j f (R, s, Y)‖ ≤ A) → ∀ (z : PressureStream.Lift S), z.2.1 = s → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (RadialPullback.normalizeSource d c f) z‖ ≤ K * A

theorem NavierStokes.VariableGaugeMean.transportIntegrals_jet_bound_fiber {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {c e M A : ℝ} (hce : c ≤ e) (v : PressureStream.Plane) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported c e f) (s : S) (j : ℕ) (hin : ∀ R ∈ Set.Icc c e, ∀ (Y : PressureStream.Plane), ‖iteratedFDeriv ℝ j f (R, s, Y)‖ ≤ A) (z : PressureStream.Lift S) (hz : z.2.1 = s) : ‖iteratedFDeriv ℝ j (TransportPrimitive.pastIntegral M (0, v) f) z‖ ≤ A * (e - c) ∧ ‖iteratedFDeriv ℝ j (TransportPrimitive.totalIntegral M (0, v) f) z‖ ≤ A * (e - c)

theorem NavierStokes.VariableGaugeMean.physicalIntegrals_finiteJets_fiber {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {c e d : ℝ} (hc : 0 < c) (hce : c < e) (hd : 0 < d) (rlo rhi : ℝ) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (M : ℝ) (v : PressureStream.Plane) (f : PressureStream.Lift S → ℝ), ContDiff ℝ (↑⊤) f → RadialAlias.RadiallySupported c e f → ∀ (A : ℝ), 0 ≤ A → ∀ (s : S), (∀ j ≤ m, ∀ R ∈ Set.Ioo c e, ∀ (Y : PressureStream.Plane), ‖iteratedFDeriv ℝ j f (R, s, Y)‖ ≤ A) → ∀ (z : PressureStream.Lift S), z.1 ∈ Set.Icc rlo rhi → z.2.1 = s → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (physicalPast d c M (0, v) f) z‖ ≤ K * A ∧ ‖iteratedFDeriv ℝ j (PressureStream.physicalTotal d c M (0, v) f) z‖ ≤ K * A

The integration and physical radial pullback cost is uniform in the transport frequency. Every input and output derivative is an actual joint jet.

structure NavierStokes.VariableGaugeMean.GaugeData (S : Type) : Type

Gauge data, collecting radial, length.

• radial : CorrectionState.ReconstructionData

  Radial of GaugeData, of type CorrectionState.ReconstructionData.

• length : ℕ → S → ℝ

  Length of GaugeData, of type ℕ → S → ℝ.

noncomputable def NavierStokes.VariableGaugeMean.similarityGauge (h d a b M : ℝ) (hab : a < b) (index : ℕ → ℕ) : GaugeData PressureStream.Plane

The actual similarity gauge in every normalized chart.

Equations

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

noncomputable def NavierStokes.VariableGaugeMean.reconstructState {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : GaugeData S) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) : CorrectionState.State (PressureStream.Lift S)

Reconstruct state as an element of CorrectionState.State (PressureStream.Lift S).

Equations

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

noncomputable def NavierStokes.VariableGaugeMean.pressureAliasState {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : GaugeData S) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) : CorrectionState.Oscillation (PressureStream.Lift S)

Pressure alias state as an element of CorrectionState.Oscillation (PressureStream.Lift S).

Equations

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

noncomputable def NavierStokes.VariableGaugeMean.temporalPotential {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : GaugeData S) (h : ℝ) (index : ℕ → ℕ) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) (n : ℕ) : PressureStream.Lift S → ℝ

Temporal potential, constructed using streamPotential.

Equations

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

noncomputable def NavierStokes.VariableGaugeMean.temporalIncrementState {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : GaugeData S) (h : ℝ) (index : ℕ → ℕ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) : MeanIncrementBounds.Triple (PressureStream.Lift S)

Temporal increment state, bundling radial, angular, axial.

Equations

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

noncomputable def NavierStokes.VariableGaugeMean.temporalAxialDifference {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : GaugeData S) (h : ℝ) (index : ℕ → ℕ) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) (n : ℕ) (z : PressureStream.Lift S) : ℝ

Temporal axial difference, constructed using MeanChartCompatibility.temporalAtIndex.

Equations

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

noncomputable def NavierStokes.VariableGaugeMean.temporalAliasState {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : GaugeData S) (h : ℝ) (index : ℕ → ℕ) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) : CorrectionState.Oscillation (PressureStream.Lift S)

Temporal alias state, defined pointwise by ![0, 0, -c.operators.fastTime (temporalAxialDifference g h index c u) n p.1].

Equations

• NavierStokes.VariableGaugeMean.temporalAliasState g h index c u n p = ![0, 0, -c.operators.fastTime (NavierStokes.VariableGaugeMean.temporalAxialDifference g h index c u) n p.1]

noncomputable def NavierStokes.VariableGaugeMean.temporalStageState {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : GaugeData S) (h : ℝ) (index : ℕ → ℕ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) : CorrectionState.State (PressureStream.Lift S)

Temporal stage state, given by reconstructState g c (u.addIncrement (temporalIncrementState g h index axial c u) 0 0 0 ⟨0, 0, temporalAliasState g h index c u⟩).

Equations

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

noncomputable def NavierStokes.VariableGaugeMean.rankPotential {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : GaugeData S) (r : CorrectionState.RankData S) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) (n : ℕ) : PressureStream.Lift S → ℝ

Rank potential, constructed using streamPotential.

Equations

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

noncomputable def NavierStokes.VariableGaugeMean.rankIncrementState {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : GaugeData S) (r : CorrectionState.RankData S) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) : MeanIncrementBounds.Triple (PressureStream.Lift S)

Rank increment state, bundling radial, angular, axial.

Equations

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

noncomputable def NavierStokes.VariableGaugeMean.rankStageState {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : GaugeData S) (r : CorrectionState.RankData S) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) : CorrectionState.State (PressureStream.Lift S)

Rank stage state, given by reconstructState g c (u.addIncrement (rankIncrementState g r axial c u) 0 0 0 CorrectionState.ExcludedErrors.zero).

Equations

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

theorem NavierStokes.VariableGaugeMean.pressureSource_eq_fixed {S : Type} {a b : ℝ} (hab : a < b) (ell : S → ℝ) (f : PressureStream.Lift S → ℝ) (z : PressureStream.Lift S) (hl : 0 < ell z.2.1) : pressureSource a b hab ell f z = PressureStream.pressureSource (ell z.2.1 * a) (ell z.2.1 * b) ⋯ f z

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

theorem NavierStokes.VariableGaugeMean.streamPotential_eq_fixed {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (ell : S → ℝ) (v : PressureStream.Plane) (f : PressureStream.Lift S → ℝ) (z : PressureStream.Lift S) : streamPotential d a b M ell v f z = PressureStream.streamPotential d (ell z.2.1 * a) (ell z.2.1 * b) M (0, v) f z

theorem NavierStokes.VariableGaugeMean.meanPressure_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 : PressureStream.Plane) (f : PressureStream.Lift S → ℝ) (z : PressureStream.Lift S) : PressureStream.meanPressure d a b M hab v f z = PressureStream.meanPressure d a' b' M hab' v f z

theorem NavierStokes.VariableGaugeMean.meanPressure_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 : PressureStream.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 : 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) : meanPressure d a b M hab ell v (MeanChartCompatibility.coverPull l P k u f) z = u / l * meanPressure d a b N hab ell' w f ((MeanChartCompatibility.chartLinear l (P.prodMap (TemporalMeanUpdate.coverMap k))) z)

Naturality on a single genuine slow fiber. The source is only required to be smooth and periodic on its open physical slow domain.

theorem NavierStokes.VariableGaugeMean.streamPotential_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 : PressureStream.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)) (hs : 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) : streamPotential d a b M ell v (MeanChartCompatibility.coverPull l P k u f) z = u / l * streamPotential d a b N ell' w f ((MeanChartCompatibility.chartLinear l (P.prodMap (TemporalMeanUpdate.coverMap k))) z)

theorem NavierStokes.VariableGaugeMean.product_jet_bound {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {f g : D → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) (hg : ContDiffOn ℝ (↑⊤) g U) {z : D} (hz : z ∈ U) {m j : ℕ} (hj : j ≤ m) {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hfa : ∀ i ≤ m, ‖iteratedFDeriv ℝ i f z‖ ≤ A) (hgb : ∀ i ≤ m, ‖iteratedFDeriv ℝ i g z‖ ≤ B) : ‖iteratedFDeriv ℝ j (fun (x : D) => f x * g x) z‖ ≤ 2 ^ m * A * B

theorem NavierStokes.VariableGaugeMean.sub_jet_norm_le {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {f g : D → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) (hg : ContDiffOn ℝ (↑⊤) g U) {z : D} (hz : z ∈ U) (j : ℕ) : ‖iteratedFDeriv ℝ j (fun (x : D) => f x - g x) z‖ ≤ ‖iteratedFDeriv ℝ j f z‖ + ‖iteratedFDeriv ℝ j g z‖

theorem NavierStokes.VariableGaugeMean.physicalIntegrals_finiteJets_local {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {c e d : ℝ} (hc : 0 < c) (hce : c < e) (hd : 0 < d) (rlo rhi : ℝ) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (U : Set S), IsOpen U → ∀ (M : ℝ) (v : PressureStream.Plane) (f : PressureStream.Lift S → ℝ), ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U) → PhysicalMeanDomain.SupportedOn c e U f → ∀ (A : ℝ), 0 ≤ A → ∀ (z : PressureStream.Lift S), z.2.1 ∈ U → z.1 ∈ Set.Icc rlo rhi → (∀ j ≤ m, ∀ R ∈ Set.Ioo c e, ∀ (Y : PressureStream.Plane), ‖iteratedFDeriv ℝ j f (R, z.2.1, Y)‖ ≤ A) → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (physicalPast d c M (0, v) f) z‖ ≤ K * A ∧ ‖iteratedFDeriv ℝ j (PressureStream.physicalTotal d c M (0, v) f) z‖ ≤ K * A

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

theorem NavierStokes.VariableGaugeMean.compactPrimitive_finiteJets_local {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {c e d a b : ℝ} (hc : 0 < c) (hce : c < e) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (rlo rhi : ℝ) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (U : Set S), IsOpen U → ∀ (ell : S → ℝ), ContDiffOn ℝ (↑⊤) ell U → (∀ s ∈ U, 0 < ell s) → (∀ s ∈ U, c ≤ ell s * a) → (∀ s ∈ U, ell s * b ≤ e) → ∀ (M : ℝ) (v : PressureStream.Plane) (f : PressureStream.Lift S → ℝ), ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U) → SupportedGauge a b ell U f → ∀ (A B : ℝ), 0 ≤ A → 0 ≤ B → ∀ (z : PressureStream.Lift S), z.2.1 ∈ U → z.1 ∈ Set.Icc rlo rhi → (∀ j ≤ m, ∀ R ∈ Set.Ioo c e, ∀ (Y : PressureStream.Plane), ‖iteratedFDeriv ℝ j f (R, z.2.1, Y)‖ ≤ A) → (∀ j ≤ m, ‖iteratedFDeriv ℝ j (cutoff d a b ell) z‖ ≤ B) → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (compactPrimitive d a b M ell v f) z‖ ≤ K * (1 + 2 ^ m * B) * A

Full Leibniz control with an explicit cutoff-jet bound. The integration constant is chosen before the domain, scale function, frequency and source.

noncomputable def NavierStokes.VariableGaugeMean.slowToChartTZ (h : ℝ) (n : ℕ) : TorusInverse.Plane →L[ℝ] TorusInverse.Plane

The same physical change, in the rank/domain order (T,Z).

Equations

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

noncomputable def NavierStokes.VariableGaugeMean.swapSlow : PressureStream.Lift TorusInverse.Plane →L[ℝ] PressureStream.Lift TorusInverse.Plane

Swap slow as an element of PressureStream.Lift Plane →L[ℝ] PressureStream.Lift Plane.

Equations

• NavierStokes.VariableGaugeMean.swapSlow = (ContinuousLinearMap.id ℝ ℝ).prodMap ((↑(ContinuousLinearEquiv.prodComm ℝ ℝ ℝ)).prodMap (ContinuousLinearMap.id ℝ NavierStokes.TorusInverse.Plane))

noncomputable def NavierStokes.VariableGaugeMean.physicalToChartTZ (h : ℝ) (n i : ℕ) : PressureStream.Lift TorusInverse.Plane →L[ℝ] PressureStream.Lift TorusInverse.Plane

Physical to chart TZ, given by chartLinear (chartScale n) ((slowToChartTZ h n).prodMap (TemporalMeanUpdate.coverMap i)).

Equations

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

theorem NavierStokes.VariableGaugeMean.physicalToChartTZ_swap (h : ℝ) (n i : ℕ) (z : PressureStream.Lift TorusInverse.Plane) : (physicalToChartTZ h n i) (swapSlow z) = swapSlow ((MeanChartCompatibility.physicalToChart h n i) z)

noncomputable def NavierStokes.VariableGaugeMean.fieldOnPhysicalTZ (h : ℝ) (n i : ℕ) (a : ℝ) (f : PressureStream.Lift TorusInverse.Plane → ℝ) : PressureStream.Lift TorusInverse.Plane → ℝ

Field on physical TZ, given by coverPull (chartScale n) (slowToChartTZ h n) i (ChartScales.Q n ^ (-a)) f.

Equations

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

theorem NavierStokes.VariableGaugeMean.qLength_chart {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (n : ℕ) {s : TorusInverse.Plane} (hs : 0 < s.1) : qLength (2 * h) ((slowToChartTZ h n) s) = MeanChartCompatibility.chartScale n * qLength (2 * h) s

theorem NavierStokes.VariableGaugeMean.cutoff_chart {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (n i : ℕ) (d a b : ℝ) {z : PressureStream.Lift TorusInverse.Plane} (hz : 0 < z.2.1.1) : cutoff d a b (qLength (2 * h)) ((physicalToChartTZ h n i) z) = cutoff d a b (qLength (2 * h)) z

theorem NavierStokes.VariableGaugeMean.density_chart {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (n i : ℕ) {a b : ℝ} (hab : a < b) {z : PressureStream.Lift TorusInverse.Plane} (hz : 0 < z.2.1.1) : density a b hab (qLength (2 * h)) ((physicalToChartTZ h n i) z) = (MeanChartCompatibility.chartScale n)⁻¹ * density a b hab (qLength (2 * h)) z

theorem NavierStokes.VariableGaugeMean.physicalMeanPressure_naturality {h d a b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (n i : ℕ) (M : ℝ) {U : Set TorusInverse.Plane} (hU : IsOpen U) {f : PressureStream.Lift TorusInverse.Plane → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hp : PhysicalMeanDomain.PeriodicOn U f) (hs : SupportedGauge a b (qLength (2 * h)) U f) (z : PressureStream.Lift TorusInverse.Plane) (hz : 0 < z.2.1.1) (hzU : (slowToChartTZ h n) z.2.1 ∈ U) : meanPressure d a b M hab (qLength (2 * h)) (TorusInverse.vector TorusInverse.Direction.radial) (fieldOnPhysicalTZ h n i (2 * CoordinateAlgebra.A h + 1 / 2) f) z = fieldOnPhysicalTZ h n i (2 * CoordinateAlgebra.A h) (meanPressure d a b (MeanChartCompatibility.radialFrequency h n i d M) hab (qLength (2 * h)) (TorusInverse.vector TorusInverse.Direction.radial) f) z

The actual variable-gauge chart pressures are the same physical operator, with the exact pressure and momentum units.

theorem NavierStokes.VariableGaugeMean.stream_unit_factor (h : ℝ) (n : ℕ) : ChartScales.Q n ^ (-CoordinateAlgebra.A h) / MeanChartCompatibility.chartScale n = ChartScales.Q n ^ (-(CoordinateAlgebra.A h - 1 / 2))

theorem NavierStokes.VariableGaugeMean.physicalStreamPotential_naturality {h d a b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (n i : ℕ) (M : ℝ) {U : Set TorusInverse.Plane} (hU : IsOpen U) {f : PressureStream.Lift TorusInverse.Plane → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hs : SupportedGauge a b (qLength (2 * h)) U f) (z : PressureStream.Lift TorusInverse.Plane) (hz : 0 < z.2.1.1) (hzU : (slowToChartTZ h n) z.2.1 ∈ U) : streamPotential d a b M (qLength (2 * h)) (TorusInverse.vector TorusInverse.Direction.radial) (fieldOnPhysicalTZ h n i (CoordinateAlgebra.A h) f) z = fieldOnPhysicalTZ h n i (CoordinateAlgebra.A h - 1 / 2) (streamPotential d a b (MeanChartCompatibility.radialFrequency h n i d M) (qLength (2 * h)) (TorusInverse.vector TorusInverse.Direction.radial) f) z

theorem NavierStokes.VariableGaugeMean.iteratedFDeriv_supportedGauge_fiber {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a b : ℝ} {ell : S → ℝ} {U : Set S} (hU : IsOpen U) (hell : ContinuousOn ell U) {f : PressureStream.Lift S → V} (hs : ∀ (z : PressureStream.Lift S), z.2.1 ∈ U → f z ≠ 0 → z.1 ∈ Set.Icc (ell z.2.1 * a) (ell z.2.1 * b)) {s : S} (hsU : s ∈ U) (j : ℕ) : RadialAlias.RadiallySupported (ell s * a) (ell s * b) (PhysicalMeanDomain.freezeSlow s (iteratedFDeriv ℝ j f))

theorem NavierStokes.VariableGaugeMean.iteratedFDeriv_zero_outsideGauge {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a b : ℝ} {ell : S → ℝ} {U : Set S} (hU : IsOpen U) (hell : ContinuousOn ell U) {f : PressureStream.Lift S → V} (hf : ContDiff ℝ (↑⊤) f) (hs : ∀ (z : PressureStream.Lift S), z.2.1 ∈ U → f z ≠ 0 → z.1 ∈ Set.Icc (ell z.2.1 * a) (ell z.2.1 * b)) {z : PressureStream.Lift S} (hz : z.2.1 ∈ U) (hR : z.1 ∉ Set.Ioo (ell z.2.1 * a) (ell z.2.1 * b)) (j : ℕ) : iteratedFDeriv ℝ j f z = 0

theorem NavierStokes.VariableGaugeMean.integral_scaled {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {l : ℝ} (hl : l ≠ 0) (f : ℝ → V) (a b : ℝ) : ∫ (x : ℝ) in l * a..l * b, f x = l • ∫ (x : ℝ) in a..b, f (l * x)

theorem NavierStokes.VariableGaugeMean.radialScale_supported {E V : Type} [NormedAddCommGroup V] {l a b : ℝ} (hl : 0 < l) {f : ℝ × E → V} (hs : RadialAlias.RadiallySupported (l * a) (l * b) f) : RadialAlias.RadiallySupported a b fun (z : ℝ × E) => f (l * z.1, z.2)

theorem NavierStokes.VariableGaugeMean.radialSlice_scaled {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {l : ℝ} (hl : l ≠ 0) (M : ℝ) (v : E) (f : ℝ × E → V) (z : ℝ × E) (s : ℝ) : WeightedRadialPrimitive.radialSlice (M * l) v (fun (q : ℝ × E) => f (l * q.1, q.2)) (z.1 / l, z.2) s = WeightedRadialPrimitive.radialSlice M v f z (l * s)

theorem NavierStokes.VariableGaugeMean.pastIntegral_scaled {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {l a b : ℝ} (hl : 0 < l) (M : ℝ) (v : E) {f : ℝ × E → V} (hf : Continuous f) (hs : RadialAlias.RadiallySupported (l * a) (l * b) f) (z : ℝ × E) : TransportPrimitive.pastIntegral M v f z = l • TransportPrimitive.pastIntegral (M * l) v (fun (q : ℝ × E) => f (l * q.1, q.2)) (z.1 / l, z.2)

theorem NavierStokes.VariableGaugeMean.futureIntegral_scaled {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {l a b : ℝ} (hl : 0 < l) (M : ℝ) (v : E) {f : ℝ × E → V} (hf : Continuous f) (hs : RadialAlias.RadiallySupported (l * a) (l * b) f) (z : ℝ × E) : TransportPrimitive.futureIntegral M v f z = l • TransportPrimitive.futureIntegral (M * l) v (fun (q : ℝ × E) => f (l * q.1, q.2)) (z.1 / l, z.2)

theorem NavierStokes.VariableGaugeMean.scaled_transport_past_left_uniform {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b cL cR L : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (hL : 0 < L) (p : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (l : ℝ), 0 < l → l ≤ L → ∀ (M : ℝ) (v : E) (f : ℝ × E → V), Continuous f → RadialAlias.RadiallySupported (l * a) (l * b) f → ∀ (A : ℝ), 0 ≤ A → (∀ (R : ℝ), R / l ∈ Set.Ioo a b → ∀ (Y : E), ‖f (R, Y)‖ ≤ A * WeightedRadialPrimitive.logWeight cL cR a b p (R / l)) → ∀ (z : ℝ × E), z.1 / l ∈ Set.Ioo a b → WeightedRadialPrimitive.logPosition a (z.1 / l) ≤ WeightedRadialPrimitive.logLength a b / 2 → ‖TransportPrimitive.pastIntegral M v f z‖ ≤ K * A * WeightedRadialPrimitive.logWeight cL cR a b p (z.1 / l)

theorem NavierStokes.VariableGaugeMean.scaled_transport_future_right_uniform {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b cL cR L : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (hL : 0 < L) (p : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (l : ℝ), 0 < l → l ≤ L → ∀ (M : ℝ) (v : E) (f : ℝ × E → V), Continuous f → RadialAlias.RadiallySupported (l * a) (l * b) f → ∀ (A : ℝ), 0 ≤ A → (∀ (R : ℝ), R / l ∈ Set.Ioo a b → ∀ (Y : E), ‖f (R, Y)‖ ≤ A * WeightedRadialPrimitive.logWeight cL cR a b p (R / l)) → ∀ (z : ℝ × E), z.1 / l ∈ Set.Ioo a b → WeightedRadialPrimitive.logLength a b / 2 ≤ WeightedRadialPrimitive.logPosition a (z.1 / l) → ‖TransportPrimitive.futureIntegral M v f z‖ ≤ K * A * WeightedRadialPrimitive.logWeight cL cR a b p (z.1 / l)

theorem NavierStokes.VariableGaugeMean.normalizeSource_gauge_finiteJets {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {c e a b d : ℝ} (hc : 0 < c) (hce : c < e) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (cL cR : ℝ) (p m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (l : ℝ), 0 < l → c ≤ l * a → l * b ≤ e → ∀ (f : PressureStream.Lift S → ℝ), ContDiff ℝ (↑⊤) f → ∀ (A : ℝ), 0 ≤ A → ∀ (s : S), (∀ j ≤ m, ∀ (R : ℝ), R / l ∈ Set.Ioo a b → ∀ (Y : PressureStream.Plane), ‖iteratedFDeriv ℝ j f (R, s, Y)‖ ≤ A * WeightedRadialPrimitive.logWeight cL cR a b p (R / l)) → ∀ (z : PressureStream.Lift S), z.1 / l ^ d ∈ Set.Ioo (a ^ d) (b ^ d) → z.2.1 = s → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (RadialPullback.normalizeSource d c f) z‖ ≤ K * A * WeightedRadialPrimitive.logWeight (d ^ 2 * cL) (d ^ 2 * cR) (a ^ d) (b ^ d) p (z.1 / l ^ d)

The fixed normalization map has uniform weighted jet bounds when the weight is read on any admissible dilated radial fiber.

theorem NavierStokes.VariableGaugeMean.normalizeSource_supportedGauge {S : Type} {c e a b d : ℝ} (hc : 0 < c) (hce : c < e) (ha : 0 < a) (hab : a < b) (hd : 0 < d) {ell : S → ℝ} {U : Set S} (hl : ∀ s ∈ U, 0 < ell s) {f : PressureStream.Lift S → ℝ} (hs : RadialAlias.RadiallySupported c e f) (hsg : SupportedGauge a b ell U f) : SupportedGauge (a ^ d) (b ^ d) (fun (s : S) => ell s ^ d) U (RadialPullback.normalizeSource d c f)

noncomputable def NavierStokes.VariableGaugeMean.normalizedCutoff {S : Type} (a b : ℝ) (ell : S → ℝ) (z : PressureStream.Lift S) : ℝ

Normalized cutoff, given by TransportPrimitive.interiorCutoff a b (radialRatio ell z).

Equations

• NavierStokes.VariableGaugeMean.normalizedCutoff a b ell z = NavierStokes.TransportPrimitive.interiorCutoff a b (NavierStokes.VariableGaugeMean.radialRatio ell z)

noncomputable def NavierStokes.VariableGaugeMean.transportGauge {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (a b M : ℝ) (ell : S → ℝ) (v : PressureStream.Plane) (f : PressureStream.Lift S → ℝ) (z : PressureStream.Lift S) : ℝ

Transport gauge, constructed using TransportPrimitive.pastIntegral.

Equations

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

theorem NavierStokes.VariableGaugeMean.normalizedCutoff_contDiffOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (a b : ℝ) {ell : S → ℝ} {U : Set S} (hell : ContDiffOn ℝ (↑⊤) ell U) (hl : ∀ s ∈ U, 0 < ell s) : ContDiffOn ℝ (↑⊤) (normalizedCutoff a b ell) (PhysicalMeanDomain.slowDomain U)

theorem NavierStokes.VariableGaugeMean.transportGauge_contDiffOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {c e a b M : ℝ} {ell : S → ℝ} {U : Set S} (hell : ContDiffOn ℝ (↑⊤) ell U) (hl : ∀ s ∈ U, 0 < ell s) (v : PressureStream.Plane) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported c e f) : ContDiffOn ℝ (↑⊤) (transportGauge a b M ell v f) (PhysicalMeanDomain.slowDomain U)

theorem NavierStokes.VariableGaugeMean.transportGauge_finiteJets {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {c e a b cL cR L : ℝ} (hce : c < e) (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (hL : 0 < L) (p m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (U : Set S), IsOpen U → ∀ (ell : S → ℝ), ContDiffOn ℝ (↑⊤) ell U → (∀ s ∈ U, 0 < ell s) → (∀ s ∈ U, ell s ≤ L) → ∀ (M : ℝ) (v : PressureStream.Plane) (f : PressureStream.Lift S → ℝ), ContDiff ℝ (↑⊤) f → RadialAlias.RadiallySupported c e f → SupportedGauge a b ell U f → ∀ (A B : ℝ), 0 ≤ A → 0 ≤ B → ∀ (z : PressureStream.Lift S), z.2.1 ∈ U → z.1 / ell z.2.1 ∈ Set.Ioo a b → (∀ j ≤ m, ∀ (R : ℝ), R / ell z.2.1 ∈ Set.Ioo a b → ∀ (Y : PressureStream.Plane), ‖iteratedFDeriv ℝ j f (R, z.2.1, Y)‖ ≤ A * WeightedRadialPrimitive.logWeight cL cR a b p (R / ell z.2.1)) → (∀ j ≤ m, ‖iteratedFDeriv ℝ j (normalizedCutoff a b ell) z‖ ≤ B) → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (transportGauge a b M ell v f) z‖ ≤ K * (1 + B) * A * WeightedRadialPrimitive.logWeight cL cR a b p (z.1 / ell z.2.1)

No derivative is taken after the scalar change of integration variable. The estimate uses the original full joint derivatives under the fixed-u integral.

theorem NavierStokes.VariableGaugeMean.radial_comp_finiteJets_local {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (a b : ℝ) {φ : ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (U : Set S), IsOpen U → ∀ (F : PressureStream.Lift S → ℝ), ContDiffOn ℝ (↑⊤) F (PhysicalMeanDomain.slowDomain U) → ∀ (z : PressureStream.Lift S), z.2.1 ∈ U → z.1 ∈ Set.Icc a b → ∀ (C : ℝ), 0 ≤ C → (∀ i ≤ m, ‖iteratedFDeriv ℝ i F (RadialPullback.liftChart φ z)‖ ≤ C) → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (F ∘ RadialPullback.liftChart φ) z‖ ≤ K * C

theorem NavierStokes.VariableGaugeMean.cutoff_eq_normalizedCutoff {S : Type} {c a b d : ℝ} (hc : 0 < c) (ha : 0 < a) (ell : S → ℝ) (z : PressureStream.Lift S) (hl : 0 < ell z.2.1) (hleft : c ≤ ell z.2.1 * a) (hR : z.1 / ell z.2.1 ∈ Set.Ioo a b) : cutoff d a b ell z = normalizedCutoff (a ^ d) (b ^ d) (fun (s : S) => ell s ^ d) (RadialPullback.liftChart (RadialPullback.powerChart d c) z)

theorem NavierStokes.VariableGaugeMean.compactPrimitive_eq_transportGauge {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {c a b d M : ℝ} (hc : 0 < c) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (ell : S → ℝ) (v : PressureStream.Plane) {U : Set S} (hU : IsOpen U) (hl : ∀ s ∈ U, 0 < ell s) (hleft : ∀ s ∈ U, c ≤ ell s * a) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hs : SupportedGauge a b ell U f) (z : PressureStream.Lift S) (hz : z.2.1 ∈ U) (hR : z.1 / ell z.2.1 ∈ Set.Ioo a b) : compactPrimitive d a b M ell v f z = transportGauge (a ^ d) (b ^ d) M (fun (s : S) => ell s ^ d) v (RadialPullback.normalizeSource d c f) (RadialPullback.liftChart (RadialPullback.powerChart d c) z)

theorem NavierStokes.VariableGaugeMean.compactPrimitive_transportGauge_germ {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {c a b d M : ℝ} (hc : 0 < c) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (ell : S → ℝ) (v : PressureStream.Plane) {U : Set S} (hU : IsOpen U) (hell : ContDiffOn ℝ (↑⊤) ell U) (hl : ∀ s ∈ U, 0 < ell s) (hleft : ∀ s ∈ U, c ≤ ell s * a) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hs : SupportedGauge a b ell U f) (z : PressureStream.Lift S) (hz : z.2.1 ∈ U) (hR : z.1 / ell z.2.1 ∈ Set.Ioo a b) : compactPrimitive d a b M ell v f =ᶠ[nhds z] transportGauge (a ^ d) (b ^ d) M (fun (s : S) => ell s ^ d) v (RadialPullback.normalizeSource d c f) ∘ RadialPullback.liftChart (RadialPullback.powerChart d c)

theorem NavierStokes.VariableGaugeMean.qLength_reference_bounds {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) : ∃ (c : ℝ) (e : ℝ) (L : ℝ), 0 < c ∧ c < e ∧ 0 < L ∧ (∀ s ∈ U.carrier, 0 < qLength coord s) ∧ (∀ s ∈ U.carrier, c ≤ qLength coord s * a) ∧ (∀ s ∈ U.carrier, qLength coord s * b ≤ e) ∧ ∀ s ∈ U.carrier, qLength coord s ≤ L

A fixed containing shell is used only to normalize the integral. The weight and the actual cutoff continue to use the moving profile endpoints.

noncomputable def NavierStokes.VariableGaugeMean.normalizedCutoffModel (d a b : ℝ) (y : MeanRankUpdate.ModelPoint) : ℝ

Normalized cutoff model, given by TransportPrimitive.interiorCutoff (a ^ d) (b ^ d) (y.2.1 / (Real.sqrt y.1) ^ d).

Equations

• NavierStokes.VariableGaugeMean.normalizedCutoffModel d a b y = NavierStokes.TransportPrimitive.interiorCutoff (a ^ d) (b ^ d) (y.2.1 / √y.1 ^ d)

theorem NavierStokes.VariableGaugeMean.normalizedCutoffModel_contDiffOn (d a b : ℝ) : ContDiffOn ℝ (↑⊤) (normalizedCutoffModel d a b) PhysicalCoordinateBounds.positiveTime

theorem NavierStokes.VariableGaugeMean.normalizedCutoff_q_eq_kernel (coord d a b : ℝ) : (normalizedCutoff (a ^ d) (b ^ d) fun (s : TorusInverse.Plane) => qLength coord s ^ d) = MeanRankUpdate.chartKernel coord (normalizedCutoffModel d a b)

theorem NavierStokes.VariableGaugeMean.normalizedCutoff_q_finiteJets {coord qlo qhi rlo rhi : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (hqlo : 0 < qlo) (d a b : ℝ) {V : Set MeanRankUpdate.ChartPoint} (hT : ∀ z ∈ V, MeanRankUpdate.chartInput z ∈ PhysicalCoordinateBounds.positiveTime) (hq : ∀ z ∈ V, MeanRankUpdate.chartQ coord z ∈ Set.Icc qlo qhi) (hR : ∀ z ∈ V, z.1 ∈ Set.Icc rlo rhi) (m : ℕ) : ∃ (B : ℝ), 0 ≤ B ∧ JetBounds.FiniteJetBound m (normalizedCutoff (a ^ d) (b ^ d) fun (s : TorusInverse.Plane) => qLength coord s ^ d) V B

theorem NavierStokes.VariableGaugeMean.compactPrimitive_q_finiteJets_global {coord a b c e d cL cR L : ℝ} (U : LocalSignedRequest.SlowRegion coord) (hc : 0 < c) (hce : c < e) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (hL : 0 < L) (hl : ∀ s ∈ U.carrier, 0 < qLength coord s) (hleft : ∀ s ∈ U.carrier, c ≤ qLength coord s * a) (hright : ∀ s ∈ U.carrier, qLength coord s * b ≤ e) (hupp : ∀ s ∈ U.carrier, qLength coord s ≤ L) (p m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (M : ℝ) (v : PressureStream.Plane) (f : PressureStream.Lift PressureStream.Plane → ℝ), ContDiff ℝ (↑⊤) f → RadialAlias.RadiallySupported c e f → SupportedGauge a b (qLength coord) U.carrier f → ∀ (A : ℝ), 0 ≤ A → ∀ (z : PressureStream.Lift PressureStream.Plane), z.2.1 ∈ U.carrier → z.1 / qLength coord z.2.1 ∈ Set.Ioo a b → (∀ j ≤ m, ∀ (R : ℝ), R / qLength coord z.2.1 ∈ Set.Ioo a b → ∀ (Y : PressureStream.Plane), ‖iteratedFDeriv ℝ j f (R, z.2.1, Y)‖ ≤ A * WeightedRadialPrimitive.logWeight cL cR a b p (R / qLength coord z.2.1)) → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (compactPrimitive d a b M (qLength coord) v f) z‖ ≤ K * A * WeightedRadialPrimitive.logWeight cL cR a b p (z.1 / qLength coord z.2.1)

Uniform finite seminorm inequality for the actual q-gauge primitive. The constant precedes all frequencies, sources, amplitudes and evaluation points.

theorem NavierStokes.VariableGaugeMean.localize_supportedGauge {S : Type} {a b : ℝ} {ell : S → ℝ} {U : Set S} {f : PressureStream.Lift S → ℝ} (hs : SupportedGauge a b ell U f) (χ : S → ℝ) : SupportedGauge a b ell U (PhysicalMeanDomain.localize χ f)

theorem NavierStokes.VariableGaugeMean.iteratedFDeriv_zero_outsideGauge_on {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b : ℝ} {ell : S → ℝ} {U : Set S} (hU : IsOpen U) (hell : ContinuousOn ell U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hs : SupportedGauge a b ell U f) {z : PressureStream.Lift S} (hz : z.2.1 ∈ U) (hR : z.1 ∉ Set.Ioo (ell z.2.1 * a) (ell z.2.1 * b)) (j : ℕ) : iteratedFDeriv ℝ j f z = 0

theorem NavierStokes.VariableGaugeMean.compactPrimitive_q_contDiffOn {coord a b d : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (M : ℝ) (v : PressureStream.Plane) {f : LocalSignedRequest.Point → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) (hs : SupportedGauge a b (qLength coord) U.carrier f) : ContDiffOn ℝ (↑⊤) (compactPrimitive d a b M (qLength coord) v f) (PhysicalMeanDomain.slowDomain U.carrier)

theorem NavierStokes.VariableGaugeMean.compactPrimitive_q_finiteJets {coord a b d cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (p m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (M : ℝ) (v : PressureStream.Plane) (f : LocalSignedRequest.Point → ℝ), ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier) → SupportedGauge a b (qLength coord) U.carrier f → ∀ (A : ℝ), 0 ≤ A → ∀ (z : LocalSignedRequest.Point), z.2.1 ∈ U.carrier → z.1 / qLength coord z.2.1 ∈ Set.Ioo a b → (∀ j ≤ m, ∀ (R : ℝ), R / qLength coord z.2.1 ∈ Set.Ioo a b → ∀ (Y : PressureStream.Plane), ‖iteratedFDeriv ℝ j f (R, z.2.1, Y)‖ ≤ A * WeightedRadialPrimitive.logWeight cL cR a b p (R / qLength coord z.2.1)) → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (compactPrimitive d a b M (qLength coord) v f) z‖ ≤ K * A * WeightedRadialPrimitive.logWeight cL cR a b p (z.1 / qLength coord z.2.1)

theorem NavierStokes.VariableGaugeMean.meanClass_compactPrimitive {coord a b d cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (hab : a < b) (hd : 0 < d) {α : ℝ} {f : ℕ → LocalSignedRequest.Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : ∀ (n : ℕ), SupportedGauge a b (qLength coord) U.carrier (f n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α fun (n : ℕ) => compactPrimitive d a b (M n) (qLength coord) (v n) (f n)

theorem NavierStokes.VariableGaugeMean.meanClass_moving_localBandJets {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {α : ℝ} {f : ℕ → LocalSignedRequest.Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : ∀ (n : ℕ), SupportedGauge a b (qLength coord) U.carrier (f n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) : PhysicalMeanDomain.LocalBandJets U.carrier ε L α f

theorem NavierStokes.VariableGaugeMean.localBandJets_unweighted_moving {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {α : ℝ} {f : ℕ → LocalSignedRequest.Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hb : PhysicalMeanDomain.LocalBandJets U.carrier ε L α f) : WeightedClasses.UnweightedClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f

theorem NavierStokes.VariableGaugeMean.meanClass_pressureMass_moving {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (hab : a < b) {α : ℝ} {f : ℕ → LocalSignedRequest.Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : ∀ (n : ℕ), SupportedGauge a b (qLength coord) U.carrier (f n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) : WeightedClasses.UnweightedClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α fun (n : ℕ) => MeanMomentBounds.liftedPressureMass (f n)

theorem NavierStokes.VariableGaugeMean.chartKernel_unweighted_moving {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (g : MeanRankUpdate.ModelPoint → ℝ) (hg : ContDiffOn ℝ (↑⊤) g PhysicalCoordinateBounds.positiveTime) : WeightedClasses.UnweightedClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) 0 fun (x : ℕ) => MeanRankUpdate.chartKernel coord g

theorem NavierStokes.VariableGaugeMean.inverseLength_unweighted_moving {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) : WeightedClasses.UnweightedClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) 0 fun (x : ℕ) (z : LocalSignedRequest.Point) => (qLength coord z.2.1)⁻¹

theorem NavierStokes.VariableGaugeMean.density_meanClass_moving {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (hab : a < b) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) 0 fun (x : ℕ) => density a b hab (qLength coord)

theorem NavierStokes.VariableGaugeMean.pressureSource_q_contDiffOn {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) {f : LocalSignedRequest.Point → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) (hs : SupportedGauge a b (qLength coord) U.carrier f) : ContDiffOn ℝ (↑⊤) (pressureSource a b hab (qLength coord) f) (PhysicalMeanDomain.slowDomain U.carrier)

theorem NavierStokes.VariableGaugeMean.meanPressure_q_contDiffOn {coord a b d : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (M : ℝ) (v : PressureStream.Plane) {f : LocalSignedRequest.Point → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) (hs : SupportedGauge a b (qLength coord) U.carrier f) : ContDiffOn ℝ (↑⊤) (meanPressure d a b M hab (qLength coord) v f) (PhysicalMeanDomain.slowDomain U.carrier)

theorem NavierStokes.VariableGaugeMean.meanPressure_q_supportedGauge {coord a b d : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (M : ℝ) (v : PressureStream.Plane) {f : LocalSignedRequest.Point → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) (hs : SupportedGauge a b (qLength coord) U.carrier f) : SupportedGauge a b (qLength coord) U.carrier (meanPressure d a b M hab (qLength coord) v f)

theorem NavierStokes.VariableGaugeMean.meanClass_pressureSource {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (hab : a < b) {α : ℝ} {f : ℕ → LocalSignedRequest.Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : ∀ (n : ℕ), SupportedGauge a b (qLength coord) U.carrier (f n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α fun (n : ℕ) => pressureSource a b hab (qLength coord) (f n)

theorem NavierStokes.VariableGaugeMean.meanClass_meanPressure {coord a b d cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (hab : a < b) (hd : 0 < d) {α : ℝ} {f : ℕ → LocalSignedRequest.Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : ∀ (n : ℕ), SupportedGauge a b (qLength coord) U.carrier (f n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α fun (n : ℕ) => meanPressure d a b (M n) hab (qLength coord) (v n) (f n)

theorem NavierStokes.VariableGaugeMean.compactPrimitive_periodicOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (ell : S → ℝ) (v : PressureStream.Plane) {U : Set S} {f : PressureStream.Lift S → ℝ} (hp : PhysicalMeanDomain.PeriodicOn U f) : PhysicalMeanDomain.PeriodicOn U (compactPrimitive d a b M ell v f)

theorem NavierStokes.VariableGaugeMean.pressureSource_periodicOn {S : Type} {a b : ℝ} (hab : a < b) (ell : S → ℝ) {U : Set S} {f : PressureStream.Lift S → ℝ} (hp : PhysicalMeanDomain.PeriodicOn U f) : PhysicalMeanDomain.PeriodicOn U (pressureSource a b hab ell f)

theorem NavierStokes.VariableGaugeMean.meanPressure_periodicOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} (hab : a < b) (d M : ℝ) (ell : S → ℝ) (v : PressureStream.Plane) {U : Set S} {f : PressureStream.Lift S → ℝ} (hp : PhysicalMeanDomain.PeriodicOn U f) : PhysicalMeanDomain.PeriodicOn U (meanPressure d a b M hab ell v f)

theorem NavierStokes.VariableGaugeMean.streamPotential_periodicOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (ell : S → ℝ) (v : PressureStream.Plane) {U : Set S} {f : PressureStream.Lift S → ℝ} (hp : PhysicalMeanDomain.PeriodicOn U f) : PhysicalMeanDomain.PeriodicOn U (streamPotential d a b M ell v f)

theorem NavierStokes.VariableGaugeMean.localBandJets_meanClass_of_gaugeInteriorSupport {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {c e α : ℝ} (hac : a < c) (heb : e < b) {f : ℕ → LocalSignedRequest.Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : ∀ (n : ℕ), SupportedGauge c e (qLength coord) U.carrier (f n)) (hb : PhysicalMeanDomain.LocalBandJets U.carrier ε L α f) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f

theorem NavierStokes.VariableGaugeMean.meanClass_radialMultiply_moving {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {φ : ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) {α : ℝ} {f : ℕ → LocalSignedRequest.Point → ℝ} (hf : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α fun (n : ℕ) (z : LocalSignedRequest.Point) => φ z.1 * f n z

theorem NavierStokes.VariableGaugeMean.meanClass_divideRadius_moving {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {α : ℝ} {f : ℕ → LocalSignedRequest.Point → ℝ} (hf : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α fun (n : ℕ) => PressureStream.divideRadius (f n)

theorem NavierStokes.VariableGaugeMean.meanClass_streamPotential {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {d : ℝ} (hab : a < b) (hd : 0 < d) {α : ℝ} {f : ℕ → LocalSignedRequest.Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : ∀ (n : ℕ), SupportedGauge a b (qLength coord) U.carrier (f n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α fun (n : ℕ) => streamPotential d a b (M n) (qLength coord) (v n) (f n)

theorem NavierStokes.VariableGaugeMean.meanClass_streamBeta {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {d : ℝ} (hab : a < b) (hd : 0 < d) {α : ℝ} {f : ℕ → LocalSignedRequest.Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : ∀ (n : ℕ), SupportedGauge a b (qLength coord) U.carrier (f n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) (w : PressureStream.Plane × PressureStream.Plane) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α fun (n : ℕ) => PressureStream.streamBeta w (streamPotential d a b (M n) (qLength coord) (v n) (f n))

theorem NavierStokes.VariableGaugeMean.fderiv_eq_on_radialFiber {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {f g : PressureStream.Lift S → ℝ} {z : PressureStream.Lift S} (hf : DifferentiableAt ℝ f z) (hg : DifferentiableAt ℝ g z) (he : ∀ (r : ℝ) (Y : PressureStream.Plane), f (r, z.2.1, Y) = g (r, z.2.1, Y)) (r : ℝ) (Y : PressureStream.Plane) : (fderiv ℝ f z) (r, 0, Y) = (fderiv ℝ g z) (r, 0, Y)

theorem NavierStokes.VariableGaugeMean.graphDr_eq_on_radialFiber {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {f g : PressureStream.Lift S → ℝ} {z : PressureStream.Lift S} (hf : DifferentiableAt ℝ f z) (hg : DifferentiableAt ℝ g z) (he : ∀ (r : ℝ) (Y : PressureStream.Plane), f (r, z.2.1, Y) = g (r, z.2.1, Y)) (k : ℝ → ℝ) (v : PressureStream.Plane) : PressureStream.graphDr k (0, v) f z = PressureStream.graphDr k (0, v) g z

theorem NavierStokes.VariableGaugeMean.divideRadius_fiberLocal {S : Type} : PhysicalMeanDomain.FiberLocal PressureStream.divideRadius

theorem NavierStokes.VariableGaugeMean.divideRadius_contDiffOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b : ℝ} (ha : 0 < a) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanDomain.SupportedOn a b U f) : ContDiffOn ℝ (↑⊤) (PressureStream.divideRadius f) (PhysicalMeanDomain.slowDomain U)

theorem NavierStokes.VariableGaugeMean.compactPrimitive_radial_identity {coord a b d : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (M : ℝ) (v : PressureStream.Plane) {f : LocalSignedRequest.Point → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) (hs : SupportedGauge a b (qLength coord) U.carrier f) {z : LocalSignedRequest.Point} (hz : z.2.1 ∈ U.carrier) : PressureStream.graphDr (PressureStream.physicalSpeed d M) (0, v) (compactPrimitive d a b M (qLength coord) v f) z = f z - compactAlias d a b M (qLength coord) v f z

theorem NavierStokes.VariableGaugeMean.meanPressure_radial_identity {coord a b d : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (M : ℝ) (v : PressureStream.Plane) {f : LocalSignedRequest.Point → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) (hs : SupportedGauge a b (qLength coord) U.carrier f) {z : LocalSignedRequest.Point} (hz : z.2.1 ∈ U.carrier) : PressureStream.graphDr (PressureStream.physicalSpeed d M) (0, v) (meanPressure d a b M hab (qLength coord) v f) z = f z - density a b hab (qLength coord) z * PressureStream.pressureMass f z.2.1 - compactAlias d a b M (qLength coord) v (pressureSource a b hab (qLength coord) f) z

theorem NavierStokes.VariableGaugeMean.streamPotential_q_contDiffOn {coord a b d : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (M : ℝ) (v : PressureStream.Plane) {f : LocalSignedRequest.Point → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) (hs : SupportedGauge a b (qLength coord) U.carrier f) : ContDiffOn ℝ (↑⊤) (streamPotential d a b M (qLength coord) v f) (PhysicalMeanDomain.slowDomain U.carrier)

theorem NavierStokes.VariableGaugeMean.streamGamma_eq_desired_sub_alias {coord a b d : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (M : ℝ) (v : PressureStream.Plane) {f : LocalSignedRequest.Point → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) (hs : SupportedGauge a b (qLength coord) U.carrier f) {z : LocalSignedRequest.Point} (hz : z.2.1 ∈ U.carrier) (hr : z.1 ≠ 0) : PressureStream.streamGamma (PressureStream.physicalSpeed d M) (0, v) (streamPotential d a b M (qLength coord) v f) z = f z - compactAlias d a b M (qLength coord) v (PressureStream.weightedSource f) z / z.1

theorem NavierStokes.VariableGaugeMean.stream_divergence_zero {coord a b d : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (M : ℝ) (v : PressureStream.Plane) (w : PressureStream.Plane × PressureStream.Plane) {f : LocalSignedRequest.Point → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) (hs : SupportedGauge a b (qLength coord) U.carrier f) {z : LocalSignedRequest.Point} (hz : z.2.1 ∈ U.carrier) (hr : z.1 ≠ 0) : PressureStream.graphDivergence (PressureStream.physicalSpeed d M) (0, v) w (PressureStream.streamBeta w (streamPotential d a b M (qLength coord) v f)) (PressureStream.streamGamma (PressureStream.physicalSpeed d M) (0, v) (streamPotential d a b M (qLength coord) v f)) z = 0

noncomputable def NavierStokes.VariableGaugeMean.cutoffRadialDerivative {S : Type} (d a b : ℝ) (ell : S → ℝ) (z : PressureStream.Lift S) : ℝ

Cutoff radial derivative, given by (ell z.2.1)⁻¹ * deriv (physicalCutoff d a b) (radialRatio ell z).

Equations

• NavierStokes.VariableGaugeMean.cutoffRadialDerivative d a b ell z = (ell z.2.1)⁻¹ * deriv (NavierStokes.RadialPullback.physicalCutoff d a b) (NavierStokes.VariableGaugeMean.radialRatio ell z)

theorem NavierStokes.VariableGaugeMean.deriv_physicalCutoff_scale {l a b : ℝ} (hl : 0 < l) (ha : 0 < a) (hab : a < b) (d R : ℝ) : deriv (RadialPullback.physicalCutoff d (l * a) (l * b)) R = l⁻¹ * deriv (RadialPullback.physicalCutoff d a b) (R / l)

theorem NavierStokes.VariableGaugeMean.compactAlias_eq_movingTotal {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b d M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (ell : S → ℝ) (v : PressureStream.Plane) (f : PressureStream.Lift S → ℝ) (z : PressureStream.Lift S) (hl : 0 < ell z.2.1) : compactAlias d a b M ell v f z = cutoffRadialDerivative d a b ell z * PressureStream.physicalTotal d (ell z.2.1 * a) M (0, v) f z

theorem NavierStokes.VariableGaugeMean.physicalTotal_anchor_eq {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {c a b d M : ℝ} (hc : 0 < c) (hca : c ≤ a) (hab : a < b) (hd : 0 < d) (v : S × PressureStream.Plane) {f : PressureStream.Lift S → ℝ} (hs : RadialAlias.RadiallySupported a b f) (z : PressureStream.Lift S) (hz : a ≤ z.1) : PressureStream.physicalTotal d c M v f z = PressureStream.physicalTotal d a M v f z

theorem NavierStokes.VariableGaugeMean.compactAlias_reference {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {c a b d M : ℝ} (hc : 0 < c) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (ell : S → ℝ) (v : PressureStream.Plane) {U : Set S} (hl : ∀ s ∈ U, 0 < ell s) (hleft : ∀ s ∈ U, c ≤ ell s * a) {f : PressureStream.Lift S → ℝ} (hs : SupportedGauge a b ell U f) (z : PressureStream.Lift S) (hz : z.2.1 ∈ U) : compactAlias d a b M ell v f z = cutoffRadialDerivative d a b ell z * PressureStream.physicalTotal d c M (0, v) f z

theorem NavierStokes.VariableGaugeMean.cutoffRadialDerivative_contDiffOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a : ℝ} (ha : 0 < a) (d b : ℝ) {ell : S → ℝ} {U : Set S} (hell : ContDiffOn ℝ (↑⊤) ell U) (hl : ∀ s ∈ U, 0 < ell s) : ContDiffOn ℝ (↑⊤) (cutoffRadialDerivative d a b ell) (PhysicalMeanDomain.slowDomain U)

theorem NavierStokes.VariableGaugeMean.cutoffRadialDerivative_interior_support {S : Type} {a b d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) : ∃ (c : ℝ) (e : ℝ), a < c ∧ c < e ∧ e < b ∧ ∀ (ell : S → ℝ) (U : Set S), (∀ s ∈ U, 0 < ell s) → SupportedGauge c e ell U (cutoffRadialDerivative d a b ell)

The derivative of the actual cutoff is supported in one reserved profile interval, independently of the source and transport frequency.

theorem NavierStokes.VariableGaugeMean.compactAlias_interior_support {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) : ∃ (c : ℝ) (e : ℝ), a < c ∧ c < e ∧ e < b ∧ ∀ (ell : S → ℝ) (U : Set S), (∀ s ∈ U, 0 < ell s) → ∀ (M : ℝ) (v : PressureStream.Plane) (f : PressureStream.Lift S → ℝ), SupportedGauge c e ell U (compactAlias d a b M ell v f)

theorem NavierStokes.VariableGaugeMean.SupportedGauge.sub {S : Type} {a b : ℝ} {ell : S → ℝ} {U : Set S} {f g : PressureStream.Lift S → ℝ} (hf : SupportedGauge a b ell U f) (hg : SupportedGauge a b ell U g) : SupportedGauge a b ell U fun (z : PressureStream.Lift S) => f z - g z

theorem NavierStokes.VariableGaugeMean.meanPressure_sub_on {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b d M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (ell : S → ℝ) (v : PressureStream.Plane) {U : Set S} (hU : IsOpen U) {f g : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hg : ContDiffOn ℝ (↑⊤) g (PhysicalMeanDomain.slowDomain U)) (hsf : SupportedGauge a b ell U f) (hsg : SupportedGauge a b ell U g) {z : PressureStream.Lift S} (hz : z.2.1 ∈ U) (hl : 0 < ell z.2.1) : meanPressure d a b M hab ell v (fun (p : PressureStream.Lift S) => f p - g p) z = meanPressure d a b M hab ell v f z - meanPressure d a b M hab ell v g z

theorem NavierStokes.VariableGaugeMean.meanClass_meanPressure_change {coord a b cL cR d : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {α : ℝ} {f g : ℕ → LocalSignedRequest.Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hg : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (g n) (PhysicalMeanDomain.slowDomain U.carrier)) (hsf : ∀ (n : ℕ), SupportedGauge a b (qLength coord) U.carrier (f n)) (hsg : ∀ (n : ℕ), SupportedGauge a b (qLength coord) U.carrier (g n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α (f - g)) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α fun (n : ℕ) (z : LocalSignedRequest.Point) => meanPressure d a b (M n) hab (qLength coord) (v n) (f n) z - meanPressure d a b (M n) hab (qLength coord) (v n) (g n) z

theorem NavierStokes.VariableGaugeMean.meanClass_liftedTorusAverage_moving {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {α : ℝ} {f : ℕ → LocalSignedRequest.Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α fun (n : ℕ) => MeanMomentBounds.liftedTorusAverage (f n)

theorem NavierStokes.VariableGaugeMean.meanClass_centered_moving {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {α : ℝ} {f : ℕ → LocalSignedRequest.Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α fun (n : ℕ) => TemporalMeanUpdate.centered (f n)

theorem NavierStokes.VariableGaugeMean.meanClass_temporalInverse_moving {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {α : ℝ} {f : ℕ → LocalSignedRequest.Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (f n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α fun (n : ℕ) => TemporalMeanUpdate.temporalInverse (f n)

theorem NavierStokes.VariableGaugeMean.meanClass_desiredIncrement_moving {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {h α : ℝ} (hh : 0 ≤ h) (hscale : ∀ (n : ℕ), ChartScales.S n ≤ L n) {f : ℕ → LocalSignedRequest.Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (f n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α fun (n : ℕ) => TemporalMeanUpdate.desiredIncrement h n (f n)

theorem NavierStokes.VariableGaugeMean.meanClass_temporalAtIndex_moving {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {h α : ℝ} (hh : 0 ≤ h) (hscale : ∀ (n : ℕ), ChartScales.S n ≤ L n) (index : ℕ → ℕ) (D : ℕ) (hgap : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + D) {f : ℕ → LocalSignedRequest.Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (f n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α fun (n : ℕ) => MeanChartCompatibility.temporalAtIndex h n (index n) (f n)

theorem NavierStokes.VariableGaugeMean.temporalAtIndex_fiberLocal {S : Type} (h : ℝ) (n i : ℕ) : PhysicalMeanDomain.FiberLocal (MeanChartCompatibility.temporalAtIndex h n i)

theorem NavierStokes.VariableGaugeMean.temporalAtIndex_supportedGauge {S : Type} (h : ℝ) (n i : ℕ) {a b : ℝ} {ell : S → ℝ} {U : Set S} {f : PressureStream.Lift S → ℝ} (hs : SupportedGauge a b ell U f) : SupportedGauge a b ell U (MeanChartCompatibility.temporalAtIndex h n i f)

theorem NavierStokes.VariableGaugeMean.temporalAtIndex_contDiffOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (h : ℝ) (n i : ℕ) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hp : PhysicalMeanDomain.PeriodicOn U f) : ContDiffOn ℝ (↑⊤) (MeanChartCompatibility.temporalAtIndex h n i f) (PhysicalMeanDomain.slowDomain U)

theorem NavierStokes.VariableGaugeMean.temporalAtIndex_fast_cancellation_on {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (h : ℝ) (n i : ℕ) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hp : PhysicalMeanDomain.PeriodicOn U f) {z : PressureStream.Lift S} (hz : z.2.1 ∈ U) : MeanChartCompatibility.fastAtIndex h n i (MeanChartCompatibility.temporalAtIndex h n i f) z = -TemporalMeanUpdate.centered f z

noncomputable def NavierStokes.VariableGaugeMean.cutoffRadialDerivativeModel (d a b : ℝ) (y : MeanRankUpdate.ModelPoint) : ℝ

Cutoff radial derivative model, given by (Real.sqrt y.1)⁻¹ * deriv (physicalCutoff d a b) (y.2.1 / Real.sqrt y.1).

Equations

• NavierStokes.VariableGaugeMean.cutoffRadialDerivativeModel d a b y = (√y.1)⁻¹ * deriv (NavierStokes.RadialPullback.physicalCutoff d a b) (y.2.1 / √y.1)

theorem NavierStokes.VariableGaugeMean.cutoffRadialDerivativeModel_contDiffOn {a : ℝ} (ha : 0 < a) (d b : ℝ) : ContDiffOn ℝ (↑⊤) (cutoffRadialDerivativeModel d a b) PhysicalCoordinateBounds.positiveTime

theorem NavierStokes.VariableGaugeMean.cutoffRadialDerivative_q_eq_kernel (coord d a b : ℝ) : cutoffRadialDerivative d a b (qLength coord) = MeanRankUpdate.chartKernel coord (cutoffRadialDerivativeModel d a b)

theorem NavierStokes.VariableGaugeMean.cutoffRadialDerivative_q_finiteJets {coord qlo qhi rlo rhi a : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (hqlo : 0 < qlo) (ha : 0 < a) (d b : ℝ) {V : Set MeanRankUpdate.ChartPoint} (hT : ∀ z ∈ V, MeanRankUpdate.chartInput z ∈ PhysicalCoordinateBounds.positiveTime) (hq : ∀ z ∈ V, MeanRankUpdate.chartQ coord z ∈ Set.Icc qlo qhi) (hR : ∀ z ∈ V, z.1 ∈ Set.Icc rlo rhi) (m : ℕ) : ∃ (B : ℝ), 0 ≤ B ∧ JetBounds.FiniteJetBound m (cutoffRadialDerivative d a b (qLength coord)) V B

theorem NavierStokes.VariableGaugeMean.compactAlias_q_contDiffOn {coord a b d : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (M : ℝ) (v : PressureStream.Plane) {f : LocalSignedRequest.Point → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) (hs : SupportedGauge a b (qLength coord) U.carrier f) : ContDiffOn ℝ (↑⊤) (compactAlias d a b M (qLength coord) v f) (PhysicalMeanDomain.slowDomain U.carrier)

theorem NavierStokes.VariableGaugeMean.compactAlias_q_supportedGauge {coord a b d : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (M : ℝ) (v : PressureStream.Plane) (f : LocalSignedRequest.Point → ℝ) : SupportedGauge a b (qLength coord) U.carrier (compactAlias d a b M (qLength coord) v f)

theorem NavierStokes.VariableGaugeMean.localBandJets_compactAlias {coord a b d : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) {ε L : ℕ → ℝ} {α : ℝ} {f : ℕ → LocalSignedRequest.Point → ℝ} (hε : ∀ (n : ℕ), 0 < ε n) (hL : ∀ (n : ℕ), 1 ≤ L n) (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : ∀ (n : ℕ), SupportedGauge a b (qLength coord) U.carrier (f n)) (hb : PhysicalMeanDomain.LocalBandJets U.carrier ε L α f) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) : PhysicalMeanDomain.LocalBandJets U.carrier ε L α fun (n : ℕ) => compactAlias d a b (M n) (qLength coord) (v n) (f n)

theorem NavierStokes.VariableGaugeMean.meanClass_compactAlias {coord a b d : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {α : ℝ} {f : ℕ → LocalSignedRequest.Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : ∀ (n : ℕ), SupportedGauge a b (qLength coord) U.carrier (f n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α fun (n : ℕ) => compactAlias d a b (M n) (qLength coord) (v n) (f n)

theorem NavierStokes.VariableGaugeMean.meanClass_dividedCompactAlias {coord a b d : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {α : ℝ} {f : ℕ → LocalSignedRequest.Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : ∀ (n : ℕ), SupportedGauge a b (qLength coord) U.carrier (f n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α fun (n : ℕ) => PressureStream.divideRadius (compactAlias d a b (M n) (qLength coord) (v n) (f n))

theorem NavierStokes.VariableGaugeMean.meanClass_streamGamma {coord a b d : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {α : ℝ} {f : ℕ → LocalSignedRequest.Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : ∀ (n : ℕ), SupportedGauge a b (qLength coord) U.carrier (f n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α fun (n : ℕ) => PressureStream.streamGamma (PressureStream.physicalSpeed d (M n)) (0, v n) (streamPotential d a b (M n) (qLength coord) (v n) (f n))

theorem NavierStokes.VariableGaugeMean.meanClass_temporalStreamPotential {coord a b cL cR d : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {h α : ℝ} (hh : 0 ≤ h) (hscale : ∀ (n : ℕ), ChartScales.S n ≤ L n) (index : ℕ → ℕ) (D : ℕ) (hgap : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + D) {f : ℕ → LocalSignedRequest.Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (f n)) (hs : ∀ (n : ℕ), SupportedGauge a b (qLength coord) U.carrier (f n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α fun (n : ℕ) => streamPotential d a b (M n) (qLength coord) (v n) (MeanChartCompatibility.temporalAtIndex h n (index n) (f n))

theorem NavierStokes.VariableGaugeMean.meanClass_temporalStreamGamma {coord a b cL cR d : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {h α : ℝ} (hh : 0 ≤ h) (hscale : ∀ (n : ℕ), ChartScales.S n ≤ L n) (index : ℕ → ℕ) (D : ℕ) (hgap : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + D) {f : ℕ → LocalSignedRequest.Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (f n)) (hs : ∀ (n : ℕ), SupportedGauge a b (qLength coord) U.carrier (f n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α fun (n : ℕ) => PressureStream.streamGamma (PressureStream.physicalSpeed d (M n)) (0, v n) (streamPotential d a b (M n) (qLength coord) (v n) (MeanChartCompatibility.temporalAtIndex h n (index n) (f n)))

theorem NavierStokes.VariableGaugeMean.streamBeta_smul_direction {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (r : ℝ) (w : E) (f : ℝ × E → ℝ) : PressureStream.streamBeta (r • w) f = fun (z : ℝ × E) => r • PressureStream.streamBeta w f z

theorem NavierStokes.VariableGaugeMean.meanClass_scaledTemporalStreamBeta {coord a b cL cR d : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {h α : ℝ} (hh : 0 ≤ h) (hscale : ∀ (n : ℕ), ChartScales.S n ≤ L n) (index : ℕ → ℕ) (D : ℕ) (hgap : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + D) {f : ℕ → LocalSignedRequest.Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (f n)) (hs : ∀ (n : ℕ), SupportedGauge a b (qLength coord) U.carrier (f n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) (w : PressureStream.Plane × PressureStream.Plane) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) (α + 1) fun (n : ℕ) => PressureStream.streamBeta (ε n • w) (streamPotential d a b (M n) (qLength coord) (v n) (MeanChartCompatibility.temporalAtIndex h n (index n) (f n)))

theorem NavierStokes.VariableGaugeMean.reconstructState_pressure_class {coord cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : GaugeData PressureStream.Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (hell : ∀ (n : ℕ), g.length n = qLength coord) (c : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) {α : ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.gr c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : ∀ (n : ℕ), SupportedGauge g.radial.inner g.radial.outer (qLength coord) U.carrier (u.gr c n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) α (u.gr c)) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) α (reconstructState g c u).pressure

theorem NavierStokes.VariableGaugeMean.reconstructState_pressure_change_class {coord cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : GaugeData PressureStream.Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (hell : ∀ (n : ℕ), g.length n = qLength coord) (c : CorrectionState.Context LocalSignedRequest.Point) (u v : CorrectionState.State LocalSignedRequest.Point) {α : ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.gr c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hg : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (v.gr c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hsf : ∀ (n : ℕ), SupportedGauge g.radial.inner g.radial.outer (qLength coord) U.carrier (u.gr c n)) (hsg : ∀ (n : ℕ), SupportedGauge g.radial.inner g.radial.outer (qLength coord) U.carrier (v.gr c n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) α (u.gr c - v.gr c)) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) α ((reconstructState g c u).pressure - (reconstructState g c v).pressure)

theorem NavierStokes.VariableGaugeMean.temporalIncrementState_classes {coord cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : GaugeData PressureStream.Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (hell : ∀ (n : ℕ), g.length n = qLength coord) {h α : ℝ} (hh : 0 ≤ h) (hscale : ∀ (n : ℕ), ChartScales.S n ≤ L n) (index : ℕ → ℕ) (D : ℕ) (hgap : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + D) (axial : PressureStream.Plane × PressureStream.Plane) (c : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) (heps : c.operators.epsilon = ε) (hθ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.thetaResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hz : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.axialResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hpθ : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.thetaResidual c n)) (hpz : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.axialResidual c n)) (hsz : ∀ (n : ℕ), SupportedGauge g.radial.inner g.radial.outer (qLength coord) U.carrier (u.axialResidual c n)) (hcθ : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) α (u.thetaResidual c)) (hcz : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) α (u.axialResidual c)) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) (α + 1) (temporalIncrementState g h index axial c u).radial ∧ WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) α (temporalIncrementState g h index axial c u).angular ∧ WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) α (temporalIncrementState g h index axial c u).axial

theorem NavierStokes.VariableGaugeMean.fderiv_apply_supportedGauge {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} {ell : S → ℝ} {U : Set S} (hU : IsOpen U) (hell : ContinuousOn ell U) {f : PressureStream.Lift S → ℝ} (hs : SupportedGauge a b ell U f) (w : PressureStream.Lift S → PressureStream.Lift S) : SupportedGauge a b ell U fun (z : PressureStream.Lift S) => (fderiv ℝ f z) (w z)

theorem NavierStokes.VariableGaugeMean.divideRadius_supportedGauge {S : Type} {a b : ℝ} {ell : S → ℝ} {U : Set S} {f : PressureStream.Lift S → ℝ} (hs : SupportedGauge a b ell U f) : SupportedGauge a b ell U (PressureStream.divideRadius f)

theorem NavierStokes.VariableGaugeMean.streamBeta_supportedGauge {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} {ell : S → ℝ} {U : Set S} (hU : IsOpen U) (hell : ContinuousOn ell U) {f : PressureStream.Lift S → ℝ} (hs : SupportedGauge a b ell U f) (w : S × PressureStream.Plane) : SupportedGauge a b ell U (PressureStream.streamBeta w f)

theorem NavierStokes.VariableGaugeMean.streamGamma_supportedGauge {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} {ell : S → ℝ} {U : Set S} (hU : IsOpen U) (hell : ContinuousOn ell U) {f : PressureStream.Lift S → ℝ} (hs : SupportedGauge a b ell U f) (k : ℝ → ℝ) (v : S × PressureStream.Plane) : SupportedGauge a b ell U (PressureStream.streamGamma k v f)

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

theorem NavierStokes.VariableGaugeMean.reconstructState_radial_identity {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : GaugeData PressureStream.Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hell : ∀ (n : ℕ), g.length n = qLength coord) (c : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) (n : ℕ) (hf : ContDiffOn ℝ (↑⊤) (u.gr c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : SupportedGauge g.radial.inner g.radial.outer (qLength coord) U.carrier (u.gr c n)) {z : LocalSignedRequest.Point} (hz : z.2.1 ∈ U.carrier) : PressureStream.graphDr (PressureStream.physicalSpeed g.radial.exponent (g.radial.frequency n)) (0, g.radial.radialDirection) ((reconstructState g c u).pressure n) z = u.gr c n z - density g.radial.inner g.radial.outer ⋯ (g.length n) z * PressureStream.pressureMass (u.gr c n) z.2.1 - compactAlias g.radial.exponent g.radial.inner g.radial.outer (g.radial.frequency n) (g.length n) g.radial.radialDirection (pressureSource g.radial.inner g.radial.outer ⋯ (g.length n) (u.gr c n)) z

theorem NavierStokes.VariableGaugeMean.temporalAxialDifference_eq_dividedAlias {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : GaugeData PressureStream.Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hell : ∀ (n : ℕ), g.length n = qLength coord) (c : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) (h : ℝ) (index : ℕ → ℕ) (n : ℕ) (hf : ContDiffOn ℝ (↑⊤) (u.axialResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hp : PhysicalMeanDomain.PeriodicOn U.carrier (u.axialResidual c n)) (hs : SupportedGauge g.radial.inner g.radial.outer (qLength coord) U.carrier (u.axialResidual c n)) {z : LocalSignedRequest.Point} (hz : z.2.1 ∈ U.carrier) (hr : z.1 ≠ 0) : temporalAxialDifference g h index c u n z = compactAlias g.radial.exponent g.radial.inner g.radial.outer (g.radial.frequency n) (g.length n) g.radial.radialDirection (PressureStream.weightedSource (MeanChartCompatibility.temporalAtIndex h n (index n) (u.axialResidual c n))) z / z.1

theorem NavierStokes.VariableGaugeMean.temporalIncrementState_divergence_zero {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : GaugeData PressureStream.Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hell : ∀ (n : ℕ), g.length n = qLength coord) (c : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) (h : ℝ) (index : ℕ → ℕ) (axial : PressureStream.Plane × PressureStream.Plane) (n : ℕ) (hf : ContDiffOn ℝ (↑⊤) (u.axialResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hp : PhysicalMeanDomain.PeriodicOn U.carrier (u.axialResidual c n)) (hs : SupportedGauge g.radial.inner g.radial.outer (qLength coord) U.carrier (u.axialResidual c n)) {z : LocalSignedRequest.Point} (hz : z.2.1 ∈ U.carrier) (hr : z.1 ≠ 0) : PressureStream.graphDivergence (PressureStream.physicalSpeed g.radial.exponent (g.radial.frequency n)) (0, g.radial.radialDirection) (c.operators.epsilon n • axial) ((temporalIncrementState g h index axial c u).radial n) ((temporalIncrementState g h index axial c u).axial n) z = 0

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