The radial weight ‖x‖ ^ (-3/2) on balls

The linear-growth hypothesis of the Liouville step needs the exact scaling of the integral of ‖x‖ ^ (-3/2) over a ball of radius ρ in three dimensions: it grows like ρ ^ (3/2), so its 2/3 power grows linearly in ρ. The crude bound by the supremum of the weight times the volume of the ball would only give ρ ^ 3, which is too weak. The scaling identity below replaces the dyadic shell sum by a single change of variables.

theorem CKN.lintegral_ball_inv_norm_rpow_eq {ρ : ℝ} (hρ : 0 < ρ) : ∫⁻ (x : Foundation.Parabolic.Vec3) in Metric.ball 0 ρ, ENNReal.ofReal (‖x‖ ^ (-(3 / 2))) = ENNReal.ofReal (ρ ^ (3 / 2)) * ∫⁻ (x : Foundation.Parabolic.Vec3) in Metric.ball 0 1, ENNReal.ofReal (‖x‖ ^ (-(3 / 2)))

Scaling identity for the radial weight ‖x‖ ^ (-3/2) on balls of the ambient three-dimensional space.

noncomputable def CKN.invNormBallConstant : ℝ

The universal constant in the ball estimate for the radial weight: the integral of ‖x‖ ^ (-3/2) over the unit ball of three-dimensional space.

Equations

• CKN.invNormBallConstant = (∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in Metric.ball 0 1, ENNReal.ofReal (‖x‖ ^ (-(3 / 2)))).toReal

theorem CKN.invNormBallConstant_nonneg : 0 ≤ invNormBallConstant

theorem CKN.lintegral_ball_inv_norm_rpow_eq_const {ρ : ℝ} (hρ : 0 < ρ) : ∫⁻ (x : Foundation.Parabolic.Vec3) in Metric.ball 0 ρ, ENNReal.ofReal (‖x‖ ^ (-(3 / 2))) = ENNReal.ofReal (invNormBallConstant * ρ ^ (3 / 2))

The scale-invariant ball estimate: the integral of the radial weight ‖x‖ ^ (-3/2) over the ball of radius ρ is invNormBallConstant * ρ ^ (3/2).