OAI/Geometry/BallPacking/Campanato/TranslatedSquare.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HigherDimensionalBallPacking.Rigidity.translatedSquare line 15
2. instance OAI.HigherDimensionalBallPacking.Rigidity.translatedSquare_finite line 18
3. lemma OAI.HigherDimensionalBallPacking.Rigidity.translatedSquare_mass line 22
4. lemma OAI.HigherDimensionalBallPacking.Rigidity.translatedSquare_integrable line 29
5. lemma OAI.HigherDimensionalBallPacking.Rigidity.translatedSquare_average line 36
6. lemma OAI.HigherDimensionalBallPacking.Rigidity.translatedSquare_le line 46
7. lemma OAI.HigherDimensionalBallPacking.Rigidity.translated_square_means_energy line 64
8. lemma OAI.HigherDimensionalBallPacking.Rigidity.correction_norm_triangle line 91
9. lemma OAI.HigherDimensionalBallPacking.Rigidity.square_dirichlet_le_total line 94
10. lemma OAI.HigherDimensionalBallPacking.Rigidity.centered_dirichlet_integrable line 100
11. lemma OAI.HigherDimensionalBallPacking.Rigidity.centered_dirichlet_integral line 108
12. def OAI.HigherDimensionalBallPacking.Rigidity.curveSquareAverage line 112
13. lemma OAI.HigherDimensionalBallPacking.Rigidity.curveSquareAverage_translated line 115
14. lemma OAI.HigherDimensionalBallPacking.Rigidity.curveSquareAverage_zero line 119
15. lemma OAI.HigherDimensionalBallPacking.Rigidity.growing_square_step line 126
16. lemma OAI.HigherDimensionalBallPacking.Rigidity.growing_square_telescope line 140
17. lemma OAI.HigherDimensionalBallPacking.Rigidity.neighboring_growing_means line 155
18. lemma OAI.HigherDimensionalBallPacking.Rigidity.correction_growth_by_scales line 178
19. lemma OAI.HigherDimensionalBallPacking.Rigidity.realProd_norm_le line 196
20. lemma OAI.HigherDimensionalBallPacking.Rigidity.translated_camp_mean_bound line 200
21. lemma OAI.HigherDimensionalBallPacking.Rigidity.centeredCurve_zero line 223
22. lemma OAI.HigherDimensionalBallPacking.Rigidity.centeredCurve_centered line 227
23. lemma OAI.HigherDimensionalBallPacking.Rigidity.campanato_oscillation_zero line 232
24. lemma OAI.HigherDimensionalBallPacking.Rigidity.campanato_oscillation line 272
25. lemma OAI.HigherDimensionalBallPacking.Rigidity.energy_uniform_modulus line 288
26. lemma OAI.HigherDimensionalBallPacking.Rigidity.energy_decay_uniformContinuous line 307
27. def OAI.HigherDimensionalBallPacking.Rigidity.dilatedCurve line 317
28. lemma OAI.HigherDimensionalBallPacking.Rigidity.dilatedCurve_smooth line 319
29. lemma OAI.HigherDimensionalBallPacking.Rigidity.dilatedCurve_fderiv line 322
30. lemma OAI.HigherDimensionalBallPacking.Rigidity.dilatedCurve_CR line 329
31. lemma OAI.HigherDimensionalBallPacking.Rigidity.dilatedCurve_slope line 340
32. lemma OAI.HigherDimensionalBallPacking.Rigidity.AffineLineCurve.dilate line 352
33. def OAI.HigherDimensionalBallPacking.Rigidity.slopeScale line 362
34. lemma OAI.HigherDimensionalBallPacking.Rigidity.slopeScale_pos line 364
35. lemma OAI.HigherDimensionalBallPacking.Rigidity.normalizedSlope_unit line 368
36. lemma OAI.HigherDimensionalBallPacking.Rigidity.exact_line_local_energy_of_slope line 376
37. lemma OAI.HigherDimensionalBallPacking.Rigidity.exact_normalized_line_energy line 395
38. lemma OAI.HigherDimensionalBallPacking.Rigidity.complex_norm_le_two_plane_norm line 425
39. lemma OAI.HigherDimensionalBallPacking.Rigidity.unit_slope_norm_le line 433
40. lemma OAI.HigherDimensionalBallPacking.Rigidity.correction_local_average line 438
41. lemma OAI.HigherDimensionalBallPacking.Rigidity.scale_growth_squared line 481
42. theorem OAI.HigherDimensionalBallPacking.Rigidity.exact_unit_line_correction_growth line 512
43. lemma OAI.HigherDimensionalBallPacking.Rigidity.stdDot_le_dimension_norm_sq line 551
44. lemma OAI.HigherDimensionalBallPacking.Rigidity.unit_slope_linear_norm line 559
45. lemma OAI.HigherDimensionalBallPacking.Rigidity.nonnegative_quadratic_bound line 567
46. lemma OAI.HigherDimensionalBallPacking.Rigidity.sublinear_correction_preimage_bound line 574
47. theorem OAI.HigherDimensionalBallPacking.Rigidity.exact_unit_line_source_escape line 596
48. lemma OAI.HigherDimensionalBallPacking.Rigidity.dilatedCurve_original_second_mark line 611
49. theorem OAI.HigherDimensionalBallPacking.Rigidity.exact_line_slope_lower_bound line 621
50. theorem OAI.HigherDimensionalBallPacking.Rigidity.exact_line_slope_upper_bound line 648
51. theorem OAI.HigherDimensionalBallPacking.Rigidity.exact_marked_line_slope_bounds line 671
52. lemma OAI.HigherDimensionalBallPacking.Rigidity.anchored_uniform_point_bound line 691
53. lemma OAI.HigherDimensionalBallPacking.Rigidity.energy_family_point_bound line 725