OAI/Geometry/IntegralFillings/Currents/Summation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpIntegralFillings.tsum_lintegral_norm_ne_top line 32
2. lemma OAI.SharpIntegralFillings.ae_summable_norm_of_integral line 44
3. lemma OAI.SharpIntegralFillings.integrable_series_norm line 54
4. lemma OAI.SharpIntegralFillings.integrable_series line 69
5. lemma OAI.SharpIntegralFillings.summable_actions_all line 86
6. theorem OAI.SharpIntegralFillings.isMetricCurrent_tsum line 93
7. lemma OAI.SharpIntegralFillings.mass_tsum_le line 123