OAI/Geometry/RCD/Sobolev/TightL2Difference.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

L² difference from a local bound and two square-integrable tails

  1. theorem OAI.RegularPointCoordinates.tight_L2_norm_sub_sq_le line 15