MaximalPairs.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Finite maximal selection of jointly independent direction/difference pairs.

def OAI.TwoPointCorrelations.pairFamily line 15
def OAI.TwoPointCorrelations.insertPairEquiv line 18
theorem OAI.TwoPointCorrelations.independent_insert_pair line 51

theorem OAI.TwoPointCorrelations.exists_maximal_independent_pairs line 62

Source documentation

A maximal collection exists among the finitely many candidate pairs. No further pair can be adjoined, and its span has twice the selected size.

theorem exists_maximal_independent_pairs (v : κ → Fin 2 → V) :
    ∃ S : Finset κ, LinearIndependent K (pairFamily v S) ∧
      Module.finrank K (span K (Set.range (pairFamily v S))) = 2 * S.card ∧
      ∀ k ∉ S, ¬LinearIndependent K (Sum.elim (pairFamily v S) (v k)) := by
…

Mentions: OAI.TwoPointCorrelations.pairFamily

theorem OAI.TwoPointCorrelations.exists_maximal_pair_quotient line 85

Source documentation

Maximal pair selection forces each unselected direction/difference pair onto one line in the quotient by the selected span.

theorem exists_maximal_pair_quotient (v : κ → Fin 2 → V) :
    ∃ S : Finset κ, LinearIndependent K (pairFamily v S) ∧
      Module.finrank K (span K (Set.range (pairFamily v S))) = 2 * S.card ∧
      ∀ k, (span K (Set.range (pairFamily v S))).mkQ (v k 1) ≠ 0 →
        ∃ c : K, (span K (Set.range (pairFamily v S))).mkQ (v k 0) =
          c • (span K (Set.range (pairFamily v S))).mkQ (v k 1) := by
…

Mentions: OAI.TwoPointCorrelations.pairFamily

theorem OAI.TwoPointCorrelations.independent_pairFamily_mono line 107
Source documentation
Restriction to fewer candidate pairs preserves joint independence.
```
theorem independent_pairFamily_mono (v : κ → Fin 2 → V) {S T : Finset κ}
    (hTS : T ⊆ S) (hS : LinearIndependent K (pairFamily v S)) :
    LinearIndependent K (pairFamily v T) := by
…
```
Mentions: OAI.TwoPointCorrelations.pairFamily

theorem OAI.TwoPointCorrelations.exists_small_maximal_independent_pairs line 120

Source documentation

Excluding r independent pairs bounds every maximal collection by r-1.

theorem exists_small_maximal_independent_pairs (v : κ → Fin 2 → V) (r : ℕ)
    (hno : ∀ S : Finset κ, S.card = r → ¬LinearIndependent K (pairFamily v S)) :
    ∃ S : Finset κ, S.card < r ∧ LinearIndependent K (pairFamily v S) ∧
      Module.finrank K (span K (Set.range (pairFamily v S))) = 2 * S.card ∧
      ∀ k ∉ S, ¬LinearIndependent K (Sum.elim (pairFamily v S) (v k)) := by
…

Mentions: OAI.TwoPointCorrelations.pairFamily