OAI/Geometry/BallPacking/Rigidity/CorrectedInfinity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialPrimitiveCLM_eq_moment line 14
  2. theorem OAI.HigherDimensionalBallPacking.Rigidity.capacity_tendsto_atTop line 23
  3. theorem OAI.HigherDimensionalBallPacking.Rigidity.AffineLineCurve.radial_infinity_limit line 31
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.correctedPrimitive_eq_radial_at_infinity line 64
  5. theorem OAI.HigherDimensionalBallPacking.Rigidity.AffineLineCurve.corrected_infinity_limit line 75
  6. theorem OAI.HigherDimensionalBallPacking.Rigidity.AffineLineCurve.finite_real_centre_fibre line 101
  7. theorem OAI.HigherDimensionalBallPacking.Rigidity.two_ball_line_area line 109
  8. theorem OAI.HigherDimensionalBallPacking.Rigidity.two_ball_capacity_of_adapted_line line 221
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.packing_two_line_reduction line 261