OAI/Probability/CriticalZ3/QuarterFaces.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

The 24 signed-coordinate quarter-faces, symmetry and the Harris root bound. The probability statements here are for the actual infinite lattice laws.

  1. abbrev OAI.CriticalZ3.FaceIndex line 14
  2. def OAI.CriticalZ3.QuarterFace line 16
  3. def OAI.CriticalZ3.canonicalFace line 21
  4. theorem OAI.CriticalZ3.quarterFace_subset_boundary line 23
  5. theorem OAI.CriticalZ3.boundary_eq_union_quarterFace line 39
  6. theorem OAI.CriticalZ3.rtg_equiv_iff line 57
  7. theorem OAI.CriticalZ3.SignedSymmetry.bondWithin_map line 71
  8. theorem OAI.CriticalZ3.SignedSymmetry.siteWithin_map line 76
  9. theorem OAI.CriticalZ3.SignedSymmetry.bondSeedReaches_map line 81
  10. theorem OAI.CriticalZ3.SignedSymmetry.siteSeedReaches_map line 96
  11. def OAI.CriticalZ3.faceSymmetry line 114
  12. theorem OAI.CriticalZ3.faceSymmetry_zero line 117
  13. theorem OAI.CriticalZ3.quarterFace_preimage line 122
  14. theorem OAI.ProductCylinder.reindex_probability line 169
  15. theorem OAI.CriticalZ3.measurableSet_bondSeedReaches line 180
  16. theorem OAI.CriticalZ3.measurableSet_siteSeedReaches line 184
  17. theorem OAI.CriticalZ3.bondQuarterFace_probability line 188
  18. theorem OAI.CriticalZ3.siteQuarterFace_probability line 202
  19. theorem OAI.CriticalZ3.bondQuarterFace_compl_real line 216
  20. theorem OAI.CriticalZ3.siteQuarterFace_compl_real line 223
  21. theorem OAI.CriticalZ3.bondBoundary_eq_union_reachesFaces line 230
  22. theorem OAI.CriticalZ3.siteBoundary_eq_union_reachesFaces line 240
  23. theorem OAI.CriticalZ3.card_faceIndex line 250
  24. theorem OAI.CriticalZ3.bondQuarterFace_Harris line 253
  25. theorem OAI.CriticalZ3.siteQuarterFace_Harris line 266
  26. theorem OAI.CriticalZ3.bondQuarterFace_root_bound line 279
  27. theorem OAI.CriticalZ3.siteQuarterFace_root_bound line 287
  28. theorem OAI.CriticalZ3.bondSeedMiss_tendsto_zero line 300
  29. theorem OAI.CriticalZ3.siteSeedMiss_tendsto_zero line 307
  30. theorem OAI.CriticalZ3.exists_bondSeed line 314
  31. theorem OAI.CriticalZ3.exists_siteSeed line 319
  32. theorem OAI.CriticalZ3.continuous_parameter line 324
  33. theorem OAI.CriticalZ3.continuous_bondSeedReaches line 327
  34. theorem OAI.CriticalZ3.continuous_siteSeedReaches line 332
  35. theorem OAI.CriticalZ3.continuous_bondSeedMiss line 337
  36. theorem OAI.CriticalZ3.continuous_siteSeedMiss line 342
  37. theorem OAI.CriticalZ3.exists_lower_forall line 348

    Source documentation

    A single strictly lower parameter preserves simultaneous finite strict bounds.

    theorem exists_lower_forall {I : Type uI} [Finite I] {p γ : ℝ} (hp : 0 < p)
    (g : I → ℝ → ℝ) (hg : ∀ i, Continuous (g i)) (hgp : ∀ i, g i p < γ) :
    ∃ q ∈ Set.Ioo (p/2) p, ∀ i, g i q < γ := by
…
  38. theorem OAI.CriticalZ3.bond_lower_quarterFaces line 366

    Source documentation

    Quarter-face estimates at any fixed finite family of enclosing radii, at one parameter below p, uniformly over every center and all 24 faces.

    theorem bond_lower_quarterFaces {p γ : ℝ} (hp : 0 < p) (hγ : 0 < γ)
    {m : ℕ} (hseed : (bondLaw p).real (bondSeedInfinite 0 m)ᶜ < (γ/2)^24)
    (s : Finset ℕ) (hs : ∀ n ∈ s, m ≤ n) :
    ∃ q ∈ Set.Ioo (p/2) p, ∀ n ∈ s, ∀ c f,
      1-γ < (bondLaw q).real (bondSeedReaches c m n (QuarterFace c n f)) := by
…

    Mentions: OAI.CriticalZ3.bondLaw, OAI.CriticalZ3.bondSeedInfinite, OAI.CriticalZ3.bondSeedReaches, OAI.CriticalZ3.QuarterFace

  39. theorem OAI.CriticalZ3.site_lower_quarterFaces line 383