OAI/Analysis/SegmentLenses/Components.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Component partitions and completion decompositions

  1. structure OAI.SegmentLenses.ComponentPartition line 24
  2. def OAI.SegmentLenses.ComponentPartition.blockTest line 39
  3. theorem OAI.SegmentLenses.ComponentPartition.blockTest_apply line 44
  4. theorem OAI.SegmentLenses.ComponentPartition.norm_blockTest_le line 54
  5. theorem OAI.SegmentLenses.ComponentPartition.segment_same_index line 62
  6. def OAI.SegmentLenses.ComponentPartition.familyAtBlock line 72
  7. theorem OAI.SegmentLenses.ComponentPartition.atBlock_seminorm line 80
  8. def OAI.SegmentLenses.ComponentPartition.testIndices line 109
  9. theorem OAI.SegmentLenses.ComponentPartition.blockTest_eq_zero line 111
  10. theorem OAI.SegmentLenses.ComponentPartition.blockTest_idem line 123
  11. theorem OAI.SegmentLenses.ComponentPartition.blockTest_ne line 130
  12. theorem OAI.SegmentLenses.ComponentPartition.norm_sq_decomposition line 142
  13. def OAI.SegmentLenses.ComponentPartition.blockTests line 214
  14. theorem OAI.SegmentLenses.ComponentPartition.mem_blockTests line 216
  15. abbrev OAI.SegmentLenses.ComponentPartition.BlockPrimal line 224
  16. def OAI.SegmentLenses.ComponentPartition.completedBlockTest line 236
  17. theorem OAI.SegmentLenses.ComponentPartition.norm_completedBlockTest line 240
  18. theorem OAI.SegmentLenses.ComponentPartition.completedBlockTest_zero line 249
  19. def OAI.SegmentLenses.ComponentPartition.blockVector line 254
  20. theorem OAI.SegmentLenses.ComponentPartition.blockVector_apply line 257
  21. def OAI.SegmentLenses.ComponentPartition.testBlocks line 268
  22. theorem OAI.SegmentLenses.ComponentPartition.testBlocks_apply line 279
  23. theorem OAI.SegmentLenses.ComponentPartition.norm_testBlocks line 282
  24. theorem OAI.SegmentLenses.ComponentPartition.testBlocks_of_height line 291
  25. theorem OAI.SegmentLenses.ComponentPartition.testBlocks_dense line 310
  26. def OAI.SegmentLenses.ComponentPartition.l2Equiv line 328
  27. theorem OAI.SegmentLenses.ComponentPartition.l2Equiv_test line 337