Volume scaling for the interior harmonic gradient display

The interior harmonic gradient display of the paper carries the factor ρ ^ (-3) and is integrated over the half ball B_{ρ/2}(x₀). Its L^{5/6}-type norm against the spatial measure therefore carries the half ball volume raised to the power 5 / 6. This file records the resulting scale bookkeeping: the product of the ρ ^ (-3) weight with |B_{ρ/2}(x₀)| ^ (5/6) is bounded by ρ ^ (-1/2), which is exactly the factor appearing in display (3.5) of the paper.

The only input is the closed formula for the volume of a Euclidean ball in three dimensions, volume_vec3Ball_eq.

theorem CKN.Core.Step4.halfBall_volume_rpow_five_sixths_mul_inv_cube_le (x₀ : Foundation.Parabolic.Vec3) {ρ C : ℝ} (hρ : 0 < ρ) (hC : 0 ≤ C) : ENNReal.ofReal (C * (ρ ^ 3)⁻¹) * MeasureTheory.volume (euclideanBall x₀ (ρ / 2)) ^ (5 / 6) ≤ ENNReal.ofReal (C * ρ ^ (-1 / 2))

Display (3.5), volume factor: the interior harmonic gradient display carries the weight ρ ^ (-3) on the half ball B_{ρ/2}(x₀), and its 5/6-power against the spatial measure is bounded by the single factor ρ ^ (-1/2) that appears in the display. Concretely, C ρ ^ (-3) · |B_{ρ/2}(x₀)| ^ (5/6) ≤ C ρ ^ (-1/2) for ρ > 0 and C ≥ 0.