Documentation

MIPRE.Tailored.Sofic.Measure.MainTheorem

Main Theorem I (2), and the refutation of the Aldous–Lyons conjecture #

mainTheoremI_two: a primitive recursive, non-increasing dyadic sequence tending to the ergodic value — the running minimum upperMin of the upper approximation upperSeq, which is at least the ergodic value (valErg_le_upperSeq) and tends to it (tendsto_upperSeq). With Main Theorem I (1) and the conjecture this makes the sofic value approximable (sofValueApproximable_of_aldousLyons, Corollary I:605), and with Main Theorem II and a halting reduction to tailored games it refutes the conjecture (aldous_lyons_false_of, Corollary I:2144).

source
theorem MIPRE.Tailored.Sofic.Measure.ergUpperApprox :
ErgUpperApprox

Clause (2) as used by the corollary: the upper approximation.

source
def MIPRE.Tailored.Sofic.Measure.upperMin (T : SubgroupTestValue.SubgroupTestData) :
ℕ → ℕ

The running minimum of the upper approximation, as a numerator over 2^t.

Equations
Instances For
    source
    theorem MIPRE.Tailored.Sofic.Measure.upperMin_eq_rec (T : SubgroupTestValue.SubgroupTestData) (t : ℕ) :
    upperMin T t = Nat.rec (upperSeq T 0) (fun (n m : ℕ) => min (2 * m) (upperSeq T (n + 1))) t
    source
    theorem MIPRE.Tailored.Sofic.Measure.primrec_upperMin :
    Primrec₂ upperMin
    source
    theorem MIPRE.Tailored.Sofic.Measure.dyadic_min_succ (a b t : ℕ) :
    dyadic (min (2 * a) b) (t + 1) = min (dyadic a t) (dyadic b (t + 1))
    source
    theorem MIPRE.Tailored.Sofic.Measure.valErg_le_upperMin (T : SubgroupTestValue.SubgroupTestData) (t : ℕ) :
    T.valErg ≤ dyadic (upperMin T t) t
    source
    theorem MIPRE.Tailored.Sofic.Measure.upperMin_le (T : SubgroupTestValue.SubgroupTestData) (t : ℕ) :
    dyadic (upperMin T t) t ≤ dyadic (upperSeq T t) t
    source
    theorem MIPRE.Tailored.Sofic.Measure.antitone_upperMin (T : SubgroupTestValue.SubgroupTestData) :
    Antitone fun (t : ℕ) => dyadic (upperMin T t) t
    source
    theorem MIPRE.Tailored.Sofic.Measure.mainTheoremI_two :
    ∃ (β : SubgroupTestValue.SubgroupTestData → ℕ → ℕ), Primrec₂ β ∧ ∀ (T : SubgroupTestValue.SubgroupTestData), (Antitone fun (t : ℕ) => dyadic (β T t) t) ∧ (∀ (t : ℕ), T.valErg ≤ dyadic (β T t) t) ∧ Filter.Tendsto (fun (t : ℕ) => dyadic (β T t) t) Filter.atTop (nhds T.valErg)

    Main Theorem I (2) (I:594): a primitive recursive, non-increasing sequence of dyadic numbers β T t / 2^t tending to the ergodic value.

    source
    theorem MIPRE.Tailored.Sofic.Measure.mainTheoremITwo :
    MainTheoremITwo
    source
    theorem MIPRE.Tailored.Sofic.Measure.sofValueApproximable_of_aldousLyons (hAL : SubgroupTestValue.AldousLyons) :
    SubgroupTestValue.SofValueApproximable

    The Aldous–Lyons conjecture makes the sofic value approximable (Corollary I:605).

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

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