OAI/Analysis/SegmentLenses/Projections.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Primal projections and Euclidean coordinate bounds

  1. def OAI.SegmentLenses.primalHead line 20
  2. def OAI.SegmentLenses.primalTail line 23
  3. theorem OAI.SegmentLenses.primalHead_apply line 26
  4. theorem OAI.SegmentLenses.primalHead_test line 31
  5. theorem OAI.SegmentLenses.primalTail_test line 50
  6. theorem OAI.SegmentLenses.head_adjoint line 63
  7. theorem OAI.SegmentLenses.tail_adjoint line 71
  8. theorem OAI.SegmentLenses.coordinate_primalHead line 76
  9. theorem OAI.SegmentLenses.primalHead_fix line 80
  10. theorem OAI.SegmentLenses.norm_primalHead_le line 93
  11. theorem OAI.SegmentLenses.norm_primalTail_le line 102
  12. theorem OAI.SegmentLenses.singleton_square_sum_le line 118
  13. theorem OAI.SegmentLenses.norm_coordinate_sum_le line 128
  14. theorem OAI.SegmentLenses.norm_predualCoordinate_sum_le line 147
  15. theorem OAI.SegmentLenses.functional_coordinate_square_sum line 165
  16. theorem OAI.SegmentLenses.functional_coordinates_summable_sq line 179
  17. theorem OAI.SegmentLenses.distinct_coordinates_weakly_null line 185