Lax Lean Archive

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

Lax54.BipartiteCombLemma

Bipartite comb lemma

concepts/Lax54/BipartiteCombLemma.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

    The d=1/2d=1/2 case of Theorem 2.1, with denominators cleared. Let AA and BB be disjoint vertex sets. Suppose that every vertex of BB has a neighbor in AA and that every vertex of AA has at most Δ\Delta neighbors in BB. For every Γ>0\Gamma>0, either there is a comb with t≥1t\geq 1 teeth whose blocks satisfy Γ≤t2∣Bi∣\Gamma\leq t^2|B_i|, or ∣B∣2≤1282ΓΔ|B|^2\leq 128^2\Gamma\Delta.

    The constant 128128 is an absolute constant obtained from an integral four-adic form of the peeling argument. Its precise value is not used later.

    Lean source view on GitHub

    1import Lax54.GraphDefinitions
    2
    3/-!
    4---
    5title: Bipartite comb lemma
    6type: theorem
    7---
    8The d=1/2d=1/2 case of Theorem 2.1, with denominators cleared. Let AA and BB be
    9disjoint vertex sets. Suppose that every vertex of BB has a neighbor in AA
    10and that every vertex of AA has at most Δ\Delta neighbors in BB. For every
    11Γ>0\Gamma>0, either there is a comb with t≥1t\geq 1 teeth whose blocks satisfy
    12Γ≤t2∣Bi∣\Gamma\leq t^2|B_i|, or
    13∣B∣2≤1282ΓΔ|B|^2\leq 128^2\Gamma\Delta.
    14
    15The constant 128128 is an absolute constant obtained from an integral
    16four-adic form of the peeling argument. Its precise value is not used later.
    17-/
    18
    19namespace Lax54.BipartiteCombLemma
    20
    21universe u
    22
    23/--
    24A comb with distinct teeth in `A` and pairwise disjoint blocks in `B`. Each
    25tooth is adjacent to its own block and nonadjacent to every other block.
    26-/
    27structure CombBetween {V : Type u} [DecidableEq V]
    28 (G : SimpleGraph V) (A B : Finset V) (t : ℕ) where
    29 tooth : Fin t → V
    30 block : Fin t → Finset V
    31 tooth_mem : ∀ i, tooth i ∈ A
    32 tooth_injective : Function.Injective tooth
    33 block_subset : ∀ i, block i ⊆ B
    34 blocks_disjoint : ∀ {i j}, i ≠ j → Disjoint (block i) (block j)
    35 tooth_adj_block : ∀ i, ∀ x ∈ block i, G.Adj (tooth i) x
    36 tooth_nonadj_other : ∀ {i j}, i ≠ j →
    37 ∀ x ∈ block j, ¬ G.Adj (tooth i) x
    38
    39/-- The sparse alternative in the `d = 1/2` case of Theorem 2.1. -/
    40def SmallSideBound (C Gamma Delta b : ℕ) : Prop :=
    41 b ^ 2 ≤ C ^ 2 * Gamma * Delta
    42
    43/-- The `d = 1/2` case of Theorem 2.1, with denominators cleared. -/
    44axiom bipartite_comb_lemma :
    45 ∀ {V : Type u} [Fintype V] [DecidableEq V]
    46 (G : SimpleGraph V) [DecidableRel G.Adj]
    47 (A B : Finset V) (Gamma Delta : ℕ),
    48 Disjoint A B → 0 < Gamma →
    49 (∀ b ∈ B, ∃ a ∈ A, G.Adj a b) →
    50 (∀ a ∈ A, (B.filter fun b ↦ G.Adj a b).card ≤ Delta) →
    51 (∃ (t : ℕ) (Cmb : CombBetween G A B t),
    52 0 < t ∧ ∀ i : Fin t, Gamma ≤ t ^ 2 * (Cmb.block i).card) ∨
    53 SmallSideBound 128 Gamma Delta B.card
    54
    55end Lax54.BipartiteCombLemma
    56
    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…