OAI/Combinatorics/ContingencyTables/Rooted/ForestLargeMarginal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual companion large-cell sum has its removal signature

Small coordinates are the actual two views of small cells, and every large cell is summed once at its physical balance width. All line and unary factors have the manuscript's row/column and forest parameters.

  1. def OAI.ContingencyTables.ForestLargeMarginal.largeMarginal line 23
  2. theorem OAI.ContingencyTables.ForestLargeMarginal.largeMarginal_nonnegative line 32
  3. theorem OAI.ContingencyTables.ForestLargeMarginal.largeMarginal_eq_eliminate line 41
  4. theorem OAI.ContingencyTables.ForestLargeMarginal.largeMarginal_removal line 55

    Source documentation

    This is a proved signature of the literal all-large finite count, with the physical widths, retained small views, and coordinate map made explicit.

    theorem largeMarginal_removal (small : I×J → Bool)
    (T : SimpleGraph (I⊕J)) (b : I → J → ℕ) (ell : I → J → ℤ)
    (M : I → J → ℕ) (r : I → ℤ) (c : J → ℤ) (alpha : ℝ)
    {n : ℕ} (e : Fin n ≃ LargeCell small) (m : SmallView small → ℕ) (p : ℕ)
    (ha : 0≤alpha) (hwidth : ∀ k, 2≤M (e k).val.1 (e k).val.2) :
    RemovalSlice (largeMarginal small T b ell M r c alpha e) m p := by
…

    Mentions: OAI.ContingencyTables.ForestLargeMarginal.largeMarginal

  5. theorem OAI.ContingencyTables.ForestLargeMarginal.largeMarginal_reflected line 79

    Source documentation

    Reflecting the retained views and every eliminated large pair proves the complementary factorial lift's actual addition input.

    theorem largeMarginal_reflected (small : I×J → Bool)
    (T : SimpleGraph (I⊕J)) (b : I → J → ℕ) (ell : I → J → ℤ)
    (M : I → J → ℕ) (r : I → ℤ) (c : J → ℤ) (alpha : ℝ)
    {n : ℕ} (e : Fin n ≃ LargeCell small) (m : SmallView small → ℕ) (p : ℕ)
    (ha : 0≤alpha) (hwidth : ∀ k, 2≤M (e k).val.1 (e k).val.2) :
    RemovalSlice (fun z => largeMarginal small T b ell M r c alpha e
      (IntegerReflection.reflect m z)) m p := by
…

    Mentions: OAI.ContingencyTables.ForestLargeMarginal.largeMarginal, OAI.ContingencyTables.IntegerReflection.reflect