OAI/Analysis/SegmentLenses/IndexedDual.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Indexed forest duals and unbounded-height obstructions

  1. def OAI.SegmentLenses.dualTransport line 24
  2. theorem OAI.SegmentLenses.dualTransport_apply line 40
  3. theorem OAI.SegmentLenses.l2DualEquiv_symm_apply line 49
  4. def OAI.SegmentLenses.IndexedForest.dualL2Equiv line 64
  5. theorem OAI.SegmentLenses.IndexedForest.dualL2Equiv_apply line 67
  6. theorem OAI.SegmentLenses.IndexedForest.dualL2Equiv_on_test line 74
  7. theorem OAI.SegmentLenses.IndexedForest.coordinateSpan_eq_top line 83
  8. theorem OAI.SegmentLenses.IndexedForest.separable line 86
  9. def OAI.SegmentLenses.IndexedForest.forestRoot line 96
  10. def OAI.SegmentLenses.IndexedForest.forestNode line 97
  11. theorem OAI.SegmentLenses.IndexedForest.forest_iic_segment line 100
  12. def OAI.SegmentLenses.IndexedForest.forestPath line 113
  13. theorem OAI.SegmentLenses.IndexedForest.norm_forestPath line 116
  14. theorem OAI.SegmentLenses.IndexedForest.forestPath_child line 122
  15. theorem OAI.SegmentLenses.IndexedForest.forestPath_children_weakly_null line 152
  16. theorem OAI.SegmentLenses.IndexedForest.unbounded_unit_finite_paths line 167
  17. theorem OAI.SegmentLenses.IndexedForest.unbounded_vertices_infinite line 179
  18. theorem OAI.SegmentLenses.IndexedForest.unbounded_equivalent_modulus_zero line 190
  19. theorem OAI.SegmentLenses.IndexedForest.unbounded_no_equivalent_AUC line 200