ProductIntegerSignature.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Raw integer signatures of the actual line and unary product

The line groups are disjoint. Integer counts at zero are masked; a repeated removal from a count below two uses a zero second-update factor. This identifies the actual integer matrix, including its box boundaries, with a congruence of the proved line/unary update matrix.

def OAI.ContingencyTables.ProductIntegerSignature.lineTotal line 22
def OAI.ContingencyTables.ProductIntegerSignature.productWeight line 25
lemma OAI.ContingencyTables.ProductIntegerSignature.lineTotal_removeOne line 29
lemma OAI.ContingencyTables.ProductIntegerSignature.lineTotal_removeTwo line 47

theorem OAI.ContingencyTables.ProductIntegerSignature.productWeight_removeTwo line 59

Source documentation

Literal product values after a valid integer removal coincide with all line and unary update products.

theorem productWeight_removeTwo (line : I → G) (a : G → ℕ → ℝ) (b : I → ℕ → ℝ)
    (z : I → ℕ) (i j : I) (hvalid : ValidPair z i j) :
    productWeight line a b (removeTwo z i j) =
      lineUnaryRemoval line
        (fun g => a g (lineTotal line z g))
        (fun g => a g (lineTotal line z g-1))
        (fun g => if 2 ≤ lineTotal line z g then a g (lineTotal line z g-2) else 0)
        (fun k => b k (z k)) (fun k => b k (z k-1))
        (fun k => if 2 ≤ z k then b k (z k-2) else 0) i j := by
…

Mentions: OAI.ContingencyTables.ProductIntegerSignature.productWeight, OAI.ContingencyTables.lineUnaryRemoval, OAI.ContingencyTables.ProductIntegerSignature.lineTotal

def OAI.ContingencyTables.ProductIntegerSignature.activeMask line 105

theorem OAI.ContingencyTables.ProductIntegerSignature.integerRemoval_product_matrix line 109

Source documentation

The raw matrix is exactly the line/unary matrix with inactive integer coordinates set to zero. Invalid repeated removals are also zero.

theorem integerRemoval_product_matrix (line : I → G) (a : G → ℕ → ℝ) (b : I → ℕ → ℝ)
    (z : I → ℕ) :
    integerRemovalMatrix (productWeight line a b) z =
      scaledMatrix (lineUnaryRemoval line
        (fun g => a g (lineTotal line z g))
        (fun g => a g (lineTotal line z g-1))
        (fun g => if 2 ≤ lineTotal line z g then a g (lineTotal line z g-2) else 0)
        (fun k => b k (z k)) (fun k => b k (z k-1))
        (fun k => if 2 ≤ z k then b k (z k-2) else 0)) (activeMask z) := by
…

Mentions: OAI.ContingencyTables.ProductIntegerSignature.productWeight, OAI.ContingencyTables.scaledMatrix, OAI.ContingencyTables.lineUnaryRemoval, OAI.ContingencyTables.ProductIntegerSignature.lineTotal, OAI.ContingencyTables.ProductIntegerSignature.activeMask

theorem OAI.ContingencyTables.ProductIntegerSignature.product_removal_onePositive line 142

Source documentation

Log-concavity of the actual scalar sequences gives the integer signature required by factorial lifting and balanced marginalization.

theorem product_removal_onePositive (line : I → G) (a : G → ℕ → ℝ) (b : I → ℕ → ℝ)
    (z : I → ℕ)
    (ha : ∀ g n, n ≤ lineTotal line z g → 0 < a g n)
    (hb : ∀ i n, n ≤ z i → 0 < b i n)
    (halc : ∀ g, 2 ≤ lineTotal line z g →
      a g (lineTotal line z g) * a g (lineTotal line z g-2) ≤ a g (lineTotal line z g-1)^2)
    (hblc : ∀ i, 2 ≤ z i → b i (z i) * b i (z i-2) ≤ b i (z i-1)^2) :
    OnePositiveDirection (integerRemovalMatrix (productWeight line a b) z).toBilin' := by
…

Mentions: OAI.ContingencyTables.ProductIntegerSignature.lineTotal, OAI.ContingencyTables.OnePositiveDirection, OAI.ContingencyTables.ProductIntegerSignature.productWeight