OAI/Combinatorics/ContingencyTables/Rooted/RootedEstimatorMedianLaw.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The executed inner median is the analysed amplified weight oracle

  1. def OAI.ContingencyTables.RootedEstimatorMedianProgram.context line 18
  2. def OAI.ContingencyTables.RootedEstimatorMedianProgram.value line 22
  3. theorem OAI.ContingencyTables.RootedEstimatorMedianProgram.sameLaw line 31

    Source documentation

    Exact observable transport, including the outputs on inaccurate sample histories, lets the original median analysis apply unchanged.

    theorem sameLaw (A : Instance (Fin m) (Fin n)) (C K j : ℕ)
    (hC : 0 < C) (hj : j ≤ rationalHeight A C) (hK : 1 ≤ K)
    (hW : 100*A.d*K ≤ A.W) (hB : (K:ℝ)=CompanionOracleDensity.binWidth A C)
    (epsilon delta : ℚ) (he : 0 < epsilon)
    (z : View A → ℕ) (hz : BalancedBox.InBox (bounds A) z)
    (v : Grid (I := Fin (RootedCatalogGrid.freeCount A)) K) (degree depth : List Bool)
…

    Mentions: OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.RootedCatalogGrid.freeCount

  4. theorem OAI.ContingencyTables.RootedEstimatorMedianProgram.success line 75