OAI/Combinatorics/ContingencyTables/Rooted/RootedTerminalMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.RootedTerminalMass.total_near_mass_le line 21

   Source documentation

   Actual endpoint tables and the proved scalar signature estimates control the entire union of narrow tree violations.

   lemma total_near_mass_le (A : Instance I J) (R : RootedCompletion.Selection A.T) (E : Endpoints A) (alpha gamma : ℝ)
       (ha : 0 ≤ alpha) (hg : 0 < gamma) (hW : 20*A.d ≤ A.W) (B K : ℕ)
       (hB : (∏ a : I×J,(A.b a.1 a.2+1)) ≤ 2^B) (hBK : 2*B ≤ K) (hK : 0 < K) :
       (∑ t : TreeCell A,nearMass A R alpha t.val gamma) ≤
         (4*A.d*gamma*K:ℝ)*physicalMass A R alpha := by
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection

2. lemma OAI.ContingencyTables.RootedTerminalMass.mass_le_table_far_near line 44
3. theorem OAI.ContingencyTables.RootedTerminalMass.terminal_count_estimate line 75

   Source documentation

   The terminal normalizer estimate follows from the finite table bijection, root integrality, far bound and tree-marginal estimates. The manuscript's explicit choices of K, gamma and the final coefficient satisfy its arithmetic conditions.

   theorem terminal_count_estimate (A : Instance I J) (R : RootedCompletion.Selection A.T) (E : Endpoints A)
       (alpha gamma epsilon : ℝ) (B K : ℕ)
       (ha : 0 < alpha) (hg : 0 < gamma) (hg1 : gamma ≤ 1)
       (he : 0 < epsilon) (he1 : epsilon < 1)
       (hscale : 4*(K:ℝ) ≤ alpha*gamma) (hnear : 4*(A.d:ℝ)*gamma*K ≤ epsilon/128)
       (hfar : (2:ℝ)^(-(3*K:ℕ):ℝ) ≤ epsilon/128)
       (hW : 20*A.d ≤ A.W) (hB : (∏ a : I×J,(A.b a.1 a.2+1)) ≤ 2^B)
       (hBK : 2*B ≤ K) (hK : 0 < K) :
       tableCount A ≤ CommonBasesFPRAS.slotTotal TwoLiftStates.pairs (RootedFactorialApplication.f A R alpha) ∅ ∧
         CommonBasesFPRAS.slotTotal TwoLiftStates.pairs (RootedFactorialApplication.f A R alpha) ∅ ≤ (1+epsilon/32)*tableCount A := by
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.CommonBasesFPRAS.slotTotal, OAI.ContingencyTables.TwoLiftStates.pairs, OAI.ContingencyTables.RootedFactorialApplication.f