OAI/Geometry/BallPacking/Necessity/FiniteReduction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HigherDimensionalBallPacking.Rigidity.compactHolderMul line 46
2. lemma OAI.HigherDimensionalBallPacking.Rigidity.compactHolderMul_value line 55
3. lemma OAI.HigherDimensionalBallPacking.Rigidity.frameInverse_smooth line 60
4. lemma OAI.HigherDimensionalBallPacking.Rigidity.frameInverse_compact_difference line 71
5. def OAI.HigherDimensionalBallPacking.Rigidity.inverseFrameHolder line 93
6. lemma OAI.HigherDimensionalBallPacking.Rigidity.inverseFrameHolder_value line 104
7. theorem OAI.HigherDimensionalBallPacking.Rigidity.exists_normalized_nonlinear_chart line 133
8. theorem OAI.HigherDimensionalBallPacking.Rigidity.AffineLineCurve.exists_holder_profile line 239
9. theorem OAI.HigherDimensionalBallPacking.Rigidity.AffineLineCurve.exists_nonlinear_fredholm_section line 311
10. theorem OAI.HigherDimensionalBallPacking.Rigidity.local_section_zero_iff line 343
11. theorem OAI.HigherDimensionalBallPacking.Rigidity.fredholm_local_finite_reduction line 386
12. theorem OAI.HigherDimensionalBallPacking.Rigidity.AffineLineCurve.exists_finite_reduction line 492
13. theorem OAI.HigherDimensionalBallPacking.Rigidity.normalized_section_package_finrank line 550