OAI/Analysis/SegmentLenses/IndexedForest.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Arbitrarily indexed finite-height forests

  1. def OAI.SegmentLenses.IndexedForest.Vertex line 22
  2. def OAI.SegmentLenses.IndexedForest.Ancestor line 24
  3. theorem OAI.SegmentLenses.IndexedForest.ancestor_refl line 29
  4. theorem OAI.SegmentLenses.IndexedForest.ancestor_antisymm line 30
  5. instance OAI.SegmentLenses.IndexedForest.(instance at line 33) line 33
  6. instance OAI.SegmentLenses.IndexedForest.(instance at line 44) line 44
  7. instance OAI.SegmentLenses.IndexedForest.(instance at line 51) line 51
  8. instance OAI.SegmentLenses.IndexedForest.(instance at line 58) line 58
  9. instance OAI.SegmentLenses.IndexedForest.(instance at line 61) line 61
  10. instance OAI.SegmentLenses.IndexedForest.(instance at line 72) line 72
  11. instance OAI.SegmentLenses.IndexedForest.(instance at line 86) line 86
  12. abbrev OAI.SegmentLenses.IndexedForest.J line 88
  13. abbrev OAI.SegmentLenses.IndexedForest.X line 89
  14. def OAI.SegmentLenses.IndexedForest.heightTest line 96
  15. theorem OAI.SegmentLenses.IndexedForest.heightTest_apply line 101
  16. theorem OAI.SegmentLenses.IndexedForest.norm_heightTest_le line 104
  17. theorem OAI.SegmentLenses.IndexedForest.segment_same_height line 111
  18. theorem OAI.SegmentLenses.IndexedForest.segment_level_injective line 118
  19. theorem OAI.SegmentLenses.IndexedForest.segment_card_bound line 131
  20. def OAI.SegmentLenses.IndexedForest.familyAtHeight line 147
  21. theorem OAI.SegmentLenses.IndexedForest.atHeight_seminorm line 155
  22. theorem OAI.SegmentLenses.IndexedForest.height_hilbert_upper line 182
  23. def OAI.SegmentLenses.IndexedForest.testHeights line 225
  24. theorem OAI.SegmentLenses.IndexedForest.heightTest_eq_zero line 227
  25. theorem OAI.SegmentLenses.IndexedForest.heightTest_idem line 239
  26. theorem OAI.SegmentLenses.IndexedForest.heightTest_ne line 246
  27. theorem OAI.SegmentLenses.IndexedForest.forest_norm_sq_decomposition line 258
  28. def OAI.SegmentLenses.IndexedForest.heightTests line 334
  29. theorem OAI.SegmentLenses.IndexedForest.mem_heightTests line 336
  30. abbrev OAI.SegmentLenses.IndexedForest.HeightPrimal line 344
  31. def OAI.SegmentLenses.IndexedForest.heightHilbert line 346
  32. theorem OAI.SegmentLenses.IndexedForest.heightHilbert_closed line 352
  33. instance OAI.SegmentLenses.IndexedForest.(instance at line 362) line 362
  34. def OAI.SegmentLenses.IndexedForest.heightToHilbert line 365
  35. theorem OAI.SegmentLenses.IndexedForest.heightToHilbert_apply line 373
  36. theorem OAI.SegmentLenses.IndexedForest.heightToHilbert_dense line 377
  37. def OAI.SegmentLenses.IndexedForest.heightHilbertEquiv line 410
  38. theorem OAI.SegmentLenses.IndexedForest.heightPrimal_reflexive line 430
  39. def OAI.SegmentLenses.IndexedForest.heightBlockTest line 445
  40. theorem OAI.SegmentLenses.IndexedForest.norm_heightBlockTest line 449
  41. theorem OAI.SegmentLenses.IndexedForest.heightBlockTest_zero line 452
  42. def OAI.SegmentLenses.IndexedForest.forestBlockVector line 457
  43. theorem OAI.SegmentLenses.IndexedForest.forestBlockVector_apply line 460
  44. def OAI.SegmentLenses.IndexedForest.forestTestBlocks line 471
  45. theorem OAI.SegmentLenses.IndexedForest.forestTestBlocks_apply line 482
  46. theorem OAI.SegmentLenses.IndexedForest.norm_forestTestBlocks line 485
  47. theorem OAI.SegmentLenses.IndexedForest.forestTestBlocks_of_height line 494
  48. theorem OAI.SegmentLenses.IndexedForest.forestTestBlocks_dense line 513
  49. def OAI.SegmentLenses.IndexedForest.forestL2Equiv line 531
  50. theorem OAI.SegmentLenses.IndexedForest.forestL2Equiv_test line 540
  51. theorem OAI.SegmentLenses.IndexedForest.forest_primal_reflexive line 552
  52. theorem OAI.SegmentLenses.IndexedForest.forest_dual_reflexive line 557