Lax Lean Archive

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

Finite sequential tests

Lax342547.SequentialTests · concepts/Lax342547/SequentialTests.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

    Independent finite draws satisfy sequential lower bounds under prefix-dependent tests, including a bounded sampling horizon.

    Concept map
    14 concepts; 8 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 accepts_pointwise proven

    2 bounded_sequential_failure_lower proven

    3 bounded_sequential_lower_probability proven

    4 safe_failure_mass proven

    5 sequential_failure_lower proven

    6 sequential_lower_probability proven

    7 step_probability proven

    Lean source view on GitHub

    1import Lax342547.FiniteSampling
    2import Mathlib.Data.Fin.Tuple.Basic
    3
    4/-!
    5---
    6title: Finite sequential tests
    7type: lemma
    8---
    9Independent finite draws satisfy sequential lower bounds under prefix-dependent tests, including a bounded sampling horizon.
    10-/
    11
    12namespace Lax342547.SequentialTests
    13
    14open Lax342547.MomentSpace Lax342547.RelativeEntropy Lax342547.RetainedImages Lax342547.FiniteSampling
    15open scoped BigOperators
    16
    17def accepts {Ω : Type} (P : ∀ j,(Fin j → Ω) → Ω → Prop) : ∀ n,(Fin n → Ω) → Prop
    18 | 0,_ => True
    19 | n+1,s => accepts P n (Fin.init s) ∧ P n (Fin.init s) (s (Fin.last n))
    20
    21axiom step_probability {Ω : Type} [Fintype Ω] (μ : Ω → ℝ)
    22 (P : ∀ j,(Fin j → Ω) → Ω → Prop) (n : ℕ) :
    23 by
    24 classical
    25 exact cellMass (productLaw (fun _ : Fin (n+1) => μ)) (accepts P (n+1)) =
    26 ∑ s : Fin n → Ω,productLaw (fun _ : Fin n => μ) s*
    27 (if accepts P n s then cellMass μ (P n s) else 0)
    28
    29axiom sequential_lower_probability {Ω : Type} [Fintype Ω] (μ : Ω → ℝ)
    30 (P : ∀ j,(Fin j → Ω) → Ω → Prop) (c : ℝ)
    31 (hμ : Probability μ) (hc : 0 ≤ c)
    32 (hstep : ∀ j s,accepts P j s → c ≤ cellMass μ (P j s)) (n : ℕ) :
    33 c^n ≤ cellMass (productLaw (fun _ : Fin n => μ)) (accepts P n)
    34
    35axiom bounded_sequential_lower_probability {Ω : Type} [Fintype Ω] (μ : Ω → ℝ)
    36 (P : ∀ j,(Fin j → Ω) → Ω → Prop) (c : ℝ)
    37 (hμ : Probability μ) (hc : 0 ≤ c)
    38 (n : ℕ) (hstep : ∀ j,j < n → ∀ s,accepts P j s → c ≤ cellMass μ (P j s)) :
    39 c^n ≤ cellMass (productLaw (fun _ : Fin n => μ)) (accepts P n)
    40
    41axiom safe_failure_mass {Ω : Type} [Fintype Ω] (μ : Ω → ℝ)
    42 (F S : Ω → Prop) (hμ : ∀ x,0 ≤ μ x) :
    43 cellMass μ F-cellMass μ (fun x => ¬ S x) ≤ cellMass μ (fun x => F x ∧ S x)
    44
    45axiom sequential_failure_lower {Ω : Type} [Fintype Ω] (μ : Ω → ℝ)
    46 (F : Ω → Prop) (S : ∀ j,(Fin j → Ω) → Ω → Prop) (η δ : ℝ)
    47 (hμ : Probability μ) (hgap : δ ≤ η) (hF : η ≤ cellMass μ F)
    48 (havoid : ∀ j s,accepts (fun j s x => F x ∧ S j s x) j s →
    49 cellMass μ (fun x => ¬ S j s x) ≤ δ) (n : ℕ) :
    50 (η-δ)^n ≤ cellMass (productLaw (fun _ : Fin n => μ))
    51 (accepts (fun j s x => F x ∧ S j s x) n)
    52
    53axiom bounded_sequential_failure_lower {Ω : Type} [Fintype Ω] (μ : Ω → ℝ)
    54 (F : Ω → Prop) (S : ∀ j,(Fin j → Ω) → Ω → Prop) (η δ : ℝ)
    55 (hμ : Probability μ) (hgap : δ ≤ η) (hF : η ≤ cellMass μ F)
    56 (n : ℕ) (havoid : ∀ j,j < n → ∀ s,accepts (fun j s x => F x ∧ S j s x) j s →
    57 cellMass μ (fun x => ¬ S j s x) ≤ δ) :
    58 (η-δ)^n ≤ cellMass (productLaw (fun _ : Fin n => μ))
    59 (accepts (fun j s x => F x ∧ S j s x) n)
    60
    61axiom accepts_pointwise {Ω : Type} (P : ∀ j,(Fin j → Ω) → Ω → Prop) (F : Ω → Prop)
    62 (hP : ∀ j t x,P j t x → F x) (n : ℕ) (s : Fin n → Ω)
    63 (hs : accepts P n s) : ∀ i,F (s i)
    64
    65end Lax342547.SequentialTests
    66
    Show ProofShow 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…