Lax Lean Archive

Lax41.MoserTardos

The Moser–Tardos theorem

concepts/Lax41/MoserTardos.lean · lax-41

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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    Each proof establishes this claim relative to its assumptions.

    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.

    Lean source view on GitHub

    1import Mathlib
    2import Lax41.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 Lax41.MoserTardos
    27
    28open Lax41.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 Lax41.MoserTardos
    60
    Show Proof

    Builds on

    Used by

    none

    From Mathlib

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…