Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax54.AveragingLemma

Sparse graph thinning lemma

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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    Each proof establishes this claim relative to its assumptions.

    Theorem

    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.

    Lean source view on GitHub

    1import Lax54.GraphDefinitions
    2
    3/-!
    4---
    5title: Sparse graph thinning lemma
    6type: theorem
    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

    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…