OAI/Analysis/SegmentLenses/ConeBlocks.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Component and cone decompositions

  1. theorem OAI.SegmentLenses.SegmentEmbedding.norm_testL2_map line 22
  2. theorem OAI.SegmentLenses.SingleTree.component_estimate line 36
  3. theorem OAI.SegmentLenses.SingleTree.levels_component_estimate line 51
  4. def OAI.SegmentLenses.SingleTree.extensionSteps line 60
  5. def OAI.SegmentLenses.SingleTree.root line 62
  6. def OAI.SegmentLenses.SingleTree.zeroLeaf line 64
  7. theorem OAI.SegmentLenses.SingleTree.root_steps line 66
  8. theorem OAI.SegmentLenses.SingleTree.leaf_steps line 67
  9. theorem OAI.SegmentLenses.SingleTree.child_steps line 69
  10. theorem OAI.SegmentLenses.SingleTree.n_levels_path line 72
  11. theorem OAI.SegmentLenses.ComponentPartition.regionL2Equiv_regionMap line 89
  12. theorem OAI.SegmentLenses.ComponentPartition.regionDualL2Equiv_apply line 108
  13. abbrev OAI.SegmentLenses.ConeVertex line 124
  14. def OAI.SegmentLenses.coneEmbedding line 126
  15. def OAI.SegmentLenses.coneBlockOrderEmbedding line 130
  16. theorem OAI.SegmentLenses.coneBlockOrderEmbedding_surjective line 139
  17. def OAI.SegmentLenses.coneBlockEmbedding line 145
  18. def OAI.SegmentLenses.coneBlockEquiv line 151
  19. def OAI.SegmentLenses.exteriorConeL2Equiv line 157
  20. def OAI.SegmentLenses.exteriorConeDualL2Equiv line 162