Arbitrary decay of the actual moving-gauge compactification alias

The finite-jet estimates are local in the slow variables. The radial frequency is finally specialized to the actual manuscript exponent.

@[reducible, inline]

abbrev NavierStokes.GaugeAliasDecay.Plane : Type

Plane: an abbreviation for TorusInverse.Plane.

Equations

• NavierStokes.GaugeAliasDecay.Plane = NavierStokes.TorusInverse.Plane

@[reducible, inline]

abbrev NavierStokes.GaugeAliasDecay.Point (S : Type) : Type

Point: an abbreviation for PressureStream.Lift S.

Equations

• NavierStokes.GaugeAliasDecay.Point S = NavierStokes.PressureStream.Lift S

noncomputable def NavierStokes.GaugeAliasDecay.fiberShell {S : Type} (a b : ℝ) (s : S) : Set (Point S)

Fiber shell, given by {z | z.1 ∈ Icc a b ∧ z.2.1 = s}.

Equations

• NavierStokes.GaugeAliasDecay.fiberShell a b s = {z : NavierStokes.GaugeAliasDecay.Point S | z.1 ∈ Set.Icc a b ∧ z.2.1 = s}

theorem NavierStokes.GaugeAliasDecay.familyInverse_finiteJets_fiber {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (d : TorusInverse.Direction) (a b : ℝ) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : Point S → ℂ), ContDiff ℝ (↑⊤) f → SmoothFamilyTorusInverse.Periodic (UniformFourierAlias.toProduct f) → ∀ (C : ℝ), 0 ≤ C → ∀ (s : S), JetBounds.FiniteJetBound (m + 5) f (fiberShell a b s) C → JetBounds.FiniteJetBound m (UniformFourierAlias.familyInverse d f) (fiberShell a b s) (K * C)

The torus inverse estimate uses only jets on the designated slow fiber.

