OAI/Analysis/SegmentLenses/Canonical.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Endpoint vectors and canonical bidual identifications

  1. def OAI.SegmentLenses.dominatedL2 line 23
  2. theorem OAI.SegmentLenses.dominatedL2_apply line 30
  3. theorem OAI.SegmentLenses.endpoint_law_vectors line 44
  4. theorem OAI.SegmentLenses.primal_coordinate_density line 85
  5. theorem OAI.SegmentLenses.coordinatePredual_complete line 102
  6. theorem OAI.SegmentLenses.primalHead_idempotent line 107
  7. theorem OAI.SegmentLenses.primalTail_idempotent line 121
  8. def OAI.SegmentLenses.canonicalBidualEquiv line 132
  9. theorem OAI.SegmentLenses.canonicalBidualEquiv_apply line 135
  10. def OAI.SegmentLenses.forestCanonicalDual line 139
  11. theorem OAI.SegmentLenses.forestCanonicalDual_apply line 141
  12. theorem OAI.SegmentLenses.infinite_main_tail_internal line 147
  13. theorem OAI.SegmentLenses.forest_radial_tail line 156
  14. theorem OAI.SegmentLenses.infinite_original_coefficient_average line 164
  15. abbrev OAI.SegmentLenses.LevelForest.Index line 181
  16. abbrev OAI.SegmentLenses.LevelForest.Vertex line 182
  17. abbrev OAI.SegmentLenses.LevelForest.J line 183
  18. abbrev OAI.SegmentLenses.LevelForest.X line 184
  19. def OAI.SegmentLenses.LevelForest.shiftOrderEmbedding line 187
  20. theorem OAI.SegmentLenses.LevelForest.shiftOrderEmbedding_surjective line 214
  21. def OAI.SegmentLenses.LevelForest.shiftEmbedding line 222
  22. def OAI.SegmentLenses.LevelForest.heightEquiv line 228
  23. def OAI.SegmentLenses.LevelForest.primalSplit line 232
  24. def OAI.SegmentLenses.LevelForest.dualSplit line 235
  25. theorem OAI.SegmentLenses.LevelForest.shift_component line 238
  26. theorem OAI.SegmentLenses.LevelForest.shift_word line 241
  27. def OAI.SegmentLenses.SingleTree.IsLeaf line 249
  28. theorem OAI.SegmentLenses.SingleTree.leaf_iff_full_height line 251
  29. theorem OAI.SegmentLenses.SingleTree.every_n_levels_leaf_steps line 274