StableMatrixStages.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Stable coefficients on growing matrix stages

Finite Schur--Weyl spanning, compatibility of normalized contractions, and the actual matrix-unit endpoint estimate produce one stable coefficient family. The small-cycle coefficients are proved zero; neither stability nor those zeros are added as assumptions.

theorem OAI.KadisonSimilarity.exists_stable_matrix_expansion line 25

Source documentation

Coefficients chosen by finite Schur--Weyl spanning agree at every stage once their normalized contractions restrict to the common initial stage.

theorem exists_stable_matrix_expansion
    (spanning : ∀ s, SchurWeylMultilinearSpanning ι (A s))
    (F : ∀ s, MultilinearMap ℂ (fun _ : ι => Matrix (A s) (A s) ℂ) ℂ)
    (hF : ∀ s, UnitaryConjugationInvariant (F s))
    (embed : ∀ s, Matrix (A 0) (A 0) ℂ → Matrix (A s) (A s) ℂ)
    (hform : ∀ s v, F s (fun i => embed s (v i)) = F 0 v)
    (hcontraction : ∀ s (π : Equiv.Perm ι) (v : ι → Matrix (A 0) (A 0) ℂ),
      normalizedPermutationContraction π (fun i => embed s (v i)) =
        normalizedPermutationContraction π v)
    (labels : ι → A 0) (hlabels : Function.Injective labels) :
    ∃ c : Equiv.Perm ι → ℂ, ∀ s v,
      F s v = ∑ π, c π * normalizedPermutationContraction π v := by
…

Mentions: OAI.KadisonSimilarity.SchurWeylMultilinearSpanning, OAI.KadisonSimilarity.UnitaryConjugationInvariant, OAI.KadisonSimilarity.normalizedPermutationContraction

theorem OAI.KadisonSimilarity.stable_matrix_coefficient_zero line 54

Source documentation

The endpoint test eliminates every stable coefficient below the cycle threshold. The input bound is on the original stage form at explicit matrix units, not on already-isolated coefficients.

theorem stable_matrix_coefficient_zero
    (F : ∀ s, MultilinearMap ℂ (fun _ : ι => Matrix (A s) (A s) ℂ) ℂ)
    (c : Equiv.Perm ι → ℂ)
    (hexp : ∀ s v, F s v = ∑ π, c π * normalizedPermutationContraction π v)
    (labels : ∀ s, ι → A s) (hlabels : ∀ s, Function.Injective (labels s))
    (hsize : Tendsto (fun s => (Fintype.card (A s) : ℝ)) atTop atTop)
    (tailDegree : ℕ) (C : ℝ)
    (hbound : ∀ s π, ‖F s (permutationTest (labels s) π)‖ ≤
      C * (Fintype.card (A s) : ℝ) ^ (-1 - (tailDegree : ℝ) / 2))
    (π : Equiv.Perm ι)
    (hfew : (permutationCycleCount π : ℝ) < 1 + (tailDegree : ℝ) / 2) : c π = 0 := by
…

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

theorem OAI.KadisonSimilarity.exists_stable_tail_pairing_expansion line 78

Source documentation

Assemble finite Schur--Weyl spanning, coefficient stability, endpoint matrix-unit estimates, and the proved pair-trace factorization.

theorem exists_stable_tail_pairing_expansion
    (rank : T → ℕ) (hrank : Function.Injective rank)
    (spanning : ∀ s, SchurWeylMultilinearSpanning (Option T) (A s))
    (F : ∀ s, MultilinearMap ℂ (fun _ : Option T => Matrix (A s) (A s) ℂ) ℂ)
    (hF : ∀ s, UnitaryConjugationInvariant (F s))
    (embed : ∀ s, Matrix (A 0) (A 0) ℂ → Matrix (A s) (A s) ℂ)
    (hform : ∀ s v, F s (fun i => embed s (v i)) = F 0 v)
    (hcontraction : ∀ s (π : Equiv.Perm (Option T))
      (v : Option T → Matrix (A 0) (A 0) ℂ),
      normalizedPermutationContraction π (fun i => embed s (v i)) =
        normalizedPermutationContraction π v)
    (labels : ∀ s, Option T → A s) (hlabels : ∀ s, Function.Injective (labels s))
…

Mentions: OAI.KadisonSimilarity.SchurWeylMultilinearSpanning, OAI.KadisonSimilarity.UnitaryConjugationInvariant, OAI.KadisonSimilarity.normalizedPermutationContraction