OAI/Analysis/SegmentLenses/Pairing.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Finite heads and the completion–dual pairing

  1. theorem OAI.SegmentLenses.subinterval_isSegment line 21
  2. theorem OAI.SegmentLenses.norm_filter_le line 49
  3. theorem OAI.SegmentLenses.norm_headTest_le line 77
  4. theorem OAI.SegmentLenses.norm_tailTest_le line 81
  5. theorem OAI.SegmentLenses.coordinate_apply_test line 90
  6. theorem OAI.SegmentLenses.coordinate_unitVector line 95
  7. theorem OAI.SegmentLenses.dual_norm_le line 102
  8. theorem OAI.SegmentLenses.test_as_sum line 111
  9. theorem OAI.SegmentLenses.dual_apply_test line 128
  10. theorem OAI.SegmentLenses.head_apply_test line 133
  11. def OAI.SegmentLenses.segmentFunctional line 138
  12. theorem OAI.SegmentLenses.segmentFunctional_apply line 140
  13. structure OAI.SegmentLenses.Representation line 145
  14. def OAI.SegmentLenses.Representation.value line 149
  15. def OAI.SegmentLenses.Representation.energy line 152
  16. theorem OAI.SegmentLenses.Representation.apply_test line 154
  17. theorem OAI.SegmentLenses.Representation.norm_le line 159
  18. theorem OAI.SegmentLenses.dual_ext_test line 181
  19. theorem OAI.SegmentLenses.head_unitVector line 188
  20. theorem OAI.SegmentLenses.head_head line 192
  21. theorem OAI.SegmentLenses.head_pairing line 200
  22. theorem OAI.SegmentLenses.tail_pairing line 220
  23. theorem OAI.SegmentLenses.norm_head_le line 237
  24. theorem OAI.SegmentLenses.norm_tail_le line 246
  25. def OAI.SegmentLenses.SegmentFamily.ofPieces line 261
  26. theorem OAI.SegmentLenses.SegmentFamily.ofPieces_sq line 276
  27. theorem OAI.SegmentLenses.clip_segment line 299
  28. theorem OAI.SegmentLenses.clip_disjoint line 310
  29. def OAI.SegmentLenses.SegmentFamily.clip line 320
  30. theorem OAI.SegmentLenses.SegmentFamily.clip_subset line 324
  31. theorem OAI.SegmentLenses.SegmentFamily.clip_seminorm line 330