OAI/Geometry/BallPacking/Necessity/FrozenInverse.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HigherDimensionalBallPacking.Rigidity.c1HolderMap line 50
  2. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1HolderMap_value line 59
  3. theorem OAI.HigherDimensionalBallPacking.Rigidity.inverseField_continuous line 63
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.inverseField_bound line 69
  5. theorem OAI.HigherDimensionalBallPacking.Rigidity.inverseField_sub line 82
  6. theorem OAI.HigherDimensionalBallPacking.Rigidity.inverseField_holder line 89
  7. def OAI.HigherDimensionalBallPacking.Rigidity.holderInverse line 105
  8. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderInverse_value line 117
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.frame_product_decay line 147
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.frame_product_inhomogeneous line 156
  11. theorem OAI.HigherDimensionalBallPacking.Rigidity.unmarked_density_equation line 170
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.framed_density_equation line 183
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.framed_frozen_solution line 211
  14. def OAI.HigherDimensionalBallPacking.Rigidity.frozenPrincipal line 237
  15. theorem OAI.HigherDimensionalBallPacking.Rigidity.frozenPrincipal_value line 249
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactHolderValue_injective line 260
  17. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1_potential_yields_frozen_density line 266
  18. def OAI.HigherDimensionalBallPacking.Rigidity.normalizedHolderFrame line 318
  19. theorem OAI.HigherDimensionalBallPacking.Rigidity.normalizedHolderFrame_value line 324
  20. theorem OAI.HigherDimensionalBallPacking.Rigidity.normalizedFrame_intertwines line 331
  21. theorem OAI.HigherDimensionalBallPacking.Rigidity.normalizedFrame_invertible line 340
  22. theorem OAI.HigherDimensionalBallPacking.Rigidity.normalizedFrame_standard line 351
  23. theorem OAI.HigherDimensionalBallPacking.Rigidity.constant_outside_fderiv line 360
  24. def OAI.HigherDimensionalBallPacking.Rigidity.holderComp line 368
  25. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderComp_value line 372
  26. def OAI.HigherDimensionalBallPacking.Rigidity.principalFrameLower line 376
  27. theorem OAI.HigherDimensionalBallPacking.Rigidity.principalFrameLower_value line 385
  28. theorem OAI.HigherDimensionalBallPacking.Rigidity.principalFrameLower_support line 397
  29. theorem OAI.HigherDimensionalBallPacking.Rigidity.principalFrameLower_equation line 430
  30. theorem OAI.HigherDimensionalBallPacking.Rigidity.normalizedHolderFrame_intertwines line 448
  31. theorem OAI.HigherDimensionalBallPacking.Rigidity.compatible_frozen_solution line 456
  32. theorem OAI.HigherDimensionalBallPacking.Rigidity.frozenPrincipal_injective line 480
  33. theorem OAI.HigherDimensionalBallPacking.Rigidity.frozenPrincipal_surjective line 502
  34. theorem OAI.HigherDimensionalBallPacking.Rigidity.frozenPrincipal_isInvertible line 518