Lax Lean Archive

Lax41.MoserTardosDefinitions

Definitions for the Moser–Tardos resampling algorithm

concepts/Lax41/MoserTardosDefinitions.lean · lax-41

definition

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

    Definition

    This file gives the semantic closure of the Moser–Tardos theorem. A bad event is represented by the set of local assignments on the finite collection of independent random variables that determines it. An infinite table supplies fresh independent samples. A measurable rule repeatedly chooses a currently true bad event, whose variables are then advanced to their next samples. The definitions below give the dependency neighborhood, the probability of an event, and the expected number of times each event is resampled.

    Lean source view on GitHub

    1import Mathlib
    2
    3/-!
    4---
    5title: Definitions for the Moser–Tardos resampling algorithm
    6type: definition
    7---
    8This file gives the semantic closure of the Moser--Tardos theorem. A bad event
    9is represented by the set of local assignments on the finite collection of
    10independent random variables that determines it. An infinite table supplies
    11fresh independent samples. A measurable rule repeatedly chooses a currently
    12true bad event, whose variables are then advanced to their next samples. The
    13definitions below give the dependency neighborhood, the probability of an
    14event, and the expected number of times each event is resampled.
    15-/
    16
    17set_option autoImplicit false
    18
    19open scoped ENNReal
    20
    21namespace Lax41.MoserTardosDefinitions
    22
    23variable {Event : Type} [Fintype Event] [DecidableEq Event]
    24variable {Variable : Type} [Fintype Variable] [DecidableEq Variable]
    25variable (Value : Variable → Type) [∀ i, MeasurableSpace (Value i)]
    26
    27/-- A coordinate of the infinite resampling table. -/
    28abbrev TableIndex := (i : Variable) × Nat
    29
    30/-- An infinite table of fresh samples, one row for each independent variable. -/
    31abbrev ResamplingTable := (j : TableIndex (Variable := Variable)) → Value j.1
    32
    33/-- An assignment to the variables in a finite scope. -/
    34abbrev LocalAssignment (indices : Finset Variable) :=
    35 (i : indices) → Value i.1
    36
    37/-- The product law of an infinite resampling table. -/
    38noncomputable def tableMeasure
    39 (distribution : ∀ i, MeasureTheory.Measure (Value i)) :
    40 MeasureTheory.Measure (ResamplingTable Value) :=
    41 MeasureTheory.Measure.infinitePi
    42 fun j : TableIndex (Variable := Variable) ↦ distribution j.1
    43
    44/-- The product law restricted to a finite collection of variables. -/
    45noncomputable def localMeasure
    46 (distribution : ∀ i, MeasureTheory.Measure (Value i))
    47 (indices : Finset Variable) :
    48 MeasureTheory.Measure (LocalAssignment Value indices) :=
    49 MeasureTheory.Measure.infinitePi fun i : indices ↦ distribution i.1
    50
    51/-- The probability of a bad event under the original product distribution. -/
    52noncomputable def eventProbability
    53 (distribution : ∀ i, MeasureTheory.Measure (Value i))
    54 (variablesOf : Event → Finset Variable)
    55 (badEvent : ∀ A, Set (LocalAssignment Value (variablesOf A)))
    56 (A : Event) : ℝ≥0∞ :=
    57 localMeasure Value distribution (variablesOf A) (badEvent A)
    58
    59/-- A complete assignment to the finite family of independent variables. -/
    60abbrev Assignment := ∀ i, Value i
    61
    62/-- Restriction of a complete assignment to an event's scope. -/
    63def restrictAssignment (variablesOf : Event → Finset Variable)
    64 (assignment : Assignment Value) (A : Event) :
    65 LocalAssignment Value (variablesOf A) :=
    66 fun i ↦ assignment i.1
    67
    68/-- The bad event `A` is true under `assignment`. -/
    69def violates (variablesOf : Event → Finset Variable)
    70 (badEvent : ∀ A, Set (LocalAssignment Value (variablesOf A)))
    71 (assignment : Assignment Value) (A : Event) : Prop :=
    72 restrictAssignment Value variablesOf assignment A ∈ badEvent A
    73
    74/--
    75A measurable deterministic implementation of "choose any currently true bad
    76event". It returns `none` exactly when no bad event is true.
    77-/
    78structure ResamplingRule (variablesOf : Event → Finset Variable)
    79 (badEvent : ∀ A, Set (LocalAssignment Value (variablesOf A))) where
    80 choose : Assignment Value → Option Event
    81 measurable_fiber : ∀ result, MeasurableSet {assignment | choose assignment = result}
    82 sound : ∀ ⦃assignment : Assignment Value⦄ ⦃A : Event⦄,
    83 choose assignment = some A →
    84 violates Value variablesOf badEvent assignment A
    85 complete : ∀ ⦃assignment : Assignment Value⦄,
    86 choose assignment = none →
    87 ∀ A, ¬violates Value variablesOf badEvent assignment A
    88
    89/-- The assignment exposed by a resampling table at the given row counters. -/
    90def currentAssignment (table : ResamplingTable Value) (counts : Variable → Nat) :
    91 Assignment Value :=
    92 fun i ↦ table ⟨i, counts i⟩
    93
    94/-- Increment precisely the counters in the scope of the selected event. -/
    95def advanceCounts (variablesOf : Event → Finset Variable)
    96 (counts : Variable → Nat) (selected : Option Event) : Variable → Nat :=
    97 selected.elim counts fun A i ↦
    98 if i ∈ variablesOf A then counts i + 1 else counts i
    99
    100/-- The row counters after the first `n` iterations of the resampling algorithm. -/
    101def runCounts (variablesOf : Event → Finset Variable)
    102 (badEvent : ∀ A, Set (LocalAssignment Value (variablesOf A)))
    103 (selectionRule : ResamplingRule Value variablesOf badEvent)
    104 (table : ResamplingTable Value) : Nat → Variable → Nat :=
    105 Nat.rec (fun _ ↦ 0) fun _ counts ↦
    106 advanceCounts variablesOf counts
    107 (selectionRule.choose (currentAssignment Value table counts))
    108
    109/-- The event resampled at time `n`, or `none` once no bad event remains. -/
    110def resamplingLog (variablesOf : Event → Finset Variable)
    111 (badEvent : ∀ A, Set (LocalAssignment Value (variablesOf A)))
    112 (selectionRule : ResamplingRule Value variablesOf badEvent)
    113 (table : ResamplingTable Value) (n : Nat) : Option Event :=
    114 selectionRule.choose (currentAssignment Value table
    115 (runCounts Value variablesOf badEvent selectionRule table n))
    116
    117/-- The (possibly infinite) number of times the bad event `A` is resampled. -/
    118noncomputable def resamplingCount (variablesOf : Event → Finset Variable)
    119 (badEvent : ∀ A, Set (LocalAssignment Value (variablesOf A)))
    120 (selectionRule : ResamplingRule Value variablesOf badEvent)
    121 (table : ResamplingTable Value) (A : Event) : ℝ≥0∞ :=
    122 ∑' t : Nat, Set.indicator
    123 {t | resamplingLog Value variablesOf badEvent selectionRule table t = some A}
    124 (fun _ ↦ (1 : ℝ≥0∞)) t
    125
    126/-- The expected number of resamplings of one event. -/
    127noncomputable def expectedResamplings
    128 (distribution : ∀ i, MeasureTheory.Measure (Value i))
    129 (variablesOf : Event → Finset Variable)
    130 (badEvent : ∀ A, Set (LocalAssignment Value (variablesOf A)))
    131 (selectionRule : ResamplingRule Value variablesOf badEvent)
    132 (A : Event) : ℝ≥0∞ :=
    133 ∫⁻ table, resamplingCount Value variablesOf badEvent selectionRule table A
    134 ∂tableMeasure Value distribution
    135
    136/-- The other bad events that share at least one random variable with `A`. -/
    137def dependencyNeighborhood (variablesOf : Event → Finset Variable)
    138 (A : Event) : Finset Event :=
    139 Finset.univ.filter fun B ↦
    140 B ≠ A ∧ ¬Disjoint (variablesOf A) (variablesOf B)
    141
    142end Lax41.MoserTardosDefinitions
    143

    Builds on

    none

    Used by

    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…