BinaryContraction.lean`

37 declarations, 0 contain sorry, 0 declared as axioms

Fixed-degree binary cubic contraction

The full-matrix cubic contraction in paper 200-02, Lemma lem:binary-contraction, follows from the generic spectral theorem CommonBasesFPRAS.cubic_signature and its closed-limit lemma. A symmetric cubic tensor is positive on distinct triples and zero on repetitions; its coordinate slices have the quadratic signature; contraction by an arbitrary nonnegative vector, in particular a pair indicator, preserves that signature on the full remaining index set.

There is no assumption of positivity on unrelated subset cardinalities.

lemma OAI.ContingencyTables.BinaryContraction.signature_iff line 31
Source documentation
Our signature convention and the existing library convention agree for symmetric forms; only the orthogonality argument order differs.
```
lemma signature_iff (B : BilinForm ℝ (I → ℝ)) (hsymm : B.IsSymm) :
    OnePositiveDirection B ↔ CommonBasesFPRAS.OnePositive B := by
…
```
Mentions: OAI.ContingencyTables.OnePositiveDirection, OAI.CommonBasesFPRAS.OnePositive
lemma OAI.ContingencyTables.BinaryContraction.exists_third line 39

lemma OAI.ContingencyTables.BinaryContraction.tensor_nonnegative line 58

Source documentation

Every tensor entry is nonnegative on the actual cubic domain.

lemma tensor_nonnegative (C : I → Matrix I I ℝ)
    (hzero : ∀ i j k, i = j ∨ i = k ∨ j = k → C i j k = 0)
    (hpos : ∀ i j k, i ≠ j → i ≠ k → j ≠ k → 0 < C i j k)
    (i j k : I) : 0 ≤ C i j k := by
…

lemma OAI.ContingencyTables.BinaryContraction.slice_square_positive line 69

Source documentation

Strictly positive directions give positive slice squares, including when the ground set has exactly three elements.

lemma slice_square_positive (C : I → Matrix I I ℝ) (hcard : 3 ≤ Fintype.card I)
    (hzero : ∀ i j k, i = j ∨ i = k ∨ j = k → C i j k = 0)
    (hpos : ∀ i j k, i ≠ j → i ≠ k → j ≠ k → 0 < C i j k)
    (x : I → ℝ) (hx : ∀ i, 0 < x i) (i : I) :
    0 < (C i).toBilin' x x := by
…

theorem OAI.ContingencyTables.BinaryContraction.positive_cubic_contraction line 91

Source documentation

Strict-direction specialization of the existing generic spectral argument, with every positivity condition proved from distinct triples.

theorem positive_cubic_contraction (C : I → Matrix I I ℝ)
    (hcard : 3 ≤ Fintype.card I)
    (hCs : ∀ i j k, C i j k = C i k j)
    (hCt : ∀ i j k, C i j k = C j i k)
    (hzero : ∀ i j k, i = j ∨ i = k ∨ j = k → C i j k = 0)
    (hpos : ∀ i j k, i ≠ j → i ≠ k → j ≠ k → 0 < C i j k)
    (hsig : ∀ i, OnePositiveDirection (C i).toBilin')
    (x : I → ℝ) (hx : ∀ i, 0 < x i) :
    CommonBasesFPRAS.OnePositive (cubicContraction C x).toBilin' := by
…

Mentions: OAI.ContingencyTables.OnePositiveDirection, OAI.CommonBasesFPRAS.OnePositive

theorem OAI.ContingencyTables.BinaryContraction.nonnegative_cubic_contraction line 117

Source documentation

Nonnegative contractions follow by the actual positive perturbation and closed matrix limit from the paper. The contracted indices are retained.

theorem nonnegative_cubic_contraction (C : I → Matrix I I ℝ)
    (hcard : 3 ≤ Fintype.card I)
    (hCs : ∀ i j k, C i j k = C i k j)
    (hCt : ∀ i j k, C i j k = C j i k)
    (hzero : ∀ i j k, i = j ∨ i = k ∨ j = k → C i j k = 0)
    (hpos : ∀ i j k, i ≠ j → i ≠ k → j ≠ k → 0 < C i j k)
    (hsig : ∀ i, OnePositiveDirection (C i).toBilin')
    (x : I → ℝ) (hx : ∀ i, 0 ≤ x i) :
    OnePositiveDirection (cubicContraction C x).toBilin' := by
…

Mentions: OAI.ContingencyTables.OnePositiveDirection

theorem OAI.ContingencyTables.BinaryContraction.pair_cubic_contraction line 150

Source documentation

The pair-indicator contraction in Lemma binary-contraction is the sum of the two coordinate slices on the full ground set. No principal restriction has been taken yet.

theorem pair_cubic_contraction (C : I → Matrix I I ℝ)
    (hcard : 3 ≤ Fintype.card I)
    (hCs : ∀ i j k, C i j k = C i k j)
    (hCt : ∀ i j k, C i j k = C j i k)
    (hzero : ∀ i j k, i = j ∨ i = k ∨ j = k → C i j k = 0)
    (hpos : ∀ i j k, i ≠ j → i ≠ k → j ≠ k → 0 < C i j k)
    (hsig : ∀ i, OnePositiveDirection (C i).toBilin') (p q : I) :
    OnePositiveDirection (C p + C q).toBilin' := by
…

Mentions: OAI.ContingencyTables.OnePositiveDirection

def OAI.ContingencyTables.BinaryContraction.DegreePositive line 173
Source documentation
Positivity is required only on the paper's valid subset degree.
```
def DegreePositive (f : Set I → ℝ) (k : ℕ) : Prop :=
…
```
def OAI.ContingencyTables.BinaryContraction.AdditionProperty line 178
Source documentation
The paper's addition property: fix precisely k-2 elements and test only the remaining quadratic matrix.
```
def AdditionProperty (f : Set I → ℝ) (k : ℕ) : Prop :=
…
```
lemma OAI.ContingencyTables.BinaryContraction.fixedDegree_slice line 183
Source documentation
A coordinate slice of a valid-degree cubic tensor is a padded addition matrix of the original weight.
```
lemma fixedDegree_slice (f : Set I → ℝ) (k : ℕ)
    (hsig : AdditionProperty f k) (A : Set I) (hA : A.ncard + 3 = k)
    (i : {i // i ∉ A}) : CommonBasesFPRAS.OnePositive (faceCubic f A i).toBilin' := by
…
```
Mentions: OAI.ContingencyTables.BinaryContraction.AdditionProperty, OAI.CommonBasesFPRAS.OnePositive
theorem OAI.ContingencyTables.BinaryContraction.fixedDegree_pair_contraction line 198
Source documentation
The full-ground pair contraction for a weight positive only at its specified subset degree. This is the actual cubic tensor used by the paper.
```
theorem fixedDegree_pair_contraction (f : Set I → ℝ) (k : ℕ)
    (hk : k ≤ Fintype.card I) (hpos : DegreePositive f k)
    (hsig : AdditionProperty f k) (A : Set I) (hA : A.ncard + 3 = k)
    (p q : {i // i ∉ A}) :
    OnePositiveDirection (faceCubic f A p + faceCubic f A q).toBilin' := by
…
```
Mentions: OAI.ContingencyTables.BinaryContraction.DegreePositive, OAI.ContingencyTables.BinaryContraction.AdditionProperty, OAI.ContingencyTables.OnePositiveDirection
abbrev OAI.ContingencyTables.BinaryContraction.PairRest line 220
def OAI.ContingencyTables.BinaryContraction.pairSum line 223
Source documentation
Summing a labeled pair at occupancy one, on its actual remaining ground set.
```
noncomputable def pairSum (f : Set I → ℝ) (p q : I) (U : Set (PairRest p q)) : ℝ :=
…
```
Mentions: OAI.ContingencyTables.BinaryContraction.PairRest
lemma OAI.ContingencyTables.BinaryContraction.pairSum_positive line 227
Source documentation
Every valid residual weight is the sum of two strictly positive weights.
```
lemma pairSum_positive (f : Set I → ℝ) (k : ℕ) (hpos : DegreePositive f k)
    (p q : I) (U : Set (PairRest p q)) (hU : U.ncard + 1 = k) :
    0 < pairSum f p q U := by
…
```
Mentions: OAI.ContingencyTables.BinaryContraction.DegreePositive, OAI.ContingencyTables.BinaryContraction.PairRest, OAI.ContingencyTables.BinaryContraction.pairSum
theorem OAI.ContingencyTables.BinaryContraction.pairSum_addition line 250
Source documentation
Occupancy-one pair summation preserves the valid-degree addition property. The proof contracts on the full index set first and then takes the exact principal submatrix after removing the pair.
```
theorem pairSum_addition (f : Set I → ℝ) (k : ℕ)
    (hk : k ≤ Fintype.card I) (hpos : DegreePositive f k)
    (hsig : AdditionProperty f k) (p q : I) :
    AdditionProperty (pairSum f p q) (k - 1) := by
…
```
Mentions: OAI.ContingencyTables.BinaryContraction.DegreePositive, OAI.ContingencyTables.BinaryContraction.AdditionProperty, OAI.ContingencyTables.BinaryContraction.pairSum
theorem OAI.ContingencyTables.BinaryContraction.pairSum_degreePositive line 302
Source documentation
The output positivity statement in its fixed-degree form.
```
theorem pairSum_degreePositive (f : Set I → ℝ) (k : ℕ) (hk : 1 ≤ k)
    (hpos : DegreePositive f k) (p q : I) : DegreePositive (pairSum f p q) (k - 1) := by
…
```
Mentions: OAI.ContingencyTables.BinaryContraction.DegreePositive, OAI.ContingencyTables.BinaryContraction.pairSum
abbrev OAI.ContingencyTables.BinaryContraction.FixedRest line 308
def OAI.ContingencyTables.BinaryContraction.fixIncluded line 310
def OAI.ContingencyTables.BinaryContraction.fixExcluded line 313
lemma OAI.ContingencyTables.BinaryContraction.fixIncluded_degreePositive line 316
lemma OAI.ContingencyTables.BinaryContraction.fixExcluded_degreePositive line 328
theorem OAI.ContingencyTables.BinaryContraction.fixExcluded_addition line 337
Source documentation
Fixing an exclusion restricts each quadratic test to a principal submatrix.
```
theorem fixExcluded_addition (f : Set I → ℝ) (k : ℕ)
    (hsig : AdditionProperty f k) (p : I) : AdditionProperty (fixExcluded f p) k := by
…
```
Mentions: OAI.ContingencyTables.BinaryContraction.AdditionProperty, OAI.ContingencyTables.BinaryContraction.fixExcluded
theorem OAI.ContingencyTables.BinaryContraction.fixIncluded_addition line 366
Source documentation
Fixing an inclusion enlarges the fixed set in each quadratic test.
```
theorem fixIncluded_addition (f : Set I → ℝ) (k : ℕ)
    (hsig : AdditionProperty f k) (p : I) : AdditionProperty (fixIncluded f p) (k - 1) := by
…
```
Mentions: OAI.ContingencyTables.BinaryContraction.AdditionProperty, OAI.ContingencyTables.BinaryContraction.fixIncluded
def OAI.ContingencyTables.BinaryContraction.complementWeight line 408
def OAI.ContingencyTables.BinaryContraction.OmissionProperty line 410
lemma OAI.ContingencyTables.BinaryContraction.complement_degreePositive line 414
lemma OAI.ContingencyTables.BinaryContraction.pairRest_image_avoids line 424
lemma OAI.ContingencyTables.BinaryContraction.pair_complement_set line 434
Source documentation
Complementation swaps which member of the pair is included.
```
lemma pair_complement_set (p q : I) (hpq : p ≠ q) (U : Set (PairRest p q)) :
    insert p (Subtype.val '' Uᶜ) = (insert q (Subtype.val '' U))ᶜ := by
…
```
Mentions: OAI.ContingencyTables.BinaryContraction.PairRest
lemma OAI.ContingencyTables.BinaryContraction.pairSum_complement line 457
lemma OAI.ContingencyTables.BinaryContraction.card_pairRest line 466
theorem OAI.ContingencyTables.BinaryContraction.pairSum_omission line 474
Source documentation
Complementation preserves occupancy one, so the proved addition closure gives omission closure on every valid residual degree.
```
theorem pairSum_omission (f : Set I → ℝ) (k : ℕ)
    (hk : 1 ≤ k) (hkupper : k + 1 ≤ Fintype.card I)
    (hpos : DegreePositive f k) (hsig : OmissionProperty f k)
    (p q : I) (hpq : p ≠ q) : OmissionProperty (pairSum f p q) (k - 1) := by
…
```
Mentions: OAI.ContingencyTables.BinaryContraction.DegreePositive, OAI.ContingencyTables.BinaryContraction.OmissionProperty, OAI.ContingencyTables.BinaryContraction.pairSum
lemma OAI.ContingencyTables.BinaryContraction.fixed_complement_set line 491
lemma OAI.ContingencyTables.BinaryContraction.fixIncluded_complement line 512
lemma OAI.ContingencyTables.BinaryContraction.fixExcluded_complement line 518
lemma OAI.ContingencyTables.BinaryContraction.card_fixedRest line 526
theorem OAI.ContingencyTables.BinaryContraction.fixIncluded_omission line 532
Source documentation
Complementation swaps a fixed inclusion with a fixed exclusion.
```
theorem fixIncluded_omission (f : Set I → ℝ) (k : ℕ) (hk : 1 ≤ k)
    (hsig : OmissionProperty f k) (p : I) : OmissionProperty (fixIncluded f p) (k - 1) := by
…
```
Mentions: OAI.ContingencyTables.BinaryContraction.OmissionProperty, OAI.ContingencyTables.BinaryContraction.fixIncluded
theorem OAI.ContingencyTables.BinaryContraction.fixExcluded_omission line 544
Source documentation
Complementation swaps a fixed exclusion with a fixed inclusion.
```
theorem fixExcluded_omission (f : Set I → ℝ) (k : ℕ)
    (hsig : OmissionProperty f k) (p : I) : OmissionProperty (fixExcluded f p) k := by
…
```
Mentions: OAI.ContingencyTables.BinaryContraction.OmissionProperty, OAI.ContingencyTables.BinaryContraction.fixExcluded