OAI/Analysis/SegmentLenses/ForestDual.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Full-forest reflexivity and coordinate identification

  1. def OAI.SegmentLenses.heightTests line 22
  2. theorem OAI.SegmentLenses.mem_heightTests line 24
  3. abbrev OAI.SegmentLenses.HeightPrimal line 32
  4. def OAI.SegmentLenses.heightHilbert line 34
  5. theorem OAI.SegmentLenses.heightHilbert_closed line 40
  6. instance OAI.SegmentLenses.(instance at line 49) line 49
  7. def OAI.SegmentLenses.heightToHilbert line 52
  8. theorem OAI.SegmentLenses.heightToHilbert_apply line 60
  9. theorem OAI.SegmentLenses.heightToHilbert_dense line 64
  10. def OAI.SegmentLenses.heightHilbertEquiv line 97
  11. theorem OAI.SegmentLenses.heightPrimal_reflexive line 117
  12. def OAI.SegmentLenses.heightBlockTest line 132
  13. theorem OAI.SegmentLenses.norm_heightBlockTest line 136
  14. theorem OAI.SegmentLenses.heightBlockTest_zero line 139
  15. def OAI.SegmentLenses.forestBlockVector line 144
  16. theorem OAI.SegmentLenses.forestBlockVector_apply line 147
  17. def OAI.SegmentLenses.forestTestBlocks line 158
  18. theorem OAI.SegmentLenses.forestTestBlocks_apply line 169
  19. theorem OAI.SegmentLenses.norm_forestTestBlocks line 172
  20. theorem OAI.SegmentLenses.forestTestBlocks_of_height line 181
  21. theorem OAI.SegmentLenses.forestTestBlocks_dense line 200
  22. def OAI.SegmentLenses.forestL2Equiv line 218
  23. theorem OAI.SegmentLenses.forestL2Equiv_test line 227
  24. theorem OAI.SegmentLenses.forest_primal_reflexive line 239
  25. theorem OAI.SegmentLenses.forest_dual_reflexive line 244