OAI/Geometry/PlaneColoring/CircleMaps.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.EuclideanFiveColor.RealPlane line 9
  2. def OAI.EuclideanFiveColor.circleSum line 10
  3. def OAI.EuclideanFiveColor.circleSumDeriv line 12
  4. lemma OAI.EuclideanFiveColor.circleSum_strict line 17
  5. lemma OAI.EuclideanFiveColor.circleSum_continuous line 27
  6. lemma OAI.EuclideanFiveColor.circleSumDeriv_injective line 29
  7. def OAI.EuclideanFiveColor.circleSumDerivEquiv line 45
  8. lemma OAI.EuclideanFiveColor.circleSum_local_antilipschitz line 51
  9. lemma OAI.EuclideanFiveColor.realDirection_lipschitz line 60
  10. def OAI.EuclideanFiveColor.circleInverseHomeo line 69
  11. def OAI.EuclideanFiveColor.circleInverse line 73
  12. lemma OAI.EuclideanFiveColor.circleInverse_measurable line 76
  13. lemma OAI.EuclideanFiveColor.circleInverse_eq line 80
  14. lemma OAI.EuclideanFiveColor.circleInverse_at line 82
  15. lemma OAI.EuclideanFiveColor.circleInverse_continuousAt line 88
  16. lemma OAI.EuclideanFiveColor.circleInverse_strict line 93
  17. lemma OAI.EuclideanFiveColor.circleInverse_right line 102
  18. lemma OAI.EuclideanFiveColor.circleInverse_regular line 106
  19. lemma OAI.EuclideanFiveColor.triangular_injective line 122
  20. lemma OAI.EuclideanFiveColor.triangular_surjective line 137
  21. lemma OAI.EuclideanFiveColor.strict_fiber_uniform_antilipschitz line 149

    Source documentation

    Joint strict differentiability and a nonzero fiber derivative give one inverse Lipschitz bound simultaneously for every nearby parameter.

    lemma strict_fiber_uniform_antilipschitz {S : E × ℝ → ℝ} {L : E × ℝ →L[ℝ] ℝ}
    {p : E} {t : ℝ} (hS : HasStrictFDerivAt S L (p,t)) (hc : L (0,1) ≠ 0) :
    ∃ P : Set E, ∃ I : Set ℝ, IsOpen P ∧ p ∈ P ∧ IsOpen I ∧ t ∈ I ∧
      ∃ K : ℝ≥0, ∀ q ∈ P, AntilipschitzWith K (I.domRestrict (fun u => S (q,u))) := by
…
  22. abbrev OAI.EuclideanFiveColor.CircleParameter line 181
  23. abbrev OAI.EuclideanFiveColor.CircleJet line 182
  24. def OAI.EuclideanFiveColor.jetCenter line 183
  25. def OAI.EuclideanFiveColor.jetRadius line 185
  26. def OAI.EuclideanFiveColor.jetAngle line 187
  27. def OAI.EuclideanFiveColor.circleTarget line 188
  28. def OAI.EuclideanFiveColor.circleTargetDeriv line 189
  29. lemma OAI.EuclideanFiveColor.circleTarget_strict line 192
  30. lemma OAI.EuclideanFiveColor.circleTarget_continuous line 196
  31. def OAI.EuclideanFiveColor.circleEndpoint line 199
  32. def OAI.EuclideanFiveColor.circleEndpointDeriv line 200
  33. lemma OAI.EuclideanFiveColor.circleEndpoint_measurable line 204
  34. lemma OAI.EuclideanFiveColor.circleEndpoint_strict line 206
  35. lemma OAI.EuclideanFiveColor.inverse_tangent_first_ne line 211
  36. lemma OAI.EuclideanFiveColor.circleEndpoint_fiber_ne line 227
  37. lemma OAI.EuclideanFiveColor.circleEndpoint_uniform line 235
  38. lemma OAI.EuclideanFiveColor.circleEndpoint_good_neighborhood line 248
  39. def OAI.EuclideanFiveColor.angleChart line 297
  40. def OAI.EuclideanFiveColor.angleChartMeasure line 298
  41. lemma OAI.EuclideanFiveColor.angleChartMeas_le line 300
  42. instance OAI.EuclideanFiveColor.(instance at line 301) line 301
  43. lemma OAI.EuclideanFiveColor.angleChart_preserving line 307
  44. lemma OAI.EuclideanFiveColor.angleChart_measure line 314
  45. lemma OAI.EuclideanFiveColor.integral_angular_eq_chart line 319
  46. lemma OAI.EuclideanFiveColor.direction_realPlane line 327
  47. lemma OAI.EuclideanFiveColor.circleSum_chart line 331
  48. lemma OAI.EuclideanFiveColor.volume_preimage_bound line 346
  49. lemma OAI.EuclideanFiveColor.map_restrict_volume_le line 360
  50. lemma OAI.EuclideanFiveColor.antilipschitz_small_perturbation line 373
  51. lemma OAI.EuclideanFiveColor.realDirection_norm_le line 396
  52. lemma OAI.EuclideanFiveColor.circleSum_decompose line 400
  53. lemma OAI.EuclideanFiveColor.circleSum_norm_le line 402
  54. lemma OAI.EuclideanFiveColor.circleSum_perturb_identity line 408
  55. lemma OAI.EuclideanFiveColor.circleSum_parameter_tendsto line 415
  56. lemma OAI.EuclideanFiveColor.circleSum_eventual_image line 419
  57. lemma OAI.EuclideanFiveColor.circleSum_limit_image line 436
  58. lemma OAI.EuclideanFiveColor.circleSum_eventual_antilipschitz line 441
  59. lemma OAI.EuclideanFiveColor.circleSum_limit_antilipschitz line 459
  60. lemma OAI.EuclideanFiveColor.measure_null_of_locally_null_on_conull line 473
  61. lemma OAI.EuclideanFiveColor.circleSum_regular_ae line 488
  62. lemma OAI.EuclideanFiveColor.circleSum_preimage_null line 499
  63. lemma OAI.EuclideanFiveColor.circleSum_quasiMeasurePreserving line 509