Lax Lean Archive

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

Conditioning graph routes on uniform endpoints

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

    Multiply the probability of a route with endpoints (u,v)(u,v) by n2n^2 to obtain the conditional route law for this ordered endpoint pair. Every conditional law is a probability distribution supported on routes with those endpoints. Averaging over a uniformly sampled pair recovers the original law. Averaging independently over four endpoints gives the product law for two routes. These identities support sampling nonincident source edges while sharing endpoint images for incident edges.

    Concept map
    15 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 conditional_correct proven

    2 independent_pair_mixture proven

    3 mixture_identity proven

    Lean source view on GitHub

    1import Lax263307.RouteDistributions
    2
    3/-!
    4---
    5title: Conditioning graph routes on uniform endpoints
    6type: theorem
    7---
    8Multiply the probability of a route with endpoints (u,v)(u,v) by n2n^2 to
    9obtain the conditional route law for this ordered endpoint pair. Every
    10conditional law is a probability distribution supported on routes with
    11those endpoints. Averaging over a uniformly sampled pair recovers the
    12original law. Averaging independently over four endpoints gives the product
    13law for two routes. These identities support sampling nonincident source
    14edges while sharing endpoint images for incident edges.
    15
    16# Attribution
    17
    18Bonnet–Chang, the coupled route sampling construction in Lemma 11.
    19-/
    20
    21namespace Lax263307.ConditionalRoutes
    22
    23open Lax263307.RouteDistributions
    24
    25noncomputable def conditional {n q : ℕ} {G : SimpleGraph (Fin n)}
    26 (D : Distribution G q) (u v : Fin n) (i : Fin q) : ℝ :=
    27 if (D.route i).head? = some u ∧ (D.route i).getLast? = some v then
    28 (n : ℝ) ^ 2 * D.probability i else 0
    29
    30axiom conditional_correct {n q : ℕ} {G : SimpleGraph (Fin n)}
    31 (D : Distribution G q) (hn : 0 < n) (u v : Fin n) :
    32 (∀ i, 0 ≤ conditional D u v i) ∧ (∑ i, conditional D u v i) = 1 ∧
    33 (∀ i, 0 < conditional D u v i → (D.route i).head? = some u ∧
    34 (D.route i).getLast? = some v ∧ (D.route i).Nodup ∧ (D.route i).IsChain G.Adj)
    35
    36axiom mixture_identity {n q : ℕ} {G : SimpleGraph (Fin n)}
    37 (D : Distribution G q) (i : Fin q) :
    38 (∑ u, ∑ v, conditional D u v i) = (n : ℝ) ^ 2 * D.probability i
    39
    40axiom independent_pair_mixture {n q : ℕ} {G : SimpleGraph (Fin n)}
    41 (D : Distribution G q) (hn : 0 < n) (i j : Fin q) :
    42 (∑ u, ∑ v, ∑ s, ∑ t,
    43 conditional D u v i * conditional D s t j / (n : ℝ) ^ 4) =
    44 D.probability i * D.probability j
    45
    46end Lax263307.ConditionalRoutes
    47
    Show ProofShow ProofShow Proof

    Attribution

    Bonnet–Chang, the coupled route sampling construction 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…