OAI/Geometry/RCD/Harmonic/EuclideanRadialWeight.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.glue_derivative line 14
2. def OAI.RegularPointCoordinates.euclideanRadialPotential line 19
3. def OAI.RegularPointCoordinates.euclideanRadialWeight line 22
4. theorem OAI.RegularPointCoordinates.euclideanRadialPotential_smooth line 25
5. theorem OAI.RegularPointCoordinates.euclideanRadialWeight_smooth line 28
6. theorem OAI.RegularPointCoordinates.euclideanRadialWeight_nonneg line 35
7. theorem OAI.RegularPointCoordinates.euclideanRadialWeight_zero_pos line 41
8. theorem OAI.RegularPointCoordinates.euclideanRadialWeight_support line 46
9. theorem OAI.RegularPointCoordinates.euclideanRadialPotential_support line 56
10. theorem OAI.RegularPointCoordinates.euclideanRadialWeight_compact line 64
11. theorem OAI.RegularPointCoordinates.euclideanRadialPotential_compact line 67
12. theorem OAI.RegularPointCoordinates.euclideanRadialWeight_mass_pos line 70
13. theorem OAI.RegularPointCoordinates.euclideanRadialPotential_fderiv line 78

    Source documentation

    The radial potential converts a dilation derivative into a gradient pairing, to which the compact-test Green identity applies.

    theorem euclideanRadialPotential_fderiv (n : ℕ) (x v : Euclidean n) :
        fderiv ℝ (euclideanRadialPotential n) x v =
          -euclideanRadialWeight n x*inner ℝ x v := by
    …

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