RegularLineAnchors.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Choosing one common affine line for all lit occurrences of each regular label.

theorem OAI.TwoPointCorrelations.exists_regular_line_anchors line 16

Source documentation

A low-rank family gives independent regular directions and one anchor per label, shared by every lit departure in every perfect block.

theorem exists_regular_line_anchors (label : ι → α) (offset : ι → α → K) (r : ℕ)
    (hno : ∀ S : Finset (EqualLabelPairs label), S.card = r →
      ¬LinearIndependent K (pairFamily (labelPairVectors label offset) S)) :
    ∃ (D : Submodule K (α → K)) (R : Finset α)
      (anchor : R → (α → K) ⧸ D), Rᶜ.card < 2 * r ∧
      LinearIndependent K (fun z : R => D.mkQ (Pi.basisFun K α z)) ∧
      ∀ (z : R) i, label i = z →
        ∃ c : K, D.mkQ (offset i) = anchor z + c • D.mkQ (Pi.basisFun K α z) := by
…

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