OAI/Analysis/SegmentLenses/Subtrees.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Subtree projections and exact weighted radii

  1. theorem OAI.SegmentLenses.SegmentEmbedding.primal_range_coordinateClosure line 25
  2. def OAI.SegmentLenses.SegmentEmbedding.primalProjection line 50
  3. theorem OAI.SegmentLenses.SegmentEmbedding.primalProjection_apply line 53
  4. theorem OAI.SegmentLenses.SegmentEmbedding.norm_primalProjection_le line 56
  5. theorem OAI.SegmentLenses.SegmentEmbedding.primalProjection_idempotent line 61
  6. theorem OAI.SegmentLenses.SegmentEmbedding.primalProjection_unitVector line 65
  7. theorem OAI.SegmentLenses.SegmentEmbedding.primalProjection_unitVector_outside line 69
  8. def OAI.SegmentLenses.SegmentEmbedding.dualRestriction line 81
  9. def OAI.SegmentLenses.SegmentEmbedding.dualProjection line 86
  10. theorem OAI.SegmentLenses.SegmentEmbedding.norm_dualProjection_le line 89
  11. theorem OAI.SegmentLenses.SegmentEmbedding.norm_dualRestriction_eq line 98
  12. theorem OAI.SegmentLenses.SegmentEmbedding.dualProjection_coordinate line 114
  13. theorem OAI.SegmentLenses.SegmentEmbedding.dualProjection_coordinate_outside line 119
  14. theorem OAI.SegmentLenses.weighted_stability line 134
  15. theorem OAI.SegmentLenses.safety_radius_le line 156
  16. theorem OAI.SegmentLenses.infinite_obstruction_radii line 165
  17. theorem OAI.SegmentLenses.forest_obstruction_radii line 176
  18. theorem OAI.SegmentLenses.IndexedForest.unbounded_obstruction_radii line 191