OAI/Geometry/RCD/Heat/CompactHeatHarmonicAffineMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Affine means for original harmonic constant-energy coordinates

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.affine_original_harmonic_mean line 21