Actual slow moments of flat weighted mean fields

The two-edge weight absorbs every fixed inverse-edge polynomial. Consequently the actual derivatives of a supported mean field have global band bounds. Finite torus averaging and radial integration preserve these bounds. All derivatives in this file are iteratedFDeriv of the actual integral.

noncomputable def NavierStokes.MeanMomentBounds.GlobalBandJets {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (ε S : ℕ → ℝ) (α : ℝ) (f : ℕ → D → E) : Prop

A global finite-prefix bound, with the discrete band and slow polynomial still visible. This is a proved consequence of the flat weighted class below.

Equations

• NavierStokes.MeanMomentBounds.GlobalBandJets ε S α f = ∀ (m : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ) (x : D), ∀ j ≤ m, ‖iteratedFDeriv ℝ j (f n) x‖ ≤ C * ε n ^ α * S n ^ p

theorem NavierStokes.MeanMomentBounds.supported_zero_outside_open {D E : Type} [NormedAddCommGroup D] [NormedAddCommGroup E] {a b : ℝ} {f : ℝ × D → E} (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) {x : ℝ × D} (hx : x.1 ∉ Set.Ioo a b) : f x = 0

theorem NavierStokes.MeanMomentBounds.meanClass_globalBandJets {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) {α : ℝ} {f : ℕ → ℝ × D → E} (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) (hclass : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α f) : GlobalBandJets ε S α f

Flatness, rather than a new global-bound hypothesis, removes the radial edge loss. The input is the manuscript's concrete logarithmic mean class.

theorem NavierStokes.MeanMomentBounds.iteratedFDeriv_affine {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : D →L[ℝ] E) (v : E) {f : E → F} (hf : ContDiff ℝ (↑⊤) f) (j : ℕ) (x : D) : iteratedFDeriv ℝ j (fun (y : D) => f (L y + v)) x = (iteratedFDeriv ℝ j f (L x + v)).compContinuousLinearMap fun (x : Fin j) => L

Exact higher chain rule for an affine map.

theorem NavierStokes.MeanMomentBounds.norm_iteratedFDeriv_affine_le {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : D →L[ℝ] E) (hL : ‖L‖ ≤ 1) (v : E) {f : E → F} (hf : ContDiff ℝ (↑⊤) f) (j : ℕ) (x : D) : ‖iteratedFDeriv ℝ j (fun (y : D) => f (L y + v)) x‖ ≤ ‖iteratedFDeriv ℝ j f (L x + v)‖

noncomputable def NavierStokes.MeanMomentBounds.slowStripData {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) : WeightedClasses.StripData D

The unweighted slow strip keeps precisely the same band scales.

Equations

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

theorem NavierStokes.MeanMomentBounds.globalBandJets_unweighted {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {ε S : ℕ → ℝ} {α : ℝ} {f : ℕ → D → E} (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hjets : GlobalBandJets ε S α f) : WeightedClasses.UnweightedClass (slowStripData ε S hε hεone hS) α f

theorem NavierStokes.MeanMomentBounds.globalBandJets_unweighted_log {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) {ε S : ℕ → ℝ} {α : ℝ} {f : ℕ → ℝ × D → E} (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hjets : GlobalBandJets ε S α f) : WeightedClasses.UnweightedClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α f

theorem NavierStokes.MeanMomentBounds.GlobalBandJets.compLinear {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {ε S : ℕ → ℝ} {α : ℝ} {f : ℕ → E → F} (hjets : GlobalBandJets ε S α f) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (L : D →L[ℝ] E) (hL : ‖L‖ ≤ 1) : GlobalBandJets ε S α fun (n : ℕ) (x : D) => f n (L x)

noncomputable def NavierStokes.MeanMomentBounds.affineAverage {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : D →L[ℝ] E) (v : E) (a b : ℝ) (f : E → F) (x : D) : F

A finite affine average; coordinate projections and torus insertion are special cases.

Equations

• NavierStokes.MeanMomentBounds.affineAverage L v a b f x = ∫ (t : ℝ) in a..b, f (L x + t • v)

theorem NavierStokes.MeanMomentBounds.affineAverage_contDiff {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (L : D →L[ℝ] E) (v : E) (a b : ℝ) {f : E → F} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (affineAverage L v a b f)

theorem NavierStokes.MeanMomentBounds.iteratedFDeriv_affineAverage {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : D →L[ℝ] E) (hL : ‖L‖ ≤ 1) (v : E) {a b : ℝ} (hab : a ≤ b) {f : E → F} (hf : ContDiff ℝ (↑⊤) f) (hb : ∀ (k : ℕ), ∃ (C : ℝ), ∀ (x : E), ‖iteratedFDeriv ℝ k f x‖ ≤ C) (j : ℕ) (x : D) : iteratedFDeriv ℝ j (affineAverage L v a b f) x = ∫ (t : ℝ) in a..b, iteratedFDeriv ℝ j (fun (y : D) => f (L y + t • v)) x

theorem NavierStokes.MeanMomentBounds.affineAverage_jet_bound {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : D →L[ℝ] E) (hL : ‖L‖ ≤ 1) (v : E) {a b : ℝ} (hab : a ≤ b) {f : E → F} (hf : ContDiff ℝ (↑⊤) f) (hb : ∀ (k : ℕ), ∃ (C : ℝ), ∀ (x : E), ‖iteratedFDeriv ℝ k f x‖ ≤ C) (j : ℕ) (x : D) (C : ℝ) (hC : ∀ t ∈ Set.Icc a b, ‖iteratedFDeriv ℝ j f (L x + t • v)‖ ≤ C) : ‖iteratedFDeriv ℝ j (affineAverage L v a b f) x‖ ≤ C * (b - a)

theorem NavierStokes.MeanMomentBounds.GlobalBandJets.affineAverage {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {ε S : ℕ → ℝ} {α : ℝ} {f : ℕ → E → F} (hjets : GlobalBandJets ε S α f) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (L : D →L[ℝ] E) (hL : ‖L‖ ≤ 1) (v : E) {a b : ℝ} (hab : a ≤ b) : GlobalBandJets ε S α fun (n : ℕ) => MeanMomentBounds.affineAverage L v a b (f n)

noncomputable def NavierStokes.MeanMomentBounds.eraseAuxX {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] : PressureStream.Lift P →L[ℝ] PressureStream.Lift P

Erase auxiliary X, bundling toFun, map_add, map_smul, cont.

Equations

• NavierStokes.MeanMomentBounds.eraseAuxX = { toFun := fun (x : NavierStokes.PressureStream.Lift P) => (x.1, x.2.1, 0, x.2.2.2), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

noncomputable def NavierStokes.MeanMomentBounds.eraseAuxY {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] : PressureStream.Lift P →L[ℝ] PressureStream.Lift P

Erase auxiliary Y, bundling toFun, map_add, map_smul, cont.

Equations

• NavierStokes.MeanMomentBounds.eraseAuxY = { toFun := fun (x : NavierStokes.PressureStream.Lift P) => (x.1, x.2.1, x.2.2.1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

theorem NavierStokes.MeanMomentBounds.norm_eraseAuxX_le {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] : ‖eraseAuxX‖ ≤ 1

theorem NavierStokes.MeanMomentBounds.norm_eraseAuxY_le {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] : ‖eraseAuxY‖ ≤ 1

noncomputable def NavierStokes.MeanMomentBounds.auxX {P : Type} [NormedAddCommGroup P] : PressureStream.Lift P

Aux X, given by (0, (0, (1, 0))).

Equations

• NavierStokes.MeanMomentBounds.auxX = (0, 0, 1, 0)

noncomputable def NavierStokes.MeanMomentBounds.auxY {P : Type} [NormedAddCommGroup P] : PressureStream.Lift P

Aux Y, given by (0, (0, (0, 1))).

Equations

• NavierStokes.MeanMomentBounds.auxY = (0, 0, 0, 1)

@[simp]

theorem NavierStokes.MeanMomentBounds.eraseAuxX_add_smul {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (x : PressureStream.Lift P) (t : ℝ) : eraseAuxX x + t • auxX = (x.1, x.2.1, t, x.2.2.2)

@[simp]

theorem NavierStokes.MeanMomentBounds.eraseAuxY_add_smul {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (x : PressureStream.Lift P) (t : ℝ) : eraseAuxY x + t • auxY = (x.1, x.2.1, x.2.2.1, t)

noncomputable def NavierStokes.MeanMomentBounds.liftedTorusAverage {P : Type} (f : PressureStream.Lift P → ℝ) (x : PressureStream.Lift P) : ℝ

Lifted torus average, given by PressureStream.torusAverage f (x.1, x.2.1).

Equations

• NavierStokes.MeanMomentBounds.liftedTorusAverage f x = NavierStokes.PressureStream.torusAverage f (x.1, x.2.1)

theorem NavierStokes.MeanMomentBounds.liftedTorusAverage_eq_affine {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (f : PressureStream.Lift P → ℝ) : liftedTorusAverage f = affineAverage eraseAuxY auxY 0 1 (affineAverage eraseAuxX auxX 0 1 f)

theorem NavierStokes.MeanMomentBounds.liftedTorusAverage_contDiff {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : PressureStream.Lift P → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (liftedTorusAverage f)

theorem NavierStokes.MeanMomentBounds.liftedTorusAverage_supported {P : Type} {a b : ℝ} {f : PressureStream.Lift P → ℝ} (hs : RadialAlias.RadiallySupported a b f) : RadialAlias.RadiallySupported a b (liftedTorusAverage f)

theorem NavierStokes.MeanMomentBounds.GlobalBandJets.liftedTorusAverage {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {ε S : ℕ → ℝ} {α : ℝ} {f : ℕ → PressureStream.Lift P → ℝ} (hjets : GlobalBandJets ε S α f) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) : GlobalBandJets ε S α fun (n : ℕ) => MeanMomentBounds.liftedTorusAverage (f n)

theorem NavierStokes.MeanMomentBounds.totalIntegral_zero_eq {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ × D → E) (x : ℝ × D) : TransportPrimitive.totalIntegral 0 0 f x = ∫ (r : ℝ), f (r, x.2)

theorem NavierStokes.MeanMomentBounds.GlobalBandJets.radialIntegral {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {ε S : ℕ → ℝ} {α a b : ℝ} {f : ℕ → ℝ × D → E} (hjets : GlobalBandJets ε S α f) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) (hab : a ≤ b) : GlobalBandJets ε S α fun (n : ℕ) => TransportPrimitive.totalIntegral 0 0 (f n)

noncomputable def NavierStokes.MeanMomentBounds.liftedPressureMass {P : Type} (f : PressureStream.Lift P → ℝ) (x : PressureStream.Lift P) : ℝ

Lifted pressure mass, given by PressureStream.pressureMass f x.2.1.

Equations

• NavierStokes.MeanMomentBounds.liftedPressureMass f x = NavierStokes.PressureStream.pressureMass f x.2.1

theorem NavierStokes.MeanMomentBounds.liftedPressureMass_eq {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (f : PressureStream.Lift P → ℝ) : liftedPressureMass f = TransportPrimitive.totalIntegral 0 0 (liftedTorusAverage f)

theorem NavierStokes.MeanMomentBounds.liftedPressureMass_contDiff {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f : PressureStream.Lift P → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) : ContDiff ℝ (↑⊤) (liftedPressureMass f)

theorem NavierStokes.MeanMomentBounds.GlobalBandJets.liftedPressureMass {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {ε S : ℕ → ℝ} {α a b : ℝ} {f : ℕ → PressureStream.Lift P → ℝ} (hjets : GlobalBandJets ε S α f) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) (hab : a ≤ b) : GlobalBandJets ε S α fun (n : ℕ) => MeanMomentBounds.liftedPressureMass (f n)

theorem NavierStokes.MeanMomentBounds.meanClass_pressureMass_lift {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) {α : ℝ} {f : ℕ → PressureStream.Lift P → ℝ} (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) (hclass : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α f) : WeightedClasses.UnweightedClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α fun (n : ℕ) (x : PressureStream.Lift P) => PressureStream.pressureMass (f n) x.2.1

The actual pressure defect, lifted to the original strip, belongs to S_α. There is no pressure-mass or differentiated-integral estimate premise.

noncomputable def NavierStokes.MeanMomentBounds.insertSlow {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] : P →L[ℝ] PressureStream.Lift P

Insert slow, bundling toFun, map_add, map_smul, cont.

Equations

• NavierStokes.MeanMomentBounds.insertSlow = { toFun := fun (p : P) => (0, p, 0, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

theorem NavierStokes.MeanMomentBounds.norm_insertSlow_le {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] : ‖insertSlow‖ ≤ 1

theorem NavierStokes.MeanMomentBounds.meanClass_pressureMass {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) {α : ℝ} {f : ℕ → PressureStream.Lift P → ℝ} (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) (hclass : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α f) : WeightedClasses.UnweightedClass (slowStripData ε S hε hεone hS) α fun (n : ℕ) => PressureStream.pressureMass (f n)

The same actual pressure moment as a function of only the slow variables.

theorem NavierStokes.MeanMomentBounds.radialCoefficient_unweighted {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) {g : ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) : WeightedClasses.UnweightedClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) 0 fun (x : ℕ) (x_1 : ℝ × P) => g x_1.1

noncomputable def NavierStokes.MeanMomentBounds.radialWeighted {P : Type} (k : ℕ) (f : ℝ × P → ℝ) (x : ℝ × P) : ℝ

Radial weighted, given by x.1 ^ k * f x.

Equations

• NavierStokes.MeanMomentBounds.radialWeighted k f x = x.1 ^ k * f x

theorem NavierStokes.MeanMomentBounds.radialWeighted_contDiff {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (k : ℕ) {f : ℝ × P → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (radialWeighted k f)

theorem NavierStokes.MeanMomentBounds.radialWeighted_supported {P : Type} (k : ℕ) {a b : ℝ} {f : ℝ × P → ℝ} (hs : RadialAlias.RadiallySupported a b f) : RadialAlias.RadiallySupported a b (radialWeighted k f)

theorem NavierStokes.MeanMomentBounds.meanClass_radialWeighted {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) {α : ℝ} {f : ℕ → ℝ × P → ℝ} (hclass : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α f) (k : ℕ) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α fun (n : ℕ) => radialWeighted k (f n)

theorem NavierStokes.MeanMomentBounds.pressureMass_radialWeighted {P : Type} (k : ℕ) (f : PressureStream.Lift P → ℝ) (p : P) : PressureStream.pressureMass (radialWeighted k f) p = IntegratedMeanBalances.radialMoment k (PressureStream.torusAverage f) p

The radial power is outside the auxiliary torus average, exactly as in the pressure and two integrated flux defects.

theorem NavierStokes.MeanMomentBounds.pressureMass_radialWeighted_fun {P : Type} (k : ℕ) (f : PressureStream.Lift P → ℝ) : PressureStream.pressureMass (radialWeighted k f) = IntegratedMeanBalances.radialMoment k (PressureStream.torusAverage f)

theorem NavierStokes.MeanMomentBounds.meanClass_radialMoment {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) {α : ℝ} {f : ℕ → PressureStream.Lift P → ℝ} (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) (hclass : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α f) (k : ℕ) : WeightedClasses.UnweightedClass (slowStripData ε S hε hεone hS) α fun (n : ℕ) => IntegratedMeanBalances.radialMoment k (PressureStream.torusAverage (f n))

Every fixed radial moment of the actual torus mean is an unweighted slow coefficient of the same band order.

theorem NavierStokes.MeanMomentBounds.meanClass_radialMoment_lift {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) {α : ℝ} {f : ℕ → PressureStream.Lift P → ℝ} (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) (hclass : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α f) (k : ℕ) : WeightedClasses.UnweightedClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α fun (n : ℕ) (x : PressureStream.Lift P) => IntegratedMeanBalances.radialMoment k (PressureStream.torusAverage (f n)) x.2.1