Interior Regularity #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.Foundation.Heat.mollify_memLp_of_memLp
{g : Parabolic.Vec3 → ℝ}
{p : ENNReal}
(hp : 1 ≤ p)
(hp_top : p ≠ ⊤)
(hg : MeasureTheory.MemLp g p MeasureTheory.volume)
{ε : ℝ}
(hε : 0 < ε)
:
MeasureTheory.MemLp (mollify g ε hε) p MeasureTheory.volume
theorem
CKN.Foundation.Heat.lpNorm_restrict_mono
{U A : Set Parabolic.Vec3}
(hAsub : A ⊆ U)
{f : Parabolic.Vec3 → ℝ}
(hf : MeasureTheory.MemLp f (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict U))
:
MeasureTheory.lpNorm f (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict A) ≤ MeasureTheory.lpNorm f (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict U)
theorem
CKN.Foundation.Heat.weak_rep_sub_eq
{f g : Parabolic.Vec3 → ℝ}
{x x₀ : Parabolic.Vec3}
{ρ : ℝ}
(hρ : 0 < ρ)
(hx : x ∈ euclideanBall x₀ (ρ / 2))
(hf : MeasureTheory.MemLp f (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ)))
(hg : MeasureTheory.MemLp g (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ)))
:
weakHarmonicInteriorRepresentative f x₀ hρ x - weakHarmonicInteriorRepresentative g x₀ hρ x = weakHarmonicInteriorRepresentative (fun (y : Parabolic.Vec3) => f y - g y) x₀ hρ x
theorem
CKN.Foundation.Heat.approximation_scale_tendsto
{ρ : ℝ}
:
0 < ρ → Filter.Tendsto (fun (n : ℕ) => ρ / (12 * (↑n + 1))) Filter.atTop (nhds 0)
theorem
CKN.Foundation.Heat.closedBall_subset_euclideanBall
{x₀ y : Parabolic.Vec3}
{ρ ε : ℝ}
(hρ : 0 < ρ)
:
0 < ε → ∀ (hy : y ∈ euclideanBall x₀ (3 * ρ / 4)) (hε_le : ε ≤ ρ / 12), Metric.closedBall y ε ⊆ euclideanBall x₀ ρ
theorem
CKN.Foundation.Heat.weakly_harmonic_interior_representative_ae
{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 =ᵐ[MeasureTheory.volume.restrict (euclideanBall x₀ (ρ / 2))] fun (x : Vec 3) =>
weakHarmonicInteriorRepresentative ((euclideanBall x₀ ρ).indicator h) x₀ hρ x
theorem
CKN.Foundation.Heat.weak_harmonic_interior_representative_bound
{h : Parabolic.Vec3 → ℝ}
{x₀ : Parabolic.Vec3}
{ρ : ℝ}
(hρ : 0 < ρ)
(hmem : MeasureTheory.MemLp h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ)))
(x : Vec 3)
:
x ∈ euclideanBall x₀ (ρ / 2) →
|weakHarmonicInteriorRepresentative h x₀ hρ x| ≤ weakHarmonicInteriorSupConstant * (ρ ^ 2)⁻¹ * MeasureTheory.lpNorm h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ))