TreeExteriorMass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Actual exterior tree masses, normalized by the original companion count

lemma OAI.ContingencyTables.TreeMarginalSignature.scalar_sum_eq_physicalMass line 18

theorem OAI.ContingencyTables.TreeMarginalSignature.lower_exterior_point line 27

Source documentation

A lower exterior tree position is controlled by the actual feasible table attaining its upper bound, exactly as in the manuscript.

theorem lower_exterior_point (A : Instance I J) (alpha : ℝ) (t : I×J)
    (ht : A.T.Adj (.inl t.1) (.inr t.2)) (ha : 0 ≤ alpha)
    (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)
    (Y : I → J → ℤ) (hY : ∀ i j,0 ≤ Y i j ∧ Y i j ≤ A.b i j)
    (hr : ∀ i,(∑ j,Y i j)=A.r i) (hc : ∀ j,(∑ i,Y i j)=A.c j)
    (hy : Y t.1 t.2=(A.b t.1 t.2:ℤ)) (k : ℕ) (hk : k < 10*A.d*A.b t.1 t.2) :
    scalarExact A alpha t k/physicalMass A alpha ≤ (2*K:ℝ)/A.b t.1 t.2 := by
…

Mentions: OAI.ContingencyTables.TreeMarginalSignature.scalarExact

theorem OAI.ContingencyTables.TreeMarginalSignature.upper_exterior_point line 46