OAI/Probability/CriticalZ3/Basic.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

Finite alterations, tail invariance, and the infinite seed limit.

  1. theorem OAI.CriticalZ3.parameter_coe line 11
  2. theorem OAI.CriticalZ3.parameter_zero line 15
  3. theorem OAI.CriticalZ3.parameter_one line 16
  4. instance OAI.CriticalZ3.bondLaw_probability line 18
  5. instance OAI.CriticalZ3.siteLaw_probability line 22
  6. theorem OAI.CriticalZ3.bondLaw_zero line 26
  7. theorem OAI.CriticalZ3.siteLaw_zero line 29
  8. theorem OAI.CriticalZ3.bondLaw_one line 32
  9. theorem OAI.CriticalZ3.siteLaw_one line 35
  10. theorem OAI.CriticalZ3.nearestNeighbor_symm line 38
  11. theorem OAI.CriticalZ3.bondOpen_symm line 43
  12. theorem OAI.CriticalZ3.siteOpen_symm line 46
  13. def OAI.CriticalZ3.PathLength line 50

    Source documentation

    Finite path length, used solely to prove measurability of reachability.

    def PathLength {V : Type uV} (r : V → V → Prop) : ℕ → V → V → Prop
  | 0, x, y => x = y
  | n + 1, x, y => ∃ z, PathLength r n x z ∧ r z y
  14. theorem OAI.CriticalZ3.pathLength_rtg line 54
  15. theorem OAI.CriticalZ3.rtg_iff_exists_pathLength line 62
  16. theorem OAI.CriticalZ3.measurableSet_rtg line 74
  17. theorem OAI.CriticalZ3.measurableSet_bondOpen line 86
  18. theorem OAI.CriticalZ3.measurableSet_siteOpen line 96
  19. theorem OAI.CriticalZ3.measurableSet_bondConnected line 102
  20. theorem OAI.CriticalZ3.measurableSet_siteConnected line 106
  21. theorem OAI.CriticalZ3.infinite_iff_escape_finset line 111
  22. theorem OAI.CriticalZ3.measurableSet_infinite_fiber line 120
  23. theorem OAI.CriticalZ3.measurableSet_bondInfiniteAt line 130
  24. theorem OAI.CriticalZ3.measurableSet_siteInfiniteAt line 134
  25. def OAI.CriticalZ3.ray line 139

    Source documentation

    An infinite nearest-neighbor ray, used to certify supercriticality at one.

    def ray (x : Vertex) (n : ℕ) : Vertex :=
…

    Mentions: OAI.CriticalZ3.Vertex

  26. theorem OAI.CriticalZ3.ray_zero line 142
  27. theorem OAI.CriticalZ3.ray_succ line 146
  28. theorem OAI.CriticalZ3.ray_injective line 152
  29. theorem OAI.CriticalZ3.bondConnected_open_ray line 158
  30. theorem OAI.CriticalZ3.siteConnected_open_ray line 166
  31. theorem OAI.CriticalZ3.bondCluster_open_infinite line 175
  32. theorem OAI.CriticalZ3.siteCluster_open_infinite line 179
  33. theorem OAI.CriticalZ3.bondCluster_closed line 183
  34. theorem OAI.CriticalZ3.siteCluster_closed line 190
  35. theorem OAI.CriticalZ3.bondLaw_zero_infinite line 194
  36. theorem OAI.CriticalZ3.siteLaw_zero_infinite line 198
  37. theorem OAI.CriticalZ3.bondLaw_one_infinite line 202
  38. theorem OAI.CriticalZ3.siteLaw_one_infinite line 206
  39. theorem OAI.CriticalZ3.bond_supercritical_nonempty line 210
  40. theorem OAI.CriticalZ3.site_supercritical_nonempty line 214
  41. theorem OAI.CriticalZ3.bondCritical_mem line 218
  42. theorem OAI.CriticalZ3.siteCritical_mem line 223
  43. theorem OAI.CriticalZ3.bond_subcritical_origin line 228
  44. theorem OAI.CriticalZ3.site_subcritical_origin line 235
  45. theorem OAI.CriticalZ3.rtg_covered_by_roots line 246

    Source documentation

    A path with finitely many types of exceptional arrivals ends in the unperturbed component of its starting point or of an exceptional vertex.

    theorem rtg_covered_by_roots {V : Type uV} {r s : V → V → Prop} {F : Set V}
    (h : ∀ a b, r a b → s a b ∨ b ∈ F) {x y : V}
    (hxy : Relation.ReflTransGen r x y) :
    ∃ z ∈ insert x F, Relation.ReflTransGen s z y := by
