OAI/Combinatorics/ContingencyTables/Rooted/RootedTreeBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContingencyTables.RootedTreeMarginal.scalar_soft_le_two_pow line 18
2. theorem OAI.ContingencyTables.RootedTreeMarginal.scalar_exact_nonnegative line 42
3. lemma OAI.ContingencyTables.RootedTreeMarginal.scalar_exact_le_soft line 49
4. theorem OAI.ContingencyTables.RootedTreeMarginal.scalar_exact_half_window line 59

   Source documentation

   A feasible table attaining the endpoint cell value supplies the lower bound for finite interpolation through the equality limit.

   theorem scalar_exact_half_window (A : Instance I J) (R : RootedCompletion.Selection A.T) (alpha : ℝ) (t : I×J)
       (ha : 0 ≤ alpha) (hW : 20*A.d ≤ A.W) (B K k N : ℕ)
       (hB : (∏ a : I×J,(A.b a.1 a.2+1)) ≤ 2^B) (hBK : 2*B ≤ K)
       (hK : 1 ≤ K) (hN : 0 < N) (hkN : k+N ≤ cellWidth A t)
       (hend : 1 ≤ scalarExact A R alpha t (k+N))
       (r : ℕ) (hr : r*K ≤ N) :
       scalarExact A R alpha t k/2 ≤ scalarExact A R alpha t (k+r) := by
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedTreeMarginal.scalarExact

5. theorem OAI.ContingencyTables.RootedTreeMarginal.scalar_exact_backward_half_window line 81

   Source documentation

   The same physical half-height estimate when the feasible endpoint lies to the left of an exterior tree position.

   theorem scalar_exact_backward_half_window (A : Instance I J) (R : RootedCompletion.Selection A.T) (alpha : ℝ) (t : I×J)
       (ha : 0 ≤ alpha) (hW : 20*A.d ≤ A.W) (B K k N : ℕ)
       (hB : (∏ a : I×J,(A.b a.1 a.2+1)) ≤ 2^B) (hBK : 2*B ≤ K)
       (hK : 1 ≤ K) (hN : 0 < N) (hNk : N ≤ k) (hk : k ≤ cellWidth A t)
       (hend : 1 ≤ scalarExact A R alpha t (k-N)) (r : ℕ) (hr : r*K ≤ N) :
       scalarExact A R alpha t k/2 ≤ scalarExact A R alpha t (k-r) := by
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedTreeMarginal.scalarExact

6. theorem OAI.ContingencyTables.RootedTreeMarginal.scalar_exact_forward_point_bound line 105

   Source documentation

   The actual physical exterior point has normalized mass at most 2K/b whenever a feasible unit-mass endpoint lies at least b places to its right, after eliminating all soft parameters.

   theorem scalar_exact_forward_point_bound (A : Instance I J) (R : RootedCompletion.Selection A.T) (alpha : ℝ) (t : I×J)
       (ha : 0 ≤ alpha) (hW : 20*A.d ≤ A.W) (B K k N b : ℕ)
       (hB : (∏ a : I×J,(A.b a.1 a.2+1)) ≤ 2^B) (hBK : 2*B ≤ K)
       (hK : 0 < K) (hN : 0 < N) (hb : 0 < b) (hbN : b ≤ N)
       (hkN : k+N ≤ cellWidth A t) (hend : 1 ≤ scalarExact A R alpha t (k+N)) :
       scalarExact A R alpha t k/(∑ q ∈ Finset.range (cellWidth A t+1),scalarExact A R alpha t q) ≤
         (2*K:ℝ)/b := by
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedTreeMarginal.scalarExact

7. theorem OAI.ContingencyTables.RootedTreeMarginal.scalar_exact_backward_point_bound line 124