InvariantTensors.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

Matrix-unit isolation of invariant-tensor coefficients

The permutation contractions are given by their coordinate sums. Their normalization is the number of cycles, including fixed points. We prove the matrix-unit isolation and uniqueness steps in the invariant-intertwiner argument. Schur--Weyl spanning is expressed as a multilinear-form property.

def OAI.KadisonSimilarity.permutationContraction line 27
Source documentation
The coordinate formula for the trace contraction of a permutation tensor. Each index follows the successor convention in the manuscript.
```
def permutationContraction (π : Equiv.Perm ι) (v : ι → Matrix α α ℂ) : ℂ :=
…
```
def OAI.KadisonSimilarity.tensorMatrixUnit line 31
Source documentation
A matrix unit with row a and column b.
```
def tensorMatrixUnit (a b : α) : Matrix α α ℂ :=
…
```
theorem OAI.KadisonSimilarity.tensorMatrixUnit_apply line 35
def OAI.KadisonSimilarity.permutationTest line 40
Source documentation
Distinct labels assigned to the vertices of a permutation give its test tuple of matrix units.
```
def permutationTest (j : ι → α) (π : Equiv.Perm ι) : ι → Matrix α α ℂ :=
…
```
theorem OAI.KadisonSimilarity.contraction_test_summand line 44
theorem OAI.KadisonSimilarity.permutationContraction_test line 72
Source documentation
A matrix-unit tuple isolates exactly its prescribed permutation. This proves the independence assertion, independently of Schur--Weyl duality.
```
theorem permutationContraction_test (j : ι → α) (hj : Function.Injective j)
    (π ρ : Equiv.Perm ι) :
    permutationContraction ρ (permutationTest j π) = if ρ = π then 1 else 0 := by
…
```
Mentions: OAI.KadisonSimilarity.permutationContraction, OAI.KadisonSimilarity.permutationTest
def OAI.KadisonSimilarity.permutationCycleCount line 80
Source documentation
The number of cycles of a permutation, with singleton cycles included.
```
def permutationCycleCount (π : Equiv.Perm ι) : ℕ :=
…
```
def OAI.KadisonSimilarity.normalizedPermutationContraction line 85
Source documentation
Normalizing each cycle trace by the matrix dimension gives the coordinate formula for the normalized cycle-trace form Φ_π in the paper.
```
def normalizedPermutationContraction (π : Equiv.Perm ι)
    (v : ι → Matrix α α ℂ) : ℂ :=
…
```
theorem OAI.KadisonSimilarity.normalizedPermutationContraction_test line 89
theorem OAI.KadisonSimilarity.normalizedPermutationContraction_sum_test line 99
Source documentation
Evaluation at the associated matrix units recovers one coefficient of any expansion in normalized permutation contractions.
```
theorem normalizedPermutationContraction_sum_test
    (j : ι → α) (hj : Function.Injective j) (π : Equiv.Perm ι)
    (c : Equiv.Perm ι → ℂ) :
    (∑ ρ, c ρ * normalizedPermutationContraction ρ (permutationTest j π)) =
      c π * (Fintype.card α : ℂ)⁻¹ ^ permutationCycleCount π := by
…
```
Mentions: OAI.KadisonSimilarity.normalizedPermutationContraction, OAI.KadisonSimilarity.permutationTest, OAI.KadisonSimilarity.permutationCycleCount

theorem OAI.KadisonSimilarity.normalizedPermutationContraction_coefficients_unique line 109

Source documentation

In the stable range, expansion coefficients are unique. This is the specific independence step needed when comparing nested matrix stages.

theorem normalizedPermutationContraction_coefficients_unique
    [Nonempty α] (j : ι → α) (hj : Function.Injective j)
    (c d : Equiv.Perm ι → ℂ)
    (heq : ∀ v : ι → Matrix α α ℂ,
      (∑ π, c π * normalizedPermutationContraction π v) =
        ∑ π, d π * normalizedPermutationContraction π v) : c = d := by
…

Mentions: OAI.KadisonSimilarity.normalizedPermutationContraction

