LineUnarySignature.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The line and unary factors of the bounded-table application

The bounded-table signature argument uses disjoint row/column line factors and unary tree penalties. Factoring the product after two removals expresses unary factors as nonnegative diagonal corrections of the line kernel.

def OAI.ContingencyTables.productTwoUpdates line 21

theorem OAI.ContingencyTables.productTwoUpdates_factor line 27

Source documentation

Exact factorization of the actual product after two coordinate changes, including a repeated change of the same coordinate.

theorem productTwoUpdates_factor (a₀ a₁ a₂ : A → ℝ)
    (h₀ : ∀ k, a₀ k ≠ 0) (h₁ : ∀ k, a₁ k ≠ 0) (i j : A) :
    productTwoUpdates a₀ a₁ a₂ i j =
      (∏ k, a₀ k) * (a₁ i / a₀ i) * (a₁ j / a₀ j) *
        (if i = j then a₀ i * a₂ i / (a₁ i) ^ 2 else 1) := by
…

Mentions: OAI.ContingencyTables.productTwoUpdates

def OAI.ContingencyTables.lineUnaryRemoval line 67
Source documentation
Values of every line factor and every unary factor after zero, one, and two removals give exactly this two-removal matrix.
```
def lineUnaryRemoval (line : I → G) (a₀ a₁ a₂ : G → ℝ) (b₀ b₁ b₂ : I → ℝ) :
    Matrix I I ℝ := fun i j =>
…
```
theorem OAI.ContingencyTables.lineUnaryRemoval_factor line 71
theorem OAI.ContingencyTables.normalized_line_unary_correction line 85

theorem OAI.ContingencyTables.lineUnaryRemoval_onePositive line 103

Source documentation

The actual line/unary two-removal matrix has the required signature when each factor satisfies its scalar log-concavity inequality.

theorem lineUnaryRemoval_onePositive (line : I → G)
    (a₀ a₁ a₂ : G → ℝ) (b₀ b₁ b₂ : I → ℝ)
    (ha₀ : ∀ g, 0 < a₀ g) (ha₁ : ∀ g, 0 < a₁ g) (ha₂ : ∀ g, 0 ≤ a₂ g)
    (hb₀ : ∀ i, 0 < b₀ i) (hb₁ : ∀ i, 0 < b₁ i)
    (halc : ∀ g, a₀ g * a₂ g ≤ (a₁ g) ^ 2)
    (hblc : ∀ i, b₀ i * b₂ i ≤ (b₁ i) ^ 2) :
    OnePositiveDirection (lineUnaryRemoval line a₀ a₁ a₂ b₀ b₁ b₂).toBilin' := by
…

Mentions: OAI.ContingencyTables.OnePositiveDirection, OAI.ContingencyTables.lineUnaryRemoval