OAI/Geometry/BallPacking/Campanato/MeasureEnergy.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HigherDimensionalBallPacking.Rigidity.integral_stdDot_variance line 15
2. lemma OAI.HigherDimensionalBallPacking.Rigidity.stdDot_integral_sq_le line 30
3. lemma OAI.HigherDimensionalBallPacking.Rigidity.stdDot_average_sq_le line 49
4. lemma OAI.HigherDimensionalBallPacking.Rigidity.norm_sq_le_stdDot line 61
5. def OAI.HigherDimensionalBallPacking.Rigidity.phaseAverage line 81
6. lemma OAI.HigherDimensionalBallPacking.Rigidity.integrable_stdDot_const_sub line 84
7. lemma OAI.HigherDimensionalBallPacking.Rigidity.phaseAverage_const_sub line 94
8. lemma OAI.HigherDimensionalBallPacking.Rigidity.phaseAverage_deviation_energy_le line 100
9. lemma OAI.HigherDimensionalBallPacking.Rigidity.stdDot_sub_self_le line 117
10. lemma OAI.HigherDimensionalBallPacking.Rigidity.curve_pair_energy_le line 121
11. lemma OAI.HigherDimensionalBallPacking.Rigidity.horizontal_curve_deriv line 131
12. lemma OAI.HigherDimensionalBallPacking.Rigidity.vertical_curve_deriv line 138
13. def OAI.HigherDimensionalBallPacking.Rigidity.horizontalEnergy line 145
14. def OAI.HigherDimensionalBallPacking.Rigidity.verticalEnergy line 148
15. lemma OAI.HigherDimensionalBallPacking.Rigidity.horizontalEnergy_continuous line 151
16. lemma OAI.HigherDimensionalBallPacking.Rigidity.verticalEnergy_continuous line 156
17. lemma OAI.HigherDimensionalBallPacking.Rigidity.rectangle_pair_energy_bound line 161
18. def OAI.HigherDimensionalBallPacking.Rigidity.squareMeasure line 181
19. lemma OAI.HigherDimensionalBallPacking.Rigidity.squareMeasure_eq line 184
20. instance OAI.HigherDimensionalBallPacking.Rigidity.squareMeasure_finite line 188
21. lemma OAI.HigherDimensionalBallPacking.Rigidity.squareMeasure_mass line 192
22. lemma OAI.HigherDimensionalBallPacking.Rigidity.intervalMeasure_mass line 198
23. lemma OAI.HigherDimensionalBallPacking.Rigidity.continuous_square_integrable line 202
24. lemma OAI.HigherDimensionalBallPacking.Rigidity.square_ae_mem line 207
25. lemma OAI.HigherDimensionalBallPacking.Rigidity.square_integral line 211
26. lemma OAI.HigherDimensionalBallPacking.Rigidity.square_integral_swap line 216
27. lemma OAI.HigherDimensionalBallPacking.Rigidity.integral_Icc_eq_interval line 221
28. def OAI.HigherDimensionalBallPacking.Rigidity.horizontalSlice line 227
29. def OAI.HigherDimensionalBallPacking.Rigidity.verticalSlice line 229
30. lemma OAI.HigherDimensionalBallPacking.Rigidity.horizontalSlice_integrable line 232
31. lemma OAI.HigherDimensionalBallPacking.Rigidity.verticalSlice_integrable line 236
32. lemma OAI.HigherDimensionalBallPacking.Rigidity.square_point_deviation_bound line 240
33. lemma OAI.HigherDimensionalBallPacking.Rigidity.square_poincare line 280
34. lemma OAI.HigherDimensionalBallPacking.Rigidity.stdDot_sub_swap line 311
35. lemma OAI.HigherDimensionalBallPacking.Rigidity.square_energy_mono line 316
36. lemma OAI.HigherDimensionalBallPacking.Rigidity.square_means_energy line 325
37. lemma OAI.HigherDimensionalBallPacking.Rigidity.quarter_square_mean_norm line 349
38. lemma OAI.HigherDimensionalBallPacking.Rigidity.square_dirichlet_le_radial line 361
39. lemma OAI.HigherDimensionalBallPacking.Rigidity.phaseAverage_norm_le line 384
40. lemma OAI.HigherDimensionalBallPacking.Rigidity.plane_norm_le_square line 392
41. lemma OAI.HigherDimensionalBallPacking.Rigidity.squareAverage_tendsto line 396
42. def OAI.HigherDimensionalBallPacking.Rigidity.campRadius line 420
43. lemma OAI.HigherDimensionalBallPacking.Rigidity.campRadius_pos line 422
44. lemma OAI.HigherDimensionalBallPacking.Rigidity.campRadius_succ line 424
45. lemma OAI.HigherDimensionalBallPacking.Rigidity.campRadius_sq line 429
46. lemma OAI.HigherDimensionalBallPacking.Rigidity.campRadius_tendsto line 438
47. lemma OAI.HigherDimensionalBallPacking.Rigidity.geometric_sqrt_norm_bound line 443
48. lemma OAI.HigherDimensionalBallPacking.Rigidity.campanato_point_mean line 451