Lin34 Slice Fubini

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

Fubini steps for the cylinder quantities of prop:lin34

The cylinder quantities D(z,r) and C_hat(z,ρ) of eq:Chat in paper/ckn.tex are defined as integrals over a parabolic cylinder, while the monotonicity and scaling statements of prop:lin34 are phrased in terms of the spatial slice quantities obtained by fixing the time variable. This file records the two Fubini facts that pass between the two points of view.

The cylinder parabolicCylinder x t r is the product vec3Ball x r ×ˢ Ioc (t - r ^ 2) t and the volume on ParabolicPoint is the product of the spatial and time volumes, so an integrability hypothesis over the cylinder is an integrability hypothesis for the product measure. Applying the Fubini API with the time variable as the outer variable then yields the integrability of the time slices.

theorem CKN.lin34_slice_integrable_of_cylinder {g : Foundation.Parabolic.ParabolicPoint → ℝ} {x : Foundation.Parabolic.Vec3} {t r : ℝ} (hg : MeasureTheory.IntegrableOn g (Foundation.Parabolic.parabolicCylinder x t r) MeasureTheory.volume) : MeasureTheory.Integrable (fun (s : ℝ) => ∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x r, g (y, s)) (MeasureTheory.volume.restrict (Set.Ioc (t - r ^ 2) t))

Fubini step of prop:lin34: if a function is integrable on the parabolic cylinder Q_r(z), then the spatial slice integrals integrate in time against the time interval of the cylinder.

theorem CKN.lin34_slice_integrableOn_ball_ae {g : Foundation.Parabolic.ParabolicPoint → ℝ} {x : Foundation.Parabolic.Vec3} {t r : ℝ} (hg : MeasureTheory.IntegrableOn g (Foundation.Parabolic.parabolicCylinder x t r) MeasureTheory.volume) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t - r ^ 2) t), MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => g (y, s)) (Foundation.Parabolic.vec3Ball x r) MeasureTheory.volume

Fubini step of prop:lin34: if a function is integrable on the parabolic cylinder Q_r(z), then for almost every time in the time interval of the cylinder its spatial slice is integrable on the spatial ball.

theorem CKN.lin34_integrableOn_pressure_pow_cylinder {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z : Foundation.Parabolic.ParabolicPoint} {r : ℝ} (hr : 0 < r) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) ⊆ spaceTimeSet Ω I) : MeasureTheory.IntegrableOn (fun (w : Foundation.Parabolic.ParabolicPoint) => |p w| ^ (3 / 2)) (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) MeasureTheory.volume

prop:lin34: on a cylinder whose closure lies in the carrier of a suitable weak solution, the pressure raised to the exponent 3 / 2 of eq:Chat is integrable.