Averaged Suitable

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.measurePreserving_rotZ (φ : ℝ) : MeasureTheory.MeasurePreserving (rotZ φ) MeasureTheory.volume MeasureTheory.volume

The rotation rotZ φ preserves Lebesgue measure on Vec3: it is the linear map with matrix !![cos φ, -sin φ, 0; sin φ, cos φ, 0; 0, 0, 1], whose determinant is 1.

theorem CIV.measurePreserving_rotZ_prod (φ : ℝ) : MeasureTheory.MeasurePreserving (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => (rotZ φ z.1, z.2)) MeasureTheory.volume MeasureTheory.volume

The map z ↦ (rotZ φ z.1, z.2) preserves Lebesgue measure on ParabolicPoint.

theorem CIV.measurePreserving_rotZ_unitCylinder (φ : ℝ) : MeasureTheory.MeasurePreserving (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => (rotZ φ z.1, z.2)) (MeasureTheory.volume.restrict unitCylinder) (MeasureTheory.volume.restrict unitCylinder)

The map z ↦ (rotZ φ z.1, z.2) preserves Lebesgue measure restricted to the unit cylinder, which is invariant under every rotation about the axis.

theorem CIV.quasiMeasurePreserving_rotZ_prod : MeasureTheory.QuasiMeasurePreserving (fun (q : CKN.Foundation.Parabolic.ParabolicPoint × ℝ) => (rotZ (-q.2) q.1.1, q.1.2)) ((MeasureTheory.volume.restrict unitCylinder).prod (MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi)))) (MeasureTheory.volume.restrict unitCylinder)

The map (z, φ) ↦ (rotZ (-φ) z.1, z.2) is quasi-measure-preserving from the product of the unit cylinder with an angle interval to the unit cylinder: a set of measure zero in the target has preimage of measure zero, since each fixed-angle slice is exactly measure preserving on the unit cylinder.

theorem CIV.aestronglyMeasurable_angularMeanScalar {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hp : MeasureTheory.AEStronglyMeasurable p (MeasureTheory.volume.restrict unitCylinder)) : MeasureTheory.AEStronglyMeasurable (angularMeanScalar p) (MeasureTheory.volume.restrict unitCylinder)

The angular mean of an almost-everywhere strongly measurable scalar field on the unit cylinder is again almost-everywhere strongly measurable there: it is a parametric integral of p composed with the (quasi-measure-preserving) joint rotation map, so AEStronglyMeasurable.integral_prod_right' applies after transporting p's a.e. strong measurability through quasiMeasurePreserving_rotZ_prod.

theorem CIV.lintegral_angularMeanScalar_rpow_lt_top {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hp : MeasureTheory.AEStronglyMeasurable p (MeasureTheory.volume.restrict unitCylinder)) (hK : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in unitCylinder, ‖p z‖ₑ ^ (3 / 2) < ⊤) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in unitCylinder, ‖angularMeanScalar p z‖ₑ ^ (3 / 2) < ⊤

The pressure energy bound for the angular mean. If p lies in L^{3/2} on the unit cylinder then so does its angular mean angularMeanScalar p, with the same L^{3/2} seminorm bound. This is the scalar Minkowski-integral-inequality step of globalEnergyClass_angularMeanScalar: Jensen's inequality (key_bound) pointwise a.e. in space, MeasureTheory.lintegral_lintegral_swap (Tonelli) to interchange the angle and space integrals, and lintegral_rotate_eq (exact rotation invariance) to identify the inner space integral with ∫⁻ ‖p‖ₑ ^ (3/2) for every angle.

theorem CIV.globalEnergyClass_angularMeanScalar (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (henergy : GlobalEnergyClass u Du p) : GlobalEnergyClass u Du (angularMeanScalar p)

The angular mean of a triple in the energy class eq:interior:energy:class is again in that class: GlobalEnergyClass leaves u and Du unchanged and asks only that the pressure lie in L^{3/2}(Q), and averaging over rotations cannot increase that norm (lintegral_angularMeanScalar_rpow_lt_top).