OAI/Geometry/RCD/Sobolev/EuclideanWeakHarmonicSmooth.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Smoothness needed to recover the actual local harmonic model

The proved radial mean identity identifies the function locally with a convolution against a compact smooth kernel, at every derivative order.

  1. theorem OAI.RegularPointCoordinates.compact_continuous_weak_harmonic_smooth line 16
  2. theorem OAI.RegularPointCoordinates.continuous_weak_harmonic_smooth line 44