TreeMarginalBounds.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Uniform mass and interpolation bounds for the physical tree marginal

The finite positive softening has at most the actual expanded physical box's number of summands. Consequently its interpolation estimate passes to the exact equality-constrained marginal even when that marginal has zero entries outside its feasible interval.

theorem OAI.ContingencyTables.EqualitySoftening.exactWeight_le_softenedWeight line 24
Source documentation
Softening only adds mass to an exact equality indicator. This comparison holds for every parameter value, because all soft factors are positive and the equality case has factor one.
```
theorem exactWeight_le_softenedWeight (line : C → G) (root : G → Bool)
    (rate offset slope : G → ℝ) (urate ell uslope cap : C → ℝ) (L : ℝ) (z : C → ℕ) :
    exactWeight line root rate offset slope urate ell uslope cap z ≤
      softenedWeight line root rate offset slope urate ell uslope cap L z := by
…
```
Mentions: OAI.ContingencyTables.EqualitySoftening.exactWeight, OAI.ContingencyTables.EqualitySoftening.softenedWeight
lemma OAI.ContingencyTables.TreeMarginalSignature.other_card_le_full line 57
theorem OAI.ContingencyTables.TreeMarginalSignature.scalar_soft_le_two_pow line 78
theorem OAI.ContingencyTables.TreeMarginalSignature.scalar_exact_nonnegative line 102
lemma OAI.ContingencyTables.TreeMarginalSignature.scalar_exact_le_soft line 109

theorem OAI.ContingencyTables.TreeMarginalSignature.scalar_exact_half_window line 119

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) (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 alpha t (k+N))
    (r : ℕ) (hr : r*K ≤ N) :
    scalarExact A alpha t k/2 ≤ scalarExact A alpha t (k+r) := by
…

Mentions: OAI.ContingencyTables.TreeMarginalSignature.cellWidth, OAI.ContingencyTables.TreeMarginalSignature.scalarExact

theorem OAI.ContingencyTables.TreeMarginalSignature.scalar_exact_backward_half_window line 141

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) (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 alpha t (k-N)) (r : ℕ) (hr : r*K ≤ N) :
    scalarExact A alpha t k/2 ≤ scalarExact A alpha t (k-r) := by
…

Mentions: OAI.ContingencyTables.TreeMarginalSignature.cellWidth, OAI.ContingencyTables.TreeMarginalSignature.scalarExact

theorem OAI.ContingencyTables.TreeMarginalSignature.scalar_exact_forward_point_bound line 165

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) (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 alpha t (k+N)) :
    scalarExact A alpha t k/(∑ q ∈ Finset.range (cellWidth A t+1),scalarExact A alpha t q) ≤
      (2*K:ℝ)/b := by
…

Mentions: OAI.ContingencyTables.TreeMarginalSignature.cellWidth, OAI.ContingencyTables.TreeMarginalSignature.scalarExact

theorem OAI.ContingencyTables.TreeMarginalSignature.scalar_exact_backward_point_bound line 184