QuotientLines.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Quotient coordinates in the forest code

The quotient keeps a basis chosen from the original coordinate directions. Failure to extend an independent family by a direction and a departure difference forces that difference onto the corresponding quotient line.

theorem OAI.TwoPointCorrelations.quotient_line_of_nonextendable_pair line 22

Source documentation

The exact maximality consequence used for a regular label.

theorem quotient_line_of_nonextendable_pair (v : κ → V) (hv : LinearIndependent K v)
    (x y : V) (hx : (span K (Set.range v)).mkQ x ≠ 0)
    (hmax : ¬LinearIndependent K (Sum.elim v ![y, x])) :
    ∃ c : K, (span K (Set.range v)).mkQ y = c • (span K (Set.range v)).mkQ x := by
…

theorem OAI.TwoPointCorrelations.quotient_departures_on_line line 45

Source documentation

All designated departures for a regular label lie on one quotient line.

theorem quotient_departures_on_line (v : κ → V) (hv : LinearIndependent K v)
    (direction : V) (departure : ι → V) (base : ι)
    (hx : (span K (Set.range v)).mkQ direction ≠ 0)
    (hmax : ∀ i, ¬LinearIndependent K
      (Sum.elim v ![departure i - departure base, direction])) :
    ∀ i, ∃ c : K, (span K (Set.range v)).mkQ (departure i) =
      (span K (Set.range v)).mkQ (departure base) +
        c • (span K (Set.range v)).mkQ direction := by
…

theorem OAI.TwoPointCorrelations.exists_coordinate_quotient_basis line 63

Source documentation

A coordinate basis survives the quotient after exactly dim D labels are omitted. This fixes the count, even when the subspace is not spanned by coordinate vectors.

theorem exists_coordinate_quotient_basis [Fintype ι] [DecidableEq ι]
    (D : Submodule K (ι → K)) :
    ∃ S : Finset ι, Sᶜ.card = Module.finrank K D ∧
      LinearIndependent K (fun i : S => D.mkQ (Pi.basisFun K ι i)) ∧
      span K (Set.range (fun i : S => D.mkQ (Pi.basisFun K ι i))) = ⊤ := by
…