OAI/Geometry/CAT0Fillings/Swept/Current.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CAT0Fillings.ChartGeometry line 20
  2. theorem OAI.CAT0Fillings.exists_chartGeometry line 47
  3. def OAI.CAT0Fillings.ChartGeometry.gram line 89
  4. def OAI.CAT0Fillings.ChartGeometry.density line 91
  5. lemma OAI.CAT0Fillings.ChartGeometry.density_integrable line 94
  6. lemma OAI.CAT0Fillings.ChartGeometry.density_summable line 96
  7. lemma OAI.CAT0Fillings.ChartGeometry.density_mass line 99
  8. lemma OAI.CAT0Fillings.endpoint_lipschitz line 119
  9. theorem OAI.CAT0Fillings.swept_boundary_integral line 125
  10. def OAI.CAT0Fillings.ChartGeometry.sweptMass line 174
  11. lemma OAI.CAT0Fillings.ChartGeometry.swept_integrable_summable line 178
  12. lemma OAI.CAT0Fillings.ChartGeometry.sweptMass_nonneg line 192
  13. lemma OAI.CAT0Fillings.ChartGeometry.sweptMass_const_mul line 200
  14. theorem OAI.CAT0Fillings.exists_swept_current line 211