definition
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Definition
An -regular pair in a finite simple graph is a pair of nonempty vertex sets such that every and with and has density within of the density of .
This is the standard textbook definition, stated with real-valued densities. The definition itself does not require and to be disjoint; in the regularity lemma they are used as distinct blocks of a vertex partition, hence are disjoint there.
Lean source view on GitHub
| 1 | import Lax18.EdgeDensity |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Regular pairs |
| 6 | type: definition |
| 7 | --- |
| 8 | An \(\varepsilon\)-regular pair in a finite simple graph is a pair of nonempty |
| 9 | vertex sets \(A,B\) such that every \(X\subseteq A\) and \(Y\subseteq B\) with |
| 10 | \(|X|\ge \varepsilon |A|\) and \(|Y|\ge \varepsilon |B|\) has density within |
| 11 | \(\varepsilon\) of the density of \(A,B\). |
| 12 | |
| 13 | This is the standard textbook definition, stated with real-valued densities. |
| 14 | The definition itself does not require \(A\) and \(B\) to be disjoint; in the |
| 15 | regularity lemma they are used as distinct blocks of a vertex partition, hence |
| 16 | are disjoint there. |
| 17 | -/ |
| 18 | |
| 19 | namespace Lax18.RegularPairs |
| 20 | |
| 21 | open Lax18.EdgeDensity |
| 22 | |
| 23 | universe u |
| 24 | |
| 25 | variable {V : Type u} [Fintype V] [DecidableEq V] |
| 26 | |
| 27 | /-- `X` is a large enough subset of `A` for the threshold `ε`. -/ |
| 28 | def LargeSubset (ε : ℝ) (A X : Finset V) : Prop := |
| 29 | X ⊆ A ∧ ε * (A.card : ℝ) ≤ (X.card : ℝ) |
| 30 | |
| 31 | /-- The pair `(A,B)` is `ε`-regular in `G`. -/ |
| 32 | def IsRegularPair (G : SimpleGraph V) (ε : ℝ) (A B : Finset V) : Prop := |
| 33 | A.Nonempty ∧ B.Nonempty ∧ |
| 34 | ∀ X Y : Finset V, |
| 35 | LargeSubset ε A X → |
| 36 | LargeSubset ε B Y → |
| 37 | |density G X Y - density G A B| ≤ ε |
| 38 | |
| 39 | end Lax18.RegularPairs |
| 40 |
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