def OAI.KadisonSimilarity.permutationContractionMultilinear line 123
Source documentation
The contraction is multilinear in its matrix variables.
```
def permutationContractionMultilinear (π : Equiv.Perm ι) :
    MultilinearMap ℂ (fun _ : ι => Matrix α α ℂ) ℂ :=
…
```
theorem OAI.KadisonSimilarity.permutationContractionMultilinear_apply line 129

def OAI.KadisonSimilarity.normalizedPermutationMultilinear line 135

Source documentation

The bundled normalized cycle-trace form.

def normalizedPermutationMultilinear (π : Equiv.Perm ι) :
    MultilinearMap ℂ (fun _ : ι => Matrix α α ℂ) ℂ :=
…

theorem OAI.KadisonSimilarity.normalizedPermutationMultilinear_apply line 141
def OAI.KadisonSimilarity.UnitaryConjugationInvariant line 147
Source documentation
Invariance under simultaneous conjugation of all matrix arguments.
```
def UnitaryConjugationInvariant
    (F : MultilinearMap ℂ (fun _ : ι => Matrix α α ℂ) ℂ) : Prop :=
…
```
def OAI.KadisonSimilarity.SchurWeylMultilinearSpanning line 157
Source documentation
The finite-dimensional consequence of Schur--Weyl duality used in the paper. Source: Grinko--Ozols, Linear programming with unitary-equivariant constraints, Comm. Math. Phys. 405 (2024), article 278, Theorem 3.1, combined with the nondegenerate matrix trace pairing. Matrix-unit isolation and uniqueness establish independence in the stable range.
```
def SchurWeylMultilinearSpanning (ι α : Type*) [Fintype ι] [DecidableEq ι]
    [Fintype α] [DecidableEq α] : Prop :=
…
```
theorem OAI.KadisonSimilarity.existsUnique_invariant_expansion line 166
Source documentation
The stable-range uniqueness part of the invariant expansion follows from the explicit tests, and is not a second published assumption.
```
theorem existsUnique_invariant_expansion [Nonempty α]
    (spanning : SchurWeylMultilinearSpanning ι α)
    (j : ι → α) (hj : Function.Injective j)
    (F : MultilinearMap ℂ (fun _ : ι => Matrix α α ℂ) ℂ)
    (hF : UnitaryConjugationInvariant F) :
    ∃! c : Equiv.Perm ι → ℂ, ∀ v,
      F v = ∑ π, c π * normalizedPermutationContraction π v := by
…
```
Mentions: OAI.KadisonSimilarity.SchurWeylMultilinearSpanning, OAI.KadisonSimilarity.UnitaryConjugationInvariant, OAI.KadisonSimilarity.normalizedPermutationContraction
theorem OAI.KadisonSimilarity.norm_normalizedPermutationContraction_sum_test line 181
Source documentation
The norm of the isolated coefficient has exactly the decay factor used in the endpoint estimate.
```
theorem norm_normalizedPermutationContraction_sum_test
    (j : ι → α) (hj : Function.Injective j) (π : Equiv.Perm ι)
    (c : Equiv.Perm ι → ℂ) :
    ‖∑ ρ, c ρ * normalizedPermutationContraction ρ (permutationTest j π)‖ =
      ‖c π‖ * (Fintype.card α : ℝ) ^ (-(permutationCycleCount π : ℝ)) := by
…
```
Mentions: OAI.KadisonSimilarity.normalizedPermutationContraction, OAI.KadisonSimilarity.permutationTest, OAI.KadisonSimilarity.permutationCycleCount

theorem OAI.KadisonSimilarity.cycle_coefficient_zero_of_matrix_stage_tests line 193

Source documentation

Passing the actual matrix-stage test estimate to the coefficient limit removes every permutation below the cycle threshold. The finite-stage forms and their test estimates are explicit local data; the invariant conclusion is not assumed.

theorem cycle_coefficient_zero_of_matrix_stage_tests
    (p k l : ℕ) (m : ℕ → ℕ) (hm : ∀ s, 0 < m s)
    (hmp : ∀ s, p ≤ m s)
    (hmTop : Filter.Tendsto (fun s => (m s : ℝ)) Filter.atTop Filter.atTop)
    (c : Equiv.Perm (Fin p) → ℂ) (π : Equiv.Perm (Fin p)) (C : ℝ)
    (hfew : (permutationCycleCount π : ℝ) < 1 + ((k : ℝ) + l) / 2)
    (htest : ∀ s,
      ‖∑ ρ, c ρ * normalizedPermutationContraction ρ
          (permutationTest (Fin.castLE (hmp s)) π)‖ ≤
        C * (m s : ℝ) ^ (-1 - ((k : ℝ) + l) / 2)) : c π = 0 := by
