Riesz Second L2 Global

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

theorem CKN.Foundation.Euclidean.riesz_second_l2_bound_global {F : Parabolic.Vec3 → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hFc : HasCompactSupport F) (i j : Fin 3) : ∫⁻ (x : Parabolic.Vec3), absE (fun (y : Parabolic.Vec3) => mixedSecond (pressureNewtonianPotential F) i j y) x ^ 2 ≤ ENNReal.ofReal (1 ^ 2) * ∫⁻ (x : Parabolic.Vec3), absE F x ^ 2

The global strong (2,2) estimate for one Hessian component of the Newtonian potential, in the ENNReal interface used by interpolation.

theorem CKN.Foundation.Euclidean.riesz_second_l2_bound_global_real {F : Parabolic.Vec3 → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hFc : HasCompactSupport F) (i j : Fin 3) : ∫ (x : Parabolic.Vec3), mixedSecond (pressureNewtonianPotential F) i j x ^ 2 ≤ ∫ (x : Parabolic.Vec3), F x ^ 2

The same endpoint estimate as a finite real Lebesgue-integral inequality.