OAI/Geometry/RCD/Coordinates/NormalizedL2LimitBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Retaining the exact normalized L2 bound in a value limit

  1. theorem OAI.RegularPointCoordinates.square_add_le_weighted line 12
  2. theorem OAI.RegularPointCoordinates.normalized_L2_limit_le_one line 22