ForestCountIdentification.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The companion signature marginal is the literal weighted completion count

The physical all-large product is split bijectively into tree and free assignments. Exact nonroot equations then retain one tree completion per free assignment, with exactly its root/tree exponential penalty.

def OAI.ContingencyTables.ForestCountIdentification.smallX line 23
def OAI.ContingencyTables.ForestCountIdentification.smallY line 27
lemma OAI.ContingencyTables.ForestCountIdentification.split_profile line 32
theorem OAI.ContingencyTables.ForestCountIdentification.physical_sum_split line 47
def OAI.ContingencyTables.ForestCountIdentification.sourceMarginal line 67
theorem OAI.ContingencyTables.ForestCountIdentification.sourceMarginal_positive line 77

theorem OAI.ContingencyTables.ForestCountIdentification.sourceMarginal_zero line 89

Source documentation

At annealing parameter zero the original count is exactly the product of the free interval lengths.

theorem sourceMarginal_zero (small : I → J → Bool) (T : SimpleGraph (I⊕J))
    (d : ℕ) (b : I → J → ℕ) (r : I → ℤ) (c : J → ℤ)
    (z : SmallView (fun a : I×J => small a.1 a.2) → ℕ) :
    sourceMarginal small T d b r c 0 z=
      ∏ a : FreeCell small T, ((b a.val.1 a.val.2+1:ℕ):ℝ) := by
…

Mentions: OAI.ContingencyTables.ForestCountIdentification.sourceMarginal

theorem OAI.ContingencyTables.ForestCountIdentification.sourceMarginal_eq_largeMarginal line 98

Source documentation

The source's actual free-assignment count is precisely the all-large physical marginal with its raw removal signature.

theorem sourceMarginal_eq_largeMarginal (small : I → J → Bool) (b : I → J → ℕ)
    (T : SimpleGraph (I⊕J)) (hTG : T≤cellGraph small) (hT : T.IsAcyclic)
    (hmax : ∀ F : SimpleGraph (I⊕J), F≤cellGraph small → F.IsAcyclic →
      MaximumForest.weight F (capacity b)≤MaximumForest.weight T (capacity b))
    (r : I → ℤ) (c : J → ℤ) (X : I → J → ℤ)
    (d W : ℕ) (alpha : ℝ) (hd : 1≤d) (hcard : Fintype.card I*Fintype.card J≤d)
    (hlarge : ∀ i j, small i j=false → W≤b i j ∧ 1≤b i j)
    (hsmall : ∀ i j, small i j=true → b i j<W)
    (hX : ∀ i j, 0≤X i j ∧ X i j≤b i j)
    (hXr : ∀ i, (∑ j, X i j)=r i) (hXc : ∀ j, (∑ i, X i j)=c j)
    {n : ℕ} (e : Fin n ≃ LargeCell (fun a : I×J => small a.1 a.2))
    (z : SmallView (fun a : I×J => small a.1 a.2) → ℕ)
…

Mentions: OAI.ContingencyTables.MaximumForest.weight