Homogeneous Sobolev estimates in three dimensions

The compact-support estimate is the Gagliardo--Nirenberg--Sobolev inequality used in the cutoff step of lem:J-weak-div.

theorem CKN.euclideanBall_volume_rpow_third_le {R : ℝ} (hR : 0 < R) : MeasureTheory.volume (euclideanBall 0 R) ^ (1 / 3) ≤ ENNReal.ofReal (2 * R)

The cube-root volume of a three-dimensional Euclidean ball is bounded by twice its radius.

theorem CKN.eLpNorm_indicator_compl_euclideanBall_tendsto_zero {f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm ((euclideanBall 0 ↑n)ᶜ.indicator f) 2 MeasureTheory.volume) Filter.atTop (nhds 0)

The L² tail outside expanding Euclidean balls tends to zero.