theorem NavierStokes.GaugeAliasDecay.sourceJet_finiteJets_fiber {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (d : TorusInverse.Direction) (a b : ℝ) (p m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : Point S → ℂ), UniformFourierAlias.Admissible a b f → ∀ (C : ℝ), 0 ≤ C → ∀ (s : S), JetBounds.FiniteJetBound (m + 6 * p) f (fiberShell a b s) C → JetBounds.FiniteJetBound m (RadialAlias.sourceJet (UniformFourierAlias.familyInverse d) f p) (fiberShell a b s) (K * C)

theorem NavierStokes.GaugeAliasDecay.totalIntegral_finiteJets_fiber {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (d : TorusInverse.Direction) {a b : ℝ} (hab : a ≤ b) (m p : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : Point S → ℂ), UniformFourierAlias.Admissible a b f → ∀ (C : ℝ), 0 ≤ C → ∀ (s : S), JetBounds.FiniteJetBound (m + 6 * p) f (fiberShell a b s) C → ∀ (M : ℝ), M ≠ 0 → ∀ j ≤ m, ∀ (z : Point S), z.2.1 = s → ‖iteratedFDeriv ℝ j (TransportPrimitive.totalIntegral M (0, TorusInverse.vector d) f) z‖ ≤ K * C * |M|⁻¹ ^ p

Every IBP step costs six genuine source-jet orders. The constant is chosen before the slow point, source, or frequency.

theorem NavierStokes.GaugeAliasDecay.real_totalIntegral_finiteJets_fiber {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (d : TorusInverse.Direction) {a b : ℝ} (hab : a ≤ b) (m p : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : Point S → ℝ), ContDiff ℝ (↑⊤) f → UniformFourierAlias.SourcePeriodic f → (∀ (q : ℝ × S), UniformFourierAlias.sourceMean f q = 0) → RadialAlias.RadiallySupported a b f → ∀ (C : ℝ), 0 ≤ C → ∀ (s : S), JetBounds.FiniteJetBound (m + 6 * p) f (fiberShell a b s) C → ∀ (M : ℝ), M ≠ 0 → ∀ j ≤ m, ∀ (z : Point S), z.2.1 = s → ‖iteratedFDeriv ℝ j (TransportPrimitive.totalIntegral M (0, TorusInverse.vector d) f) z‖ ≤ K * C * |M|⁻¹ ^ p

theorem NavierStokes.GaugeAliasDecay.realCenterSource_finiteJets_fiber {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (a b : ℝ) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : Point S → ℝ), ContDiff ℝ (↑⊤) f → UniformFourierAlias.SourcePeriodic f → ∀ (C : ℝ), 0 ≤ C → ∀ (s : S), JetBounds.FiniteJetBound (m + 4) f (fiberShell a b s) C → JetBounds.FiniteJetBound m (UniformFourierAlias.realCenterSource f) (fiberShell a b s) (K * C)

theorem NavierStokes.GaugeAliasDecay.real_totalIntegral_finiteJets_fiber_of_mass_zero {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (d : TorusInverse.Direction) {a b : ℝ} (hab : a ≤ b) (m p : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : Point S → ℝ), ContDiff ℝ (↑⊤) f → UniformFourierAlias.SourcePeriodic f → (∀ (s : S), ∫ (R : ℝ) in a..b, UniformFourierAlias.sourceMean f (R, s) = 0) → RadialAlias.RadiallySupported a b f → ∀ (C : ℝ), 0 ≤ C → ∀ (s : S), JetBounds.FiniteJetBound (m + 6 * p + 4) f (fiberShell a b s) C → ∀ (M : ℝ), M ≠ 0 → ∀ j ≤ m, ∀ (z : Point S), z.2.1 = s → ‖iteratedFDeriv ℝ j (TransportPrimitive.totalIntegral M (0, TorusInverse.vector d) f) z‖ ≤ K * C * |M|⁻¹ ^ p

Radial mean zero suffices. Subtracting the torus mean changes the exact total integral by zero and costs four additional source orders.

theorem NavierStokes.GaugeAliasDecay.normalizeSource_mean_integral {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {c e d : ℝ} (hc : 0 < c) (hce : c < e) (hd : 0 < d) {f : Point S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported c e f) (s : S) : ∫ (u : ℝ) in c ^ d..e ^ d, UniformFourierAlias.sourceMean (RadialPullback.normalizeSource d c f) (u, s) = PressureStream.pressureMass f s

theorem NavierStokes.GaugeAliasDecay.physicalTotal_finiteJets_fiber {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (direction : TorusInverse.Direction) {c e d : ℝ} (hc : 0 < c) (hce : c < e) (hd : 0 < d) (rlo rhi : ℝ) (m p : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : Point S → ℝ), ContDiff ℝ (↑⊤) f → RadialAlias.RadiallySupported c e f → UniformFourierAlias.SourcePeriodic f → (∀ (s : S), PressureStream.pressureMass f s = 0) → ∀ (A : ℝ), 0 ≤ A → ∀ (s : S), (∀ j ≤ m + 6 * p + 4, ∀ R ∈ Set.Ioo c e, ∀ (Y : Plane), ‖iteratedFDeriv ℝ j f (R, s, Y)‖ ≤ A) → ∀ (M : ℝ), M ≠ 0 → ∀ (z : Point S), z.1 ∈ Set.Icc rlo rhi → z.2.1 = s → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (PressureStream.physicalTotal d c M (0, TorusInverse.vector direction) f) z‖ ≤ K * A * |M|⁻¹ ^ p

theorem NavierStokes.GaugeAliasDecay.pressureMass_localize {S : Type} (χ : S → ℝ) (f : Point S → ℝ) (s : S) : PressureStream.pressureMass (PhysicalMeanDomain.localize χ f) s = χ s * PressureStream.pressureMass f s

theorem NavierStokes.GaugeAliasDecay.physicalTotal_finiteJets_local {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (direction : TorusInverse.Direction) {c e d : ℝ} (hc : 0 < c) (hce : c < e) (hd : 0 < d) (rlo rhi : ℝ) (m p : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (U : Set S), IsOpen U → ∀ (f : Point S → ℝ), ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U) → PhysicalMeanDomain.SupportedOn c e U f → PhysicalMeanDomain.PeriodicOn U f → (∀ s ∈ U, PressureStream.pressureMass f s = 0) → ∀ (A : ℝ), 0 ≤ A → ∀ (M : ℝ), M ≠ 0 → ∀ (z : Point S), z.2.1 ∈ U → z.1 ∈ Set.Icc rlo rhi → (∀ j ≤ m + 6 * p + 4, ∀ R ∈ Set.Ioo c e, ∀ (Y : Plane), ‖iteratedFDeriv ℝ j f (R, z.2.1, Y)‖ ≤ A) → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (PressureStream.physicalTotal d c M (0, TorusInverse.vector direction) f) z‖ ≤ K * A * |M|⁻¹ ^ p

Slow localization is removed by germ equality. No derivative bound on the auxiliary slow cutoff enters the constant.

theorem NavierStokes.GaugeAliasDecay.compactAlias_finiteJets_local {coord a b d : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (direction : TorusInverse.Direction) (m p : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : Point Plane → ℝ), ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier) → VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) U.carrier f → PhysicalMeanDomain.PeriodicOn U.carrier f → (∀ s ∈ U.carrier, PressureStream.pressureMass f s = 0) → ∀ (A : ℝ), 0 ≤ A → ∀ (M : ℝ), M ≠ 0 → ∀ (z : Point Plane), z.2.1 ∈ U.carrier → (∀ j ≤ m + 6 * p + 4, ∀ (R : ℝ) (Y : Plane), ‖iteratedFDeriv ℝ j f (R, z.2.1, Y)‖ ≤ A) → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (VariableGaugeMean.compactAlias d a b M (VariableGaugeMean.qLength coord) (TorusInverse.vector direction) f) z‖ ≤ K * A * |M|⁻¹ ^ p

Source-uniform arbitrary inverse-frequency gain for the actual moving alias. The input seminorm uses one entire slow fiber, never all slow space.

theorem NavierStokes.GaugeAliasDecay.localBandJets_compactAlias_gain {coord a b d α κ B : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (direction : TorusInverse.Direction) (ε L M : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (hκ : 0 < κ) (hB : 0 ≤ B) (q : ℕ) (hM : ∀ (n : ℕ), M n ≠ 0) (hfreq : ∀ (n : ℕ), |M n|⁻¹ ≤ B * ε n ^ κ * L n ^ q) {f : ℕ → Point Plane → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) U.carrier (f n)) (hp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (f n)) (hm : ∀ (n : ℕ), ∀ s ∈ U.carrier, PressureStream.pressureMass (f n) s = 0) (hsource : PhysicalMeanDomain.LocalBandJets U.carrier ε L α f) (β : ℝ) : PhysicalMeanDomain.LocalBandJets U.carrier ε L β fun (n : ℕ) => VariableGaugeMean.compactAlias d a b (M n) (VariableGaugeMean.qLength coord) (TorusInverse.vector direction) (f n)

theorem NavierStokes.GaugeAliasDecay.scalar_bound_of_tail (f w : ℕ → ℝ) (hw : ∀ (n : ℕ), 0 < w n) (A : ℝ) (hA : 0 ≤ A) (N : ℕ) (htail : ∀ (n : ℕ), N ≤ n → |f n| ≤ A * w n) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), |f n| ≤ C * w n

A finite initial set of bands does not change an all-band bound with a strictly positive weight. This lemma constructs its enlarged constant.

theorem NavierStokes.GaugeAliasDecay.radialFrequency_abs (h : ℝ) (n i : ℕ) (d Mbase : ℝ) : |MeanChartCompatibility.radialFrequency h n i d Mbase| = |Mbase| * ChartScales.Lambda ^ i * ChartScales.Q n ^ (d / 2)

theorem NavierStokes.GaugeAliasDecay.radialFrequency_ne_zero (h : ℝ) (n i : ℕ) (d : ℝ) {Mbase : ℝ} (hM : Mbase ≠ 0) : MeanChartCompatibility.radialFrequency h n i d Mbase ≠ 0

theorem NavierStokes.GaugeAliasDecay.radialFrequency_inv_compare {h Mbase : ℝ} {n i D : ℕ} (hM : Mbase ≠ 0) (hgap : ChartScales.nativeIndex h n ≤ i + D) : |MeanChartCompatibility.radialFrequency h n i (ChartScales.radialExponent h) Mbase|⁻¹ ≤ ChartScales.Lambda ^ D / |Mbase| * (ChartScales.radialCoefficient h n)⁻¹

theorem NavierStokes.GaugeAliasDecay.actual_inverse_frequency_bound {h Mbase : ℝ} (hh : 0 < h) (hM : Mbase ≠ 0) (index : ℕ → ℕ) (D : ℕ) (hgap : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + D) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 1 ≤ L n) (hS : ∀ (n : ℕ), ChartScales.S n ≤ L n) : ∃ (B : ℝ), 0 ≤ B ∧ ∃ (q : ℕ), ∀ (n : ℕ), |MeanChartCompatibility.radialFrequency h n (index n) (ChartScales.radialExponent h) Mbase|⁻¹ ≤ B * ChartScales.epsilon h n ^ ChartScales.kappa * L n ^ q

The inverse frequency has a positive epsilon power in every band for the actual graph exponent. The finite initial bands are included.

theorem NavierStokes.GaugeAliasDecay.actual_fast_coefficient_bound {h : ℝ} (hh : 0 < h) (index : ℕ → ℕ) (D : ℕ) (hgap : ∀ (n : ℕ), index n ≤ ChartScales.nativeIndex h n + D) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), |ChartScales.Tg ^ index n * ChartScales.Q n ^ (1 + h)| ≤ C

The actual common fast coefficient is uniformly bounded when the common index stays a bounded amount above the native one.

theorem NavierStokes.GaugeAliasDecay.meanClass_compactAlias_superflat {coord a b h Mbase α : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 < h) (hM : Mbase ≠ 0) (index : ℕ → ℕ) (D : ℕ) (hgap : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + D) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 1 ≤ L n) (hS : ∀ (n : ℕ), ChartScales.S n ≤ L n) {f : ℕ → Point Plane → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) U.carrier (f n)) (hp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (f n)) (hm : ∀ (n : ℕ), ∀ s ∈ U.carrier, PressureStream.pressureMass (f n) s = 0) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR (ChartScales.epsilon h) L ⋯ ⋯ hL) α f) (β : ℝ) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR (ChartScales.epsilon h) L ⋯ ⋯ hL) β fun (n : ℕ) => VariableGaugeMean.compactAlias (ChartScales.radialExponent h) a b (MeanChartCompatibility.radialFrequency h n (index n) (ChartScales.radialExponent h) Mbase) (VariableGaugeMean.qLength coord) (TorusInverse.vector TorusInverse.Direction.radial) (f n)

