OAI/Geometry/BallPacking/Energy/CircularEnergy.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HigherDimensionalBallPacking.Rigidity.circlePlane line 15
  2. def OAI.HigherDimensionalBallPacking.Rigidity.circleTrace line 17
  3. lemma OAI.HigherDimensionalBallPacking.Rigidity.circlePlane_smooth line 19
  4. lemma OAI.HigherDimensionalBallPacking.Rigidity.circleTrace_smooth line 23
  5. lemma OAI.HigherDimensionalBallPacking.Rigidity.circlePlane_hasDerivAt line 26
  6. lemma OAI.HigherDimensionalBallPacking.Rigidity.circleTrace_deriv line 32
  7. lemma OAI.HigherDimensionalBallPacking.Rigidity.circleTrace_closed line 37
  8. lemma OAI.HigherDimensionalBallPacking.Rigidity.plane_linear_energy_identity line 40
  9. lemma OAI.HigherDimensionalBallPacking.Rigidity.circleTrace_energy_le line 55
  10. lemma OAI.HigherDimensionalBallPacking.Rigidity.circle_pullback_flux_le line 68
  11. lemma OAI.HigherDimensionalBallPacking.Rigidity.integrable_polar_pullback line 101
  12. lemma OAI.HigherDimensionalBallPacking.Rigidity.integral_polar_slices line 113
  13. lemma OAI.HigherDimensionalBallPacking.Rigidity.integrable_polar_slices line 127
  14. def OAI.HigherDimensionalBallPacking.Rigidity.angularCurveFlux line 148
  15. lemma OAI.HigherDimensionalBallPacking.Rigidity.angularCurveFlux_continuous line 151
  16. lemma OAI.HigherDimensionalBallPacking.Rigidity.radiusSq_circlePlane line 156
  17. lemma OAI.HigherDimensionalBallPacking.Rigidity.integral_radial_angularFlux_le line 161
  18. lemma OAI.HigherDimensionalBallPacking.Rigidity.curveAreaDensity_continuous line 184
  19. lemma OAI.HigherDimensionalBallPacking.Rigidity.standard_primitive_curl_area line 190
  20. lemma OAI.HigherDimensionalBallPacking.Rigidity.radial_stokes_area_eq_flux line 195
  21. theorem OAI.HigherDimensionalBallPacking.Rigidity.calibrated_radial_energy_bound line 214
  22. lemma OAI.HigherDimensionalBallPacking.Rigidity.smoothTransition_deriv_zero_outside line 241
  23. lemma OAI.HigherDimensionalBallPacking.Rigidity.smoothTransition_deriv_le_bound line 253
  24. lemma OAI.HigherDimensionalBallPacking.Rigidity.outerProfile_deriv_zero_after line 264
  25. lemma OAI.HigherDimensionalBallPacking.Rigidity.outerProfile_weight_uniform_bound line 273
  26. lemma OAI.HigherDimensionalBallPacking.Rigidity.outerProfile_weight_tendsto_zero line 293
  27. lemma OAI.HigherDimensionalBallPacking.Rigidity.radial_boundary_integral_tendsto_zero line 301
  28. lemma OAI.HigherDimensionalBallPacking.Rigidity.radial_energy_integral_tendsto line 322
  29. lemma OAI.HigherDimensionalBallPacking.Rigidity.dirichletEnergy_zero_fderiv line 341
  30. theorem OAI.HigherDimensionalBallPacking.Rigidity.finite_energy_calibrated_curve_constant line 361
  31. theorem OAI.HigherDimensionalBallPacking.Rigidity.exact_homotopy_no_finite_energy_bubbles line 385
  32. lemma OAI.HigherDimensionalBallPacking.Rigidity.outerProfile_mono_parameter line 395
  33. lemma OAI.HigherDimensionalBallPacking.Rigidity.outerProfile_zero_after line 405
  34. lemma OAI.HigherDimensionalBallPacking.Rigidity.cutoff_weight_annulus_bound line 410
  35. def OAI.HigherDimensionalBallPacking.Rigidity.radialCurveEnergy line 433
  36. lemma OAI.HigherDimensionalBallPacking.Rigidity.radialCurveEnergy_nonneg line 436
  37. lemma OAI.HigherDimensionalBallPacking.Rigidity.radialCurveEnergy_mono line 439
  38. theorem OAI.HigherDimensionalBallPacking.Rigidity.calibrated_energy_hole_filling line 446
  39. lemma OAI.HigherDimensionalBallPacking.Rigidity.radialCurveEnergy_geometric_bound line 484
  40. theorem OAI.HigherDimensionalBallPacking.Rigidity.exact_homotopy_geometric_energy_decay line 500
  41. def OAI.HigherDimensionalBallPacking.Rigidity.centeredCurve line 514
  42. lemma OAI.HigherDimensionalBallPacking.Rigidity.centeredCurve_smooth line 516
  43. lemma OAI.HigherDimensionalBallPacking.Rigidity.realCurve_centered line 519
  44. lemma OAI.HigherDimensionalBallPacking.Rigidity.centeredCurve_fderiv line 524
  45. lemma OAI.HigherDimensionalBallPacking.Rigidity.dirichletEnergy_centered line 533
  46. lemma OAI.HigherDimensionalBallPacking.Rigidity.curveAreaDensity_centered line 537
  47. lemma OAI.HigherDimensionalBallPacking.Rigidity.stdDot_add_self_le line 541
  48. lemma OAI.HigherDimensionalBallPacking.Rigidity.stdDot_standardJ_self line 549
  49. lemma OAI.HigherDimensionalBallPacking.Rigidity.dirichletEnergy_add_le line 553
  50. lemma OAI.HigherDimensionalBallPacking.Rigidity.dirichletEnergy_linear line 564
  51. lemma OAI.HigherDimensionalBallPacking.Rigidity.dirichletEnergy_le_affineCorrection line 577
  52. lemma OAI.HigherDimensionalBallPacking.Rigidity.centered_unit_energy_bound line 590
  53. theorem OAI.HigherDimensionalBallPacking.Rigidity.AffineLineCurve.affine_correction_energy_of_slope line 620
  54. theorem OAI.HigherDimensionalBallPacking.Rigidity.exact_line_uniform_local_energy line 654