Lin34 Slice Holder

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

The Hölder steps of Proposition prop:lin34

Proposition prop:lin34 of paper/ckn.tex turns a bound for an L¹ integral over a spatial ball into a bound for an L^{3/2} integral (display eq:lin34-pointwise). The step is Hölder's inequality on the ball, with the volume (4π/3) ρ³ of the ball producing the prefactor. This file isolates that analytic step.

• lin34_ball_integral_le_rpow_three_halves bounds ∫ g over vec3Ball x₀ ρ by (4π/3)^{1/3} ρ times the (2/3)-power of the L^{3/2} integral of g.

theorem CKN.lin34_ball_integral_le_rpow_three_halves {g : Foundation.Parabolic.Vec3 → ℝ} {x₀ : Foundation.Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hg : AEMeasurable g (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))) (hg0 : ∀ (y : Foundation.Parabolic.Vec3), 0 ≤ g y) (hint : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => g y ^ (3 / 2)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))) : ∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, g y ≤ (4 * Real.pi / 3) ^ (1 / 3) * ρ * (∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, g y ^ (3 / 2)) ^ (2 / 3)

The first Hölder step of prop:lin34 (display eq:lin34-pointwise): for a nonnegative g with integrable g^{3/2} on the ball vec3Ball x₀ ρ, the L¹ integral of g over the ball is bounded by (4π/3)^{1/3} ρ times the (2/3)-power of the L^{3/2} integral of g.