OAI/Geometry/BallPacking/Necessity/Properness.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HigherDimensionalBallPacking.Rigidity.projection_mean_double_bound line 38
  2. theorem OAI.HigherDimensionalBallPacking.Rigidity.projection_mean_grow_bound line 68
  3. theorem OAI.HigherDimensionalBallPacking.Rigidity.projection_error_point_bound line 87
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.affine_error_log_bound line 106
  5. theorem OAI.HigherDimensionalBallPacking.Rigidity.euclideanNorm_complex_smul line 154
  6. theorem OAI.HigherDimensionalBallPacking.Rigidity.euclideanNorm_neg line 164
  7. theorem OAI.HigherDimensionalBallPacking.Rigidity.affine_reverse_bound line 167
  8. theorem OAI.HigherDimensionalBallPacking.Rigidity.exists_linear_lt_dyadic line 176
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_uniform_properness line 193
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_slopes_bounded_above line 258
  11. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_uniform_asymptotic line 282
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_limit_has_nonzero_asymptotic line 336
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.lineMean_add_right line 405
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.squareMean_translate line 411
  15. theorem OAI.HigherDimensionalBallPacking.Rigidity.squareMean_eq_integral line 423
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.squareIntegral_translate line 431
  17. theorem OAI.HigherDimensionalBallPacking.Rigidity.fderiv_plane_translate line 440
  18. theorem OAI.HigherDimensionalBallPacking.Rigidity.planarDirichlet_translate line 447
  19. theorem OAI.HigherDimensionalBallPacking.Rigidity.squareEnergy_translate line 452
  20. theorem OAI.HigherDimensionalBallPacking.Rigidity.point_distance_le_energy_zero line 458
  21. theorem OAI.HigherDimensionalBallPacking.Rigidity.point_distance_le_energy line 484
  22. theorem OAI.HigherDimensionalBallPacking.Rigidity.affine_pair_oscillation_dyadic line 510
  23. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_uniform_modulus line 538
  24. theorem OAI.HigherDimensionalBallPacking.Rigidity.norm_le_euclideanNorm_constant line 576
  25. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_curves_uniformEquicontinuous line 585
  26. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_C0_compactness line 619
  27. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_uniform_holomorphic_exterior line 688
  28. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_C0_limit_analytic_at_infinity line 719
  29. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_C0_smooth_limit line 752
  30. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_affine_curve_compactness line 785