Slice Selected Gradient Force Holder

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

Hölder conversion for the force-slot bound

A function η supported in a ball, bounded by 1, carries an L^q bound on the ball to an L^{6/5} bound on the whole space, with an explicit volume factor.

theorem CKN.Core.Step4.eLpNorm_cutoff_mul_g_le {x₀ : Foundation.Parabolic.Vec3} {ρ q : ℝ} (hρ : 0 < ρ) (hq : 6 / 5 ≤ q) {g : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.MemLp g (ENNReal.ofReal q) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ))) : MeasureTheory.eLpNorm (fun (x : Vec 3) => mollifiedBallCutoff x₀ hρ x * g x) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ≤ MeasureTheory.eLpNorm g (ENNReal.ofReal q) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ)) * MeasureTheory.volume (euclideanBall x₀ ρ) ^ (1 / (6 / 5) - 1 / q)

The extended-norm version: η * g has its L^{6/5} norm over ℝ³ bounded by the L^q norm of g on the ball times the ball volume raised to 5/6 - 1/q.