OAI/Combinatorics/ContingencyTables/Rooted/ForestScaledPenalty.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.ForestScaledPenalty.intervalCost line 16
2. lemma OAI.ContingencyTables.ForestScaledPenalty.intervalCost_nonnegative line 18
3. lemma OAI.ContingencyTables.ForestScaledPenalty.intervalCost_change line 20
4. lemma OAI.ContingencyTables.ForestScaledPenalty.intervalCost_combine line 39
5. def OAI.ContingencyTables.ForestScaledPenalty.normalizedOffset line 54
6. def OAI.ContingencyTables.ForestScaledPenalty.normalizedCoefficient line 58
7. def OAI.ContingencyTables.ForestScaledPenalty.scaledTree line 62
8. def OAI.ContingencyTables.ForestScaledPenalty.rootConstant line 66
9. def OAI.ContingencyTables.ForestScaledPenalty.penalty line 70
10. lemma OAI.ContingencyTables.ForestScaledPenalty.penalty_nonnegative line 74
11. lemma OAI.ContingencyTables.ForestScaledPenalty.free_card_le line 83
12. lemma OAI.ContingencyTables.ForestScaledPenalty.tree_card_le line 87
13. theorem OAI.ContingencyTables.ForestScaledPenalty.penalty_change line 93

    Source documentation

    All coefficients are obtained from the actual maximum-forest cuts. The bound is 2*C*d²/B, which equals 1/8 for the source B=16*C*d².

    theorem penalty_change (A : Instance I J) (C B : ℝ) (hC : 0 ≤ C) (hB : 0 < B)
        (x q : I → J → ℤ) (v w : FreeCell A.small A.T → ℝ) (r : ℝ) (hr : 0 ≤ r)
        (hvw : ∀ f,|v f-w f| ≤ r) :
        |penalty A C B x q v-penalty A C B x q w| ≤ (2*C*(A.d:ℝ)^2/B)*r := by
    …

    Mentions: OAI.ContingencyTables.ForestScaledPenalty.penalty

14. theorem OAI.ContingencyTables.ForestScaledPenalty.penalty_convex line 122
15. theorem OAI.ContingencyTables.ForestScaledPenalty.penalty_continuous line 140