MultiplicityClassification.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

Hilbert multiplicities in the invariant-intertwiner theorem

Scalar matrix coefficients in the multiplicity Hilbert space are genuine bounded endpoint intertwiners. Tensor totality reconstructs the full operator from these slices. Repeated-letter compressions provide the bounded operator on the multiplicity space used in propagation.

def OAI.KadisonSimilarity.hilbertTensorInsert line 26
Source documentation
Insert the first tensor coordinate in a completed Hilbert tensor product.
```
def hilbertTensorInsert (a : G) : H →L[ℂ] HilbertTensor G H :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor
theorem OAI.KadisonSimilarity.hilbertTensorInsert_apply line 29
theorem OAI.KadisonSimilarity.norm_hilbertTensorInsert line 32
theorem OAI.KadisonSimilarity.inner_hilbertTensorInsert line 37
theorem OAI.KadisonSimilarity.continuousLinearMap_ext_hilbertTensorInsert line 44
Source documentation
Totality of completed elementary Hilbert tensors.
```
theorem continuousLinearMap_ext_hilbertTensorInsert
    (f g : HilbertTensor G H →L[ℂ] L)
    (h : ∀ a x, f (hilbertTensorInsert a x) = g (hilbertTensorInsert a x)) : f = g := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.hilbertTensorInsert
def OAI.KadisonSimilarity.hilbertTensorLift line 65
Source documentation
The lift of an operator leaving the first tensor coordinate unchanged.
```
def hilbertTensorLift (T : H →L[ℂ] K) : HilbertTensor G H →L[ℂ] HilbertTensor G K :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor
theorem OAI.KadisonSimilarity.hilbertTensorLift_insert line 68
theorem OAI.KadisonSimilarity.tensorSlice_insert line 78
def OAI.KadisonSimilarity.multiplicitySlice line 83
Source documentation
A scalar matrix coefficient in the multiplicity space.
```
def multiplicitySlice (Y : HilbertTensor G H →L[ℂ] HilbertTensor G K) (a b : G) : H →L[ℂ] K :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor
theorem OAI.KadisonSimilarity.tensorSlice_lift line 86

theorem OAI.KadisonSimilarity.multiplicitySlice_intertwines line 94

Source documentation

Lifted intertwining implies the scalar slice intertwining.

theorem multiplicitySlice_intertwines
    (Y : HilbertTensor G H →L[ℂ] HilbertTensor G K)
    (S : H →L[ℂ] H) (T : K →L[ℂ] K)
    (hY : Y.comp (hilbertTensorLift S) = (hilbertTensorLift T).comp Y) (a b : G) :
    (multiplicitySlice Y a b).comp S = T.comp (multiplicitySlice Y a b) := by
…

Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.hilbertTensorLift, OAI.KadisonSimilarity.multiplicitySlice

theorem OAI.KadisonSimilarity.inner_multiplicitySlice line 111
Source documentation
Inner products with elementary tensors are exactly multiplicity slices.
```
theorem inner_multiplicitySlice (Y : HilbertTensor G H →L[ℂ] HilbertTensor G K)
    (a b : G) (x : H) (z : K) :
    inner ℂ z (multiplicitySlice Y a b x) =
      inner ℂ (hilbertTensorInsert b z) (Y (hilbertTensorInsert a x)) := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.multiplicitySlice, OAI.KadisonSimilarity.hilbertTensorInsert
theorem OAI.KadisonSimilarity.multiplicitySlice_ext line 142
Source documentation
All scalar multiplicity slices determine the full bounded operator.
```
theorem multiplicitySlice_ext (Y Z : HilbertTensor G H →L[ℂ] HilbertTensor G K)
    (hslice : ∀ a b, multiplicitySlice Y a b = multiplicitySlice Z a b) : Y = Z := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.multiplicitySlice
theorem OAI.KadisonSimilarity.multiplicitySlice_zero line 162
theorem OAI.KadisonSimilarity.hilbertTensor_ext_inner_insert line 169
Source documentation
Elementary tensor coefficients separate vectors in the completed product.
```
theorem hilbertTensor_ext_inner_insert (z w : HilbertTensor G H)
    (h : ∀ a x, inner ℂ (hilbertTensorInsert a x) z =
      inner ℂ (hilbertTensorInsert a x) w) : z = w := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.hilbertTensorInsert
def OAI.KadisonSimilarity.hilbertTensorRightInsert line 182
Source documentation
Insert a fixed second tensor vector, leaving the multiplicity variable free.
```
def hilbertTensorRightInsert (w : H) : G →L[ℂ] HilbertTensor G H :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor
theorem OAI.KadisonSimilarity.hilbertTensorRightInsert_apply line 186
theorem OAI.KadisonSimilarity.norm_hilbertTensorRightInsert_le line 190
def OAI.KadisonSimilarity.multiplicityCompression line 199
Source documentation
Compression to a chosen unit vector in the non-multiplicity factor.
```
def multiplicityCompression (Y : HilbertTensor G H →L[ℂ] HilbertTensor G H) (w : H) : G →L[ℂ] G :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor
theorem OAI.KadisonSimilarity.norm_multiplicityCompression_le line 203
theorem OAI.KadisonSimilarity.inner_multiplicityCompression line 220
theorem OAI.KadisonSimilarity.norm_endpointWord_constant line 238
Source documentation
A unit endpoint and unit repeated letter give a unit vector at every level.
```
theorem norm_endpointWord_constant {n : ℕ} (Ω : E) (r : F)
    (hΩ : ‖Ω‖ = 1) (hr : ‖r‖ = 1) :
    ‖endpointWord Ω (fun _ : Fin n => r)‖ = 1 := by