Every target order is obtained for the literal moving alias at the actual radial frequency. Only the lower bound on the common index is used.

theorem NavierStokes.GaugeAliasDecay.meanClass_dividedAlias_superflat {coord a b h Mbase α : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 < h) (hM : Mbase ≠ 0) (index : ℕ → ℕ) (D : ℕ) (hgap : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + D) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 1 ≤ L n) (hS : ∀ (n : ℕ), ChartScales.S n ≤ L n) {f : ℕ → Point Plane → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) U.carrier (f n)) (hp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (f n)) (hm : ∀ (n : ℕ), ∀ s ∈ U.carrier, PressureStream.pressureMass (f n) s = 0) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR (ChartScales.epsilon h) L ⋯ ⋯ hL) α f) (β : ℝ) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR (ChartScales.epsilon h) L ⋯ ⋯ hL) β fun (n : ℕ) => PressureStream.divideRadius (VariableGaugeMean.compactAlias (ChartScales.radialExponent h) a b (MeanChartCompatibility.radialFrequency h n (index n) (ChartScales.radialExponent h) Mbase) (VariableGaugeMean.qLength coord) (TorusInverse.vector TorusInverse.Direction.radial) (f n))

theorem NavierStokes.GaugeAliasDecay.actual_fast_coefficient_bandBound (s : WeightedClasses.StripData (Point Plane)) {h : ℝ} (hh : 0 < h) (index : ℕ → ℕ) (D : ℕ) (hgap : ∀ (n : ℕ), index n ≤ ChartScales.nativeIndex h n + D) : WeightedClasses.BandBound s 0 fun (n : ℕ) => ChartScales.Tg ^ index n * ChartScales.Q n ^ (1 + h)

