Interior Gradient

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

theorem CKN.Foundation.Heat.smooth_harmonic_interior_gradient_norm_bound {H : Parabolic.Vec3 → ℝ} (hH : ContDiff ℝ (↑⊤) H) {x₀ : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hHarm : ∀ y ∈ euclideanBall x₀ ρ, spatialLaplacian H y = 0) (hHmem : MeasureTheory.MemLp H (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ))) (x : Vec 3) : x ∈ euclideanBall x₀ (ρ / 2) → Parabolic.vec3EuclideanNorm (classicalGradient H x) ≤ 3 * harmonicInteriorGradientSupConstant * (ρ ^ 3)⁻¹ * MeasureTheory.lpNorm H (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ))