OAI/Combinatorics/ContingencyTables/Counting/CompanionFarMass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.CompanionFarMass.actualWeight line 15
2. def OAI.ContingencyTables.CompanionFarMass.actualPenalty line 19
3. lemma OAI.ContingencyTables.CompanionFarMass.weight_at_large_penalty line 23
4. theorem OAI.ContingencyTables.CompanionFarMass.far_mass_le line 38

   Source documentation

   The true expanded physical box has at most 2^K summands, so the entire terminal region whose penalty is at least 4K contributes at most 2^(-3K). Neither a table-count approximation nor an oracle is assumed.

   theorem far_mass_le (A : Instance I J) (alpha : ℝ) (B K : ℕ)
       (hW : 20*A.d ≤ A.W) (hB : (∏ a : I×J,(A.b a.1 a.2+1)) ≤ 2^B) (hBK : 2*B ≤ K) :
       (∑ a : Profiles (cellWidth A),if 4*(K:ℝ) ≤ alpha*actualPenalty A a
         then actualWeight A alpha a else 0) ≤ (2:ℝ)^(-(3*K:ℕ):ℝ) := by
   …

   Mentions: OAI.ContingencyTables.CompanionFarMass.actualPenalty, OAI.ContingencyTables.CompanionFarMass.actualWeight