OAI/Geometry/IntegralFillings/Currents/CanonicalMass.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpIntegralFillings.MassMeasure.weighted line 34
2. lemma OAI.SharpIntegralFillings.MassMeasure.weighted_finite line 37
3. lemma OAI.SharpIntegralFillings.MassMeasure.integral_weighted line 43
4. lemma OAI.SharpIntegralFillings.MassMeasure.weighted_total line 51
5. lemma OAI.SharpIntegralFillings.MassMeasure.controls_splice line 58
6. lemma OAI.SharpIntegralFillings.MassMeasure.integral_cutoff_le line 95
7. lemma OAI.SharpIntegralFillings.MassMeasure.measure_closed_le line 118
8. lemma OAI.SharpIntegralFillings.MassMeasure.measure_le line 144
9. lemma OAI.SharpIntegralFillings.MassMeasure.measure_unique line 153
10. def OAI.SharpIntegralFillings.MassMeasure.currentMassMeasure line 158
11. instance OAI.SharpIntegralFillings.MassMeasure.currentMassMeasure_finite line 161
12. lemma OAI.SharpIntegralFillings.MassMeasure.currentMassMeasure_controls line 165
13. lemma OAI.SharpIntegralFillings.MassMeasure.currentMassMeasure_total line 169
14. lemma OAI.SharpIntegralFillings.MassMeasure.currentMassMeasure_le line 173