Lax Lean Archive

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

Finite independent sampling and vertex exception tails

Lax342547.FiniteSampling · concepts/Lax342547/FiniteSampling.lean · lax-342547

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

    Lemma

    Finite product weights form a probability law. Cylinder events factor over sample positions, and a subset union bound gives the binomial estimate for too many positions in a raw vertex exception.

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

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

    1 cell_mass_mono proven

    2 cell_mass_union_bound proven

    3 coordinate_set_probability proven

    4 cylinder_probability proven

    5 exceptional_positions_bound proven

    6 product_probability proven

    Lean source view on GitHub

    1import Lax342547.ContainerLaws
    2import Mathlib.Algebra.BigOperators.Ring.Finset
    3
    4/-!
    5---
    6title: Finite independent sampling and vertex exception tails
    7type: lemma
    8---
    9Finite product weights form a probability law. Cylinder events factor over sample positions, and a subset union bound gives the binomial estimate for too many positions in a raw vertex exception.
    10-/
    11
    12namespace Lax342547.FiniteSampling
    13
    14open Lax342547.RelativeEntropy Lax342547.RetainedImages
    15open scoped BigOperators
    16
    17noncomputable def productLaw {ι Ω : Type} [Fintype ι] (μ : ι → Ω → ℝ) (sample : ι → Ω) : ℝ :=
    18 ∏ i, μ i (sample i)
    19
    20axiom product_probability {ι Ω : Type} [Fintype ι] [Fintype Ω] [DecidableEq ι]
    21 (μ : ι → Ω → ℝ) (hμ : ∀ i, Probability (μ i)) : Probability (productLaw μ)
    22
    23axiom cylinder_probability {ι Ω : Type} [Fintype ι] [Fintype Ω] [DecidableEq ι]
    24 (μ : ι → Ω → ℝ) (A : ι → Ω → Prop) :
    25 cellMass (productLaw μ) (fun sample => ∀ i, A i (sample i)) = ∏ i, cellMass (μ i) (A i)
    26
    27axiom coordinate_set_probability {ι Ω : Type} [Fintype ι] [Fintype Ω] [DecidableEq ι]
    28 (μ : Ω → ℝ) (T : Finset ι) (S : Ω → Prop) (hμ : Probability μ) :
    29 cellMass (productLaw (fun _ : ι => μ)) (fun sample => ∀ i ∈ T, S (sample i)) =
    30 (cellMass μ S)^T.card
    31
    32axiom cell_mass_mono {Ω : Type} [Fintype Ω]
    33 (ρ : Ω → ℝ) (S T : Ω → Prop) (hρ : ∀ x, 0 ≤ ρ x) (hST : ∀ x, S x → T x) :
    34 cellMass ρ S ≤ cellMass ρ T
    35
    36axiom cell_mass_union_bound {Ω J : Type} [Fintype Ω]
    37 (ρ : Ω → ℝ) (A : J → Ω → Prop) (T : Finset J) (hρ : ∀ x, 0 ≤ ρ x) :
    38 cellMass ρ (fun x => ∃ j ∈ T, A j x) ≤ ∑ j ∈ T, cellMass ρ (A j)
    39
    40axiom exceptional_positions_bound {ι Ω : Type} [Fintype ι] [Fintype Ω] [DecidableEq ι]
    41 (μ : Ω → ℝ) (S : Ω → Prop) (k : ℕ) (hμ : Probability μ) : by
    42 classical
    43 exact cellMass (productLaw (fun _ : ι => μ))
    44 (fun sample => k ≤ (Finset.univ.filter (fun i => S (sample i))).card) ≤
    45 (Fintype.card ι).choose k*(cellMass μ S)^k
    46
    47end Lax342547.FiniteSampling
    48
    Show ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…