OAI/Geometry/TamingCompatibility/Charts/SummableCutoff.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.SummableCutoff.exceptional line 13
2. def OAI.TamingCompatibility.SummableCutoff.saturation line 15
3. def OAI.TamingCompatibility.SummableCutoff.tailLimit line 18
4. lemma OAI.TamingCompatibility.SummableCutoff.saturation_nonneg line 23
5. lemma OAI.TamingCompatibility.SummableCutoff.saturation_le_one line 28
6. lemma OAI.TamingCompatibility.SummableCutoff.saturation_tendsto_tail line 34
7. lemma OAI.TamingCompatibility.SummableCutoff.tail_nonneg line 48
8. lemma OAI.TamingCompatibility.SummableCutoff.tail_le_one line 53
9. lemma OAI.TamingCompatibility.SummableCutoff.tail_tendsto_indicator line 58
10. lemma OAI.TamingCompatibility.SummableCutoff.measurable_exceptional line 71
11. lemma OAI.TamingCompatibility.SummableCutoff.exceptional_null line 86
12. lemma OAI.TamingCompatibility.SummableCutoff.measurable_saturation line 100
13. lemma OAI.TamingCompatibility.SummableCutoff.measurable_tail line 105