Lax Lean Archive

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

An induced almost-embedding from a good route sample

Lax263307.SampledAlmostEmbeddings · concepts/Lax263307/SampledAlmostEmbeddings.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

    Sample the edges of any finite simple source graph from a uniform-endpoint route distribution. If the interaction union bound is at most 1/41/4 and the expected total route size is at most M>0M>0, some sample gives an induced almost-embedding of total route size at most 4M4M.

    Concept map
    24 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax263307.CoupledSamplingBounds
    2import Lax263307.AlmostEmbeddings
    3
    4/-!
    5---
    6title: An induced almost-embedding from a good route sample
    7type: theorem
    8---
    9Sample the edges of any finite simple source graph from a uniform-endpoint
    10route distribution. If the interaction union bound is at most 1/41/4 and
    11the expected total route size is at most M>0M>0, some sample gives an induced
    12almost-embedding of total route size at most 4M4M.
    13
    14# Formalization notes
    15
    16Enumerate unordered source edges only for the finite sampling construction.
    17Their two endpoints are distinct, and nonincident edges have four distinct
    18endpoints. A sampled route's ordered vertex list is a graph walk, so its
    19vertex set induces a connected graph. The shared vertex-image assignment
    20provides the endpoint condition in the almost-embedding.
    21
    22# Attribution
    23
    24Bonnet–Chang, the initial induced almost-embedding in Lemma 11.
    25-/
    26
    27namespace Lax263307.SampledAlmostEmbeddings
    28
    29open Lax263307.RouteDistributions Lax263307.AlmostEmbeddings
    30
    31axiom exists_induced_almost_embedding {t n q : ℕ} (H : SimpleGraph (Fin t)) [DecidableRel H.Adj]
    32 (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (D : Distribution G q) (hn : 0 < n)
    33 (M : ℝ) (positive : 0 < M)
    34 (bad_budget : (H.edgeSet.ncard : ℝ) ^ 2 * (Lax263307.PathSampling.collisionProbability D.toSampling +
    35 Lax263307.PathSampling.adjacencyProbability G D.toSampling) ≤ 1 / 4)
    36 (length_budget : (H.edgeSet.ncard : ℝ) * Lax263307.PathSampling.expectedSize D.toSampling ≤ M) :
    37 ∃ E : AlmostEmbedding H G, IsInduced E ∧ (∑ e, ((E.route e).card : ℝ)) ≤ 4 * M
    38
    39end Lax263307.SampledAlmostEmbeddings
    40
    Show Proof
    Formalization notes

    Enumerate unordered source edges only for the finite sampling construction. Their two endpoints are distinct, and nonincident edges have four distinct endpoints. A sampled route's ordered vertex list is a graph walk, so its vertex set induces a connected graph. The shared vertex-image assignment provides the endpoint condition in the almost-embedding.

    Attribution

    Bonnet–Chang, the initial induced almost-embedding in Lemma 11.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…