OAI/Geometry/RCD/Sobolev/EuclideanWeakHarmonicSmoothing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Smooth harmonic local averages of a distributional harmonic function

  1. def OAI.RegularPointCoordinates.EuclideanWeakHarmonicOn line 14

    Source documentation

    The compact-test distributional Laplace equation on one Euclidean ball.

    def EuclideanWeakHarmonicOn {n : ℕ} (g : Euclidean n → ℝ) (S : ℝ) : Prop :=
…

    Mentions: OAI.RegularPointCoordinates.Euclidean

  2. theorem OAI.RegularPointCoordinates.weak_harmonic_convolution line 17