NestedProductSignature.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The first paper's actual line and small-slot subgroup product

Each small-slot subgroup is contained in a disjoint line group. The literal product after two removals is factored into the two-level kernel. Zero integer counts are masked and invalid repeated removals subtract a nonnegative diagonal.

def OAI.ContingencyTables.NestedProductSignature.unitExtension line 21
def OAI.ContingencyTables.NestedProductSignature.subgroup line 23
def OAI.ContingencyTables.NestedProductSignature.nestedRemoval line 26
lemma OAI.ContingencyTables.NestedProductSignature.nestedRemoval_factor line 33

theorem OAI.ContingencyTables.NestedProductSignature.nestedRemoval_onePositive line 52

Source documentation

Signature of the literal nested product update matrix.

theorem nestedRemoval_onePositive (line : I → G) (inner : I → Bool)
    (a₀ a₁ a₂ c₀ c₁ c₂ : G → ℝ)
    (ha₀ : ∀ g, 0 < a₀ g) (ha₁ : ∀ g, 0 < a₁ g) (ha₂ : ∀ g, 0 ≤ a₂ g)
    (hc₀ : ∀ g, 0 < c₀ g) (hc₁ : ∀ g, 0 < c₁ g)
    (halc : ∀ g, a₀ g*a₂ g ≤ (a₁ g)^2)
    (hclc : ∀ g, c₀ g*c₂ g ≤ (c₁ g)^2) :
    OnePositiveDirection (nestedRemoval line inner a₀ a₁ a₂ c₀ c₁ c₂).toBilin' := by
…

Mentions: OAI.ContingencyTables.OnePositiveDirection, OAI.ContingencyTables.NestedProductSignature.nestedRemoval

def OAI.ContingencyTables.NestedProductSignature.smallTotal line 81
def OAI.ContingencyTables.NestedProductSignature.nestedWeight line 84
lemma OAI.ContingencyTables.NestedProductSignature.smallTotal_removeTwo line 89

theorem OAI.ContingencyTables.NestedProductSignature.nestedWeight_removeTwo line 99

Source documentation

Exact literal nested product at every valid integer two-removal entry.

theorem nestedWeight_removeTwo (line : I → G) (inner : I → Bool) (a c : G → ℕ → ℝ)
    (z : I → ℕ) (i j : I) (hv : ValidPair z i j) :
    nestedWeight line inner a c (removeTwo z i j) =
      nestedRemoval line inner
        (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 g => c g (smallTotal line inner z g)) (fun g => c g (smallTotal line inner z g-1))
        (fun g => if 2 ≤ smallTotal line inner z g then c g (smallTotal line inner z g-2) else 0) i j := by
…

Mentions: OAI.ContingencyTables.NestedProductSignature.nestedWeight, OAI.ContingencyTables.NestedProductSignature.nestedRemoval, OAI.ContingencyTables.NestedProductSignature.smallTotal

lemma OAI.ContingencyTables.NestedProductSignature.masked_correction line 151
lemma OAI.ContingencyTables.NestedProductSignature.updates_nonnegative line 185

theorem OAI.ContingencyTables.NestedProductSignature.nested_product_removal_onePositive line 194

Source documentation

The exact integer two-removal signature for the first paper's full line penalties and nested small-slot subset penalties.

theorem nested_product_removal_onePositive (line : I → G) (inner : I → Bool)
    (a c : G → ℕ → ℝ) (z : I → ℕ)
    (ha : ∀ g n, n ≤ lineTotal line z g → 0 < a g n)
    (hc : ∀ g n, n ≤ smallTotal line inner z g → 0 < c g 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)
    (hclc : ∀ g, 2 ≤ smallTotal line inner z g →
      c g (smallTotal line inner z g)*c g (smallTotal line inner z g-2) ≤
        c g (smallTotal line inner z g-1)^2) :
    OnePositiveDirection (integerRemovalMatrix (nestedWeight line inner a c) z).toBilin' := by
…

Mentions: OAI.ContingencyTables.NestedProductSignature.smallTotal, OAI.ContingencyTables.OnePositiveDirection, OAI.ContingencyTables.NestedProductSignature.nestedWeight