OAI/Geometry/BallPacking/Fredholm/FiniteExtensions.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HigherDimensionalBallPacking.Rigidity.fredholm_comp line 16
  2. lemma OAI.HigherDimensionalBallPacking.Rigidity.fredholm_snd_finite line 22
  3. lemma OAI.HigherDimensionalBallPacking.Rigidity.fredholm_add_finite line 34
  4. lemma OAI.HigherDimensionalBallPacking.Rigidity.fredholm_finite_extension line 42
  5. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeModel line 59
  6. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeModel_closed line 63
  7. instance OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.(instance at line 67) line 67
  8. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeCR line 78
  9. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedToFree line 81
  10. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeConst line 84
  11. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeNormalize line 91
  12. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeCoordinates line 101
  13. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeSum line 104
  14. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeSum_value line 109
  15. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeSum_deriv line 113
  16. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeEquiv line 118
  17. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.free_model_injective line 142
  18. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.affineJetValue line 173
  19. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.affineJetDeriv line 176
  20. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.affineJetValue_value line 181
  21. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.affineJetDeriv_value line 184
  22. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.affineJetSuperpose line 188
  23. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.affineJetSuperpose_value line 194
  24. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compactPerturbationJet line 197
  25. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compactPerturbationJet_value line 206
  26. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetZeroOrder line 225
  27. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetZeroOrder_value line 229
  28. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetZeroOrder_eq_localized line 234
  29. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetZeroOrder_isCompact line 247
  30. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedZeroOrder line 260
  31. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedZeroOrder_value line 270
  32. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedZeroOrder_isCompact line 274
  33. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactPerturbation_finite_kernel line 292
  34. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactPerturbation_antilipschitz line 323
  35. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactPerturbation_closed_range line 373
  36. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactPerturbation_strict line 409
  37. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactPerturbation_finite_cokernel line 425
  38. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactPerturbation_fredholm line 456
  39. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactPerturbation_filtration_stops line 473
  40. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactPerturbation_kernel_stabilizes line 512
  41. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactPerturbation_injective_of_surjective line 526