Lax Lean Archive

The Moser–Tardos theorem

Lax296731.MoserTardos · concepts/Lax296731/MoserTardos.lean · lax-296731

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Let a finite family of mutually independent random variables determine a finite family of measurable bad events. For a bad event AA, let Γ(A)\Gamma(A) be the other bad events sharing a variable with AA. If there are numbers x(A)∈(0,1)x(A)\in(0,1) such that

    Pr⁡[A]≤x(A)∏B∈Γ(A)(1−x(B)),\Pr[A] \le x(A)\prod_{B\in\Gamma(A)}(1-x(B)),

    then some assignment avoids every bad event. Moreover, the Moser–Tardos resampling algorithm resamples each AA at most an expected x(A)/(1−x(A))x(A)/(1-x(A)) times, so its expected total number of resamplings is at most the sum of these bounds.

    Concept map
    2 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Mathlib
    2import Lax296731.MoserTardosDefinitions
    3
    4/-!
    5---
    6title: The Moser–Tardos theorem
    7type: theorem
    8---
    9Let a finite family of mutually independent random variables determine a
    10finite family of measurable bad events. For a bad event AA, let Γ(A)\Gamma(A)
    11be the other bad events sharing a variable with AA. If there are numbers
    12x(A)∈(0,1)x(A)\in(0,1) such that
    13
    14Pr⁡[A]≤x(A)∏B∈Γ(A)(1−x(B)),\Pr[A] \le x(A)\prod_{B\in\Gamma(A)}(1-x(B)),
    15
    16then some assignment avoids every bad event. Moreover, the Moser--Tardos
    17resampling algorithm resamples each AA at most an expected
    18x(A)/(1−x(A))x(A)/(1-x(A)) times, so its expected total number of resamplings is at most
    19the sum of these bounds.
    20-/
    21
    22set_option autoImplicit false
    23
    24open scoped ENNReal
    25
    26namespace Lax296731.MoserTardos
    27
    28open Lax296731.MoserTardosDefinitions
    29
    30/--
    31The constructive asymmetric Lovász local lemma (Moser--Tardos, Theorem 1.2),
    32including its expected resampling bounds.
    33-/
    34axiom moser_tardos
    35 {Event : Type} [Fintype Event] [DecidableEq Event]
    36 {Variable : Type} [Fintype Variable] [DecidableEq Variable]
    37 (Value : Variable → Type) [∀ i, MeasurableSpace (Value i)]
    38 (distribution : ∀ i, MeasureTheory.Measure (Value i))
    39 [∀ i, MeasureTheory.IsProbabilityMeasure (distribution i)]
    40 (variablesOf : Event → Finset Variable)
    41 (badEvent : ∀ A, Set (LocalAssignment Value (variablesOf A)))
    42 (badEvent_measurable : ∀ A, MeasurableSet (badEvent A))
    43 (selectionRule : ResamplingRule Value variablesOf badEvent)
    44 (x : Event → NNReal)
    45 (x_positive : ∀ A, 0 < x A)
    46 (x_less_than_one : ∀ A, x A < 1)
    47 (local_lemma_hypothesis : ∀ A,
    48 eventProbability Value distribution variablesOf badEvent A ≤
    49 ((x A * ∏ B ∈ dependencyNeighborhood variablesOf A, (1 - x B) : NNReal) :
    50 ℝ≥0∞)) :
    51 (∃ assignment : Assignment Value,
    52 ∀ A, ¬violates Value variablesOf badEvent assignment A) ∧
    53 (∀ A, expectedResamplings Value distribution variablesOf badEvent selectionRule A ≤
    54 ((x A / (1 - x A) : NNReal) : ℝ≥0∞)) ∧
    55 (∑ A : Event,
    56 expectedResamplings Value distribution variablesOf badEvent selectionRule A) ≤
    57 ∑ A : Event, ((x A / (1 - x A) : NNReal) : ℝ≥0∞)
    58
    59end Lax296731.MoserTardos
    60
    Show Proof
    Builds on
    Used by

    none

    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…