Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Deleting high-degree vertices in an independent blow-up

Lax263307.BlowUpDeletion · concepts/Lax263307/BlowUpDeletion.lean · lax-263307

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

    Theorem

    Let HH be an independent blow-up of a graph of treewidth at most ww. Delete the vertices XX whose degree exceeds an integer threshold ss. Then s∣X∣≤2∣E(H)∣s|X|\le 2|E(H)|, and HH has a tree decomposition with bags of size at most

    ∣X∣+max⁡{1,s(w+1)}.|X|+\max\{1,s(w+1)\}.

    Large fibres become isolated after this deletion. The remaining nonisolated vertices therefore embed into a blow-up with at most ss copies per vertex. The maximum with one covers singleton bags for isolated vertices, including the edgeless case and threshold zero.

    Concept map
    7 concepts; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.

    1 deletion_decomposition proven

    2 high_degree_card proven

    3 power_bound proven

    Lean source view on GitHub

    1import Lax263307.BlowUpDecompositions
    2import Mathlib.Combinatorics.SimpleGraph.DegreeSum
    3import Mathlib.Analysis.SpecialFunctions.Pow.Real
    4
    5/-!
    6---
    7title: Deleting high-degree vertices in an independent blow-up
    8type: theorem
    9---
    10Let HH be an independent blow-up of a graph of treewidth at most ww.
    11Delete the vertices XX whose degree exceeds an integer threshold ss.
    12Then s∣X∣≤2∣E(H)∣s|X|\le 2|E(H)|, and HH has a tree decomposition with bags of size
    13at most
    14∣X∣+max⁡{1,s(w+1)}.|X|+\max\{1,s(w+1)\}.
    15
    16Large fibres become isolated after this deletion. The remaining nonisolated
    17vertices therefore embed into a blow-up with at most ss copies per vertex.
    18The maximum with one covers singleton bags for isolated vertices, including
    19the edgeless case and threshold zero.
    20
    21# Attribution
    22
    23Bonnet–Chang, the structural estimate in the proof of Lemma 16.
    24-/
    25
    26namespace Lax263307.BlowUpDeletion
    27
    28open IndependentBlowUp Lax228581.Treewidth
    29
    30/-- The vertices removed at degree threshold `s`. -/
    31noncomputable def highDegree {n : ℕ} (G : SimpleGraph (Fin n))
    32 (copies : Fin n → ℕ) (s : ℕ) : Finset (Vertex copies) := by
    33 classical
    34 exact Finset.univ.filter fun v => s < (graph G copies).degree v
    35
    36/-- The degree sum bounds the number of removed vertices. -/
    37axiom high_degree_card {n : ℕ} (G : SimpleGraph (Fin n))
    38 (copies : Fin n → ℕ) (s : ℕ) :
    39 s * (highDegree G copies s).card ≤ 2 * (graph G copies).edgeSet.ncard
    40
    41/-- Lift bounded fibres, add singleton bags, and restore the deleted set. -/
    42axiom deletion_decomposition {n : ℕ} (G : SimpleGraph (Fin n))
    43 (copies : Fin n → ℕ) (s w : ℕ) (width : HasTreewidthAtMost G w) :
    44 ∃ D : TreeDecomposition (graph G copies),
    45 ∀ i, (D.bag i).card ≤ (highDegree G copies s).card + max 1 (s * (w + 1))
    46
    47/-- Choosing the degree threshold balances the two terms of the estimate. -/
    48axiom power_bound {n : ℕ} (G : SimpleGraph (Fin n))
    49 (copies : Fin n → ℕ) (w : ℕ) (b c : ℝ) (hb : 0 ≤ b) (hb₁ : b < 1)
    50 (hc : 0 < c) (width : HasTreewidthAtMost G w)
    51 (width_bound : (w + 1 : ℕ) ≤
    52 c * Real.rpow ((graph G copies).edgeSet.ncard + 1) b) :
    53 ∃ D : TreeDecomposition (graph G copies), ∀ i,
    54 ((D.bag i).card : ℝ) ≤ (3 + 2 * c) *
    55 Real.rpow ((graph G copies).edgeSet.ncard + 1) ((1 + b) / 2)
    56
    57end Lax263307.BlowUpDeletion
    58
    Show ProofShow ProofShow Proof

    Attribution

    Bonnet–Chang, the structural estimate in the proof of Lemma 16.

    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…