OAI/Combinatorics/ContingencyTables/Transport/FiniteUniformHistory.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.FiniteUniformHistory.kernel line 15
2. lemma OAI.ContingencyTables.FiniteUniformHistory.kernel_nonneg line 17
3. lemma OAI.ContingencyTables.FiniteUniformHistory.kernel_mass line 21
4. lemma OAI.ContingencyTables.FiniteUniformHistory.expectation line 26
5. theorem OAI.ContingencyTables.FiniteUniformHistory.good_probability line 52

   Source documentation

   A history-dependent success predicate is evaluated on genuinely independent finite words; only its conditional one-step loss is assumed.

   theorem good_probability (Good : List X → Prop) (N : ℕ) (e : ℝ) (he : 0 ≤ e)
       (hstep : ∀ h,Good h → h.length<N →
         1-e ≤ uniformAverage (fun x : X => if Good (h++[x]) then (1:ℝ) else 0))
       (hzero : Good []) :
       1-(N:ℝ)*e ≤ uniformAverage (fun xs : Fin N → X =>
         if Good (List.ofFn xs) then (1:ℝ) else 0) := by
   …