OAI/Geometry/Cannon/Modulus/ClosedAnnulus.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CannonAtomic.record_annular_bound line 32
2. def OAI.CannonAnnularCompactness.closedAnnulus line 56
3. lemma OAI.CannonAnnularCompactness.annuli_disjoint line 59
4. theorem OAI.CannonAnnularCompactness.disjoint_atomic_energy line 66
5. theorem OAI.CannonAnnularCompactness.many_annuli_bound line 74
6. theorem OAI.CannonAnnularCompactness.equicontinuousAt_of_tail_quadratic line 88
7. lemma OAI.CannonAnnularCompactness.finite_measure_disjoint_sum line 122
8. theorem OAI.CannonAnnularCompactness.equicontinuousAt_of_disjoint_measures line 134
9. theorem OAI.CannonAnnularCompactness.equicontinuousAt_of_annular_tails line 169