theorem NavierStokes.GaugeAliasDecay.meanClass_fastAtIndex (s : WeightedClasses.StripData (Point Plane)) {h α : ℝ} (hh : 0 < h) (index : ℕ → ℕ) (D : ℕ) (hgap : ∀ (n : ℕ), index n ≤ ChartScales.nativeIndex h n + D) {f : ℕ → Point Plane → ℝ} (hf : WeightedClasses.MeanClass s α f) : WeightedClasses.MeanClass s α fun (n : ℕ) => MeanChartCompatibility.fastAtIndex h n (index n) (f n)

The common fast derivative is the actual coefficient at the common integer index. Its bounded-gap ratio to the native coefficient is proved.

theorem NavierStokes.GaugeAliasDecay.meanClass_fastDividedAlias_superflat {coord a b h Mbase α : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 < h) (hM : Mbase ≠ 0) (index : ℕ → ℕ) (D : ℕ) (hgapLower : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + D) (hgapUpper : ∀ (n : ℕ), index n ≤ ChartScales.nativeIndex h n + D) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 1 ≤ L n) (hS : ∀ (n : ℕ), ChartScales.S n ≤ L n) {f : ℕ → Point Plane → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) U.carrier (f n)) (hp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (f n)) (hm : ∀ (n : ℕ), ∀ s ∈ U.carrier, PressureStream.pressureMass (f n) s = 0) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR (ChartScales.epsilon h) L ⋯ ⋯ hL) α f) (β : ℝ) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR (ChartScales.epsilon h) L ⋯ ⋯ hL) β fun (n : ℕ) => MeanChartCompatibility.fastAtIndex h n (index n) (PressureStream.divideRadius (VariableGaugeMean.compactAlias (ChartScales.radialExponent h) a b (MeanChartCompatibility.radialFrequency h n (index n) (ChartScales.radialExponent h) Mbase) (VariableGaugeMean.qLength coord) (TorusInverse.vector TorusInverse.Direction.radial) (f n)))

