OAI/Combinatorics/ContingencyTables/Transport/FiniteMedianConfidence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContingencyTables.FiniteMedianConfidence.median_confidence_real line 16

   Source documentation

   Rational thresholds used only in the proof permit direct reuse of finite median amplification when the intended target is a real number.

   theorem median_confidence_real {X : Type*} [Fintype X] [Nonempty X]
       (output : X → ℚ) (L L' U' U : ℝ) (hL : L < L') (hU : U' < U)
       (delta : ℚ) (hdelta : 0 < delta)
       (hbad : uniformAverage (fun x =>
         if (output x:ℝ) < L' ∨ U' < (output x:ℝ) then (1:ℝ) else 0) ≤ 5/16) :
       1-(delta:ℝ) ≤ uniformAverage (fun xs : Fin (repetitionCount delta) → X =>
         if L ≤ (rationalMedian (List.ofFn (fun i => output (xs i))):ℝ) ∧
           (rationalMedian (List.ofFn (fun i => output (xs i))):ℝ) ≤ U
         then (1:ℝ) else 0) := by
   …

2. lemma OAI.ContingencyTables.FiniteMedianConfidence.rationalMedian_mem line 59