OAI/Geometry/BallPacking/Compactness/ResidualCauchy.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HigherDimensionalBallPacking.Rigidity.geometricHolder line 17
  2. lemma OAI.HigherDimensionalBallPacking.Rigidity.geometricHolder_value line 21
  3. lemma OAI.HigherDimensionalBallPacking.Rigidity.affineSource_distance line 25
  4. lemma OAI.HigherDimensionalBallPacking.Rigidity.residual_difference_pullback line 31
  5. lemma OAI.HigherDimensionalBallPacking.Rigidity.local_residual_small_differences line 40
  6. lemma OAI.HigherDimensionalBallPacking.Rigidity.geometric_residual_cauchy line 84
  7. lemma OAI.HigherDimensionalBallPacking.Rigidity.compact_structure_norm_standard line 108
  8. lemma OAI.HigherDimensionalBallPacking.Rigidity.marked_value_continuous line 115
  9. lemma OAI.HigherDimensionalBallPacking.Rigidity.cDeriv_eval_continuous line 119
  10. lemma OAI.HigherDimensionalBallPacking.Rigidity.marked_derivative_eval_continuous line 126
  11. lemma OAI.HigherDimensionalBallPacking.Rigidity.represented_line_slope_nonzero line 131
  12. lemma OAI.HigherDimensionalBallPacking.Rigidity.completed_line_cr_closed line 138
  13. lemma OAI.HigherDimensionalBallPacking.Rigidity.completed_line_slope_limit_nonzero line 160
  14. lemma OAI.HigherDimensionalBallPacking.Rigidity.completed_line_closed line 180
  15. lemma OAI.HigherDimensionalBallPacking.Rigidity.represented_line_by_inverse line 217
  16. lemma OAI.HigherDimensionalBallPacking.Rigidity.subtype_cauchySeq_of_val line 226
  17. theorem OAI.HigherDimensionalBallPacking.Rigidity.exact_marked_completed_convergence line 231
  18. theorem OAI.HigherDimensionalBallPacking.Rigidity.exact_marked_completed_compactness line 279
  19. lemma OAI.HigherDimensionalBallPacking.Rigidity.markedCurve_injective line 303
  20. def OAI.HigherDimensionalBallPacking.Rigidity.exactMarkedZeroSet line 316
  21. lemma OAI.HigherDimensionalBallPacking.Rigidity.correction_limit_zero line 320
  22. theorem OAI.HigherDimensionalBallPacking.Rigidity.exact_marked_zeroSet_compact line 327
  23. theorem OAI.HigherDimensionalBallPacking.Rigidity.exact_marked_existence_parameters_closed line 348