OAI/Combinatorics/ProgressionColoring/AdaptiveMesh.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuantitativeVanDerWaerden.rho line 13

    Source documentation

    Distance to the cut, expressed using the centered representative.

    noncomputable def rho (x : ℝ) : ℝ := 1 / 2 - |centered x|

    Mentions: OAI.QuantitativeVanDerWaerden.centered

  2. theorem OAI.QuantitativeVanDerWaerden.rho_nonneg line 15
  3. theorem OAI.QuantitativeVanDerWaerden.rho_le_half line 21
  4. theorem OAI.QuantitativeVanDerWaerden.rho_add_int line 25
  5. structure OAI.QuantitativeVanDerWaerden.AdaptiveMesh line 28
  6. def OAI.QuantitativeVanDerWaerden.AdaptiveMesh.R line 40
  7. def OAI.QuantitativeVanDerWaerden.AdaptiveMesh.m line 41
  8. def OAI.QuantitativeVanDerWaerden.AdaptiveMesh.theta line 42
  9. def OAI.QuantitativeVanDerWaerden.AdaptiveMesh.endpoint line 43
  10. def OAI.QuantitativeVanDerWaerden.AdaptiveMesh.radialWidth line 45
  11. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.argument_ge_three line 47
  12. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.one_le_R line 53
  13. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.R_pos line 60
  14. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.m_pos line 62
  15. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.m_cast_pos line 65
  16. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.theta_pos line 67
  17. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.theta_le_H line 69
  18. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.half_H_le_theta line 74
  19. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.theta_le_eighth line 86
  20. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.exp_theta_le_two line 88
  21. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.exp_theta_sub_one_le line 95
  22. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.theta_le_exp_theta_sub_one line 103
  23. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.endpoint_zero line 106
  24. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.endpoint_strictMono line 108
  25. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.endpoint_m line 116
  26. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.radialWidth_pos line 128
  27. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.radialWidth_eq line 131
  28. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.radial_width_bounds line 140

    Source documentation

    The width estimate holds on the closed radial interval; this includes the circle cut and zero once the two halves are realized as intervals.

    theorem radial_width_bounds (j : ℕ) (r : ℝ)
    (hl : A.endpoint j ≤ r) (hu : r ≤ A.endpoint (j + 1)) :
    A.H / 4 * (r + A.alpha) ≤ A.radialWidth j ∧
      A.radialWidth j ≤ 2 * A.H * (r + A.alpha) := by
…
  29. abbrev OAI.QuantitativeVanDerWaerden.AdaptiveMesh.Label line 178

    Source documentation

    false denotes the negative half and true the positive half.

    abbrev Label := Bool × Fin A.m
  30. def OAI.QuantitativeVanDerWaerden.AdaptiveMesh.left line 180
  31. def OAI.QuantitativeVanDerWaerden.AdaptiveMesh.right line 183
  32. def OAI.QuantitativeVanDerWaerden.AdaptiveMesh.Contains line 186
  33. def OAI.QuantitativeVanDerWaerden.AdaptiveMesh.width line 188
  34. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.width_eq_radialWidth line 190
  35. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.width_pos line 194
  36. theorem OAI.QuantitativeVanDerWaerden.centered_eq_of_mem line 205
  37. theorem OAI.QuantitativeVanDerWaerden.rho_eq_of_closed_mem line 211
  38. theorem OAI.QuantitativeVanDerWaerden.abs_le_abs_add_int line 218
  39. theorem OAI.QuantitativeVanDerWaerden.centered_abs_minimal line 231
  40. theorem OAI.QuantitativeVanDerWaerden.centered_abs_sub_le line 239
  41. theorem OAI.QuantitativeVanDerWaerden.rho_lipschitz line 248
  42. theorem OAI.QuantitativeVanDerWaerden.rho_lipschitz_integer line 256
  43. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.increasing_cover_Ico line 266
  44. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.increasing_cover_Ioc line 284
  45. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.endpoint_nonneg line 302
  46. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.endpoint_le_half line 306
  47. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.left_ge_neg_half line 310
  48. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.right_le_half line 316
  49. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.contains_iff_negative line 322
  50. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.contains_iff_positive line 328
  51. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.exists_label line 334
  52. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.increasing_Ico_unique line 346
  53. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.increasing_Ioc_unique line 356
  54. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.contains_negative_lt_zero line 366
  55. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.contains_positive_nonneg line 372
  56. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.label_unique line 378
  57. def OAI.QuantitativeVanDerWaerden.AdaptiveMesh.meshLabel line 396
  58. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.meshLabel_contains line 399
  59. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.meshLabel_eq_iff line 402
  60. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.meshLabel_add_int line 411
  61. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.same_label_distance line 416
  62. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.closed_radial_mem line 426
  63. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.width_bounds_of_closed_mem line 444
  64. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.width_le_two_H line 452
  65. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.neighbor_width line 464

    Source documentation

    Integer congruence is kept explicit. A displacement of at most twice the anchor width covers every point in its closed circle neighborhood.

    theorem neighbor_width (i j : A.Label) {x y : ℝ}
    (hxl : A.left i ≤ x) (hxu : x ≤ A.right i)
    (hyl : A.left j ≤ y) (hyu : y ≤ A.right j)
    (hnear : ∃ z : ℤ, |y - x - z| ≤ 2 * A.width i) :
    A.width i / 16 ≤ A.width j := by
…
  66. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.card_label line 490
  67. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.twice_m_le line 493
  68. theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.twice_m_le_of_H line 498