OAI/Geometry/BallPacking/Necessity/HolderCompletion.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform_holder_complexCurl line 31
2. lemma OAI.HigherDimensionalBallPacking.Rigidity.closedBall_subset_exterior line 53
3. lemma OAI.HigherDimensionalBallPacking.Rigidity.holomorphic_exterior_deriv_bound line 65
4. lemma OAI.HigherDimensionalBallPacking.Rigidity.holomorphic_exterior_secondDeriv_bound line 73
5. lemma OAI.HigherDimensionalBallPacking.Rigidity.real_fderiv_eq_complex_deriv line 82
6. lemma OAI.HigherDimensionalBallPacking.Rigidity.real_fderiv_norm_eq_deriv line 88
7. lemma OAI.HigherDimensionalBallPacking.Rigidity.real_fderiv_sub_norm_eq_deriv line 94
8. lemma OAI.HigherDimensionalBallPacking.Rigidity.holomorphic_exterior_fderiv_lipschitz_near line 107
9. theorem OAI.HigherDimensionalBallPacking.Rigidity.global_holder_fderiv_of_holomorphic_exterior line 128
10. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform_apply_swap line 181
11. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform_tendsto_zero line 186
12. lemma OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform_holder_holomorphic_off line 234
13. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform_holder_global line 244
14. lemma OAI.HigherDimensionalBallPacking.Rigidity.integrableKernel_smul_convolution_tendsto line 302
15. lemma OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform_tendsto_compact_data line 326
16. lemma OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform_add_compact line 349
17. lemma OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform_real_smul line 361
18. abbrev OAI.HigherDimensionalBallPacking.Rigidity.OffDiagonal line 371
19. def OAI.HigherDimensionalBallPacking.Rigidity.holderGraph line 375
20. instance OAI.HigherDimensionalBallPacking.Rigidity.holderGraph_isClosed line 391
21. abbrev OAI.HigherDimensionalBallPacking.Rigidity.HolderSpace line 402
22. instance OAI.HigherDimensionalBallPacking.Rigidity.holderSpace_complete line 404
23. def OAI.HigherDimensionalBallPacking.Rigidity.holderValue line 409
24. def OAI.HigherDimensionalBallPacking.Rigidity.holderDifference line 412
25. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderValue_apply line 415
26. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderDifference_apply line 418
27. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderSpace_relation line 421
28. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderValue_injective line 425
29. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderSpace_estimate line 440
30. def OAI.HigherDimensionalBallPacking.Rigidity.holderSpaceMk line 451
31. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderValue_mk line 476