OAI/Analysis/BiholderTransport/Volume/LocalCharts.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakMTWTransport.ae_jacobian_bounds_of_image_mass line 20
  2. lemma OAI.WeakMTWTransport.metricVolume_lipschitz_image_le_nat line 63
  3. lemma OAI.WeakMTWTransport.image_mass_in_bilipschitz_coordinates line 70