Interior Displays

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

The source-level representative has the larger value display and the gradient display on the concentric half-ball. It is extended by zero outside the half-ball, where no agreement with the original datum is required.

The four source displays, with one constant and no global smoothness assumption on the weakly harmonic datum.

theorem CKN.Foundation.Heat.weak_harmonic_interior_displays {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₀ (3 * ρ / 4), |H x| ≤ harmonicInteriorDisplayConstant * (ρ ^ 2)⁻¹ * MeasureTheory.lpNorm h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ))) ∧ (∀ x ∈ euclideanBall x₀ (ρ / 2), Parabolic.vec3EuclideanNorm (classicalGradient H x) ≤ harmonicInteriorDisplayConstant * (ρ ^ 3)⁻¹ * MeasureTheory.lpNorm h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ))) ∧ (∀ (r : ℝ), 0 < r → r ≤ ρ / 2 → (r ^ 2)⁻¹ * ∫ (y : Vec 3) in euclideanBall x₀ r, |h y| ^ (3 / 2) ≤ harmonicInteriorDisplayConstant * (r / ρ) * (ρ ^ 2)⁻¹ * ∫ (y : Vec 3) in euclideanBall x₀ ρ, |h y| ^ (3 / 2)) ∧ ∀ (r : ℝ), 0 < r → r ≤ ρ / 2 → (r ^ 2)⁻¹ * ∫ (y : Vec 3) in euclideanBall x₀ r, |h y - ⨍ (z : Vec 3) in euclideanBall x₀ r, h z| ^ (3 / 2) ≤ harmonicInteriorDisplayConstant * (r / ρ) ^ (5 / 2) * (ρ ^ 2)⁻¹ * ∫ (y : Vec 3) in euclideanBall x₀ ρ, |h y| ^ (3 / 2)