Lax Lean Archive

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

Choosing a collision-free outcome with bounded total path length

Lax263307.SamplingOutcomes · concepts/Lax263307/SamplingOutcomes.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 finite probability distribution, suppose the probability of a bad outcome is at most 1/41/4 and a nonnegative total cost has expectation at most M>0M>0. Some outcome of positive probability is not bad and has total cost at most 4M4M. This combines the union bound with Markov's inequality.

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

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

    1 good_outcome proven

    2 markov_bound proven

    Lean source view on GitHub

    1import Lax263307.PathSampling
    2
    3/-!
    4---
    5title: Choosing a collision-free outcome with bounded total path length
    6type: theorem
    7---
    8For a finite probability distribution, suppose the probability of a bad
    9outcome is at most 1/41/4 and a nonnegative total cost has expectation at most
    10M>0M>0. Some outcome of positive probability is not bad and has total cost
    11at most 4M4M. This combines the union bound with Markov's inequality.
    12
    13# Attribution
    14
    15Bonnet–Chang, the simultaneous choice of noninteracting routes and bounded
    16total path length in Lemma 11.
    17-/
    18
    19namespace Lax263307.SamplingOutcomes
    20
    21open PathSampling
    22
    23/-- Probability of an event in the finite outcome space. -/
    24noncomputable def eventProbability {n q : ℕ} (P : Distribution n q)
    25 (event : Set (Fin q)) : ℝ := by
    26 classical
    27 exact ∑ i, if i ∈ event then P.probability i else 0
    28
    29/-- Markov's inequality for a nonnegative cost and a positive threshold. -/
    30axiom markov_bound {n q : ℕ} (P : Distribution n q) (cost : Fin q → ℝ)
    31 (nonnegative : ∀ i, 0 ≤ cost i) (T : ℝ) (positive : 0 < T) :
    32 eventProbability P {i | T < cost i} ≤ (∑ i, P.probability i * cost i) / T
    33
    34/-- One positive-probability outcome meets both requirements. -/
    35axiom good_outcome {n q : ℕ} (P : Distribution n q) (bad : Set (Fin q))
    36 (cost : Fin q → ℝ) (M : ℝ) (positive : 0 < M)
    37 (nonnegative : ∀ i, 0 ≤ cost i)
    38 (bad_bound : eventProbability P bad ≤ 1 / 4)
    39 (expected_bound : (∑ i, P.probability i * cost i) ≤ M) :
    40 ∃ i, 0 < P.probability i ∧ i ∉ bad ∧ cost i ≤ 4 * M
    41
    42end Lax263307.SamplingOutcomes
    43
    Show ProofShow Proof

    Attribution

    Bonnet–Chang, the simultaneous choice of noninteracting routes and bounded total path length 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…