BatchProbability.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Reindexing the prescribed repeated tests preserves their probability budget. The finite adapted failure estimate therefore applies to the actual batch, with its repetitions, rather than just to distinct thresholds.

lemma OAI.SLEExactGauge.adapted_fin_successes_failure_exp_bound line 15
lemma OAI.SLEExactGauge.Target.repeated_batch_sum_eq line 64

theorem OAI.SLEExactGauge.repeated_batch_failure_bound line 99

Source documentation

Half of each centered success probability is enough for the paper's exponent, even when the tests are dependent and the thresholds repeat.

theorem repeated_batch_failure_bound
    {Ω : Type*} [mΩ : MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (F : Filtration ℕ mΩ) (κ : ℝ) (W : Target.WienerLaw) (n J : ℕ)
    (e : Fin J → ℤ × ℕ) (hi : Function.Injective e)
    (he : ∀ kj, kj ∈ Set.range e ↔ kj.2 < Target.multiplicity κ W n kj.1)
    (q : ℤ → ℝ) (hq0 : ∀ k, 0 ≤ q k) (hq1 : ∀ k, q k ≤ 1)
    (hbudget : (2:ℝ)^n/8 ≤ ∑' k, (Target.multiplicity κ W n k:ℝ)*q k)
    (success : Fin J → Set Ω)
    (hmeas : ∀ i, MeasurableSet[F (i.val+1)] (success i))
    (hstep : ∀ i (A : Set Ω), MeasurableSet[F i.val] A →
      ENNReal.ofReal (q (e i).1/2)*P A ≤ P (A∩success i)) :
    P (⋂ i, (success i)ᶜ) ≤ ENNReal.ofReal (Real.exp (-((2:ℝ)^n/16))) := by
…

Mentions: OAI.SLEExactGauge.Target.WienerLaw, OAI.SLEExactGauge.Target.multiplicity