OAI/Geometry/Cannon/Modulus/PathCellIndices.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CannonAnnular.pathCellIndices line 31
2. def OAI.CannonAnnular.MacroscopicAdmissible line 36
3. lemma OAI.CannonAnnular.exists_outer_point line 41
4. theorem OAI.CannonAnnular.annular_interval_cover line 54
5. theorem OAI.CannonAnnular.annular_comparison line 113
6. theorem OAI.CannonAnnular.exists_packed_annular_constant line 186
7. lemma OAI.CannonCapacity.level_radial_hit line 264
8. theorem OAI.CannonCapacity.unmarked_level_detection line 273
9. lemma OAI.CannonCapacity.sparse_transfer_energy line 379
10. theorem OAI.CannonCapacity.exists_local_transfer_constant line 409
11. theorem OAI.CannonCapacity.node_separated_capacity line 471