OAI/Geometry/RCD/Transport/SubplanAbsoluteIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Absolute errors from normalized submeasure mean bounds

  1. theorem OAI.RegularPointCoordinates.integral_abs_le_of_setIntegral_bound line 13
  2. theorem OAI.RegularPointCoordinates.integral_abs_le_of_normalized_submeans line 33