Documentation

MIPRE.Tailored.Sofic.Measure.Conclusion

The Aldous–Lyons conjecture makes the sofic value approximable #

Paper I, Corollary I:605 and the deduction of Corollary I:2144. Main Theorem I gives a computable sequence increasing to the sofic value (clause (1), mainTheoremI_one) and one decreasing to the ergodic value (clause (2)). Under the Aldous–Lyons conjecture the two values coincide (SubgroupTestData.valSof_eq_valErg), so a search for a stage where the bounds are within 1/(k+1) terminates, and rounding the lower bound up to the grid of step 1/(k+1) approximates the sofic value to within 1/(k+1) (sofValueApproximable_of). With not_sofValueApproximable_of this refutes the conjecture (aldous_lyons_false_of_upper).

Clause (2) enters through ErgUpperApprox, the part of it the argument uses: a computable dyadic sequence at least the ergodic value and tending to it. MainTheoremITwo is clause (2) as the paper states it, with the sequence non-increasing.

source
def MIPRE.Tailored.Sofic.Measure.ErgUpperApprox :
Prop

Upper approximation of the ergodic value: a computable sequence of dyadic numbers β T t / 2^t, each at least the ergodic value, tending to it.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def MIPRE.Tailored.Sofic.Measure.MainTheoremITwo :
    Prop

    Main Theorem I (2) (I:594): a computable non-increasing sequence of dyadic numbers tending to the ergodic value.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.Tailored.Sofic.Measure.MainTheoremITwo.ergUpperApprox (h : MainTheoremITwo) :
      ErgUpperApprox
      source
      def MIPRE.Tailored.Sofic.Measure.ceilDiv (x D : ℕ) :
      ℕ

      Rounding up to the grid: ⌈x / D⌉ for D > 0.

      Equations
      Instances For
        source
        theorem MIPRE.Tailored.Sofic.Measure.ceilDiv_spec {x D : ℕ} (hD : 0 < D) :
        x ≤ ceilDiv x D * D ∧ ceilDiv x D * D < x + D
        source
        theorem MIPRE.Tailored.Sofic.Measure.approx_of_bounds {v : ℝ} {a b t k : ℕ} (ha : dyadic a t ≤ v) (hb : v ≤ dyadic b t) (hab : (b - a) * (k + 1) < 2 ^ t) :
        |v - ↑(ceilDiv (a * (k + 1)) (2 ^ t)) / (↑k + 1)| ≤ 1 / (↑k + 1)

        The rounded estimate: |v − ⌈a(k+1)/2^t⌉/(k+1)| ≤ 1/(k+1) when v lies between a/2^t and b/2^t and these are within 1/(k+1).

        source
        theorem MIPRE.Tailored.Sofic.Measure.sofValueApproximable_of (hAL : SubgroupTestValue.AldousLyons) (hU : ErgUpperApprox) :
        SubgroupTestValue.SofValueApproximable

        The Aldous–Lyons conjecture makes the sofic value approximable (Corollary I:605), given the upper approximation of the ergodic value (Main Theorem I (2)).

        source
        theorem MIPRE.Tailored.Sofic.Measure.aldous_lyons_false_of_upper {K : ℕ → ℕ} (hK : Primrec K) (hMT : MainTheoremII K) (hred : TailoredGameValue.TailoredHaltingReduction) (hU : ErgUpperApprox) :
        ¬SubgroupTestValue.AldousLyons

        The Aldous–Lyons conjecture is false (Corollary I:2144), from a halting reduction to tailored games, Main Theorem II with a primitive recursive gap function, and the upper approximation of the ergodic value (Main Theorem I (2)).