OAI/Geometry/CAT0Fillings/Currents/Summation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

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