OAI/Geometry/RCD/Harmonic/MixedGramL1.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Three unit-direction energy limits identify each mixed Gram entry

  1. theorem OAI.RegularPointCoordinates.mixed_defect_le line 13
  2. theorem OAI.RegularPointCoordinates.mixed_gram_l1_tendsto line 22