Interior Smooth

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

theorem CKN.Foundation.Heat.weakly_harmonic_interior_smooth {h : Parabolic.Vec3 → ℝ} {x₀ : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hmem : MeasureTheory.MemLp h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ))) (hweak : WeaklyHarmonicOn (euclideanBall x₀ ρ) h) : ∃ (H : Parabolic.Vec3 → ℝ), ContDiffOn ℝ (↑1) H (euclideanBall x₀ (ρ / 2)) ∧ h =ᵐ[MeasureTheory.volume.restrict (euclideanBall x₀ (ρ / 2))] H ∧ (∀ x ∈ euclideanBall x₀ (ρ / 2), |H x| ≤ weakHarmonicInteriorSupConstant * (ρ ^ 2)⁻¹ * MeasureTheory.lpNorm h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ))) ∧ ∀ x ∈ euclideanBall x₀ (ρ / 2), Parabolic.vec3EuclideanNorm (classicalGradient H x) ≤ 1728 * harmonicInteriorGradientSupConstant * (ρ ^ 3)⁻¹ * MeasureTheory.lpNorm h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ))