OAI/NumberTheory/Ostmann/Arithmetic/SequentialSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Multiplying support bounds under the original independent prior

The test at a split can depend on the entire already exposed prefix. This records the order of exposure, so future validity never changes its law.

  1. def OAI.Ostmann.SplitSamples line 18
  2. instance OAI.Ostmann.splitSamplesFintype line 22
  3. def OAI.Ostmann.sequentialSupport line 27
  4. theorem OAI.Ostmann.sequentialSupport_nonneg line 32
  5. theorem OAI.Ostmann.sequentialSupport_average_le line 45

    Source documentation

    Prefix-adapted tests multiply their bounds without conditioning on the complete support event.

    theorem sequentialSupport_average_le {A : Type} [Fintype A] [Nonempty A]
    (test : List A → A → Prop) (ρ : ℝ) (hρ : 0 ≤ ρ)
    (htest : ∀ past, (Fintype.card A : ℝ)⁻¹ *
      (∑ x : A, if test past x then (1 : ℝ) else 0) ≤ ρ)
    (past : List A) (n : ℕ) :
    (Fintype.card A : ℝ)⁻¹ ^ n *
        (∑ x : SplitSamples A n, sequentialSupport test past n x) ≤ ρ ^ n := by
…

    Mentions: OAI.Ostmann.SplitSamples, OAI.Ostmann.sequentialSupport