OAI/Geometry/RCD/Harmonic/WeightedUnitDefect.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A sharp weighted upper bound and lower integral control give L1 convergence

  1. theorem OAI.RegularPointCoordinates.weighted_unit_defect_tendsto line 12