OAI/Combinatorics/ContingencyTables/Transport/FiniteIndependentFailures.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Coordinate marginals and a union bound for independent finite blocks

  1. lemma OAI.ContingencyTables.FiniteIndependentAverages.uniformAverage_coordinate line 15
  2. lemma OAI.ContingencyTables.FiniteIndependentAverages.uniform_union_bound line 24
  3. theorem OAI.ContingencyTables.FiniteIndependentAverages.independent_union_failure line 44

    Source documentation

    Each block is an actual independently uniform finite experiment. The event may test a different observable on each block.

    theorem independent_union_failure {J : Type*} [Fintype J] {X : J → Type*}
    [∀ j,Fintype (X j)] [∀ j,Nonempty (X j)] (bad : (j : J) → X j → Prop) :
    uniformAverage (fun draws : (j : J) → X j =>
      if ∃ j,bad j (draws j) then (1:ℝ) else 0) ≤
      ∑ j,uniformAverage (fun x : X j => if bad j x then (1:ℝ) else 0) := by
…