OAI/Geometry/BallPacking/Moduli/SmoothZeroCharts.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HigherDimensionalBallPacking.Rigidity.ZeroGraphChart.restrict line 20
2. lemma OAI.HigherDimensionalBallPacking.Rigidity.ZeroGraphChart.reparam_smooth line 40
3. lemma OAI.HigherDimensionalBallPacking.Rigidity.parametricSolution_smooth_neighborhood line 54
4. lemma OAI.HigherDimensionalBallPacking.Rigidity.surjective_smooth_zero_chart line 63
5. lemma OAI.HigherDimensionalBallPacking.Rigidity.smooth_common_zero_chart line 90
6. structure OAI.HigherDimensionalBallPacking.Rigidity.SmoothZeroAtlas line 110
7. def OAI.HigherDimensionalBallPacking.Rigidity.SmoothZeroAtlas.localChart line 120
8. lemma OAI.HigherDimensionalBallPacking.Rigidity.SmoothZeroAtlas.localChart_apply line 123
9. lemma OAI.HigherDimensionalBallPacking.Rigidity.SmoothZeroAtlas.localChart_target line 125
10. lemma OAI.HigherDimensionalBallPacking.Rigidity.SmoothZeroAtlas.localChart_symm_val line 128
11. def OAI.HigherDimensionalBallPacking.Rigidity.SmoothZeroAtlas.chartedSpace line 136
12. lemma OAI.HigherDimensionalBallPacking.Rigidity.SmoothZeroAtlas.transition_smooth line 148
13. lemma OAI.HigherDimensionalBallPacking.Rigidity.SmoothZeroAtlas.isManifold line 160
14. lemma OAI.HigherDimensionalBallPacking.Rigidity.timePreserving_linear_det line 175
15. lemma OAI.HigherDimensionalBallPacking.Rigidity.zeroChart_time_transition_det line 196
16. lemma OAI.HigherDimensionalBallPacking.Rigidity.StabilizedKernelFrame.smooth_zero_chart line 217
17. def OAI.HigherDimensionalBallPacking.Rigidity.framedZeroOpen line 242
18. def OAI.HigherDimensionalBallPacking.Rigidity.StabilizedKernelFrame.smoothZeroAtlas line 249
19. theorem OAI.HigherDimensionalBallPacking.Rigidity.ProperIndexZeroPath.smooth_stabilized_moduli line 261
20. lemma OAI.HigherDimensionalBallPacking.Rigidity.framedLocalChart_V line 288
21. lemma OAI.HigherDimensionalBallPacking.Rigidity.framedLocalChart_signed_transition line 296
22. lemma OAI.HigherDimensionalBallPacking.Rigidity.sign_eq_of_mul_pos line 320
23. lemma OAI.HigherDimensionalBallPacking.Rigidity.framedLocalChart_base_target line 326
24. def OAI.HigherDimensionalBallPacking.Rigidity.StabilizedKernelFrame.orientedZeroAtlas line 331
25. lemma OAI.HigherDimensionalBallPacking.Rigidity.orientedZeroAtlas_chart_apply line 382
26. lemma OAI.HigherDimensionalBallPacking.Rigidity.orientedZeroAtlas_symm_apply line 384
27. lemma OAI.HigherDimensionalBallPacking.Rigidity.orientedZeroAtlas_target line 386
28. def OAI.HigherDimensionalBallPacking.Rigidity.StabilizedKernelFrame.physicalProjection line 391
29. lemma OAI.HigherDimensionalBallPacking.Rigidity.FiniteZeroGerm.compact_zero_neighborhood line 411
30. lemma OAI.HigherDimensionalBallPacking.Rigidity.compact_zero_reservoir line 442
31. lemma OAI.HigherDimensionalBallPacking.Rigidity.compact_zero_isolating_neighborhood line 473
32. structure OAI.HigherDimensionalBallPacking.Rigidity.IsolatingStabilization line 487
33. lemma OAI.HigherDimensionalBallPacking.Rigidity.ProperIndexZeroPath.isolating_stabilization line 497
34. lemma OAI.HigherDimensionalBallPacking.Rigidity.IsolatingStabilization.small_target_boundary_avoid line 541
35. lemma OAI.HigherDimensionalBallPacking.Rigidity.IsolatingStabilization.small_target_endpoint_avoid line 567
36. lemma OAI.HigherDimensionalBallPacking.Rigidity.IsolatingStabilization.small_initial_graph line 590
37. theorem OAI.HigherDimensionalBallPacking.Rigidity.ProperIndexZeroPath.framed_isolating_stabilization line 620