OAI/Probability/CriticalZ3/ExplorationSurvival.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InfiniteConditioning.History.observe_pattern line 14
  2. def OAI.CriticalZ3.Model.Connected line 29
  3. def OAI.CriticalZ3.Model.Cluster line 33
  4. theorem OAI.CriticalZ3.Model.infiniteAt_iff line 36
  5. theorem OAI.CriticalZ3.Model.measurableSet_infiniteAt line 39
  6. theorem OAI.CriticalZ3.LatticeGraph.conn_global line 47
  7. def OAI.CriticalZ3.Coarse.Exploration.Sound line 57
  8. theorem OAI.CriticalZ3.Coarse.Exploration.accepted_event line 60
  9. theorem OAI.CriticalZ3.Coarse.Exploration.sound_advance line 68
  10. theorem OAI.CriticalZ3.Coarse.Exploration.run_pattern line 84
  11. theorem OAI.CriticalZ3.Coarse.Exploration.run_sound line 91
  12. theorem OAI.CriticalZ3.Coarse.Exploration.good_finite_of_cluster_finite line 101
  13. theorem OAI.CriticalZ3.Coarse.initial_sound line 118
  14. theorem OAI.CriticalZ3.Coarse.scales_percolate line 139
  15. theorem OAI.CriticalZ3.Coarse.lower_percolating_parameter line 175

    Source documentation

    Positive percolation is open to the left throughout the open unit interval.

    theorem lower_percolating_parameter (m : Model) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hInf : 0 < m.law p (m.InfiniteAt 0)) :
    ∃ q ∈ Set.Icc (0:ℝ) 1, q < p ∧ 0 < m.law q (m.InfiniteAt 0) := by
…

    Mentions: OAI.CriticalZ3.Model