…
```
Mentions: OAI.KadisonSimilarity.endpointWord
theorem OAI.KadisonSimilarity.exists_repeated_operator_of_slice_permutations line 248
Source documentation
Slice permutation formulas give one bounded multiplicity operator that acts on every repeated-letter word. Its definition uses a single unit reference word, but the conclusion holds for all letters, with no dependence on that word.
```
theorem exists_repeated_operator_of_slice_permutations {n : ℕ}
    (Y : HilbertTensor G (EndpointTensor E F n) →L[ℂ]
      HilbertTensor G (EndpointTensor E F n))
    (Ω : E) (hΩ : ‖Ω‖ = 1) (r₀ : F) (hr₀ : ‖r₀‖ = 1)
    (hslices : ∀ a b : G, ∃ c : PerfectMatching (Fin n ⊕ Fin n) → ℂ,
      multiplicitySlice Y a b = endpointAmplification (crossPairingOperator c)) :
    ∃ B : G →L[ℂ] G, ‖B‖ ≤ ‖Y‖ ∧ ∀ a d r,
      Y (hilbertTensorInsert a (endpointWord d (fun _ : Fin n => r))) =
        hilbertTensorInsert (B a) (endpointWord d (fun _ : Fin n => r)) := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.multiplicitySlice, OAI.KadisonSimilarity.endpointAmplification, OAI.KadisonSimilarity.crossPairingOperator, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.endpointWord

theorem OAI.KadisonSimilarity.multiplicityCompression_eq_of_repeated_action line 283

Source documentation

The compression along any unit repeated tail recovers the same multiplicity operator. This gives explicit independence of the reference tail.

theorem multiplicityCompression_eq_of_repeated_action {n : ℕ}
    (Y : HilbertTensor G (EndpointTensor E F n) →L[ℂ]
      HilbertTensor G (EndpointTensor E F n)) (B : G →L[ℂ] G)
    (hact : ∀ a d r, Y (hilbertTensorInsert a (endpointWord d (fun _ : Fin n => r))) =
      hilbertTensorInsert (B a) (endpointWord d (fun _ : Fin n => r)))
    (Ω : E) (hΩ : ‖Ω‖ = 1) (r : F) (hr : ‖r‖ = 1) :
    multiplicityCompression Y (endpointWord Ω (fun _ : Fin n => r)) = B := by
…

Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.endpointWord, OAI.KadisonSimilarity.multiplicityCompression

structure OAI.KadisonSimilarity.MultiplicityMatrixCovariance line 300
Source documentation
Word covariance before taking scalar multiplicity slices.
```
structure MultiplicityMatrixCovariance
    (R : MatrixHilbertStage (E := E) (F := F) (α := α)) (J : F →ₗᵢ⋆[ℂ] F)
…
```
Mentions: OAI.KadisonSimilarity.MatrixHilbertStage
def OAI.KadisonSimilarity.MultiplicityMatrixCovariance.slice line 320
Source documentation
Taking a scalar multiplicity coefficient preserves actual word covariance.
```
def MultiplicityMatrixCovariance.slice
    {R : MatrixHilbertStage (E := E) (F := F) (α := α)} {J : F →ₗᵢ⋆[ℂ] F}
…
```
Mentions: OAI.KadisonSimilarity.MatrixHilbertStage
theorem OAI.KadisonSimilarity.multiplicity_intertwiner_zero_of_schurWeyl line 337
Source documentation
All unequal-level blocks vanish, including their Hilbert multiplicities.
```
theorem multiplicity_intertwiner_zero_of_schurWeyl
    (T : TracialMatrixTower (E := E) (F := F) (A := A))
…
```
Mentions: OAI.KadisonSimilarity.TracialMatrixTower
theorem OAI.KadisonSimilarity.exists_multiplicity_repeated_operator_of_schurWeyl line 359
Source documentation
On equal levels a bounded operator on the multiplicity factor acts on all repeated-letter words, independently of the unit repeated letter.
```
theorem exists_multiplicity_repeated_operator_of_schurWeyl {n : ℕ}
    (T : TracialMatrixTower (E := E) (F := F) (A := A))
…
```
Mentions: OAI.KadisonSimilarity.TracialMatrixTower