OAI/Geometry/IntegralFillings/Optimality/BallCurrent.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpIntegralFillings.Optimality.innerSpace_CAT0 line 20
2. abbrev OAI.SharpIntegralFillings.Optimality.UnitBall line 44
3. instance OAI.SharpIntegralFillings.Optimality.(instance at line 46) line 46
4. lemma OAI.SharpIntegralFillings.Optimality.unitBall_CAT0 line 48
5. def OAI.SharpIntegralFillings.Optimality.ballChart line 51
6. lemma OAI.SharpIntegralFillings.Optimality.chart_integerRectifiable line 69
7. lemma OAI.SharpIntegralFillings.Optimality.det_le_one_of_clm_norm line 90
8. lemma OAI.SharpIntegralFillings.Optimality.chart_mass_le_unitLip line 109
9. lemma OAI.SharpIntegralFillings.Optimality.ballChart_mass_le line 136