…

Mentions: OAI.KadisonSimilarity.permutationCycleCount, OAI.KadisonSimilarity.normalizedPermutationContraction, OAI.KadisonSimilarity.permutationTest

abbrev OAI.KadisonSimilarity.CycleConstantLabelings line 215
Source documentation
Labels constant along each cycle are exactly functions on the cycle quotient. This is the counting mechanism behind trace normalization.
```
abbrev CycleConstantLabelings (π : Equiv.Perm ι) (β : Type*) :=
…
```
theorem OAI.KadisonSimilarity.cycleConstantLabelings_eq_of_sameCycle line 219
def OAI.KadisonSimilarity.cycleConstantLabelingsEquiv line 231
Source documentation
A concrete equivalence, rather than an assumed formula for orbit counts.
```
def cycleConstantLabelingsEquiv (π : Equiv.Perm ι) :
    CycleConstantLabelings π β ≃ (Quotient (Equiv.Perm.SameCycle.setoid π) → β) where
…
```
Mentions: OAI.KadisonSimilarity.CycleConstantLabelings
theorem OAI.KadisonSimilarity.card_cycleConstantLabelings line 242
def OAI.KadisonSimilarity.repeatedBlockMatrix line 252
Source documentation
The usual unital inclusion M_α → M_(α×β), sending a matrix to repeated diagonal blocks (equivalently, tensoring by the identity matrix).
```
def repeatedBlockMatrix (v : Matrix α α ℂ) : Matrix (α × β) (α × β) ℂ :=
…
```
theorem OAI.KadisonSimilarity.repeatedBlockMatrix_contraction_summand line 256
theorem OAI.KadisonSimilarity.permutationContraction_repeatedBlockMatrix line 274
Source documentation
Under block repetition, an unnormalized contraction gains one factor of the number of blocks for each cycle.
```
theorem permutationContraction_repeatedBlockMatrix (π : Equiv.Perm ι)
    (v : ι → Matrix α α ℂ) :
    permutationContraction π (fun i => repeatedBlockMatrix (β := β) (v i)) =
…
```
Mentions: OAI.KadisonSimilarity.permutationContraction, OAI.KadisonSimilarity.repeatedBlockMatrix
theorem OAI.KadisonSimilarity.normalizedPermutationContraction_repeatedBlockMatrix line 298
Source documentation
Normalized cycle contractions are compatible with full matrix stage inclusions. The cycle-count factors cancel exactly.
```
theorem normalizedPermutationContraction_repeatedBlockMatrix [Nonempty β]
    (π : Equiv.Perm ι) (v : ι → Matrix α α ℂ) :
    normalizedPermutationContraction π (fun i => repeatedBlockMatrix (β := β) (v i)) =
…
```
Mentions: OAI.KadisonSimilarity.normalizedPermutationContraction, OAI.KadisonSimilarity.repeatedBlockMatrix

theorem OAI.KadisonSimilarity.invariant_coefficients_stable_under_blocks line 313

Source documentation

Compatibility of the forms between two matrix stages forces their coefficients to agree. No stability assumption on coefficients is needed.

theorem invariant_coefficients_stable_under_blocks [Nonempty α] [Nonempty β]
    (j : ι → α) (hj : Function.Injective j)
    (F : (ι → Matrix α α ℂ) → ℂ)
    (G : (ι → Matrix (α × β) (α × β) ℂ) → ℂ)
    (c d : Equiv.Perm ι → ℂ)
    (hc : ∀ v, F v = ∑ π, c π * normalizedPermutationContraction π v)
    (hd : ∀ v, G v = ∑ π, d π * normalizedPermutationContraction π v)
    (hFG : ∀ v, G (fun i => repeatedBlockMatrix (v i)) = F v) : c = d := by
…

Mentions: OAI.KadisonSimilarity.normalizedPermutationContraction, OAI.KadisonSimilarity.repeatedBlockMatrix