Documentation

LeanPool.CaffarelliKohnNirenberg.Foundation.Harmonic.Liouville

Liouville #

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

source
def CKN.Foundation.Heat.liouvilleBall (n : ℕ) :
Set Parabolic.Vec3

Increasing sequence of Euclidean balls used in the Liouville argument.

Equations
Instances For
    source
    theorem CKN.Foundation.Heat.weaklyHarmonicOn_eq_zero_of_lpNorm_linear_growth {H : Parabolic.Vec3 → ℝ} {C : ℝ} (hC : 0 ≤ C) (hmem : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp H (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) (hweak : WeaklyHarmonicOn Set.univ H) (hgrowth : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm H (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ C * (1 + ρ)) :
    H =ᵐ[MeasureTheory.volume] 0

    A weakly harmonic function with at most linear local L^{3/2} growth is zero almost everywhere. The proof uses the smooth local representative and its scale-dependent interior sup estimate on expanding balls.