OAI/Geometry/BallPacking/Energy/ResidualEnergy.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HigherDimensionalBallPacking.Rigidity.lineResidualEnergy line 18
2. lemma OAI.HigherDimensionalBallPacking.Rigidity.lineResidualEnergy_nonneg line 22
3. lemma OAI.HigherDimensionalBallPacking.Rigidity.lineResidualEnergy_continuous line 25
4. lemma OAI.HigherDimensionalBallPacking.Rigidity.lineResidualEnergy_compact line 30
5. lemma OAI.HigherDimensionalBallPacking.Rigidity.geometricResidual_at_CR line 37
6. lemma OAI.HigherDimensionalBallPacking.Rigidity.realCurve_dx line 45
7. lemma OAI.HigherDimensionalBallPacking.Rigidity.lineResidualEnergy_eq_defect line 50
8. lemma OAI.HigherDimensionalBallPacking.Rigidity.lineHomotopy_outside line 56
9. lemma OAI.HigherDimensionalBallPacking.Rigidity.residualEnergy_le_radialDensity line 62
10. theorem OAI.HigherDimensionalBallPacking.Rigidity.exact_line_homotopy_residual_energy_bound line 79
11. def OAI.HigherDimensionalBallPacking.Rigidity.sourceRadialCutoff line 114
12. lemma OAI.HigherDimensionalBallPacking.Rigidity.sourceRadialCutoff_smooth line 116
13. lemma OAI.HigherDimensionalBallPacking.Rigidity.sourceRadialCutoff_compact line 119
14. lemma OAI.HigherDimensionalBallPacking.Rigidity.sourceRadialCutoff_nonneg line 122
15. lemma OAI.HigherDimensionalBallPacking.Rigidity.sourceRadialCutoff_le_one line 125
16. lemma OAI.HigherDimensionalBallPacking.Rigidity.sourceRadialCutoff_eventually_one_on_compact line 130
17. lemma OAI.HigherDimensionalBallPacking.Rigidity.sourceRadialCutoff_tendsto line 136
18. lemma OAI.HigherDimensionalBallPacking.Rigidity.smooth_cutoff_integrable_mul line 142
19. lemma OAI.HigherDimensionalBallPacking.Rigidity.radial_curl_integral_between line 147
20. lemma OAI.HigherDimensionalBallPacking.Rigidity.radial_curl_integral_tendsto line 179
21. lemma OAI.HigherDimensionalBallPacking.Rigidity.compact_integral_cutoff_eventually line 210
22. lemma OAI.HigherDimensionalBallPacking.Rigidity.integrable_of_radial_exhaustion_limit line 220
23. def OAI.HigherDimensionalBallPacking.Rigidity.dirichletEnergy line 264
24. lemma OAI.HigherDimensionalBallPacking.Rigidity.dirichletEnergy_nonneg line 268
25. lemma OAI.HigherDimensionalBallPacking.Rigidity.dirichletEnergy_continuous line 271
26. lemma OAI.HigherDimensionalBallPacking.Rigidity.residual_energy_algebra line 278
27. lemma OAI.HigherDimensionalBallPacking.Rigidity.lineResidualEnergy_real line 285
28. lemma OAI.HigherDimensionalBallPacking.Rigidity.standard_primitive_curl line 292
29. lemma OAI.HigherDimensionalBallPacking.Rigidity.affineCorrection_residual line 302
30. lemma OAI.HigherDimensionalBallPacking.Rigidity.affineCorrection_residual_energy line 313
31. lemma OAI.HigherDimensionalBallPacking.Rigidity.affineCorrection_real_flux_zero line 318
32. theorem OAI.HigherDimensionalBallPacking.Rigidity.AffineLineCurve.affine_correction_energy line 332
33. lemma OAI.HigherDimensionalBallPacking.Rigidity.stdDot_sub_self line 370
34. lemma OAI.HigherDimensionalBallPacking.Rigidity.stdOmega_le_half_energy line 376
35. lemma OAI.HigherDimensionalBallPacking.Rigidity.interval_integral_stdDot_const line 384
36. lemma OAI.HigherDimensionalBallPacking.Rigidity.interval_stdDot_variance line 388
37. lemma OAI.HigherDimensionalBallPacking.Rigidity.interval_stdDot_integral_sq_le line 403
38. lemma OAI.HigherDimensionalBallPacking.Rigidity.curve_chord_energy_le line 424
39. theorem OAI.HigherDimensionalBallPacking.Rigidity.loop_symplectic_flux_le_energy line 441
40. def OAI.HigherDimensionalBallPacking.Rigidity.curveAreaDensity line 486
41. lemma OAI.HigherDimensionalBallPacking.Rigidity.curveAreaDensity_nonneg line 489
42. lemma OAI.HigherDimensionalBallPacking.Rigidity.dirichletEnergy_eq_residual_add_area line 498
43. lemma OAI.HigherDimensionalBallPacking.Rigidity.uniform_homotopy_pointwise_calibration line 506
44. theorem OAI.HigherDimensionalBallPacking.Rigidity.exact_line_homotopy_correction_energy_bound line 532