Lax Lean Archive

Lax41.HaeuplerSahaSrinivasanDefinitions

Definitions for the Haeupler–Saha–Srinivasan distributional theorem

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

    Fix a finite collection of mutually independent random variables and a finite set of bad events determined by them. The Moser–Tardos algorithm repeatedly resamples a currently true bad event. Besides the bad events, we may observe any other event BB determined by the same variables. This file defines the bad-event restriction of the event family, the dependency neighborhood Γ(B)\Gamma(B), the event that BB is true at some stage of the algorithm, and the event that BB is true in its final output.

    Lean source view on GitHub

    1import Mathlib
    2import Lax41.MoserTardosDefinitions
    3
    4/-!
    5---
    6title: Definitions for the Haeupler–Saha–Srinivasan distributional theorem
    7type: definition
    8---
    9Fix a finite collection of mutually independent random variables and a finite
    10set of bad events determined by them. The Moser--Tardos algorithm repeatedly
    11resamples a currently true bad event. Besides the bad events, we may observe
    12any other event BB determined by the same variables. This file defines the
    13bad-event restriction of the event family, the dependency neighborhood
    14Γ(B)\Gamma(B), the event that BB is true at some stage of the algorithm, and
    15the event that BB is true in its final output.
    16-/
    17
    18set_option autoImplicit false
    19
    20open scoped ENNReal
    21
    22namespace Lax41.HaeuplerSahaSrinivasanDefinitions
    23
    24open Lax41.MoserTardosDefinitions
    25
    26variable {Event : Type} [Fintype Event] [DecidableEq Event]
    27variable {Variable : Type} [Fintype Variable] [DecidableEq Variable]
    28variable (Value : Variable → Type) [∀ i, MeasurableSpace (Value i)]
    29
    30/-- An event belonging to the finite family on which the algorithm runs. -/
    31abbrev BadEventIndex (badEvents : Finset Event) := {A // A ∈ badEvents}
    32
    33/-- The variables determining a bad event. -/
    34def badEventVariables (badEvents : Finset Event)
    35 (variablesOf : Event → Finset Variable) :
    36 BadEventIndex badEvents → Finset Variable :=
    37 fun A ↦ variablesOf A.1
    38
    39/-- The local set defining a bad event. -/
    40def badEventSet (badEvents : Finset Event)
    41 (variablesOf : Event → Finset Variable)
    42 (event : ∀ A, Set (LocalAssignment Value (variablesOf A))) :
    43 ∀ A, Set (LocalAssignment Value (badEventVariables badEvents variablesOf A)) :=
    44 fun A ↦ event A.1
    45
    46/--
    47The bad events other than `B` that share at least one determining variable
    48with `B`.
    49-/
    50def dependencyNeighborhood (badEvents : Finset Event)
    51 (variablesOf : Event → Finset Variable) (B : Event) :
    52 Finset (BadEventIndex badEvents) :=
    53 Finset.univ.filter fun A ↦
    54 A.1 ≠ B ∧ ¬Disjoint (variablesOf A.1) (variablesOf B)
    55
    56/-- The observed event `B` is true in the assignment at stage `n`. -/
    57def eventOccursAt (badEvents : Finset Event)
    58 (variablesOf : Event → Finset Variable)
    59 (event : ∀ A, Set (LocalAssignment Value (variablesOf A)))
    60 (selectionRule : ResamplingRule Value
    61 (badEventVariables badEvents variablesOf)
    62 (badEventSet Value badEvents variablesOf event))
    63 (table : ResamplingTable Value) (B : Event) (n : Nat) : Prop :=
    64 violates Value variablesOf event
    65 (currentAssignment Value table
    66 (runCounts Value (badEventVariables badEvents variablesOf)
    67 (badEventSet Value badEvents variablesOf event) selectionRule table n)) B
    68
    69/-- The set of sample tables on which `B` is true at least once. -/
    70def eventEverOccurs (badEvents : Finset Event)
    71 (variablesOf : Event → Finset Variable)
    72 (event : ∀ A, Set (LocalAssignment Value (variablesOf A)))
    73 (selectionRule : ResamplingRule Value
    74 (badEventVariables badEvents variablesOf)
    75 (badEventSet Value badEvents variablesOf event))
    76 (B : Event) : Set (ResamplingTable Value) :=
    77 {table | ∃ n, eventOccursAt Value badEvents variablesOf event selectionRule table B n}
    78
    79/--
    80The first stage at which the algorithm has terminated. On a nonterminating
    81table it is set to zero; under the local-lemma hypotheses that exceptional set
    82has probability zero.
    83-/
    84noncomputable def outputTime (badEvents : Finset Event)
    85 (variablesOf : Event → Finset Variable)
    86 (event : ∀ A, Set (LocalAssignment Value (variablesOf A)))
    87 (selectionRule : ResamplingRule Value
    88 (badEventVariables badEvents variablesOf)
    89 (badEventSet Value badEvents variablesOf event))
    90 (table : ResamplingTable Value) : Nat := by
    91 classical
    92 exact if h : ∃ n, resamplingLog Value (badEventVariables badEvents variablesOf)
    93 (badEventSet Value badEvents variablesOf event) selectionRule table n = none
    94 then Nat.find h
    95 else 0
    96
    97/-- The assignment returned when the resampling algorithm terminates. -/
    98noncomputable def outputAssignment (badEvents : Finset Event)
    99 (variablesOf : Event → Finset Variable)
    100 (event : ∀ A, Set (LocalAssignment Value (variablesOf A)))
    101 (selectionRule : ResamplingRule Value
    102 (badEventVariables badEvents variablesOf)
    103 (badEventSet Value badEvents variablesOf event))
    104 (table : ResamplingTable Value) : Assignment Value :=
    105 currentAssignment Value table
    106 (runCounts Value (badEventVariables badEvents variablesOf)
    107 (badEventSet Value badEvents variablesOf event) selectionRule table
    108 (outputTime Value badEvents variablesOf event selectionRule table))
    109
    110/-- The set of sample tables whose output assignment makes `B` true. -/
    111noncomputable def eventOccursInOutput (badEvents : Finset Event)
    112 (variablesOf : Event → Finset Variable)
    113 (event : ∀ A, Set (LocalAssignment Value (variablesOf A)))
    114 (selectionRule : ResamplingRule Value
    115 (badEventVariables badEvents variablesOf)
    116 (badEventSet Value badEvents variablesOf event))
    117 (B : Event) : Set (ResamplingTable Value) :=
    118 {table | violates Value variablesOf event
    119 (outputAssignment Value badEvents variablesOf event selectionRule table) B}
    120
    121/-- The probability that `B` is true at least once during the algorithm. -/
    122noncomputable def probabilityEventEverOccurs
    123 (distribution : ∀ i, MeasureTheory.Measure (Value i))
    124 (badEvents : Finset Event) (variablesOf : Event → Finset Variable)
    125 (event : ∀ A, Set (LocalAssignment Value (variablesOf A)))
    126 (selectionRule : ResamplingRule Value
    127 (badEventVariables badEvents variablesOf)
    128 (badEventSet Value badEvents variablesOf event))
    129 (B : Event) : ℝ≥0∞ :=
    130 tableMeasure Value distribution
    131 (eventEverOccurs Value badEvents variablesOf event selectionRule B)
    132
    133/-- The probability that `B` is true in the algorithm's output. -/
    134noncomputable def probabilityEventInOutput
    135 (distribution : ∀ i, MeasureTheory.Measure (Value i))
    136 (badEvents : Finset Event) (variablesOf : Event → Finset Variable)
    137 (event : ∀ A, Set (LocalAssignment Value (variablesOf A)))
    138 (selectionRule : ResamplingRule Value
    139 (badEventVariables badEvents variablesOf)
    140 (badEventSet Value badEvents variablesOf event))
    141 (B : Event) : ℝ≥0∞ :=
    142 tableMeasure Value distribution
    143 (eventOccursInOutput Value badEvents variablesOf event selectionRule B)
    144
    145end Lax41.HaeuplerSahaSrinivasanDefinitions
    146

    Builds on

    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…