LaminarSignature.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

The two-level laminar kernel in contingency-table weights

The factor groups in the sampling paper's laminar-signature lemma are line coordinate sets, with one nested small-slot subset in each line. Row and column coordinates belong to separate lines. The normalized kernel decomposition gives the quadratic one-positive-direction property.

def OAI.ContingencyTables.twoLevelKernel line 26
Source documentation
The normalized two-removal kernel: line factors and the nested small coordinate factor are the only factors shared by two distinct indices.
```
def twoLevelKernel (line : I → G) (inner : I → Bool) (γ δ : G → ℝ) :
    Matrix I I ℝ := fun i j =>
…
```
def OAI.ContingencyTables.lineVector line 33
Source documentation
Indicator of one line-coordinate group.
```
def lineVector (line : I → G) (g : G) (i : I) : ℝ :=
…
```
def OAI.ContingencyTables.innerVector line 37
Source documentation
Indicator of the small-coordinate subgroup of one line.
```
def innerVector (line : I → G) (inner : I → Bool) (g : G) (i : I) : ℝ :=
…
```
def OAI.ContingencyTables.outerMatrix line 41
Source documentation
The rank-one matrix associated with a vector.
```
def outerMatrix (v : I → ℝ) : Matrix I I ℝ := fun i j => v i * v j
```
def OAI.ContingencyTables.vectorSum line 44
Source documentation
The linear sum of the coordinates weighted by v.
```
def vectorSum (v : I → ℝ) : (I → ℝ) →ₗ[ℝ] ℝ :=
…
```
lemma OAI.ContingencyTables.vectorSum_apply line 48
lemma OAI.ContingencyTables.outerMatrix_form line 51

theorem OAI.ContingencyTables.twoLevelKernel_decomposition line 62

Source documentation

The precise rank-one-minus-blocks identity for the line/inner family.

theorem twoLevelKernel_decomposition (line : I → G) (inner : I → Bool) (γ δ : G → ℝ) :
    twoLevelKernel line inner γ δ =
      outerMatrix (fun _ : I => 1) -
        ∑ g, ((1 - γ g) • outerMatrix (lineVector line g) +
          (γ g * (1 - δ g)) • outerMatrix (innerVector line inner g)) := by
…

Mentions: OAI.ContingencyTables.twoLevelKernel, OAI.ContingencyTables.outerMatrix, OAI.ContingencyTables.lineVector, OAI.ContingencyTables.innerVector

theorem OAI.ContingencyTables.twoLevelKernel_form line 84

Source documentation

The corresponding bilinear decomposition makes the squares explicit when both arguments are equal.

theorem twoLevelKernel_form (line : I → G) (inner : I → Bool) (γ δ : G → ℝ)
    (x y : I → ℝ) :
    (twoLevelKernel line inner γ δ).toBilin' x y =
      vectorSum (fun _ : I => 1) x * vectorSum (fun _ : I => 1) y -
        ∑ g, ((1 - γ g) * (vectorSum (lineVector line g) x * vectorSum (lineVector line g) y) +
          (γ g * (1 - δ g)) *
            (vectorSum (innerVector line inner g) x * vectorSum (innerVector line inner g) y)) := by
…

Mentions: OAI.ContingencyTables.twoLevelKernel, OAI.ContingencyTables.vectorSum, OAI.ContingencyTables.lineVector, OAI.ContingencyTables.innerVector

theorem OAI.ContingencyTables.twoLevelKernel_onePositive line 98
Source documentation
The line/inner two-removal kernel has positive inertia at most one in quadratic-form language. Its proof uses the actual matrix decomposition.
```
theorem twoLevelKernel_onePositive (line : I → G) (inner : I → Bool) (γ δ : G → ℝ)
    (hγ0 : ∀ g, 0 ≤ γ g) (hγ1 : ∀ g, γ g ≤ 1) (hδ1 : ∀ g, δ g ≤ 1) :
    OnePositiveDirection (twoLevelKernel line inner γ δ).toBilin' := by
…
```
Mentions: OAI.ContingencyTables.OnePositiveDirection, OAI.ContingencyTables.twoLevelKernel

lemma OAI.ContingencyTables.twoLevelKernel_form_symm line 119

Source documentation

The bilinear kernel is symmetric even before positivity assumptions.

lemma twoLevelKernel_form_symm (line : I → G) (inner : I → Bool) (γ δ : G → ℝ)
    (x y : I → ℝ) :
    (twoLevelKernel line inner γ δ).toBilin' x y =
      (twoLevelKernel line inner γ δ).toBilin' y x := by
…

Mentions: OAI.ContingencyTables.twoLevelKernel

theorem OAI.ContingencyTables.twoLevelKernel_nonpositive line 131

Source documentation

The normalized kernel is nonpositive on the zero-sum hyperplane.

theorem twoLevelKernel_nonpositive (line : I → G) (inner : I → Bool) (γ δ : G → ℝ)
    (hγ0 : ∀ g, 0 ≤ γ g) (hγ1 : ∀ g, γ g ≤ 1) (hδ1 : ∀ g, δ g ≤ 1)
    (v : I → ℝ) (hv : vectorSum (fun _ : I => 1) v = 0) :
    (twoLevelKernel line inner γ δ).toBilin' v v ≤ 0 := by
…

Mentions: OAI.ContingencyTables.vectorSum, OAI.ContingencyTables.twoLevelKernel

def OAI.ContingencyTables.scaledMatrix line 143
def OAI.ContingencyTables.weightedCorrection line 148
Source documentation
Undo diagonal normalization and subtract the entries corresponding to invalid repeated removals. Zero scale coordinates also restore zero rows.
```
def weightedCorrection (K : Matrix I I ℝ) (W : ℝ) (α κ : I → ℝ) : Matrix I I ℝ :=
…
```
lemma OAI.ContingencyTables.scaledMatrix_form line 151
lemma OAI.ContingencyTables.diagonalMatrix_form line 162

theorem OAI.ContingencyTables.weightedCorrection_form line 172

Source documentation

The exact quadratic effect of scaling and invalid-diagonal removal.

theorem weightedCorrection_form (K : Matrix I I ℝ) (W : ℝ) (α κ x y : I → ℝ) :
    (weightedCorrection K W α κ).toBilin' x y =
      W * K.toBilin' (fun i => α i * x i) (fun i => α i * y i) -
        ∑ i, κ i * x i * y i := by
…

Mentions: OAI.ContingencyTables.weightedCorrection

theorem OAI.ContingencyTables.correctedTwoLevel_onePositive line 181

Source documentation

This includes the full unsummed two-removal signature: positive scalar and diagonal congruence, invalid diagonals removed, zero rows restored.

theorem correctedTwoLevel_onePositive (line : I → G) (inner : I → Bool) (γ δ : G → ℝ)
    (W : ℝ) (α κ : I → ℝ)
    (hγ0 : ∀ g, 0 ≤ γ g) (hγ1 : ∀ g, γ g ≤ 1) (hδ1 : ∀ g, δ g ≤ 1)
    (hW : 0 ≤ W) (hκ : ∀ i, 0 ≤ κ i) :
    OnePositiveDirection (weightedCorrection (twoLevelKernel line inner γ δ) W α κ).toBilin' := by
…

Mentions: OAI.ContingencyTables.OnePositiveDirection, OAI.ContingencyTables.weightedCorrection, OAI.ContingencyTables.twoLevelKernel