OAI/Combinatorics/ContingencyTables/Rooted/RootedWarmReturn.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.RootedWarmReturn.weighted_error line 23
2. lemma OAI.ContingencyTables.RootedWarmReturn.push_observation line 34
3. theorem OAI.ContingencyTables.RootedWarmReturn.distance_of_events line 40
4. def OAI.ContingencyTables.RootedWarmReturn.returnLaw line 64
5. def OAI.ContingencyTables.RootedWarmReturn.returnKernel line 71
6. lemma OAI.ContingencyTables.RootedWarmReturn.return_observation line 77
7. theorem OAI.ContingencyTables.RootedWarmReturn.warm_cap_loss line 87
8. lemma OAI.ContingencyTables.RootedWarmReturn.returnKernel_stochastic line 117
9. theorem OAI.ContingencyTables.RootedWarmReturn.weighted_return_event line 125
10. theorem OAI.ContingencyTables.RootedWarmReturn.warm_return_distance line 164

    Source documentation

    This is the law of the implemented Boolean return, compared to the literal trace on the same incoming warm distribution.

    theorem warm_return_distance (A : Instance I J) (R : RootedCompletion.Selection A.T) (C : ℕ) (hC : 0<C) (K j k n : ℕ)
        (hK : 1≤K) (hW : 100*A.d*K≤A.W) (hB : (K:ℝ)=binWidth A C)
        (hj : j≤rationalHeight A C) (xi : ℚ) (hx0 : 0<xi) (hx1 : xi≤1/4)
        (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
        (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) K))
    …

    Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger