Integral Bounds

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

theorem CKN.Foundation.Heat.heatKernelPlus_integral_rho_lt_le {R : ℝ} (hR : 0 < R) : ∫ (p : Parabolic.ParabolicPoint) in {p : Parabolic.ParabolicPoint | rhoTwo p.1 p.2 < R}, heatKernelPlus p ≤ 1000 * R ^ 2

theorem CKN.Foundation.Heat.heatKernelGradientNorm_integral_rho_lt_le {R : ℝ} (hR : 0 < R) : ∫ (p : Parabolic.ParabolicPoint) in {p : Parabolic.ParabolicPoint | rhoTwo p.1 p.2 < R}, heatKernelGradientNorm p.1 p.2 ≤ 100000 * R