OAI/Analysis/SegmentLenses/Coordinates.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Coordinate identification and bounded multipliers

  1. theorem OAI.SegmentLenses.primal_small_tail line 23
  2. theorem OAI.SegmentLenses.primal_eq_zero_of_coordinates line 38
  3. theorem OAI.SegmentLenses.coordinateSpan_eq_top_of_reflexive line 50
  4. theorem OAI.SegmentLenses.fullDual_small_tail_of_reflexive line 76
  5. theorem OAI.SegmentLenses.predual_head_tendsto line 83
  6. theorem OAI.SegmentLenses.fullDual_head_tendsto_of_reflexive line 107
  7. theorem OAI.SegmentLenses.fullDual_all_radius_average_of_reflexive line 117
  8. theorem OAI.SegmentLenses.forest_coordinateSpan_eq_top line 139
  9. theorem OAI.SegmentLenses.forest_all_radius_average line 143
  10. theorem OAI.SegmentLenses.coordinateSpan_isSeparable line 151
  11. theorem OAI.SegmentLenses.fullDual_separable_of_coordinateSpan line 154
  12. instance OAI.SegmentLenses.(instance at line 161) line 161
  13. theorem OAI.SegmentLenses.forest_separable line 163