EuclideanRadialGreen.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.RegularPointCoordinates.integral_radial_dilation_eq_laplacian line 15
Source documentation
The derivative of radial averages is a compactly supported Laplacian pairing. This identity is valid before imposing harmonicity.
```
theorem integral_radial_dilation_eq_laplacian {n : ℕ} {f : Euclidean n → ℝ}
    (hf : ContDiff ℝ 2 f) :
    (∫ x, fderiv ℝ f x x*euclideanRadialWeight n x) =
      ∫ x, (Δ f) x*euclideanRadialPotential n x := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.euclideanRadialWeight, OAI.RegularPointCoordinates.euclideanRadialPotential
theorem OAI.RegularPointCoordinates.integral_radial_dilation_eq_zero line 53
Source documentation
Harmonicity on the support of the potential makes the radial dilation pairing vanish.
```
theorem integral_radial_dilation_eq_zero {n : ℕ} {f : Euclidean n → ℝ}
    (hf : ContDiff ℝ 2 f)
    (hh : InnerProductSpace.HarmonicOnNhd f (closedBall 0 1)) :
    (∫ x, fderiv ℝ f x x*euclideanRadialWeight n x) = 0 := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.euclideanRadialWeight