OAI/Geometry/DoublingHilbert/ClusterScales.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CompactBanach.clusterScale line 12
2. theorem OAI.CompactBanach.clusterScale_pos line 14
3. theorem OAI.CompactBanach.clusterScale_add line 18
4. theorem OAI.CompactBanach.clusterScale_antitone line 23
5. theorem OAI.CompactBanach.clusterScale_half line 29
6. theorem OAI.CompactBanach.clusterScale_tendsto line 35
7. theorem OAI.CompactBanach.cluster_norm_bound line 41
8. theorem OAI.CompactBanach.cluster_separation line 52
9. theorem OAI.CompactBanach.five_scales line 70