ObservedColumnRank.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The ambient column rank is exactly the rank on its observed prime classes.

lemma OAI.TwoPointCorrelations.resampledTupleColumnPattern_label_map line 12
lemma OAI.TwoPointCorrelations.resampledTupleColumnPattern_coefficient line 18

theorem OAI.TwoPointCorrelations.tuple_column_observed_rank_iff line 26

Source documentation

The selected rank witness is unchanged by restriction to the smaller resampling space.

theorem tuple_column_observed_rank_iff {J R : ℕ} {P : Fin J → Finset ℕ}
    {ρ : Type*} (w : ColumnPrimeAssignment J R P) (hR : 0 < R)
    (forward : Fin R → Bool) (padding : Fin R → ℕ) (j : Fin J) (h : ℕ)
    (left right : ρ → ℕ) (control : ρ → patternClasses (w j)) :
    LinearIndependent ℝ (Sum.elim
      (fun i => formalDeparture (resampledTupleColumnPattern w hR forward padding j).label
          (fun t => ((resampledTupleColumnPattern w hR forward padding j).coefficient h t : ℝ)) (left i) -
        formalDeparture (resampledTupleColumnPattern w hR forward padding j).label
          (fun t => ((resampledTupleColumnPattern w hR forward padding j).coefficient h t : ℝ)) (right i))
      (fun i => Pi.basisFun ℝ (patternClasses (w j)) (control i))) ↔
    LinearIndependent ℝ (Sum.elim
      (fun i => formalDeparture (tupleColumnPattern w hR forward padding j).label
…

Mentions: OAI.TwoPointCorrelations.ColumnPrimeAssignment, OAI.TwoPointCorrelations.patternClasses, OAI.TwoPointCorrelations.formalDeparture, OAI.TwoPointCorrelations.resampledTupleColumnPattern, OAI.TwoPointCorrelations.tupleColumnPattern