Lax Lean Archive

Sparse graph thinning lemma

Lax54.AveragingLemma · concepts/Lax54/AveragingLemma.lean · lax-54

proven

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.

    Natural Language Statement

    Lemma

    Lemma 4.2 of the paper, with denominators cleared. Let ZZ induce a graph of edge density at most 1/E1/E, and suppose 2m≤∣Z∣+12m \leq |Z|+1. Then ZZ contains an mm-element set XX such that Edeg⁡G[X](x)≤4(m−1)E\deg_{G[X]}(x) \leq 4(m-1) for every x∈Xx\in X. The factor 44 results from first selecting 2m−12m-1 vertices by averaging and then retaining mm vertices of low degree.

    Concept map
    2 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 10 of this submission's paper

    Lean source view on GitHub

    1import Lax54.GraphDefinitions
    2
    3/-!
    4---
    5title: Sparse graph thinning lemma
    6type: lemma
    7---
    8Lemma 4.2 of the paper, with denominators cleared. Let ZZ induce a graph of
    9edge density at most 1/E1/E, and suppose 2m≤∣Z∣+12m \leq |Z|+1. Then ZZ contains an
    10mm-element set XX such that
    11Edeg⁡G[X](x)≤4(m−1)E\deg_{G[X]}(x) \leq 4(m-1) for every x∈Xx\in X. The factor 44 results from
    12first selecting 2m−12m-1 vertices by averaging and then retaining mm vertices
    13of low degree.
    14-/
    15
    16namespace Lax54.AveragingLemma
    17
    18open Lax54.GraphDefinitions
    19
    20universe u
    21
    22/-- Lemma 4.2, with all inequalities written over the natural numbers. -/
    23axiom sparse_graph_thinning :
    24 ∀ {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V)
    25 [DecidableRel G.Adj] (Z : Finset V) (E m : ℕ),
    26 0 < E → 2 * m ≤ Z.card + 1 →
    27 E * 2 * (G.induce (Z : Set V)).edgeFinset.card ≤
    28 Z.card * (Z.card - 1) →
    29 ∃ X : Finset V, X ⊆ Z ∧ X.card = m ∧
    30 ∀ x : {v : V // v ∈ X},
    31 E * (G.induce (X : Set V)).degree x ≤ 4 * (m - 1)
    32
    33end Lax54.AveragingLemma
    34
    Show Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…