OAI/Geometry/CylinderCovering/Beams/NeighborhoodFinite.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.BeamNeighborhoodRealization.base_covers_parallel line 13
2. lemma OAI.CylinderCovering.BeamNeighborhoodRealization.minus_intercept_identity line 31
3. lemma OAI.CylinderCovering.BeamNeighborhoodRealization.plus_intercept_identity line 41
4. lemma OAI.CylinderCovering.BeamNeighborhoodRealization.midpoint_tagged line 51
5. theorem OAI.CylinderCovering.BeamNeighborhoodRealization.cellBase_covers_minus line 58
6. theorem OAI.CylinderCovering.BeamNeighborhoodRealization.cellBase_covers_plus line 79
7. lemma OAI.CylinderCovering.BeamNeighborhoodRealization.step_le_one line 100
8. lemma OAI.CylinderCovering.BeamNeighborhoodRealization.cellBase_estimates line 105
9. lemma OAI.CylinderCovering.BeamNeighborhoodRealization.cost_bound line 137
10. lemma OAI.CylinderCovering.BeamNeighborhoodRealization.oneBeam_integral_eq line 148
11. lemma OAI.CylinderCovering.BeamNeighborhoodRealization.beamBaseMinus_eq line 160
12. lemma OAI.CylinderCovering.BeamNeighborhoodRealization.beamBasePlus_eq line 168
13. theorem OAI.CylinderCovering.BeamNeighborhoodRealization.alternativeStatement line 176