OAI/Analysis/SegmentLenses/DualSums.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Duality and reflexivity for Hilbertian sums

  1. def OAI.SegmentLenses.Reflexive line 19
  2. abbrev OAI.SegmentLenses.L2Sum line 25
  3. def OAI.SegmentLenses.l2Restriction line 27
  4. theorem OAI.SegmentLenses.l2Restriction_apply line 30
  5. theorem OAI.SegmentLenses.l2_norm_sum_single_sq line 33
  6. theorem OAI.SegmentLenses.l2Restriction_square_sum line 41
  7. def OAI.SegmentLenses.l2DualRestrictions line 107
  8. def OAI.SegmentLenses.l2DualPair line 112
  9. theorem OAI.SegmentLenses.l2DualPair_apply line 116
  10. theorem OAI.SegmentLenses.l2DualPair_norm_le line 121
  11. theorem OAI.SegmentLenses.l2DualPair_single line 126
  12. theorem OAI.SegmentLenses.l2DualPair_restrictions line 135
  13. theorem OAI.SegmentLenses.l2DualRestrictions_pair line 144
  14. theorem OAI.SegmentLenses.l2DualPair_surjective line 152
  15. theorem OAI.SegmentLenses.l2DualRestrictions_norm_le line 155
  16. theorem OAI.SegmentLenses.l2DualPair_norm_map line 161
  17. def OAI.SegmentLenses.l2DualEquiv line 168
  18. theorem OAI.SegmentLenses.l2Sum_reflexive line 174
  19. theorem OAI.SegmentLenses.Reflexive.of_equiv line 209
  20. theorem OAI.SegmentLenses.Reflexive.dual line 224
  21. theorem OAI.SegmentLenses.hilbert_reflexive line 236