How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
The symmetric Lovász Local Lemma under
Statement
Let and . Let have a dependency digraph of maximum out-degree at most . If for every and then .
Facts & Assumptions
Given: A finite event family, its dependency digraph, and satisfying the Statement.
The asymmetric Local Lemma applies when with (The asymmetric Lovász Local Lemma for finitely many events).
for every real ( for every real , hence ).
; natural powers preserve order on nonnegative bases; and positive inequalities may be multiplied and inverted using the ordered-field laws (The exponential addition formula , Integer powers , Laws of integer exponents, Monotonicity of and of , The reals form a totally ordered field).
Proof
Suppose and set every . Applying [L2] at gives , so . The hypothesis gives , and the empty neighbour product is , so [L1] applies.
Suppose and set every . From [L2] at and [L3], , hence .
Each vertex has at most out-neighbours, so by the hypothesis. Thus [L1] applies.
The cases and are exhaustive and both give positive probability that no bad event occurs.
Depends on
- The asymmetric Lovász Local Lemma for finitely many events
- $1+x\le\exp(x)$ for every real $x$, hence $(1-p)^m\le\exp(-mp)$
- The exponential addition formula $\exp(x+y)=\exp(x)\exp(y)$
- Integer powers $a^m$
- Laws of integer exponents
- Monotonicity of $x \mapsto x^n$ and of $n \mapsto a^n$
- The reals form a totally ordered field
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 119 results over 31 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- J. Matousek and J. Vondrak, The Probabilistic Method, Corollary 5.1.2 (standard reference, not scraped)
- Y. Zhao, MIT 18.218 Probabilistic Method in Combinatorics, Corollary 5.3 (standard reference, not scraped)