OAI/Analysis/SegmentLenses/Obstructions.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Equivalent-norm obstructions from weakly null paths

  1. def OAI.SegmentLenses.oneSidedOn line 20
  2. def OAI.SegmentLenses.oneSidedAt line 23
  3. def OAI.SegmentLenses.oneSidedModulus line 26
  4. def OAI.SegmentLenses.AUC line 29
  5. theorem OAI.SegmentLenses.oneSidedOn_bddBelow line 32
  6. theorem OAI.SegmentLenses.oneSidedAt_bdd line 38
  7. theorem OAI.SegmentLenses.oneSidedAt_nonneg line 48
  8. theorem OAI.SegmentLenses.oneSidedModulus_nonneg line 64
  9. theorem OAI.SegmentLenses.cofinite_gain line 69
  10. def OAI.SegmentLenses.WeaklyNull line 87
  11. theorem OAI.SegmentLenses.WeaklyNull.map line 90
  12. theorem OAI.SegmentLenses.WeaklyNull.finiteDimensional line 95
  13. theorem OAI.SegmentLenses.WeaklyNull.cofinite_approx line 106
  14. theorem OAI.SegmentLenses.WeaklyNull.smul_bounded line 125
  15. theorem OAI.SegmentLenses.unit_approx_normalize line 137
  16. theorem OAI.SegmentLenses.WeaklyNull.cofinite_unit_approx line 155
  17. theorem OAI.SegmentLenses.ray_budget line 172
  18. theorem OAI.SegmentLenses.ray_strict_gain line 182
  19. theorem OAI.SegmentLenses.cofinite_child_growth line 191
  20. theorem OAI.SegmentLenses.bounded_finite_paths_modulus_zero line 240
  21. theorem OAI.SegmentLenses.euclidean_family_weakly_null line 291
  22. def OAI.SegmentLenses.UnitFinitePaths line 320
  23. theorem OAI.SegmentLenses.equivalent_paths_modulus_zero line 329
  24. theorem OAI.SegmentLenses.equivalent_paths_not_auc line 352
  25. theorem OAI.SegmentLenses.norm_segmentFunctional line 391
  26. def OAI.SegmentLenses.predualSegment line 408
  27. theorem OAI.SegmentLenses.norm_predualSegment line 411
  28. theorem OAI.SegmentLenses.fullDual_distinct_coordinates_weakly_null line 414
  29. theorem OAI.SegmentLenses.prefix_append_single_iff line 421
  30. def OAI.SegmentLenses.infinitePath line 449
  31. theorem OAI.SegmentLenses.infinitePath_isSegment line 451
  32. theorem OAI.SegmentLenses.norm_infinitePath line 460
  33. theorem OAI.SegmentLenses.infinitePath_child line 463
  34. theorem OAI.SegmentLenses.infinitePath_child_sub line 480
  35. theorem OAI.SegmentLenses.infinitePath_children_weakly_null line 487
  36. def OAI.SegmentLenses.forestRoot line 499
  37. def OAI.SegmentLenses.forestNode line 500
  38. theorem OAI.SegmentLenses.forest_iic_segment line 503
  39. def OAI.SegmentLenses.forestPath line 515
  40. theorem OAI.SegmentLenses.norm_forestPath line 518
  41. theorem OAI.SegmentLenses.forestPath_child line 524
  42. theorem OAI.SegmentLenses.forestPath_children_weakly_null line 553
  43. theorem OAI.SegmentLenses.infinite_unit_finite_paths line 569
  44. theorem OAI.SegmentLenses.forest_unit_finite_paths line 577
  45. theorem OAI.SegmentLenses.infinite_equivalent_modulus_zero line 590
  46. theorem OAI.SegmentLenses.forest_equivalent_modulus_zero line 601
  47. theorem OAI.SegmentLenses.infinite_no_equivalent_AUC line 611
  48. theorem OAI.SegmentLenses.forest_no_equivalent_AUC line 616