HighRankMinor.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Independent lit pairs yield a disjoint integral minor

The coordinates of the selected control directions are removed before the minor is chosen. All selections use the fixed coefficient matrix, and no statement about invertibility modulo a sampled prime is needed.

lemma OAI.TwoPointCorrelations.pairFamily_sum_independent line 25

Source documentation

Convert the pair-family form used by maximal selection to two blocks.

lemma pairFamily_sum_independent (w : ρ → α → K) (control : ρ → α)
    (hind : LinearIndependent K (fun z : ρ × Fin 2 =>
      if z.2 = 0 then w z.1 else Pi.basisFun K α (control z.1))) :
    LinearIndependent K (Sum.elim w (fun i => Pi.basisFun K α (control i))) := by
…

lemma OAI.TwoPointCorrelations.independent_control_injective line 38
def OAI.TwoPointCorrelations.controlCoordinates line 46
def OAI.TwoPointCorrelations.deleteControlCoordinates line 48
lemma OAI.TwoPointCorrelations.deleteControlCoordinates_ker_le line 52

theorem OAI.TwoPointCorrelations.independent_rows_outside_controls line 75

Source documentation

The selected difference rows remain independent after every control coordinate has been deleted.

theorem independent_rows_outside_controls (w : ρ → α → K) (control : ρ → α)
    (hind : LinearIndependent K (Sum.elim w (fun i => Pi.basisFun K α (control i)))) :
    LinearIndependent K (fun i => deleteControlCoordinates control (w i)) := by
…

Mentions: OAI.TwoPointCorrelations.deleteControlCoordinates

theorem OAI.TwoPointCorrelations.independent_rows_minor line 86

Source documentation

Any independent finite row family has a square nonsingular column minor.

theorem independent_rows_minor (w : ρ → α → K) (hind : LinearIndependent K w) :
    ∃ pivot : ρ → α, Function.Injective pivot ∧
      (Matrix.of fun i j => w i (pivot j)).det ≠ 0 := by
…

theorem OAI.TwoPointCorrelations.independent_pairs_disjoint_minor line 112

Source documentation

The minor columns are disjoint from every selected controlling label.

theorem independent_pairs_disjoint_minor (w : ρ → α → K) (control : ρ → α)
    (hind : LinearIndependent K (Sum.elim w (fun i => Pi.basisFun K α (control i)))) :
    Function.Injective control ∧ ∃ pivot : ρ → α, Function.Injective pivot ∧
      (∀ i j, pivot i ≠ control j) ∧
      (Matrix.of fun i j => w i (pivot j)).det ≠ 0 := by
…

theorem OAI.TwoPointCorrelations.integral_independent_pairs_disjoint_minor line 133

Source documentation

Real independence of integral rows produces a nonzero integral minor; the determinant is transported through the injective integer cast.

theorem integral_independent_pairs_disjoint_minor (w : ρ → α → ℤ) (control : ρ → α)
    (hind : LinearIndependent ℝ (Sum.elim (fun i z => (w i z : ℝ))
      (fun i => Pi.basisFun ℝ α (control i)))) :
    Function.Injective control ∧ ∃ pivot : ρ → α, Function.Injective pivot ∧
      (∀ i j, pivot i ≠ control j) ∧ (Matrix.of fun i j => w i (pivot j)).det ≠ 0 := by
…