OAI/Geometry/Cannon/CirclePacking/AngleGradient.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

The variational angle functional for a conformal circle packing.

  1. def OAI.CannonPackingGeometry.angleGradient line 16
  2. def OAI.CannonPackingGeometry.angleEntropy line 18
  3. lemma OAI.CannonPackingGeometry.angleEntropy_continuous line 22
  4. lemma OAI.CannonPackingGeometry.half_trig_pos line 29
  5. lemma OAI.CannonPackingGeometry.angleGradient_continuousAt line 35
  6. lemma OAI.CannonPackingGeometry.angleEntropy_hasDerivAt line 47
  7. lemma OAI.CannonPackingGeometry.angleGradient_zero_limit line 66
  8. lemma OAI.CannonPackingGeometry.angleGradient_pi_sub line 85
  9. lemma OAI.CannonPackingGeometry.angleGradient_pi_limit line 91
  10. def OAI.CannonPackingGeometry.angleMove line 110
  11. lemma OAI.CannonPackingGeometry.angleMove_interior line 112
  12. lemma OAI.CannonPackingGeometry.angleMove_hasDerivAt line 125
  13. def OAI.CannonPackingGeometry.segmentGradient line 129
  14. lemma OAI.CannonPackingGeometry.segmentGradient_boundary line 131
  15. lemma OAI.CannonPackingGeometry.segmentGradient_bounded_above line 154
  16. lemma OAI.CannonPackingGeometry.sum_tendsto_atBot_of_one line 171
  17. lemma OAI.CannonPackingGeometry.entropy_segment_hasDerivAt line 184
  18. theorem OAI.CannonPackingGeometry.entropy_boundary_descent line 196
  19. def OAI.CannonPackingGeometry.angleSum line 236
  20. def OAI.CannonPackingGeometry.angleFeasible line 238
  21. lemma OAI.CannonPackingGeometry.angleSum_continuous line 241
  22. lemma OAI.CannonPackingGeometry.angleFeasible_compact line 247
  23. theorem OAI.CannonPackingGeometry.exists_interior_angle_minimizer line 260
  24. lemma OAI.CannonPackingGeometry.angleSum_line_derivative line 283
  25. lemma OAI.CannonPackingGeometry.angle_minimizer_stationary line 295
  26. theorem OAI.CannonPackingGeometry.exists_angle_multipliers line 326
  27. def OAI.CannonPackingGeometry.faceCornerSum line 359
  28. def OAI.CannonPackingGeometry.vertexCornerSum line 362
  29. def OAI.CannonPackingGeometry.cornerConstraint line 365
  30. lemma OAI.CannonPackingGeometry.vertexCornerSum_apply line 370
  31. lemma OAI.CannonPackingGeometry.faceCornerSum_single line 379
  32. lemma OAI.CannonPackingGeometry.vertexCornerSum_single line 390
  33. lemma OAI.CannonPackingGeometry.exp_angleGradient line 405
  34. theorem OAI.CannonPackingGeometry.coherent_angles_give_radii line 411
  35. def OAI.CannonPackingGeometry.neighborFaces line 458
  36. theorem OAI.CannonPackingGeometry.weighted_hall_equiv line 462
  37. theorem OAI.CannonPackingGeometry.integer_transport line 503
  38. theorem OAI.CannonPackingGeometry.positive_transport line 569