The exact temporal mean update

The native-to-absolute inverse identity is derived from the actual covering map, Fourier coefficients, and uniqueness for the zero-mean periodic directional equation. Band factors remain explicit.

noncomputable def NavierStokes.TemporalMeanUpdate.partialY (f : TorusInverse.Plane → ℂ) (z : TorusInverse.Plane) : ℂ

Partial Y, given by fderiv ℝ f z (0, 1).

Equations

• NavierStokes.TemporalMeanUpdate.partialY f z = (fderiv ℝ f z) (0, 1)

noncomputable def NavierStokes.TemporalMeanUpdate.timeDerivative (f : TorusInverse.Plane → ℂ) (z : TorusInverse.Plane) : ℂ

Time derivative, given by fderiv ℝ f z (vector .temporal).

Equations

• NavierStokes.TemporalMeanUpdate.timeDerivative f z = (fderiv ℝ f z) (NavierStokes.TorusInverse.vector NavierStokes.TorusInverse.Direction.temporal)

theorem NavierStokes.TemporalMeanUpdate.partialY_smooth {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (partialY f)

theorem NavierStokes.TemporalMeanUpdate.coefficient_const_mul (c : ℂ) (f : TorusInverse.Plane → ℂ) (k : TorusInverse.Frequency) : SmoothFourierData.coefficient (fun (z : TorusInverse.Plane) => c * f z) k = c * SmoothFourierData.coefficient f k

theorem NavierStokes.TemporalMeanUpdate.coefficient_add {f g : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (k : TorusInverse.Frequency) : SmoothFourierData.coefficient (fun (z : TorusInverse.Plane) => f z + g z) k = SmoothFourierData.coefficient f k + SmoothFourierData.coefficient g k

theorem NavierStokes.TemporalMeanUpdate.coefficient_partialX {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : SmoothFourierData.UnitPeriodic f) (k : TorusInverse.Frequency) : SmoothFourierData.coefficient (SmoothFourierData.partialX f) k = TorusInverse.omega * ↑k.1 * SmoothFourierData.coefficient f k

Fourier differentiation, including the zero first frequency.

theorem NavierStokes.TemporalMeanUpdate.swap_partialY {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) : SmoothFourierData.swapFunction (partialY f) = SmoothFourierData.partialX (SmoothFourierData.swapFunction f)

theorem NavierStokes.TemporalMeanUpdate.coefficient_partialY {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : SmoothFourierData.UnitPeriodic f) (k : TorusInverse.Frequency) : SmoothFourierData.coefficient (partialY f) k = TorusInverse.omega * ↑k.2 * SmoothFourierData.coefficient f k

theorem NavierStokes.TemporalMeanUpdate.timeDerivative_eq_partials (f : TorusInverse.Plane → ℂ) (z : TorusInverse.Plane) : timeDerivative f z = ↑(TorusInverse.vector TorusInverse.Direction.temporal).1 * SmoothFourierData.partialX f z + ↑(TorusInverse.vector TorusInverse.Direction.temporal).2 * partialY f z

theorem NavierStokes.TemporalMeanUpdate.coefficient_timeDerivative {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : SmoothFourierData.UnitPeriodic f) (k : TorusInverse.Frequency) : SmoothFourierData.coefficient (timeDerivative f) k = TorusInverse.omega * ↑(TorusInverse.symbol TorusInverse.Direction.temporal k) * SmoothFourierData.coefficient f k

The temporal Fourier symbol is the actual multiplier of the derivative.

theorem NavierStokes.TemporalMeanUpdate.timeDerivative_unique {f g : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hpf : SmoothFourierData.UnitPeriodic f) (hpg : SmoothFourierData.UnitPeriodic g) (hD : timeDerivative f = timeDerivative g) (hm : TorusAverages.squareAverage f = TorusAverages.squareAverage g) : f = g

Uniqueness for the smooth periodic temporal equation with a prescribed mean. The proof uses actual Fourier differentiation and reconstruction.

noncomputable def NavierStokes.TemporalMeanUpdate.coverLinear : TorusInverse.Plane →L[ℝ] TorusInverse.Plane

The actual integer covering as a continuous linear map.

Equations

• NavierStokes.TemporalMeanUpdate.coverLinear = (3 • ContinuousLinearMap.fst ℝ ℝ ℝ + ContinuousLinearMap.snd ℝ ℝ ℝ).prod (ContinuousLinearMap.fst ℝ ℝ ℝ + 5 • ContinuousLinearMap.snd ℝ ℝ ℝ)

theorem NavierStokes.TemporalMeanUpdate.coverLinear_apply (z : TorusInverse.Plane) : coverLinear z = TorusAverages.covering z

noncomputable def NavierStokes.TemporalMeanUpdate.coverMap : ℕ → TorusInverse.Plane →L[ℝ] TorusInverse.Plane

Cover map as an element of `ℕ → Plane →L[ℝ] Plane | 0 => ContinuousLinearMap.id ℝ Plane | n

• 1 => coverLinear.comp (coverMap n)`.

Equations

• NavierStokes.TemporalMeanUpdate.coverMap 0 = ContinuousLinearMap.id ℝ NavierStokes.TorusInverse.Plane
• NavierStokes.TemporalMeanUpdate.coverMap n.succ = NavierStokes.TemporalMeanUpdate.coverLinear ∘SL NavierStokes.TemporalMeanUpdate.coverMap n

theorem NavierStokes.TemporalMeanUpdate.coverMap_eq_iterate (n : ℕ) (z : TorusInverse.Plane) : (coverMap n) z = TorusAverages.covering^[n] z

theorem NavierStokes.TemporalMeanUpdate.coverLinear_temporal : coverLinear (TorusInverse.vector TorusInverse.Direction.temporal) = ChartScales.Tg • TorusInverse.vector TorusInverse.Direction.temporal

theorem NavierStokes.TemporalMeanUpdate.coverMap_temporal (n : ℕ) : (coverMap n) (TorusInverse.vector TorusInverse.Direction.temporal) = ChartScales.Tg ^ n • TorusInverse.vector TorusInverse.Direction.temporal

theorem NavierStokes.TemporalMeanUpdate.coverLinear_lattice (k : TorusInverse.Frequency) : coverLinear (↑k.1, ↑k.2) = (↑(DiophantineGraph.coveringFrequency k).1, ↑(DiophantineGraph.coveringFrequency k).2)

theorem NavierStokes.TemporalMeanUpdate.coverMap_lattice (n : ℕ) (k : TorusInverse.Frequency) : (coverMap n) (↑k.1, ↑k.2) = (↑(DiophantineGraph.coveringFrequency^[n] k).1, ↑(DiophantineGraph.coveringFrequency^[n] k).2)

theorem NavierStokes.TemporalMeanUpdate.periodic_coverMap {f : TorusInverse.Plane → ℂ} (hp : SmoothFourierData.UnitPeriodic f) (n : ℕ) : SmoothFourierData.UnitPeriodic fun (z : TorusInverse.Plane) => f ((coverMap n) z)

theorem NavierStokes.TemporalMeanUpdate.timeDerivative_coverMap {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (z : TorusInverse.Plane) : timeDerivative (fun (x : TorusInverse.Plane) => f ((coverMap n) x)) z = ChartScales.Tg ^ n • timeDerivative f ((coverMap n) z)

noncomputable def NavierStokes.TemporalMeanUpdate.absoluteInverse (f : TorusInverse.Plane → ℂ) : TorusInverse.Plane → ℂ

Absolute inverse, given by directionalInverse .temporal (SmoothFourierData.coefficient f).

Equations

• NavierStokes.TemporalMeanUpdate.absoluteInverse f = NavierStokes.TorusInverse.directionalInverse NavierStokes.TorusInverse.Direction.temporal (NavierStokes.SmoothFourierData.coefficient f)

theorem NavierStokes.TemporalMeanUpdate.absoluteInverse_smooth {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : SmoothFourierData.UnitPeriodic f) : ContDiff ℝ (↑⊤) (absoluteInverse f)

theorem NavierStokes.TemporalMeanUpdate.absoluteInverse_periodic (f : TorusInverse.Plane → ℂ) : SmoothFourierData.UnitPeriodic (absoluteInverse f)

theorem NavierStokes.TemporalMeanUpdate.absoluteInverse_zeroMean {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : SmoothFourierData.UnitPeriodic f) : TorusAverages.squareAverage (absoluteInverse f) = 0

theorem NavierStokes.TemporalMeanUpdate.absoluteInverse_solves {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : SmoothFourierData.UnitPeriodic f) (hm : TorusAverages.squareAverage f = 0) : timeDerivative (absoluteInverse f) = f

theorem NavierStokes.TemporalMeanUpdate.absoluteInverse_coverMap {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : SmoothFourierData.UnitPeriodic f) (hm : TorusAverages.squareAverage f = 0) (n : ℕ) : (absoluteInverse fun (z : TorusInverse.Plane) => f ((coverMap n) z)) = fun (z : TorusInverse.Plane) => (ChartScales.Tg ^ n)⁻¹ • absoluteInverse f ((coverMap n) z)

The native factor is forced by the covering derivative and zero-mean uniqueness. Both sides are the actual Fourier-defined inverse.

noncomputable def NavierStokes.TemporalMeanUpdate.chartPrefactor (h : ℝ) (n : ℕ) : ℝ

The native chart prefactor, including the physical velocity rescaling.

Equations

• NavierStokes.TemporalMeanUpdate.chartPrefactor h n = (NavierStokes.ChartScales.timeCoefficient h n)⁻¹

theorem NavierStokes.TemporalMeanUpdate.chartPrefactor_pos (h : ℝ) (n : ℕ) : 0 < chartPrefactor h n

theorem NavierStokes.TemporalMeanUpdate.chartPrefactor_eq (h : ℝ) (n : ℕ) : chartPrefactor h n = ChartScales.Q n ^ (-1 - h) * (ChartScales.Tg ^ ChartScales.nativeIndex h n)⁻¹

theorem NavierStokes.TemporalMeanUpdate.chartPrefactor_bound (h : ℝ) (hh : 0 ≤ h) {n : ℕ} (hn : 4 ≤ n) : ‖chartPrefactor h n‖ ≤ ChartScales.Tg * ChartScales.S n

The exponential-looking native factors together cost just one power of the slow band scale.

theorem NavierStokes.TemporalMeanUpdate.chartPrefactor_bandBound {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (h : ℝ) (hh : 0 ≤ h) (hs : ∀ (n : ℕ), s.slow n = ChartScales.S (n + 4)) : WeightedClasses.BandBound s 0 fun (n : ℕ) => chartPrefactor h (n + 4)

theorem NavierStokes.TemporalMeanUpdate.meanClass_chartPrefactor {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {α h : ℝ} {f : ℕ → D → E} (hh : 0 ≤ h) (hs : ∀ (n : ℕ), s.slow n = ChartScales.S (n + 4)) (hf : WeightedClasses.MeanClass s α f) : WeightedClasses.MeanClass s α fun (n : ℕ) (z : D) => chartPrefactor h (n + 4) • f n z

Multiplication by the actual chart prefactor preserves the class exponent, for bands numbered n+4 where the native-index bounds hold.

theorem NavierStokes.TemporalMeanUpdate.chartPrefactor_bandBound_all {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (h : ℝ) (hh : 0 ≤ h) (hs : ∀ (n : ℕ), ChartScales.S n ≤ s.slow n) : WeightedClasses.BandBound s 0 (chartPrefactor h)

Finite initial bands are absorbed into an explicit constant. The native indices are unchanged; the slow scale may be max 1 (S n).

theorem NavierStokes.TemporalMeanUpdate.meanClass_chartPrefactor_all {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {α h : ℝ} {f : ℕ → D → E} (hh : 0 ≤ h) (hs : ∀ (n : ℕ), ChartScales.S n ≤ s.slow n) (hf : WeightedClasses.MeanClass s α f) : WeightedClasses.MeanClass s α fun (n : ℕ) (z : D) => chartPrefactor h n • f n z

noncomputable def NavierStokes.TemporalMeanUpdate.centered {S : Type} (f : PressureStream.Lift S → ℝ) (z : PressureStream.Lift S) : ℝ

Remove exactly the auxiliary torus average, retaining every slow parameter.

Equations

• NavierStokes.TemporalMeanUpdate.centered f z = f z - NavierStokes.PressureStream.torusAverage f (z.1, z.2.1)

theorem NavierStokes.TemporalMeanUpdate.centered_smooth {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (centered f)

theorem NavierStokes.TemporalMeanUpdate.centered_zeroMean {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (p : ℝ × S) : PressureStream.torusAverage (centered f) p = 0

theorem NavierStokes.TemporalMeanUpdate.centered_periodic {S : Type} {f : PressureStream.Lift S → ℝ} (hp : PressureStream.TorusPeriodicLift f) : PressureStream.TorusPeriodicLift (centered f)

theorem NavierStokes.TemporalMeanUpdate.centered_supported {S : Type} {a b : ℝ} {f : PressureStream.Lift S → ℝ} (hs : RadialAlias.RadiallySupported a b f) : RadialAlias.RadiallySupported a b (centered f)

theorem NavierStokes.TemporalMeanUpdate.squareAverage_re {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) : (TorusAverages.squareAverage fun (z : TorusInverse.Plane) => (f z).re) = (TorusAverages.squareAverage f).re

Taking a real part commutes with the actual double integral.

noncomputable def NavierStokes.TemporalMeanUpdate.sourceToFamily {S : Type} (f : PressureStream.Lift S → ℝ) (z : (ℝ × S) × TorusInverse.Plane) : ℂ

The source in joint slow-parameter/torus coordinates, with the real source embedded isometrically in the complex Fourier construction.

Equations

• NavierStokes.TemporalMeanUpdate.sourceToFamily f z = ↑(f (z.1.1, z.1.2, z.2))

theorem NavierStokes.TemporalMeanUpdate.sourceToFamily_smooth {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (sourceToFamily f)

theorem NavierStokes.TemporalMeanUpdate.sourceToFamily_periodic {S : Type} {f : PressureStream.Lift S → ℝ} (hp : PressureStream.TorusPeriodicLift f) : SmoothFamilyTorusInverse.Periodic (sourceToFamily f)

theorem NavierStokes.TemporalMeanUpdate.sourceToFamily_mean {S : Type} (f : PressureStream.Lift S → ℝ) (p : ℝ × S) : SmoothFamilyTorusInverse.mean (sourceToFamily f) p = ↑(PressureStream.torusAverage f p)

noncomputable def NavierStokes.TemporalMeanUpdate.temporalInverse {S : Type} (f : PressureStream.Lift S → ℝ) (z : PressureStream.Lift S) : ℝ

The actual normalized temporal Fourier inverse on a real joint family.

Equations

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

theorem NavierStokes.TemporalMeanUpdate.temporalInverse_periodic {S : Type} (f : PressureStream.Lift S → ℝ) : PressureStream.TorusPeriodicLift (temporalInverse f)

theorem NavierStokes.TemporalMeanUpdate.temporalInverse_supported {S : Type} {a b : ℝ} {f : PressureStream.Lift S → ℝ} (hs : RadialAlias.RadiallySupported a b f) : RadialAlias.RadiallySupported a b (temporalInverse f)

theorem NavierStokes.TemporalMeanUpdate.temporalInverse_smooth {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) : ContDiff ℝ (↑⊤) (temporalInverse f)

theorem NavierStokes.TemporalMeanUpdate.temporalInverse_zeroMean {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (p : ℝ × S) : PressureStream.torusAverage (temporalInverse f) p = 0

theorem NavierStokes.TemporalMeanUpdate.temporalInverse_solves {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (hm : ∀ (p : ℝ × S), PressureStream.torusAverage f p = 0) (z : PressureStream.Lift S) : PressureStream.graphDz (0, TorusInverse.vector TorusInverse.Direction.temporal) (temporalInverse f) z = f z

The real joint inverse solves the genuine Fréchet directional equation.

theorem NavierStokes.TemporalMeanUpdate.temporalInverse_coverMap {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (hm : ∀ (p : ℝ × S), PressureStream.torusAverage f p = 0) (n : ℕ) (z : PressureStream.Lift S) : temporalInverse (fun (p : PressureStream.Lift S) => f (p.1, p.2.1, (coverMap n) p.2.2)) z = (ChartScales.Tg ^ n)⁻¹ * temporalInverse f (z.1, z.2.1, (coverMap n) z.2.2)

Fiberwise native-to-absolute covariance for the actual real family inverse.

noncomputable def NavierStokes.TemporalMeanUpdate.desiredIncrement {S : Type} (h : ℝ) (n : ℕ) (f : PressureStream.Lift S → ℝ) (z : PressureStream.Lift S) : ℝ

The desired angular or axial mean increment in its native chart.

Equations

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

noncomputable def NavierStokes.TemporalMeanUpdate.fastDerivative {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (h : ℝ) (n : ℕ) (f : PressureStream.Lift S → ℝ) (z : PressureStream.Lift S) : ℝ

The actual fast-time derivative, including its chart coefficient.

Equations

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

theorem NavierStokes.TemporalMeanUpdate.desiredIncrement_smooth {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (h : ℝ) (n : ℕ) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) : ContDiff ℝ (↑⊤) (desiredIncrement h n f)

theorem NavierStokes.TemporalMeanUpdate.desiredIncrement_periodic {S : Type} (h : ℝ) (n : ℕ) (f : PressureStream.Lift S → ℝ) : PressureStream.TorusPeriodicLift (desiredIncrement h n f)

theorem NavierStokes.TemporalMeanUpdate.desiredIncrement_supported {S : Type} (h : ℝ) (n : ℕ) {a b : ℝ} {f : PressureStream.Lift S → ℝ} (hs : RadialAlias.RadiallySupported a b f) : RadialAlias.RadiallySupported a b (desiredIncrement h n f)

theorem NavierStokes.TemporalMeanUpdate.desiredIncrement_zeroMean {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (h : ℝ) (n : ℕ) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (p : ℝ × S) : PressureStream.torusAverage (desiredIncrement h n f) p = 0

theorem NavierStokes.TemporalMeanUpdate.desiredIncrement_barMass {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (h : ℝ) (n : ℕ) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (w : ℝ → ℝ) (s : S) : ∫ (r : ℝ), w r * PressureStream.torusAverage (desiredIncrement h n f) (r, s) = 0

In particular this gives both the angular r² bar mass and axial r bar mass without an extra normalization term.

theorem NavierStokes.TemporalMeanUpdate.desiredIncrement_fastDerivative {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (h : ℝ) (n : ℕ) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (z : PressureStream.Lift S) : fastDerivative h n (desiredIncrement h n f) z = -centered f z

Exact cancellation of the source's zero-bar part.

theorem NavierStokes.TemporalMeanUpdate.fastDerivative_sub {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (h : ℝ) (n : ℕ) {f g : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (z : PressureStream.Lift S) : fastDerivative h n (fun (p : PressureStream.Lift S) => f p - g p) z = fastDerivative h n f z - fastDerivative h n g z

noncomputable def NavierStokes.TemporalMeanUpdate.pullbackCover {S : Type} (i : ℕ) (f : PressureStream.Lift S → ℝ) (z : PressureStream.Lift S) : ℝ

Pullback cover, given by f (z.1, (z.2.1, coverMap i z.2.2)).

Equations

• NavierStokes.TemporalMeanUpdate.pullbackCover i f z = f (z.1, z.2.1, (NavierStokes.TemporalMeanUpdate.coverMap i) z.2.2)

theorem NavierStokes.TemporalMeanUpdate.pullbackCover_smooth {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (i : ℕ) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (pullbackCover i f)

theorem NavierStokes.TemporalMeanUpdate.pullbackCover_periodic {S : Type} (i : ℕ) {f : PressureStream.Lift S → ℝ} (hp : PressureStream.TorusPeriodicLift f) : PressureStream.TorusPeriodicLift (pullbackCover i f)

theorem NavierStokes.TemporalMeanUpdate.torusAverage_pullbackCover {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (i : ℕ) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (p : ℝ × S) : PressureStream.torusAverage (pullbackCover i f) p = PressureStream.torusAverage f p

theorem NavierStokes.TemporalMeanUpdate.centered_pullbackCover {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (i : ℕ) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) : centered (pullbackCover i f) = pullbackCover i (centered f)

theorem NavierStokes.TemporalMeanUpdate.desiredIncrement_native_pullback {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (h : ℝ) (n : ℕ) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (z : PressureStream.Lift S) : pullbackCover (ChartScales.nativeIndex h n) (desiredIncrement h n f) z = -ChartScales.Q n ^ (-1 - h) * temporalInverse (centered (pullbackCover (ChartScales.nativeIndex h n) f)) z

Pulling the native update through its actual covering gives the same absolute temporal inverse. There is exactly one native Tg⁻ⁱ factor.

noncomputable def NavierStokes.TemporalMeanUpdate.axialPotential {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (v : TorusInverse.Plane) (h : ℝ) (n : ℕ) (f : PressureStream.Lift S → ℝ) : PressureStream.Lift S → ℝ

Axial potential, given by PressureStream.streamPotential d a b M ((0 : S), v) (desiredIncrement h n f).

Equations

• NavierStokes.TemporalMeanUpdate.axialPotential d a b M v h n f = NavierStokes.PressureStream.streamPotential d a b M (0, v) (NavierStokes.TemporalMeanUpdate.desiredIncrement h n f)

noncomputable def NavierStokes.TemporalMeanUpdate.axialUpdate {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (v : TorusInverse.Plane) (h : ℝ) (n : ℕ) (f : PressureStream.Lift S → ℝ) : PressureStream.Lift S → ℝ

Axial update, given by PressureStream.streamGamma (PressureStream.physicalSpeed d M) ((0 : S), v) (axialPotential d a b M v h n f).

Equations

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

noncomputable def NavierStokes.TemporalMeanUpdate.radialUpdate {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (v : TorusInverse.Plane) (w : S × TorusInverse.Plane) (h : ℝ) (n : ℕ) (f : PressureStream.Lift S → ℝ) : PressureStream.Lift S → ℝ

Radial update, given by PressureStream.streamBeta w (axialPotential d a b M v h n f).

Equations

• NavierStokes.TemporalMeanUpdate.radialUpdate d a b M v w h n f = NavierStokes.PressureStream.streamBeta w (NavierStokes.TemporalMeanUpdate.axialPotential d a b M v h n f)

theorem NavierStokes.TemporalMeanUpdate.radialUpdate_smul_direction {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (v : TorusInverse.Plane) (w : S × TorusInverse.Plane) (h c : ℝ) (n : ℕ) (f : PressureStream.Lift S → ℝ) : radialUpdate d a b M v (c • w) h n f = fun (z : PressureStream.Lift S) => c * radialUpdate d a b M v w h n f z

noncomputable def NavierStokes.TemporalMeanUpdate.axialAlias {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (v : TorusInverse.Plane) (h : ℝ) (n : ℕ) (f : PressureStream.Lift S → ℝ) : PressureStream.Lift S → ℝ

The retained compactification alias, with its physical 1/r factor.

Equations

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

theorem NavierStokes.TemporalMeanUpdate.axialAlias_eq_cutoff_total {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : TorusInverse.Plane) (h : ℝ) (n : ℕ) (f : PressureStream.Lift S → ℝ) (z : PressureStream.Lift S) : axialAlias d a b M v h n f z = deriv (RadialPullback.physicalCutoff d a b) z.1 * PressureStream.physicalTotal d a M (0, v) (PressureStream.weightedSource (desiredIncrement h n f)) z / z.1

theorem NavierStokes.TemporalMeanUpdate.axialPotential_smooth {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : TorusInverse.Plane) (h : ℝ) (n : ℕ) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (hs : RadialAlias.RadiallySupported a b f) : ContDiff ℝ (↑⊤) (axialPotential d a b M v h n f)

theorem NavierStokes.TemporalMeanUpdate.axialPotential_supported {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : TorusInverse.Plane) (h : ℝ) (n : ℕ) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (hs : RadialAlias.RadiallySupported a b f) : RadialAlias.RadiallySupported a b (axialPotential d a b M v h n f)

theorem NavierStokes.TemporalMeanUpdate.axialUpdate_smooth {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : TorusInverse.Plane) (h : ℝ) (n : ℕ) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (hs : RadialAlias.RadiallySupported a b f) : ContDiff ℝ (↑⊤) (axialUpdate d a b M v h n f)

theorem NavierStokes.TemporalMeanUpdate.axialUpdate_supported {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : TorusInverse.Plane) (h : ℝ) (n : ℕ) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (hs : RadialAlias.RadiallySupported a b f) : RadialAlias.RadiallySupported a b (axialUpdate d a b M v h n f)

theorem NavierStokes.TemporalMeanUpdate.radialUpdate_smooth {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : TorusInverse.Plane) (w : S × TorusInverse.Plane) (h : ℝ) (n : ℕ) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (hs : RadialAlias.RadiallySupported a b f) : ContDiff ℝ (↑⊤) (radialUpdate d a b M v w h n f)

theorem NavierStokes.TemporalMeanUpdate.radialUpdate_supported {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : TorusInverse.Plane) (w : S × TorusInverse.Plane) (h : ℝ) (n : ℕ) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (hs : RadialAlias.RadiallySupported a b f) : RadialAlias.RadiallySupported a b (radialUpdate d a b M v w h n f)

theorem NavierStokes.TemporalMeanUpdate.axialAlias_smooth {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : TorusInverse.Plane) (h : ℝ) (n : ℕ) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (hs : RadialAlias.RadiallySupported a b f) : ContDiff ℝ (↑⊤) (axialAlias d a b M v h n f)

theorem NavierStokes.TemporalMeanUpdate.axialAlias_supported {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : TorusInverse.Plane) (h : ℝ) (n : ℕ) (f : PressureStream.Lift S → ℝ) : RadialAlias.RadiallySupported a b (axialAlias d a b M v h n f)

theorem NavierStokes.TemporalMeanUpdate.axialUpdate_eq_desired_sub_alias {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : TorusInverse.Plane) (h : ℝ) (n : ℕ) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (hs : RadialAlias.RadiallySupported a b f) : axialUpdate d a b M v h n f = fun (z : PressureStream.Lift S) => desiredIncrement h n f z - axialAlias d a b M v h n f z

No compactification error is removed from the reconstructed axial field.

theorem NavierStokes.TemporalMeanUpdate.update_divergence_zero {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : TorusInverse.Plane) (w : S × TorusInverse.Plane) (h : ℝ) (n : ℕ) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (hs : RadialAlias.RadiallySupported a b f) (z : PressureStream.Lift S) : PressureStream.graphDivergence (PressureStream.physicalSpeed d M) (0, v) w (radialUpdate d a b M v w h n f) (axialUpdate d a b M v h n f) z = 0

theorem NavierStokes.TemporalMeanUpdate.axialUpdate_zeroMean {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : TorusInverse.Plane) (h : ℝ) (n : ℕ) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (hs : RadialAlias.RadiallySupported a b f) (p : ℝ × S) : PressureStream.torusAverage (axialUpdate d a b M v h n f) p = 0

theorem NavierStokes.TemporalMeanUpdate.axialUpdate_fast_residual {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : TorusInverse.Plane) (h : ℝ) (n : ℕ) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (hs : RadialAlias.RadiallySupported a b f) (z : PressureStream.Lift S) : fastDerivative h n (axialUpdate d a b M v h n f) z + centered f z = -fastDerivative h n (axialAlias d a b M v h n f) z

Fast time cancels the axial zero-bar source, retaining exactly the fast-time derivative of the compactification alias.

theorem NavierStokes.TemporalMeanUpdate.temporal_mean_update {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : TorusInverse.Plane) (w : S × TorusInverse.Plane) (h : ℝ) (n : ℕ) {fθ fz : PressureStream.Lift S → ℝ} (hθ : ContDiff ℝ (↑⊤) fθ) (hz : ContDiff ℝ (↑⊤) fz) (hpθ : PressureStream.TorusPeriodicLift fθ) (hpz : PressureStream.TorusPeriodicLift fz) (hsz : RadialAlias.RadiallySupported a b fz) (z : PressureStream.Lift S) : fastDerivative h n (desiredIncrement h n fθ) z + centered fθ z = 0 ∧ fastDerivative h n (axialUpdate d a b M v h n fz) z + centered fz z = -fastDerivative h n (axialAlias d a b M v h n fz) z ∧ PressureStream.graphDivergence (PressureStream.physicalSpeed d M) (0, v) w (radialUpdate d a b M v w h n fz) (axialUpdate d a b M v h n fz) z = 0 ∧ PressureStream.torusAverage (desiredIncrement h n fθ) (z.1, z.2.1) = 0 ∧ PressureStream.torusAverage (axialUpdate d a b M v h n fz) (z.1, z.2.1) = 0

The actual two-component fast-time update and incompressible stream, with the exact axial alias in the resulting residual.

theorem NavierStokes.TemporalMeanUpdate.meanClass_radialMultiply {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (a b : ℝ) {φ : ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) {s : WeightedClasses.StripData (ℝ × E)} {α : ℝ} {g : ℕ → ℝ × E → V} (hdomain : ∀ z ∈ s.domain, z.1 ∈ Set.Icc a b) (hg : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (g n)) (hclass : WeightedClasses.MeanClass s α g) : WeightedClasses.MeanClass s α fun (n : ℕ) (z : ℝ × E) => φ z.1 • g n z

A fixed smooth radial multiplier preserves the actual all-jet class. The constant is obtained from the derivative product rule on the compact annulus.

theorem NavierStokes.TemporalMeanUpdate.meanClass_divideRadius {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (ha : 0 < a) {s : WeightedClasses.StripData (ℝ × E)} {α : ℝ} {g : ℕ → ℝ × E → ℝ} (hdomain : ∀ z ∈ s.domain, z.1 ∈ Set.Icc a b) (hg : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (g n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (g n)) (hclass : WeightedClasses.MeanClass s α g) : WeightedClasses.MeanClass s α fun (n : ℕ) => PressureStream.divideRadius (g n)

Division by the positive radius preserves the class for supported fields. A globally smooth positive regularization proves all derivative bounds.

theorem NavierStokes.TemporalMeanUpdate.meanClass_streamPotential {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b d cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (ε R : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hR : ∀ (n : ℕ), 1 ≤ R n) (α : ℝ) (M : ℕ → ℝ) (v : ℕ → E) (g : ℕ → ℝ × E → ℝ) (hg : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (g n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (g n)) (hclass : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α g) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α fun (n : ℕ) => PressureStream.streamPotential d a b (M n) (v n) (g n)

The actual stream potential preserves the original exponential weight and its exponent, uniformly for all bandwise transport coefficients.

theorem NavierStokes.TemporalMeanUpdate.meanClass_streamBeta {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b d cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (ε R : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hR : ∀ (n : ℕ), 1 ≤ R n) (α : ℝ) (M : ℕ → ℝ) (v : ℕ → E) (w : E) (g : ℕ → ℝ × E → ℝ) (hg : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (g n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (g n)) (hclass : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α g) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α fun (n : ℕ) => PressureStream.streamBeta w (PressureStream.streamPotential d a b (M n) (v n) (g n))

A fixed full axial direction may include every slow variable. Its actual derivative of the stream has the same class exponent.

noncomputable def NavierStokes.TemporalMeanUpdate.aliasFactor (d a r : ℝ) : ℝ

Alias factor, given by RadialPullback.radialJacobian d (RadialPullback.positiveRadius (a / 4) r) / RadialPullback.positiveRadius (a / 4) r.

Equations

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

theorem NavierStokes.TemporalMeanUpdate.aliasFactor_smooth {a : ℝ} (ha : 0 < a) (d : ℝ) : ContDiff ℝ (↑⊤) (aliasFactor d a)

theorem NavierStokes.TemporalMeanUpdate.dividedAlias_eq_pullback {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : E) (g : ℝ × E → ℝ) : PressureStream.divideRadius (RadialPullback.physicalAlias d a b M v g) = fun (z : ℝ × E) => aliasFactor d a z.1 * UniformFourierAlias.exactAlias (TransportPrimitive.interiorCutoff (a ^ d) (b ^ d)) M v (RadialPullback.normalizeSource d a g) (RadialPullback.liftChart (RadialPullback.powerChart d a) z)

The physical divided alias is exactly a fixed radial multiplier times the normalized transport alias pulled through the power chart.

theorem NavierStokes.TemporalMeanUpdate.dividedAlias_finiteJets_transfer {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {d a b : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (M : ℝ) (v : E) (g : ℝ × E → ℝ), ContDiff ℝ (↑⊤) g → RadialAlias.RadiallySupported a b g → ∀ (C : ℝ), 0 ≤ C → (∀ j ≤ m, ∀ (z : ℝ × E), ‖iteratedFDeriv ℝ j (UniformFourierAlias.exactAlias (TransportPrimitive.interiorCutoff (a ^ d) (b ^ d)) M v (RadialPullback.normalizeSource d a g)) z‖ ≤ C) → ∀ j ≤ m, ∀ (z : ℝ × E), ‖iteratedFDeriv ℝ j (PressureStream.divideRadius (RadialPullback.physicalAlias d a b M v g)) z‖ ≤ K * C

A uniform full-jet estimate for the actual physical alias follows from the corresponding normalized alias estimate. The transfer constant is fixed before the source, transport coefficient, and transport direction are given.

theorem NavierStokes.TemporalMeanUpdate.meanClass_temporalInverse {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε R : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hR : ∀ (n : ℕ), 1 ≤ R n) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α f) (hfc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (f n)) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α fun (n : ℕ) => temporalInverse (f n)

theorem NavierStokes.TemporalMeanUpdate.meanClass_centered {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε R : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hR : ∀ (n : ℕ), 1 ≤ R n) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α f) (hfc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (f n)) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α fun (n : ℕ) => centered (f n)

theorem NavierStokes.TemporalMeanUpdate.meanClass_desiredIncrement {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b cL cR h : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 ≤ h) (ε R : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hR : ∀ (n : ℕ), 1 ≤ R n) (hscale : ∀ (n : ℕ), ChartScales.S n ≤ R n) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α f) (hfc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (f n)) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α fun (n : ℕ) => desiredIncrement h n (f n)

The complete desired temporal update preserves the original exponent in every band, including the initial bands. No inverse estimate is assumed.

theorem NavierStokes.TemporalMeanUpdate.meanClass_axialPotential {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d cL cR h : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 ≤ h) (ε R : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hR : ∀ (n : ℕ), 1 ≤ R n) (hscale : ∀ (n : ℕ), ChartScales.S n ≤ R n) (M : ℕ → ℝ) (v : ℕ → TorusInverse.Plane) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α f) (hfc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (f n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α fun (n : ℕ) => axialPotential d a b (M n) (v n) h n (f n)

theorem NavierStokes.TemporalMeanUpdate.meanClass_radialUpdate {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d cL cR h : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 ≤ h) (ε R : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hR : ∀ (n : ℕ), 1 ≤ R n) (hscale : ∀ (n : ℕ), ChartScales.S n ≤ R n) (M : ℕ → ℝ) (v : ℕ → TorusInverse.Plane) (w : S × TorusInverse.Plane) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α f) (hfc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (f n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α fun (n : ℕ) => radialUpdate d a b (M n) (v n) w h n (f n)

theorem NavierStokes.TemporalMeanUpdate.meanClass_scaledRadialUpdate {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d cL cR h : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 ≤ h) (ε R : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hR : ∀ (n : ℕ), 1 ≤ R n) (hscale : ∀ (n : ℕ), ChartScales.S n ≤ R n) (M : ℕ → ℝ) (v : ℕ → TorusInverse.Plane) (w : S × TorusInverse.Plane) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α f) (hfc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (f n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) (α + 1) fun (n : ℕ) => radialUpdate d a b (M n) (v n) (ε n • w) h n (f n)

The actual chart axial direction carries ε; its radial stream component therefore gains one full mean-class exponent.

theorem NavierStokes.TemporalMeanUpdate.normalizeSource_periodic {S : Type} (d a : ℝ) {g : PressureStream.Lift S → ℝ} (hp : PressureStream.TorusPeriodicLift g) : PressureStream.TorusPeriodicLift (RadialPullback.normalizeSource d a g)

theorem NavierStokes.TemporalMeanUpdate.normalizeSource_torusAverage {S : Type} (d a : ℝ) (g : PressureStream.Lift S → ℝ) (p : ℝ × S) : PressureStream.torusAverage (RadialPullback.normalizeSource d a g) p = RadialPullback.sourceMultiplier d a p.1 * PressureStream.torusAverage g (RadialPullback.inverseChart d a p.1, p.2)

theorem NavierStokes.TemporalMeanUpdate.dividedAlias_superflat {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d cL cR h α : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 < h) {g : ℕ → PressureStream.Lift S → ℝ} (hg : WeightedClasses.MeanClass (UniformFourierAlias.chartStrip a b cL cR ha hcL hcR h hh) α g) (hgc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (g n)) (hgp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (g n)) (hgm : ∀ (n : ℕ) (p : ℝ × S), PressureStream.torusAverage (g n) p = 0) (hgs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (g n)) (m N : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ j ≤ m, ∀ (z : PressureStream.Lift S), ‖iteratedFDeriv ℝ j (PressureStream.divideRadius (RadialPullback.physicalAlias d a b (ChartScales.radialCoefficient h n) (0, TorusInverse.vector TorusInverse.Direction.radial) (g n))) z‖ ≤ C * ChartScales.epsilon h n ^ N

The actual physical divided alias is uniformly superflat for the manuscript's radial frequencies and any jointly smooth zero-bar source family.

theorem NavierStokes.TemporalMeanUpdate.axialAlias_superflat {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d cL cR h α : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 < h) {f : ℕ → PressureStream.Lift S → ℝ} (hf : WeightedClasses.MeanClass (UniformFourierAlias.chartStrip a b cL cR ha hcL hcR h hh) α f) (hfc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (f n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) (m N : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ j ≤ m, ∀ (z : PressureStream.Lift S), ‖iteratedFDeriv ℝ j (axialAlias d a b (ChartScales.radialCoefficient h n) (TorusInverse.vector TorusInverse.Direction.radial) h n (f n)) z‖ ≤ C * ChartScales.epsilon h n ^ N

Superflatness of the exact alias in the constructed temporal axial update.

theorem NavierStokes.TemporalMeanUpdate.temporalVector_norm_le_one {S : Type} [NormedAddCommGroup S] : ‖(0, 0, TorusInverse.vector TorusInverse.Direction.temporal)‖ ≤ 1

theorem NavierStokes.TemporalMeanUpdate.timeCoefficient_norm_le_one {h : ℝ} (hh : 0 ≤ h) {n : ℕ} (hn : 4 ≤ n) : ‖ChartScales.timeCoefficient h n‖ ≤ 1

theorem NavierStokes.TemporalMeanUpdate.axialAlias_fastDerivative_superflat {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d cL cR h α : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 < h) {f : ℕ → PressureStream.Lift S → ℝ} (hf : WeightedClasses.MeanClass (UniformFourierAlias.chartStrip a b cL cR ha hcL hcR h hh) α f) (hfc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (f n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) (m N : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ j ≤ m, ∀ (z : PressureStream.Lift S), ‖iteratedFDeriv ℝ j (fastDerivative h n (axialAlias d a b (ChartScales.radialCoefficient h n) (TorusInverse.vector TorusInverse.Direction.radial) h n (f n))) z‖ ≤ C * ChartScales.epsilon h n ^ N

The actual fast-time residual alias is superflat in every full joint jet.

theorem NavierStokes.TemporalMeanUpdate.interiorCutoff_deriv_zero_left {a b U : ℝ} (hab : a < b) (hU : U < (2 * a + b) / 3) : deriv (TransportPrimitive.interiorCutoff a b) U = 0

theorem NavierStokes.TemporalMeanUpdate.interiorCutoff_deriv_zero_right {a b U : ℝ} (hab : a < b) (hU : (a + 2 * b) / 3 < U) : deriv (TransportPrimitive.interiorCutoff a b) U = 0

theorem NavierStokes.TemporalMeanUpdate.dividedAlias_interior_support {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) : ∃ (c : ℝ) (e : ℝ), a < c ∧ c < e ∧ e < b ∧ ∀ (M : ℝ) (v : E) (g : ℝ × E → ℝ), RadialAlias.RadiallySupported c e (PressureStream.divideRadius (RadialPullback.physicalAlias d a b M v g))

The physical alias has support in one fixed compact subannulus, uniformly in the source, band, and direction.

theorem NavierStokes.TemporalMeanUpdate.meanClass_of_interior_bounds {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b c e cL cR α : ℝ} (ha : 0 < a) (hac : a < c) (he : e < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε R : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hR : ∀ (n : ℕ), 1 ≤ R n) {f : ℕ → ℝ × E → V} (hfc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported c e (f n)) (hf : ∀ (m : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ), ∀ (n j : ℕ), j ≤ m → ∀ (z : ℝ × E), ‖iteratedFDeriv ℝ j (f n) z‖ ≤ C * ε n ^ α * R n ^ p) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α f

A fixed interior support converts uniform band bounds into the full weighted class by an actual positive minimum of the exponential weight.

theorem NavierStokes.TemporalMeanUpdate.dividedAlias_global_bounds {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d cL cR α : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (ε R : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hR : ∀ (n : ℕ), 1 ≤ R n) (M : ℕ → ℝ) (hM : ∀ (n : ℕ), M n ≠ 0) {g : ℕ → PressureStream.Lift S → ℝ} (hg : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α g) (hgc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (g n)) (hgp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (g n)) (hgm : ∀ (n : ℕ) (p : ℝ × S), PressureStream.torusAverage (g n) p = 0) (hgs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (g n)) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ), ∀ (n j : ℕ), j ≤ m → ∀ (z : PressureStream.Lift S), ‖iteratedFDeriv ℝ j (PressureStream.divideRadius (RadialPullback.physicalAlias d a b (M n) (0, TorusInverse.vector TorusInverse.Direction.radial) (g n))) z‖ ≤ C * ε n ^ α * R n ^ p

theorem NavierStokes.TemporalMeanUpdate.meanClass_dividedAlias {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d cL cR α : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (ε R : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hR : ∀ (n : ℕ), 1 ≤ R n) (M : ℕ → ℝ) (hM : ∀ (n : ℕ), M n ≠ 0) {g : ℕ → PressureStream.Lift S → ℝ} (hg : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α g) (hgc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (g n)) (hgp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (g n)) (hgm : ∀ (n : ℕ) (p : ℝ × S), PressureStream.torusAverage (g n) p = 0) (hgs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (g n)) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α fun (n : ℕ) => PressureStream.divideRadius (RadialPullback.physicalAlias d a b (M n) (0, TorusInverse.vector TorusInverse.Direction.radial) (g n))

The actual divided compactification alias lies in the same weighted class; its fixed interior support supplies the full edge weight.

theorem NavierStokes.TemporalMeanUpdate.meanClass_axialAlias {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d cL cR h α : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 ≤ h) (ε R : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hR : ∀ (n : ℕ), 1 ≤ R n) (hscale : ∀ (n : ℕ), ChartScales.S n ≤ R n) (M : ℕ → ℝ) (hM : ∀ (n : ℕ), M n ≠ 0) {f : ℕ → PressureStream.Lift S → ℝ} (hf : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α f) (hfc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (f n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α fun (n : ℕ) => axialAlias d a b (M n) (TorusInverse.vector TorusInverse.Direction.radial) h n (f n)

theorem NavierStokes.TemporalMeanUpdate.meanClass_axialUpdate {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d cL cR h α : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 ≤ h) (ε R : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hR : ∀ (n : ℕ), 1 ≤ R n) (hscale : ∀ (n : ℕ), ChartScales.S n ≤ R n) (M : ℕ → ℝ) (hM : ∀ (n : ℕ), M n ≠ 0) {f : ℕ → PressureStream.Lift S → ℝ} (hf : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α f) (hfc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (f n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α fun (n : ℕ) => axialUpdate d a b (M n) (TorusInverse.vector TorusInverse.Direction.radial) h n (f n)

The reconstructed axial field, including its exact nonzero alias, has the original mean-class exponent.