OAI/Combinatorics/ContingencyTables/Transport/FiniteBiasedAverages.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Independent finite experiments with an explicitly bounded mean bias

  1. theorem OAI.ContingencyTables.FiniteIndependentAverages.sampleAverage_absolute_failure line 16
  2. lemma OAI.ContingencyTables.FiniteIndependentAverages.bounded_variance line 37
  3. theorem OAI.ContingencyTables.FiniteIndependentAverages.biased_target_failure line 49

    Source documentation

    The target is an exact mathematical mean; the experiment's own mean may differ, but only by the displayed deterministic bias.

    theorem biased_target_failure (g : X → ℝ) (U target delta : ℝ)
    (hg : ∀ x,0 ≤ g x ∧ g x ≤ U) (htarget : 0 < target) (hdelta : 0 < delta)
    (hbias : |uniformAverage g-target| ≤ delta*target/2)
    (N : ℕ) (hN : 0 < N) :
    uniformAverage (fun xs : Fin N → X =>
      if delta*target < |sampleAverage g N xs-target| then (1:ℝ) else 0) ≤
      4*U^2/(N*(delta*target)^2) := by
…

    Mentions: OAI.ContingencyTables.FiniteIndependentAverages.sampleAverage