OAI/Geometry/BallPacking/Necessity/GradientLimits.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HigherDimensionalBallPacking.Rigidity.exists_nested_complex_cutoffs line 36
  2. theorem OAI.HigherDimensionalBallPacking.Rigidity.derivative_bound_of_holder_and_values line 92
  3. theorem OAI.HigherDimensionalBallPacking.Rigidity.norm_fderiv_tendsto_zero_of_holder line 122
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.exists_small_principal_const line 173
  5. theorem OAI.HigherDimensionalBallPacking.Rigidity.smallCR_sequence_derivative_zero line 192
  6. theorem OAI.HigherDimensionalBallPacking.Rigidity.locally_uniform_comp_uniform_constant line 280
  7. theorem OAI.HigherDimensionalBallPacking.Rigidity.continuousAt_comp_uniform_constant line 306
  8. theorem OAI.HigherDimensionalBallPacking.Rigidity.uniform_constant_prod line 321
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.affine_rescale_uniform_constant line 334
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.rescaled_maps_uniform_constant line 356
  11. def OAI.HigherDimensionalBallPacking.Rigidity.frameConjugation line 376
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.frameConjugation_apply line 380
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.frozenCoefficient_fderiv line 383
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.frozen_CR_no_gradient_loss line 388
  15. theorem OAI.HigherDimensionalBallPacking.Rigidity.lineHomotopy_contDiffAt line 468
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_CR_no_gradient_loss line 475
  17. def OAI.HigherDimensionalBallPacking.Rigidity.rescaleMap line 539
  18. theorem OAI.HigherDimensionalBallPacking.Rigidity.rescaleMap_smooth line 541
  19. theorem OAI.HigherDimensionalBallPacking.Rigidity.rescaleMap_fderiv line 546
  20. theorem OAI.HigherDimensionalBallPacking.Rigidity.rescaleMap_norm_fderiv line 561
  21. theorem OAI.HigherDimensionalBallPacking.Rigidity.weighted_rescale_bounds line 566
  22. theorem OAI.HigherDimensionalBallPacking.Rigidity.rescaleMap_CR line 591
  23. theorem OAI.HigherDimensionalBallPacking.Rigidity.weighted_gradient_maximum line 613
  24. theorem OAI.HigherDimensionalBallPacking.Rigidity.locally_uniform_reindex line 670
  25. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_C0_gradient_bound line 678