OAI/Combinatorics/ContingencyTables/Rooted/ForestScaledBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.ForestScaledPenalty.rowCounts line 16
2. def OAI.ContingencyTables.ForestScaledPenalty.columnCounts line 19
3. lemma OAI.ContingencyTables.ForestScaledPenalty.rowCounts_bounds line 22
4. lemma OAI.ContingencyTables.ForestScaledPenalty.columnCounts_bounds line 31
5. lemma OAI.ContingencyTables.ForestScaledPenalty.rootConstant_bound line 36
6. def OAI.ContingencyTables.ForestScaledPenalty.zeroAssignment line 65
7. lemma OAI.ContingencyTables.ForestScaledPenalty.integerCube_zero line 68
8. lemma OAI.ContingencyTables.ForestScaledPenalty.zero_tree_bound line 72
9. theorem OAI.ContingencyTables.ForestScaledPenalty.penalty_cube_bound line 102

   Source documentation

   The 1/8 local change bound and the actual baseline root/tree bounds give D(v)≤H throughout the entire continuous bin cube, including its boundary and the empty free-coordinate case.

   theorem penalty_cube_bound (A : Instance I J) (C B : ℝ) (hC : 0 ≤ C) (hB : 0 < B)
       (z : View A → ℕ) (hz : InBox (bounds A) z)
       (v : FreeCell A.small A.T → ℝ) (hv : ∀ f,0 ≤ v f ∧ v f ≤ B) :
       0 ≤ penalty A C B (rowCounts A z) (columnCounts A z) v ∧
         penalty A C B (rowCounts A z) (columnCounts A z) v ≤ C*(10*(A.d:ℝ)^2*((A.W:ℝ)+1)) := by
   …

   Mentions: OAI.ContingencyTables.ForestScaledPenalty.penalty, OAI.ContingencyTables.ForestScaledPenalty.rowCounts, OAI.ContingencyTables.ForestScaledPenalty.columnCounts