OAI/Combinatorics/ContingencyTables/Rooted/RootedFarMass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.RootedFarMass.actualWeight line 14
2. def OAI.ContingencyTables.RootedFarMass.actualPenalty line 17
3. lemma OAI.ContingencyTables.RootedFarMass.weight_at_large_penalty line 20
4. theorem OAI.ContingencyTables.RootedFarMass.far_mass_le line 35

   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) (R : RootedCompletion.Selection A.T) (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 R a
         then actualWeight A R alpha a else 0) ≤ (2:ℝ)^(-(3*K:ℕ):ℝ) := by
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedFarMass.actualPenalty, OAI.ContingencyTables.RootedFarMass.actualWeight