Documentation

LeanPool.CaffarelliKohnNirenberg.Foundation.Harmonic.InteriorSupDisplay

The interior supremum bound for weakly harmonic L^{3/2} functions #

This file proves the first display eq:harm-sup of lem:harmonic-interior in paper/ckn.tex: for a function h that is weakly harmonic on the ball B_ρ(x₀) and lies in L^{3/2}(B_ρ(x₀)),

‖h‖_{L^∞(B_{3ρ/4}(x₀))} ≤ C₁₇ ρ^{-2} ‖h‖_{L^{3/2}(B_ρ(x₀))},

with an absolute constant C₁₇.

The established interior displays weak_harmonic_interior_displays produce a continuously differentiable representative of h on the half ball together with a pointwise bound for that representative on the three-quarter ball. The essential supremum of h itself on the three-quarter ball is obtained here by applying those displays at every centre y ∈ B_{3ρ/4}(x₀) on the ball B_{ρ/4}(y) ⊆ B_ρ(x₀), which identifies h with its representative almost everywhere on B_{ρ/8}(y), and by localizing the resulting null sets: a set that is null in a neighbourhood of each of its points is null in a second-countable space.

source
noncomputable def CKN.Foundation.Heat.harmonicInteriorSupDisplayConstant :
ℝ

The absolute constant C₁₇ of eq:harm-sup.

Equations
Instances For
    source
    theorem CKN.Foundation.Heat.harmonicInteriorSupDisplayConstant_nonneg :
    0 ≤ harmonicInteriorSupDisplayConstant
    source
    theorem CKN.Foundation.Heat.weak_harmonic_interior_sup :
    ∃ (C₁₇ : ℝ), ∀ (h : Parabolic.Vec3 → ℝ) (x₀ : Parabolic.Vec3) (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ)) → WeaklyHarmonicOn (euclideanBall x₀ ρ) h → MeasureTheory.eLpNorm h ⊤ (MeasureTheory.volume.restrict (euclideanBall x₀ (3 * ρ / 4))) ≤ ENNReal.ofReal (C₁₇ * (ρ ^ 2)⁻¹ * MeasureTheory.lpNorm h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ)))

    The interior supremum bound eq:harm-sup of lem:harmonic-interior. There is an absolute constant C₁₇ such that every weakly harmonic L^{3/2} function on a ball satisfies ‖h‖_{L^∞(B_{3ρ/4})} ≤ C₁₇ ρ^{-2} ‖h‖_{L^{3/2}(B_ρ)}.