OAI/Geometry/RCD/Metric/ContainingMassL2Error.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

L2 errors normalized by the mass of a containing region

  1. theorem OAI.RegularPointCoordinates.l2_product_error_of_containing_mass line 13