OAI/Geometry/RCD/Harmonic/InnerHarmonicNormBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Changing the normalization of actual harmonic candidates

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.inner_harmonic_norm_bound line 16