noncomputable def NavierStokes.GaugeAliasDecay.temporalSource (h : ℝ) (index : ℕ → ℕ) (f : ℕ → Point Plane → ℝ) : ℕ → Point Plane → ℝ

Temporal source, defined pointwise by PressureStream.weightedSource (MeanChartCompatibility.temporalAtIndex h n (index n) (f n)).

Equations

• NavierStokes.GaugeAliasDecay.temporalSource h index f n = NavierStokes.PressureStream.weightedSource (NavierStokes.MeanChartCompatibility.temporalAtIndex h n (index n) (f n))

theorem NavierStokes.GaugeAliasDecay.temporalAtIndex_zeroMean_on {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (h : ℝ) (n i : ℕ) {f : Point Plane → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) (hp : PhysicalMeanDomain.PeriodicOn U.carrier f) (R : ℝ) {s : Plane} (hs : s ∈ U.carrier) : PressureStream.torusAverage (MeanChartCompatibility.temporalAtIndex h n i f) (R, s) = 0

theorem NavierStokes.GaugeAliasDecay.temporalSource_movingField {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) (h : ℝ) (index : ℕ → ℕ) {f : ℕ → Point Plane → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) U.carrier (f n)) (hp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (f n)) : GaugeMomentBalances.MovingField U a b (temporalSource h index f)

theorem NavierStokes.GaugeAliasDecay.temporalSource_zero_mass {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (h : ℝ) (index : ℕ → ℕ) {f : ℕ → Point Plane → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (f n)) (n : ℕ) {s : Plane} (hs : s ∈ U.carrier) : PressureStream.pressureMass (temporalSource h index f n) s = 0

theorem NavierStokes.GaugeAliasDecay.temporalSource_mem {coord a b h α : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 < h) (index : ℕ → ℕ) (D : ℕ) (hgap : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + D) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 1 ≤ L n) (hS : ∀ (n : ℕ), ChartScales.S n ≤ L n) {f : ℕ → Point Plane → ℝ} (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 (ChartScales.epsilon h) L ⋯ ⋯ hL) α f) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR (ChartScales.epsilon h) L ⋯ ⋯ hL) α (temporalSource h index f)

