Lax Lean Archive

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

A good coupled sample with bounded total route size

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

    For a source graph with mm edges, the expected total sampled route size is mm times the single-route expectation. The probability that some pair of nonincident routes intersects or has a host edge between them is at most m2m^2 times the sum of the single-pair collision and adjacency probabilities. If that bound is at most 1/41/4 and the expected total size is at most M>0M>0, there is a positive-probability sample with no such interaction and total route size at most 4M4M.

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

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

    1 bad_probability_bound proven

    2 good_route_sample proven

    3 total_length_expectation proven

    Lean source view on GitHub

    1import Lax263307.CoupledRouteSampling
    2import Lax263307.SamplingOutcomes
    3
    4/-!
    5---
    6title: A good coupled sample with bounded total route size
    7type: theorem
    8---
    9For a source graph with mm edges, the expected total sampled route size is
    10mm times the single-route expectation. The probability that some pair of
    11nonincident routes intersects or has a host edge between them is at most
    12m2m^2 times the sum of the single-pair collision and adjacency probabilities.
    13If that bound is at most 1/41/4 and the expected total size is at most M>0M>0,
    14there is a positive-probability sample with no such interaction and total
    15route size at most 4M4M.
    16
    17# Attribution
    18
    19Bonnet–Chang, the union bound and Markov step in Lemma 11.
    20-/
    21
    22namespace Lax263307.CoupledSamplingBounds
    23
    24open Lax263307.RouteDistributions Lax263307.CoupledRouteSampling
    25
    26noncomputable def Interaction {n q : ℕ} (G : SimpleGraph (Fin n))
    27 (D : Distribution G q) (i j : Fin q) : Prop :=
    28 ¬Disjoint (D.route i).toFinset (D.route j).toFinset ∨
    29 ∃ u ∈ (D.route i).toFinset, ∃ v ∈ (D.route j).toFinset, G.Adj u v
    30
    31noncomputable instance {n q : ℕ} (G : SimpleGraph (Fin n))
    32 (D : Distribution G q) (i j : Fin q) : Decidable (Interaction G D i j) := Classical.propDecidable _
    33
    34noncomputable def badProbability {n q t m : ℕ} (G : SimpleGraph (Fin n))
    35 (D : Distribution G q) (a b : Fin m → Fin t) : ℝ := by
    36 classical
    37 exact ∑ φ, ∑ ψ, if ∃ e f, Function.Injective ![a e, b e, a f, b f] ∧ Interaction G D (ψ e) (ψ f)
    38 then jointWeight D a b φ ψ else 0
    39
    40axiom total_length_expectation {n q t m : ℕ} {G : SimpleGraph (Fin n)}
    41 (D : Distribution G q) (hn : 0 < n) (a b : Fin m → Fin t)
    42 (nonloop : ∀ e, a e ≠ b e) :
    43 (∑ φ, ∑ ψ, jointWeight D a b φ ψ * (∑ e, ((D.route (ψ e)).toFinset.card : ℝ))) =
    44 (m : ℝ) * Lax263307.PathSampling.expectedSize D.toSampling
    45
    46axiom bad_probability_bound {n q t m : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    47 (D : Distribution G q) (hn : 0 < n) (a b : Fin m → Fin t) :
    48 badProbability G D a b ≤ (m : ℝ) ^ 2 *
    49 (Lax263307.PathSampling.collisionProbability D.toSampling +
    50 Lax263307.PathSampling.adjacencyProbability G D.toSampling)
    51
    52axiom good_route_sample {n q t m : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    53 (D : Distribution G q) (hn : 0 < n) (a b : Fin m → Fin t) (nonloop : ∀ e, a e ≠ b e)
    54 (M : ℝ) (positive : 0 < M)
    55 (bad_budget : (m : ℝ) ^ 2 * (Lax263307.PathSampling.collisionProbability D.toSampling +
    56 Lax263307.PathSampling.adjacencyProbability G D.toSampling) ≤ 1 / 4)
    57 (length_budget : (m : ℝ) * Lax263307.PathSampling.expectedSize D.toSampling ≤ M) :
    58 ∃ φ : Fin t → Fin n, ∃ ψ : Fin m → Fin q,
    59 0 < jointWeight D a b φ ψ ∧
    60 (∀ e f, Function.Injective ![a e, b e, a f, b f] → ¬Interaction G D (ψ e) (ψ f)) ∧
    61 (∑ e, ((D.route (ψ e)).toFinset.card : ℝ)) ≤ 4 * M
    62
    63end Lax263307.CoupledSamplingBounds
    64
    Show ProofShow ProofShow Proof

    Attribution

    Bonnet–Chang, the union bound and Markov step 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…