Lax Lean Archive

Lax41.HaeuplerSahaSrinivasanTheorem22

Haeupler–Saha–Srinivasan Theorem 2.2

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

    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.

    Lean source view on GitHub

    1import Mathlib
    2import Lax41.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 Lax41.HaeuplerSahaSrinivasanTheorem22
    26
    27open Lax41.MoserTardosDefinitions
    28open Lax41.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 Lax41.HaeuplerSahaSrinivasanTheorem22
    64
    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…