theorem NavierStokes.GaugeAliasDecay.temporalAxialDifference_mem {a b h Mbase α : ℝ} (U : LocalSignedRequest.SlowRegion (2 * h)) (ha : 0 < a) (hab : a < b) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 < h) (hM : Mbase ≠ 0) (index : ℕ → ℕ) (D : ℕ) (hgap : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + D) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 1 ≤ L n) (hS : ∀ (n : ℕ), ChartScales.S n ≤ L n) (c : CorrectionState.Context (Point Plane)) (u : CorrectionState.State (Point Plane)) (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.axialResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength (2 * h)) U.carrier (u.axialResidual c n)) (hp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.axialResidual c n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR (ChartScales.epsilon h) L ⋯ ⋯ hL) α (u.axialResidual c)) (β : ℝ) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR (ChartScales.epsilon h) L ⋯ ⋯ hL) β (VariableGaugeMean.temporalAxialDifference (VariableGaugeMean.similarityGauge h (ChartScales.radialExponent h) a b Mbase hab index) h index c u)

The actual stream error in the temporal state update has every target mean-class order. Its source is the constructed weighted temporal increment.

theorem NavierStokes.GaugeAliasDecay.temporalAliasState_axial_mem {a b h Mbase α : ℝ} (U : LocalSignedRequest.SlowRegion (2 * h)) (ha : 0 < a) (hab : a < b) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 < h) (hM : Mbase ≠ 0) (index : ℕ → ℕ) (D : ℕ) (hgapLower : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + D) (hgapUpper : ∀ (n : ℕ), index n ≤ ChartScales.nativeIndex h n + D) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 1 ≤ L n) (hS : ∀ (n : ℕ), ChartScales.S n ≤ L n) (c : CorrectionState.Context (Point Plane)) (u : CorrectionState.State (Point Plane)) (hfast : c.operators.fastCoefficient = fun (n : ℕ) => ChartScales.Tg ^ index n * ChartScales.Q n ^ (1 + h)) (hv : c.operators.vT = (0, 0, TorusInverse.vector TorusInverse.Direction.temporal)) (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.axialResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength (2 * h)) U.carrier (u.axialResidual c n)) (hp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.axialResidual c n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR (ChartScales.epsilon h) L ⋯ ⋯ hL) α (u.axialResidual c)) (β : ℝ) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR (ChartScales.epsilon h) L ⋯ ⋯ hL) β fun (n : ℕ) (z : LocalSignedRequest.Point) => VariableGaugeMean.temporalAliasState (VariableGaugeMean.similarityGauge h (ChartScales.radialExponent h) a b Mbase hab index) h index c u n (z, 0) 2

The axial coefficient stored in the actual temporal alias state is superflat with the true common fast coefficient and torus direction.

theorem NavierStokes.GaugeAliasDecay.pressureSource_zero_mass {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) (hab : a < b) {f : Point Plane → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) (hs : VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) U.carrier f) {s : Plane} (hsm : s ∈ U.carrier) : PressureStream.pressureMass (VariableGaugeMean.pressureSource a b hab (VariableGaugeMean.qLength coord) f) s = 0

The moving pressure recipe has zero measured mass, derived from its normalized physical bump, with no imposed zero-mass premise on the raw source.

theorem NavierStokes.GaugeAliasDecay.pressureAliasState_radial_mem {a b h Mbase α : ℝ} (U : LocalSignedRequest.SlowRegion (2 * h)) (ha : 0 < a) (hab : a < b) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 < h) (hM : Mbase ≠ 0) (index : ℕ → ℕ) (D : ℕ) (hgap : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + D) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 1 ≤ L n) (hS : ∀ (n : ℕ), ChartScales.S n ≤ L n) (c : CorrectionState.Context (Point Plane)) (u : CorrectionState.State (Point Plane)) (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.gr c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength (2 * h)) U.carrier (u.gr c n)) (hp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.gr c n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR (ChartScales.epsilon h) L ⋯ ⋯ hL) α (u.gr c)) (β : ℝ) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR (ChartScales.epsilon h) L ⋯ ⋯ hL) β fun (n : ℕ) (z : LocalSignedRequest.Point) => VariableGaugeMean.pressureAliasState (VariableGaugeMean.similarityGauge h (ChartScales.radialExponent h) a b Mbase hab index) c u n (z, 0) 0

Superflatness of the actual radial coefficient stored by moving pressure reconstruction. The raw gr source may have nonzero pressure debt.