Lax Lean Archive

Haeupler–Saha–Srinivasan Theorem 2.2

Lax296731.HaeuplerSahaSrinivasanTheorem22 · concepts/Lax296731/HaeuplerSahaSrinivasanTheorem22.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

    Suppose the asymmetric local-lemma conditions hold for a finite set A\mathcal A of bad events. Let BB be any event determined by the same independent random variables, whether or not BB belongs to A\mathcal A. The probability that BB is true at least once during the Moser–Tardos algorithm is at most

    Pr⁡[B]∏C∈Γ(B)(1−x(C))−1.\Pr[B]\prod_{C\in\Gamma(B)}(1-x(C))^{-1}.

    In particular, the same bound holds for the probability that BB is true in the output distribution of the algorithm.

    Concept map
    3 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.HaeuplerSahaSrinivasanDefinitions
    3
    4/-!
    5---
    6title: Haeupler–Saha–Srinivasan Theorem 2.2
    7type: theorem
    8---
    9Suppose the asymmetric local-lemma conditions hold for a finite set
    10A\mathcal A of bad events. Let BB be any event determined by the same
    11independent random variables, whether or not BB belongs to A\mathcal A.
    12The probability that BB is true at least once during the Moser--Tardos
    13algorithm is at most
    14
    15Pr⁡[B]∏C∈Γ(B)(1−x(C))−1.\Pr[B]\prod_{C\in\Gamma(B)}(1-x(C))^{-1}.
    16
    17In particular, the same bound holds for the probability that BB is true in
    18the output distribution of the algorithm.
    19-/
    20
    21set_option autoImplicit false
    22
    23open scoped ENNReal
    24
    25namespace Lax296731.HaeuplerSahaSrinivasanTheorem22
    26
    27open Lax296731.MoserTardosDefinitions
    28open Lax296731.HaeuplerSahaSrinivasanDefinitions
    29
    30/-- The distributional local lemma of Haeupler, Saha, and Srinivasan, Theorem 2.2. -/
    31axiom theorem_2_2
    32 {Event : Type} [Fintype Event] [DecidableEq Event]
    33 {Variable : Type} [Fintype Variable] [DecidableEq Variable]
    34 (Value : Variable → Type) [∀ i, MeasurableSpace (Value i)]
    35 (distribution : ∀ i, MeasureTheory.Measure (Value i))
    36 [∀ i, MeasureTheory.IsProbabilityMeasure (distribution i)]
    37 (badEvents : Finset Event)
    38 (variablesOf : Event → Finset Variable)
    39 (event : ∀ A, Set (LocalAssignment Value (variablesOf A)))
    40 (event_measurable : ∀ A, MeasurableSet (event A))
    41 (selectionRule : ResamplingRule Value
    42 (badEventVariables badEvents variablesOf)
    43 (badEventSet Value badEvents variablesOf event))
    44 (x : BadEventIndex badEvents → 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
    49 (badEventVariables badEvents variablesOf)
    50 (badEventSet Value badEvents variablesOf event) A ≤
    51 ((x A * ∏ C ∈ dependencyNeighborhood badEvents variablesOf A.1,
    52 (1 - x C) : NNReal) : ℝ≥0∞))
    53 (B : Event) :
    54 let upperBound :=
    55 eventProbability Value distribution variablesOf event B *
    56 ((∏ C ∈ dependencyNeighborhood badEvents variablesOf B,
    57 (1 - x C)⁻¹ : NNReal) : ℝ≥0∞)
    58 probabilityEventEverOccurs Value distribution badEvents variablesOf event
    59 selectionRule B ≤ upperBound ∧
    60 probabilityEventInOutput Value distribution badEvents variablesOf event
    61 selectionRule B ≤ upperBound
    62
    63end Lax296731.HaeuplerSahaSrinivasanTheorem22
    64
    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…