OAI/Analysis/SegmentLenses/Completed.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Completed midpoint bounds and coordinate density

  1. instance OAI.SegmentLenses.infiniteLocallyFiniteBot line 18
  2. instance OAI.SegmentLenses.forestLocallyFiniteBot line 23
  3. def OAI.SegmentLenses.ancestralHull line 43
  4. theorem OAI.SegmentLenses.subset_ancestralHull line 45
  5. theorem OAI.SegmentLenses.ancestralHull_ancestral line 49
  6. theorem OAI.SegmentLenses.head_pairing_of_support line 59
  7. theorem OAI.SegmentLenses.tail_head_pairing line 71
  8. theorem OAI.SegmentLenses.completed_main_tail line 87
  9. theorem OAI.SegmentLenses.forest_main_tail line 119
  10. theorem OAI.SegmentLenses.infinite_main_tail line 129
  11. theorem OAI.SegmentLenses.norm_test_unit line 140
  12. theorem OAI.SegmentLenses.norm_unitVector line 153
  13. theorem OAI.SegmentLenses.norm_coordinate line 156
  14. theorem OAI.SegmentLenses.coordinate_mem_span line 165
  15. theorem OAI.SegmentLenses.coordinate_mem line 171
  16. theorem OAI.SegmentLenses.head_mem_span line 174
  17. theorem OAI.SegmentLenses.head_mem line 180
  18. def OAI.SegmentLenses.predualCoordinate line 184
  19. theorem OAI.SegmentLenses.norm_predualCoordinate line 186
  20. theorem OAI.SegmentLenses.span_finitely_supported line 189
  21. theorem OAI.SegmentLenses.predual_finite_approx line 222
  22. theorem OAI.SegmentLenses.predual_small_tail line 235
  23. def OAI.SegmentLenses.predualHead line 250
  24. def OAI.SegmentLenses.predualTail line 261
  25. theorem OAI.SegmentLenses.predualHead_coe line 272
  26. theorem OAI.SegmentLenses.predualTail_coe line 277
  27. theorem OAI.SegmentLenses.norm_predualHead_le line 282
  28. theorem OAI.SegmentLenses.norm_predualTail_le line 287