TensorClassification.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

From finite-stage pairings to permutation operators

The operator classification follows from the finite-stage coefficient identity, using density, same-side-pair elimination, and completed tensor permutations. The finite-stage identity remains a separately stated prerequisite.

def OAI.KadisonSimilarity.sourceFirstRank line 21
Source documentation
Source letters precede all test letters in the orientation of a pair.
```
def sourceFirstRank {k l : ℕ} : Fin k ⊕ Fin l → ℕ :=
…
```
theorem OAI.KadisonSimilarity.sourceFirstRank_injective line 24
theorem OAI.KadisonSimilarity.crossPairingEquiv_left line 39
theorem OAI.KadisonSimilarity.crossPairingEquiv_right line 44
theorem OAI.KadisonSimilarity.pairingPolynomial_cross line 50
Source documentation
For a cross pairing, the full polynomial has exactly one factor per source slot.
```
theorem pairingPolynomial_cross {k l : ℕ}
    (B : E →L[ℂ] E →L[ℂ] ℂ) (P : PerfectMatching (Fin k ⊕ Fin l))
    (hcross : IsCrossPairing P.1) (x : Fin k → E) (z : Fin l → E) :
    pairingPolynomial sourceFirstRank B P (Sum.elim x z) =
      ∏ i, B (x i) (z (crossPairingEquiv P.1 P.2.1 hcross i)) := by
…
```
Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.IsCrossPairing, OAI.KadisonSimilarity.pairingPolynomial, OAI.KadisonSimilarity.sourceFirstRank, OAI.KadisonSimilarity.crossPairingEquiv

theorem OAI.KadisonSimilarity.pairingPolynomial_eq_permutation_coefficient line 72

Source documentation

The remaining contraction is the matrix coefficient of a position permutation.

theorem pairingPolynomial_eq_permutation_coefficient {n : ℕ}
    (J : E → E) (B : E →L[ℂ] E →L[ℂ] ℂ)
    (hB : ∀ x y, B x (J y) = inner ℂ y x)
    (P : PerfectMatching (Fin n ⊕ Fin n)) (hcross : IsCrossPairing P.1)
    (x y : Fin n → E) :
    pairingPolynomial sourceFirstRank B P (Sum.elim x (J ∘ y)) =
      inner ℂ (completedTensorWord y)
        (completedTensorPermutation (crossPairingEquiv P.1 P.2.1 hcross)
          (completedTensorWord x)) := by
…

Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.IsCrossPairing, OAI.KadisonSimilarity.pairingPolynomial, OAI.KadisonSimilarity.sourceFirstRank, OAI.KadisonSimilarity.completedTensorWord, OAI.KadisonSimilarity.completedTensorPermutation, OAI.KadisonSimilarity.crossPairingEquiv

instance OAI.KadisonSimilarity.crossMatchingFintype line 88
def OAI.KadisonSimilarity.crossPairingOperator line 93
Source documentation
The explicit finite sum of the operators indexed by cross pairings.
```
def crossPairingOperator {n : ℕ}
    (c : PerfectMatching (Fin n ⊕ Fin n) → ℂ) :
    CompletedTensorWord E n →L[ℂ] CompletedTensorWord E n :=
…
```
Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.CompletedTensorWord

theorem OAI.KadisonSimilarity.tensorOperator_eq_crossPairingOperator_of_stages line 102

Source documentation

Density and boundedness eliminate all same-side terms in the finite-stage formula and identify the completed operator as a finite sum of permutations.

theorem tensorOperator_eq_crossPairingOperator_of_stages {n : ℕ}
    (Y : CompletedTensorWord E n →L[ℂ] CompletedTensorWord E n)
    (J : E → E) (hJ : Continuous J) (hJJ : Function.Involutive J)
    (B : E →L[ℂ] E →L[ℂ] ℂ) (hB : ∀ x y, B x (J y) = inner ℂ y x)
    (c : PerfectMatching (Fin n ⊕ Fin n) → ℂ)
    (h : ℕ → E) (hh : Orthonormal ℂ h) (hfix : ∀ m, J (h m) = h m)
    (S : ℕ → Set E) (hmono : Monotone S) (hdense : Dense (⋃ m, S m))
    (hstage : ∀ m, ∀ v : Fin n ⊕ Fin n → E, (∀ i, v i ∈ S m) →
      tracialWordCoefficient Y J v =
        ∑ P, c P * pairingPolynomial sourceFirstRank B P v) :
    Y = crossPairingOperator c := by
…

Mentions: OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.tracialWordCoefficient, OAI.KadisonSimilarity.pairingPolynomial, OAI.KadisonSimilarity.sourceFirstRank, OAI.KadisonSimilarity.crossPairingOperator

theorem OAI.KadisonSimilarity.crossPairingOperator_mem_span_permutations line 157
Source documentation
The usual statement as membership in the span of permutation operators.
```
theorem crossPairingOperator_mem_span_permutations {n : ℕ}
    (c : PerfectMatching (Fin n ⊕ Fin n) → ℂ) :
    crossPairingOperator (E := E) c ∈ Submodule.span ℂ
…
```
Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.crossPairingOperator

theorem OAI.KadisonSimilarity.crossPairingOperator_constant line 169

Source documentation

Repeated-letter words see only the sum of the surviving coefficients.

theorem crossPairingOperator_constant {n : ℕ}
    (c : PerfectMatching (Fin n ⊕ Fin n) → ℂ) (x : E) :
    crossPairingOperator c (completedTensorWord (fun _ : Fin n => x)) =
      (∑ P : {P : PerfectMatching (Fin n ⊕ Fin n) // IsCrossPairing P.1}, c P.1) •
        completedTensorWord (fun _ : Fin n => x) := by
…

Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.crossPairingOperator, OAI.KadisonSimilarity.completedTensorWord, OAI.KadisonSimilarity.IsCrossPairing