OAI/Geometry/RCD/Harmonic/EuclideanRadialMean.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The radial mean identity derived from classical harmonicity

  1. theorem OAI.RegularPointCoordinates.fderiv_affine_dilation_apply line 14
  2. theorem OAI.RegularPointCoordinates.harmonic_radial_mean line 25

    Source documentation

    Every smooth radial weight constructed above reproduces a harmonic function whenever its rescaled support remains inside the harmonic ball.

    theorem harmonic_radial_mean {n : ℕ} {f : Euclidean n → ℝ}
    (hf : ContDiff ℝ 2 f) (hfs : HasCompactSupport f) (p : Euclidean n)
    {R r : ℝ} (hR : 0 < R) (hr : 0 < r) (hrR : r < R)
    (hh : HarmonicOnNhd f (ball p R)) :
    (∫ x, f (p+r • x)*euclideanRadialWeight n x) =
      f p*(∫ x, euclideanRadialWeight n x) := by
…

    Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.euclideanRadialWeight