OAI/Geometry/RCD/Harmonic/LocalConstantHarmonic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A genuine local constant is weakly harmonic

  1. theorem OAI.RegularPointCoordinates.isSobolevHarmonicOn_of_local_constant line 17

    Source documentation

    Gradient locality on level sets suffices; no global constant Sobolev function is needed when the ambient measure is infinite.

    theorem isSobolevHarmonicOn_of_local_constant (s : Set X) (hs : MeasurableSet s)
    (η : SobolevSpace μ hQ) (c : ℝ)
    (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ.restrict s] fun _ => c) :
    IsSobolevHarmonicOn μ hQ s η := by
…

    Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.IsSobolevHarmonicOn

  2. theorem OAI.RegularPointCoordinates.GoodLaplacianCutoff.harmonic_on_inner_ball line 34