Alphabeta MathHow 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.
A set of self-density at most has a subset of at least half its size that is -sparse
Statement
Let be a finite simple graph, let , and let be nonempty. If , then there is a subset with such that is -sparse.
Facts & Assumptions
Given: A finite simple graph , a real , and a nonempty set with .
The ordered internal edge count is the sum of the internal degrees: (Double counting: for a relation between finite sets, The sum over a finite index set, and its product form).
The self-density inequality is equivalent to (Edge counts and densities between nonempty vertex sets).
A set is -sparse exactly when every vertex of the induced graph on it has degree at most times its size (A set is -sparse exactly when the maximum degree of the graph it induces is at most times its size, -sparse, -dense and -restricted vertex sets).
Proof
By [L1] and [L2], the average internal degree of a vertex of is at most .
Let . If , then the sum of the nonnegative internal degrees would be strictly larger than , contradicting step 1.1. Hence has , and every has .
For one has , because . Thus [L3] makes -sparse.
Depends on
- $c$-sparse, $c$-dense and $c$-restricted vertex sets
- Sparsity of one vertex set to another, and weak sparsity of a pair
- For disjoint nonempty vertex sets, weak $c$-sparsity says exactly that the edge density is at most $c$
- Edge counts and densities between nonempty vertex sets
- Double counting: $\sum_{x \in X}\lvert R_x\rvert = \lvert R\rvert = \sum_{y \in Y}\lvert R^y\rvert$ for a relation between finite sets
- If $X$ is nonempty, some row fibre is at least the average size and some row fibre is at most the average size
- A relation $R \subseteq X \times Y$ between finite sets, its row fibres $R_x$ and its column fibres $R^y$
- The sum $\sum_{i \in S} a_i$ over a finite index set, and its product form
- A set is $c$-sparse exactly when the maximum degree of the graph it induces is at most $c$ times its size
Used by
- The edge-density form of Rödl's theorem implies the maximum-degree form, with ε and δ each shrunk by a constant factor Corollary
- A star has tiny self-density, yet no restricted subset containing its centre has more than two vertices Counterexample
- Bounded degree against bounded density: the two statements of Rödl's theorem, and which one is stronger Remark
Dependency tree · two levels
29 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- M. Chudnovsky, A. Scott, P. Seymour, and S. Spirkl, Strengthening Rödl's theorem, sec. 1 (standard reference, not scraped)