OAI/Geometry/RCD/Sobolev/EuclideanWeakHarmonicMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A distributional harmonic function satisfies the exact local radial mean identity

  1. theorem OAI.RegularPointCoordinates.weak_harmonic_radial_mean line 14