OAI/Geometry/BallPacking/Holder/MarkedJets.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.constJet line 22
2. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.constJet_value line 26
3. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.constJet_deriv line 28
4. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.constJet_norm_le line 31
5. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.constJetCLM line 36
6. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetEval line 43
7. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetEval_apply line 47
8. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.zeroNormalize line 49
9. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.zeroNormalize_value line 53
10. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.zeroNormalize_deriv line 56
11. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.standardJetCR line 61
12. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.standardJetCR_value line 66
13. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.standardJetCR_zeroNormalize line 72
14. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.complex_differentiable_of_curl_zero line 79
15. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.standardJetCR_injective_zeroMarked line 100
16. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.standardHolderInverse line 122
17. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.standardHolderInverse_value line 126
18. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.standardHolderInverse_zero line 132
19. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.standardHolderInverse_residual line 135
20. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compactSupport_fderiv_of_perturbation line 177
21. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.derivativeAssembly line 183
22. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.derivativeAssembly_value line 187
23. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.superposeDeriv_eq_assembly line 194
24. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.coefficient_eq_superpose line 197
25. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.superpose_eq_of_proofs line 203
26. theorem OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.superpose_contDiff_nat line 206
27. theorem OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.superpose_contDiff line 236
28. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetDirection line 257
29. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetDirection_value line 260
30. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.affine line 263
31. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.affine_hasFDerivAt line 265
32. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.affine_differentiable line 270
33. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.affine_fderiv_bound line 273
34. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.affineCurve line 276
35. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.affineCurve_hasFDerivAt line 279
36. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.affineCurve_fderiv line 283
37. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.structureAlong line 289
38. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.structureAlong_value line 292
39. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.structureAlongDeriv line 295
40. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.structureAlongDeriv_value line 299
41. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.structureAlong_hasFDerivAt line 304
42. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.crSection line 309
43. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.crSection_value line 314
44. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.crSectionDeriv line 321
45. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.crSection_hasFDerivAt line 329
46. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.crSectionDeriv_value line 351
47. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.crSection_eq_zero_iff line 360
48. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.crSection_contDiff line 376
49. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.complex_cr_iff line 388
50. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedModel line 414
51. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.mem_markedModel line 418
52. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedModel_closed line 422
53. instance OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.(instance at line 425) line 425
54. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedCR line 434
55. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedInverse line 437
56. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedCREquiv line 443
57. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedSlope line 456
58. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedCurve line 458
59. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedCurve_zero line 462
60. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedCurve_one line 466
61. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.complexSlope line 470
62. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.complexSlope_apply line 474
63. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedCurve_hasFDerivAt line 477
64. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedCurve_fderiv line 482
65. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedCurve_standardResidual line 487
66. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedSlope_continuous line 495
67. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedSlope_nonzero_open line 499
68. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedCurve_asymptote line 503