Lax Lean Archive

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

Coupled route sampling with shared vertex images

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

    Choose independently a uniform image for every source vertex, then sample one graph route per source edge from its conditional endpoint law. Positive outcomes give every route the chosen images of its source endpoints. Each edge's route has the original route distribution. Routes of two nonincident source edges have its independent product law, because the four source endpoints have independently chosen images.

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

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

    1 joint_normalized proven

    2 joint_valid proven

    3 nonincident_edge_law proven

    4 single_edge_law proven

    Lean source view on GitHub

    1import Lax263307.ConditionalRoutes
    2import Lax263307.FiniteProductSampling
    3
    4/-!
    5---
    6title: Coupled route sampling with shared vertex images
    7type: theorem
    8---
    9Choose independently a uniform image for every source vertex, then sample
    10one graph route per source edge from its conditional endpoint law. Positive
    11outcomes give every route the chosen images of its source endpoints.
    12Each edge's route has the original route distribution. Routes of two
    13nonincident source edges have its independent product law, because the four
    14source endpoints have independently chosen images.
    15
    16# Formalization notes
    17
    18The finite outcome is a pair consisting of a source-vertex image assignment
    19and a route-index assignment. Edge endpoints are given explicitly by two
    20maps; the marginal assertions require distinct endpoints for a single edge
    21and four distinct endpoints for a pair. The construction does not assume
    22independence for incident source edges.
    23
    24# Attribution
    25
    26Bonnet–Chang, the coupled sampling construction in Lemma 11.
    27-/
    28
    29namespace Lax263307.CoupledRouteSampling
    30
    31open Lax263307.RouteDistributions Lax263307.ConditionalRoutes
    32open Lax263307.FiniteProductSampling
    33
    34noncomputable def uniformWeight (n : ℕ) : Fin n → ℝ := fun _ => 1 / (n : ℝ)
    35
    36noncomputable def jointWeight {n q t m : ℕ} {G : SimpleGraph (Fin n)}
    37 (D : Distribution G q) (a b : Fin m → Fin t)
    38 (φ : Fin t → Fin n) (ψ : Fin m → Fin q) : ℝ :=
    39 weight (fun _ : Fin t => uniformWeight n) φ *
    40 weight (fun e => conditional D (φ (a e)) (φ (b e))) ψ
    41
    42axiom joint_normalized {n q t m : ℕ} {G : SimpleGraph (Fin n)}
    43 (D : Distribution G q) (hn : 0 < n) (a b : Fin m → Fin t) :
    44 (∀ φ ψ, 0 ≤ jointWeight D a b φ ψ) ∧
    45 (∑ φ, ∑ ψ, jointWeight D a b φ ψ) = 1
    46
    47axiom joint_valid {n q t m : ℕ} {G : SimpleGraph (Fin n)}
    48 (D : Distribution G q) (hn : 0 < n) (a b : Fin m → Fin t)
    49 (φ : Fin t → Fin n) (ψ : Fin m → Fin q) (positive : 0 < jointWeight D a b φ ψ) :
    50 ∀ e, (D.route (ψ e)).head? = some (φ (a e)) ∧
    51 (D.route (ψ e)).getLast? = some (φ (b e)) ∧
    52 (D.route (ψ e)).Nodup ∧ (D.route (ψ e)).IsChain G.Adj
    53
    54axiom single_edge_law {n q t m : ℕ} {G : SimpleGraph (Fin n)}
    55 (D : Distribution G q) (hn : 0 < n) (a b : Fin m → Fin t)
    56 (e : Fin m) (nonloop : a e ≠ b e) (i : Fin q) :
    57 (∑ φ, ∑ ψ, jointWeight D a b φ ψ * (if ψ e = i then (1 : ℝ) else 0)) =
    58 D.probability i
    59
    60axiom nonincident_edge_law {n q t m : ℕ} {G : SimpleGraph (Fin n)}
    61 (D : Distribution G q) (hn : 0 < n) (a b : Fin m → Fin t)
    62 (e f : Fin m) (nonincident : Function.Injective ![a e, b e, a f, b f]) (i j : Fin q) :
    63 (∑ φ, ∑ ψ, jointWeight D a b φ ψ *
    64 ((if ψ e = i then (1 : ℝ) else 0) * (if ψ f = j then (1 : ℝ) else 0))) =
    65 D.probability i * D.probability j
    66
    67end Lax263307.CoupledRouteSampling
    68
    Show ProofShow ProofShow ProofShow Proof
    Formalization notes

    The finite outcome is a pair consisting of a source-vertex image assignment and a route-index assignment. Edge endpoints are given explicitly by two maps; the marginal assertions require distinct endpoints for a single edge and four distinct endpoints for a pair. The construction does not assume independence for incident source edges.

    Attribution

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