…
  46. theorem OAI.CriticalZ3.finite_components_of_finite_perturbation line 258
  47. theorem OAI.CriticalZ3.infinite_component_of_perturbation line 267
  48. def OAI.CriticalZ3.backstep line 277

    Source documentation

    A negative coordinate step, needed only to list all finitely many neighbors.

    def backstep (x : Vertex) (i : Fin 3) : Vertex := fun j => x j - if i = j then 1 else 0

    Mentions: OAI.CriticalZ3.Vertex

  49. theorem OAI.CriticalZ3.step_backstep line 279
  50. theorem OAI.CriticalZ3.backstep_step line 283
  51. theorem OAI.CriticalZ3.nearestNeighbor_iff_steps line 287
  52. theorem OAI.CriticalZ3.finite_neighbors line 297
  53. def OAI.CriticalZ3.bondExistsInfinite line 304
  54. def OAI.CriticalZ3.siteExistsInfinite line 305
  55. theorem OAI.CriticalZ3.measurableSet_bondExistsInfinite line 307
  56. theorem OAI.CriticalZ3.measurableSet_siteExistsInfinite line 311
  57. theorem OAI.CriticalZ3.bondExistsInfinite_of_finite_alteration line 315
  58. theorem OAI.CriticalZ3.bondExistsInfinite_finite_alteration line 331
  59. theorem OAI.CriticalZ3.siteOpen_open_left line 337
  60. theorem OAI.CriticalZ3.siteOpen_open_right line 340
  61. theorem OAI.CriticalZ3.siteRtg_from_closed line 343
  62. theorem OAI.CriticalZ3.siteInfinite_iff_rtg_infinite line 350
  63. theorem OAI.CriticalZ3.siteExistsInfinite_of_finite_alteration line 359
  64. theorem OAI.CriticalZ3.siteExistsInfinite_finite_alteration line 377
  65. theorem OAI.CriticalZ3.zero_one_of_finite_alteration line 388

    Source documentation

    Kolmogorov zero-one law in the finite-alteration form needed here. This is proved for arbitrary independent bit coordinates, not assumed for clusters.

    theorem zero_one_of_finite_alteration {E : Type uE} (μ : Measure (E → Bool))
    (hi : iIndepFun (fun e (ω : E → Bool) => ω e) μ)
    (A : Set (E → Bool)) (hA : MeasurableSet A)
    (hinv : ∀ (J : Finset E) (ω ω' : E → Bool),
      (∀ e ∉ J, ω' e = ω e) → (ω' ∈ A ↔ ω ∈ A)) : μ A = 0 ∨ μ A = 1 := by
…
  66. theorem OAI.CriticalZ3.bondExistsInfinite_zero_one line 429
  67. theorem OAI.CriticalZ3.siteExistsInfinite_zero_one line 437
  68. theorem OAI.CriticalZ3.bondExistsInfinite_one line 445
  69. theorem OAI.CriticalZ3.siteExistsInfinite_one line 452
  70. def OAI.CriticalZ3.cube line 459
  71. theorem OAI.CriticalZ3.mem_cube line 462
  72. theorem OAI.CriticalZ3.cube_finite line 466
  73. theorem OAI.CriticalZ3.cube_mono line 468
  74. theorem OAI.CriticalZ3.exists_mem_cube line 476
  75. theorem OAI.CriticalZ3.iUnion_cube line 486
  76. def OAI.CriticalZ3.bondSeedInfinite line 491
  77. def OAI.CriticalZ3.siteSeedInfinite line 493
  78. theorem OAI.CriticalZ3.bondSeedInfinite_mono line 496
  79. theorem OAI.CriticalZ3.siteSeedInfinite_mono line 499
  80. theorem OAI.CriticalZ3.measurableSet_bondSeedInfinite line 503
  81. theorem OAI.CriticalZ3.measurableSet_siteSeedInfinite line 511
  82. theorem OAI.CriticalZ3.iUnion_bondSeedInfinite line 520
  83. theorem OAI.CriticalZ3.iUnion_siteSeedInfinite line 529
  84. theorem OAI.CriticalZ3.bondSeedInfinite_tendsto_one line 539
  85. theorem OAI.CriticalZ3.siteSeedInfinite_tendsto_one line 545
  86. def OAI.CriticalZ3.cubeBoundary line 552

    Source documentation

    The closed-cube vertex boundary used by the finite-scale argument.

    def cubeBoundary (c : Vertex) (n : ℕ) : Set Vertex :=
…

    Mentions: OAI.CriticalZ3.Vertex

  87. def OAI.CriticalZ3.Within line 555
  88. theorem OAI.CriticalZ3.rtg_first_exit line 558
  89. theorem OAI.CriticalZ3.nearestNeighbor_exit_boundary line 575
  90. theorem OAI.CriticalZ3.bondOpen_neighbor line 604
  91. def OAI.CriticalZ3.bondSeedReaches line 610
  92. def OAI.CriticalZ3.siteSeedReaches line 613
  93. theorem OAI.CriticalZ3.bondSeedInfinite_subset_reachesBoundary line 619

    Source documentation

    An infinite component supplies a finite path to the cube boundary; this uses no uniqueness or unproved infinite-path theorem.

    theorem bondSeedInfinite_subset_reachesBoundary (c : Vertex) {m n : ℕ} (hmn : m ≤ n) :
    bondSeedInfinite c m ⊆ bondSeedReaches c m n (cubeBoundary c n) := by
…

    Mentions: OAI.CriticalZ3.Vertex, OAI.CriticalZ3.bondSeedInfinite, OAI.CriticalZ3.bondSeedReaches, OAI.CriticalZ3.cubeBoundary

  94. theorem OAI.CriticalZ3.siteSeedInfinite_subset_reachesBoundary line 627