OAI/Analysis/SegmentLenses/ForestBlocks.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

The finite-height forest as a sum of reflexive blocks

  1. theorem OAI.SegmentLenses.exists_norming_family line 24
  2. def OAI.SegmentLenses.heightTest line 46
  3. theorem OAI.SegmentLenses.heightTest_apply line 51
  4. theorem OAI.SegmentLenses.norm_heightTest_le line 54
  5. theorem OAI.SegmentLenses.segment_same_height line 61
  6. theorem OAI.SegmentLenses.segment_level_injective line 67
  7. theorem OAI.SegmentLenses.segment_card_bound line 79
  8. def OAI.SegmentLenses.SegmentFamily.atHeight line 95
  9. theorem OAI.SegmentLenses.atHeight_seminorm line 103
  10. theorem OAI.SegmentLenses.height_hilbert_upper line 130
  11. def OAI.SegmentLenses.testHeights line 173
  12. theorem OAI.SegmentLenses.heightTest_eq_zero line 175
  13. theorem OAI.SegmentLenses.heightTest_idem line 187
  14. theorem OAI.SegmentLenses.heightTest_ne line 194
  15. theorem OAI.SegmentLenses.forest_norm_sq_decomposition line 206
  16. def OAI.SegmentLenses.testL2 line 283
  17. theorem OAI.SegmentLenses.testL2_eq_sum line 288
  18. theorem OAI.SegmentLenses.testL2_apply line 294
  19. theorem OAI.SegmentLenses.norm_testL2_sq line 305
  20. theorem OAI.SegmentLenses.norm_testL2_le line 310