RegularQuotient.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The low-rank hypothesis produces the regular quotient directions used in forest coding.

def OAI.TwoPointCorrelations.EqualLabelPairs line 17
Source documentation
All pairs of departures carrying the same label. A caller may restrict ι to the lit occurrences before applying this construction.
```
def EqualLabelPairs (label : ι → α) :=
…
```
instance OAI.TwoPointCorrelations.equalLabelPairsFintype line 20
instance OAI.TwoPointCorrelations.equalLabelPairsDecidableEq line 23
def OAI.TwoPointCorrelations.labelPairVectors line 28
Source documentation
Difference first, coordinate direction second, so the generic maximal pair theorem applies without reordering the joint independent family.
```
noncomputable def labelPairVectors (label : ι → α) (offset : ι → α → K)
    (p : EqualLabelPairs label) : Fin 2 → (α → K) :=
…
```
Mentions: OAI.TwoPointCorrelations.EqualLabelPairs

theorem OAI.TwoPointCorrelations.exists_regular_quotient line 35

Source documentation

The algebraic part of forest coding: fewer than r independent pairs leave fewer than 2r omitted labels; all remaining departures for a label lie along its independent coordinate direction in the quotient.

theorem exists_regular_quotient (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 α), Rᶜ.card < 2 * r ∧
      LinearIndependent K (fun z : R => D.mkQ (Pi.basisFun K α z)) ∧
      span K (Set.range (fun z : R => D.mkQ (Pi.basisFun K α z))) = ⊤ ∧
      ∀ (z : R) i j, label i = z → label j = z →
        ∃ c : K, D.mkQ (offset i) = D.mkQ (offset j) +
          c • D.mkQ (Pi.basisFun K α z) := by
…

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