SelectedPairRank.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A maximal jointly independent pair family yields independent blocks of difference vectors and controlling coordinate vectors.

theorem OAI.TwoPointCorrelations.selected_label_pairs_independent line 15

theorem OAI.TwoPointCorrelations.selected_label_pairs_disjoint_minor line 30

Source documentation

The exact finite maximal-pair representation produces the disjoint coordinate minor without introducing any additional rank premise.

theorem selected_label_pairs_disjoint_minor (label : ι → α) (offset : ι → α → ℝ)
    (S : Finset (EqualLabelPairs label))
    (hind : LinearIndependent ℝ (pairFamily (labelPairVectors label offset) S)) :
    Function.Injective (fun p : S => p.val.val.1) ∧
      ∃ pivot : S → α, Function.Injective pivot ∧
        (∀ (i j : S), pivot i ≠ j.val.val.1) ∧
        (Matrix.of fun (i j : S) =>
          (offset i.val.val.2.1 - offset i.val.val.2.2) (pivot j)).det ≠ 0 := by
…

Mentions: OAI.TwoPointCorrelations.EqualLabelPairs, OAI.TwoPointCorrelations.pairFamily, OAI.TwoPointCorrelations.labelPairVectors