OAI/Geometry/RCD/Harmonic/HarmonicReplacementFamily.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Harmonic replacements on a fixed inner physical ball

The annular condition is derived from the actual measured maps. The normalization remains the mass of the larger approximation ball.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.harmonic_replacement_family line 18