OAI/Geometry/IntegralFillings/Currents/WeakMass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpIntegralFillings.controls_of_weak_limits line 18
2. lemma OAI.SharpIntegralFillings.exists_controls_of_bounded_weak_limit line 30
3. lemma OAI.SharpIntegralFillings.mass_le_of_bounded_weak_limit line 56
4. lemma OAI.SharpIntegralFillings.BoundedLip.mul line 67
5. lemma OAI.SharpIntegralFillings.IsMetricCurrent.mass_bound_uniform line 93
6. lemma OAI.SharpIntegralFillings.IsMetricCurrent.eq_zero_of_mass_eq_zero line 109