OAI/Analysis/SegmentLenses/ConeNorms.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Cone norms, separated families, and level forests

  1. theorem OAI.SegmentLenses.SegmentEmbedding.primalEquivOfSurjective_eq_map line 21
  2. def OAI.SegmentLenses.coneDual line 37
  3. theorem OAI.SegmentLenses.cone_inclusion_composition line 42
  4. theorem OAI.SegmentLenses.exteriorConeDual_apply line 63
  5. theorem OAI.SegmentLenses.complementary_cone_norm line 79
  6. theorem OAI.SegmentLenses.exterior_range_eq_tail line 88
  7. def OAI.SegmentLenses.exteriorToTailEquiv line 97
  8. def OAI.SegmentLenses.complementary_cone_isometry line 104
  9. theorem OAI.SegmentLenses.infinite_separated_family line 114
  10. theorem OAI.SegmentLenses.forest_separated_family line 124
  11. def OAI.SegmentLenses.singletonTestEquiv line 145
  12. def OAI.SegmentLenses.singletonPrimalEquiv line 169
  13. theorem OAI.SegmentLenses.singletonPrimalEquiv_test line 178
  14. def OAI.SegmentLenses.realDualEquiv line 187
  15. def OAI.SegmentLenses.RealSum2Fiber line 209
  16. instance OAI.SegmentLenses.realSum2FiberGroup line 213
  17. instance OAI.SegmentLenses.realSum2FiberSpace line 218
  18. instance OAI.SegmentLenses.realSum2FiberComplete line 223
  19. abbrev OAI.SegmentLenses.RealSum2 line 230
  20. theorem OAI.SegmentLenses.realSum2_norm_sq line 232
  21. abbrev OAI.SegmentLenses.Levels.Vertex line 242
  22. abbrev OAI.SegmentLenses.Levels.J line 243
  23. abbrev OAI.SegmentLenses.Levels.X line 244
  24. def OAI.SegmentLenses.Levels.partition line 246
  25. abbrev OAI.SegmentLenses.Levels.RootBlock line 250
  26. abbrev OAI.SegmentLenses.Levels.ForestBlock line 251
  27. def OAI.SegmentLenses.Levels.root line 253
  28. instance OAI.SegmentLenses.Levels.(instance at line 255) line 255
  29. def OAI.SegmentLenses.Levels.forestOrderEmbedding line 272
  30. theorem OAI.SegmentLenses.Levels.forestOrderEmbedding_surjective line 280
  31. def OAI.SegmentLenses.Levels.forestEmbedding line 288
  32. def OAI.SegmentLenses.Levels.forestBlockEquiv line 291
  33. def OAI.SegmentLenses.Levels.primalSplit line 295
  34. def OAI.SegmentLenses.Levels.dualSplit line 303