OAI/Geometry/BallPacking/Continuation/ParameterizedImplicit.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.initial_implicit_branch line 18
2. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.globalNonlinearity line 71
3. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.globalChart line 75
4. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.globalChart_contDiff line 80
5. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.globalChart_value line 91
6. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.globalChart_at_zero line 98
7. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.globalChart_actual_value line 112
8. theorem OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.fullCoefficientBound line 159
9. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.fullLineEquation line 171
10. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.fullLineEquation_contDiff line 173
11. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.fullLineEquation_initial line 176
12. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.fullLineEquation_value line 189
13. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.fullLineEquation_zero_iff line 203
14. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.spatial_derivative_translation line 245
15. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.fullTime_slice_outside line 279
16. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.fullLineEquation_local_chart_eq line 286
17. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.fullLineEquation_spatial_fredholm line 301
18. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.fullLineDomain line 327
19. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.fullLineDomain_open line 331
20. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.marked_pair_closedEmbedding line 334
21. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.isolatedFullLineZeros line 347
22. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.isolatedFullLineZeros_eq_preimage line 352
23. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.isolatedFullLineZeros_compact line 370
24. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.fullLineEquation_fredholm_on_domain line 377
25. structure OAI.HigherDimensionalBallPacking.Rigidity.ProperIndexZeroPath line 391
26. lemma OAI.HigherDimensionalBallPacking.Rigidity.markedCurve_zero_correction line 406
27. lemma OAI.HigherDimensionalBallPacking.Rigidity.exact_marked_initial line 412
28. lemma OAI.HigherDimensionalBallPacking.Rigidity.fullLineEndpointMap line 442
29. lemma OAI.HigherDimensionalBallPacking.Rigidity.fullLineProperPath line 455
30. def OAI.HigherDimensionalBallPacking.Rigidity.FullLineReady line 479
31. theorem OAI.HigherDimensionalBallPacking.Rigidity.full_line_continuation_data line 488
32. lemma OAI.HigherDimensionalBallPacking.Rigidity.adapted_structure_capacity_bound line 507
33. lemma OAI.HigherDimensionalBallPacking.Rigidity.adapted_line_continuation_data line 530