OAI/Geometry/BallPacking/Compactness/GradientBounds.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetDirectional line 22
2. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetDirectional_value line 26
3. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.holderCoefficientAction_norm_le line 30
4. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compact_zeroMarked_schauder line 35
5. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.scalar_absorption line 45
6. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.small_coefficient_schauder line 57
7. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.standardJetCR_sub_explicit line 104
8. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.clm_principal_sub_algebra line 118
9. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.principal_difference_identity line 124
10. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.holderCoefficientAction_jet_norm_le line 141
11. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.zeroMarked_sub line 150
12. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jet_residual_sub_supported line 156
13. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.small_coefficient_difference_estimate line 162
14. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cauchySeq_of_pair_distance_bound line 185
15. theorem OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.small_coefficient_cauchy line 205
16. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoffCurveJet line 246
17. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoffCurveJet_value line 250
18. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoffCurveJet_deriv line 253
19. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoffCurveJet_zero line 263
20. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoffCurveJet_supported line 267
21. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoffCurveJet_CR line 282
22. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.small_value_elliptic_estimate line 307
23. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.ofBoundedLipschitz line 335
24. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.ofBoundedLipschitz_value line 343
25. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.clm_pair_difference line 348
26. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.clm_pair_bounds line 354
27. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoff_forcing_bounds line 373
28. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoffTransport line 414
29. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoffCommute line 417
30. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoffTransport_apply line 421
31. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoffCommute_apply line 423
32. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoffTransport_smooth line 427
33. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoffTransport_compact line 431
34. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoffCommute_smooth line 435
35. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoffCommute_compact line 439
36. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoff_transport_bounds line 449
37. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.holder_cauchy_of_uniform_values line 474
38. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.uniform_cauchy_of_tendstoUniformly line 498
39. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.holder_cauchy_of_tendstoUniformly line 512