OAI/Geometry/BallPacking/Fredholm/NonlinearReduction.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HigherDimensionalBallPacking.Rigidity.fredholm_original_coords line 18
  2. def OAI.HigherDimensionalBallPacking.Rigidity.fredholmNonlinearCoords line 28
  3. def OAI.HigherDimensionalBallPacking.Rigidity.fredholmCoordEquiv line 31
  4. lemma OAI.HigherDimensionalBallPacking.Rigidity.fredholmNonlinearCoords_contDiff line 35
  5. lemma OAI.HigherDimensionalBallPacking.Rigidity.fredholmNonlinearCoords_hasFDerivAt line 39
  6. def OAI.HigherDimensionalBallPacking.Rigidity.fredholmCoordChart line 59
  7. lemma OAI.HigherDimensionalBallPacking.Rigidity.fredholmCoordChart_value line 63
  8. lemma OAI.HigherDimensionalBallPacking.Rigidity.fredholmCoordChart_base_mem line 66
  9. lemma OAI.HigherDimensionalBallPacking.Rigidity.fredholmCoordChart_inverse_smooth line 71
  10. def OAI.HigherDimensionalBallPacking.Rigidity.fredholmObstruction line 76
  11. def OAI.HigherDimensionalBallPacking.Rigidity.fredholmSolutionParam line 79
  12. lemma OAI.HigherDimensionalBallPacking.Rigidity.fredholmSolutionParam_base line 82
  13. lemma OAI.HigherDimensionalBallPacking.Rigidity.fredholmSolutionParam_smooth line 93
  14. lemma OAI.HigherDimensionalBallPacking.Rigidity.fredholmObstruction_smooth line 102
  15. lemma OAI.HigherDimensionalBallPacking.Rigidity.fredholmParam_zero_iff line 107
  16. lemma OAI.HigherDimensionalBallPacking.Rigidity.fredholm_zero_coord_iff line 122
  17. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.fredholmPackage_balanced line 157
  18. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.fredholmObstruction_smooth_zero line 164
  19. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualMarkedPackage line 195
  20. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualMarked_package_balanced line 198
  21. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualMarkedLocalChart line 203
  22. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualMarkedFiniteObstruction line 208
  23. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualMarkedLocalParam line 213
  24. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualMarkedLocalChart_base_mem line 218
  25. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualMarked_reduced_zero_iff line 222
  26. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualMarked_reduced_smooth line 229
  27. lemma OAI.HigherDimensionalBallPacking.Rigidity.indexZero_finite_stabilizer line 243
  28. lemma OAI.HigherDimensionalBallPacking.Rigidity.local_indexZero_supplement line 262
  29. theorem OAI.HigherDimensionalBallPacking.Rigidity.compact_indexZero_supplement line 275
  30. def OAI.HigherDimensionalBallPacking.Rigidity.pathSpatialDerivative line 295
  31. lemma OAI.HigherDimensionalBallPacking.Rigidity.pathSpatialDerivative_eq line 299
  32. lemma OAI.HigherDimensionalBallPacking.Rigidity.pathSpatialDerivative_continuous line 308
  33. def OAI.HigherDimensionalBallPacking.Rigidity.finiteTargetAugment line 312
  34. lemma OAI.HigherDimensionalBallPacking.Rigidity.finiteTargetAugment_smooth line 316
  35. lemma OAI.HigherDimensionalBallPacking.Rigidity.finiteTargetAugment_spatial_derivative line 322
  36. theorem OAI.HigherDimensionalBallPacking.Rigidity.ProperIndexZeroPath.finite_target_supplement line 337
  37. def OAI.HigherDimensionalBallPacking.Rigidity.parametricEssential line 360
  38. def OAI.HigherDimensionalBallPacking.Rigidity.parametricBase line 363
  39. lemma OAI.HigherDimensionalBallPacking.Rigidity.parametricEssential_smooth line 367
  40. lemma OAI.HigherDimensionalBallPacking.Rigidity.parametricEssential_vertical_derivative line 377
  41. lemma OAI.HigherDimensionalBallPacking.Rigidity.parametricEssential_invertible line 401
  42. def OAI.HigherDimensionalBallPacking.Rigidity.parametricInfiniteSolution line 413
  43. def OAI.HigherDimensionalBallPacking.Rigidity.parametricSolution line 417
  44. def OAI.HigherDimensionalBallPacking.Rigidity.parametricObstruction line 420
  45. lemma OAI.HigherDimensionalBallPacking.Rigidity.parametricInfiniteSolution_base line 423
  46. lemma OAI.HigherDimensionalBallPacking.Rigidity.parametricSolution_base line 428
  47. lemma OAI.HigherDimensionalBallPacking.Rigidity.parametricSolution_smooth line 432
  48. lemma OAI.HigherDimensionalBallPacking.Rigidity.parametricObstruction_smooth line 438
  49. lemma OAI.HigherDimensionalBallPacking.Rigidity.parametricSolution_zero_iff line 444
  50. lemma OAI.HigherDimensionalBallPacking.Rigidity.parametric_zero_is_solution line 464
  51. lemma OAI.HigherDimensionalBallPacking.Rigidity.finite_ker_augment line 492
  52. lemma OAI.HigherDimensionalBallPacking.Rigidity.augment_fredholm line 517