InvariantCoefficients.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The coefficient-vanishing steps in the invariant-tensor argument

These are the two limiting arguments in lem:invariant-intertwiners. They do not assume the classification of intertwiners: the finite-stage coefficient identities and their norm bounds still have to be constructed.

theorem OAI.KadisonSimilarity.coefficient_zero_of_power_bound line 21

theorem OAI.KadisonSimilarity.cycle_coefficient_zero line 40

Source documentation

The endpoint L¹ bound removes a stable cycle coefficient whose number of cycles is below 1 + (k+l)/2. Matrix sizes may run through any cofinal sequence, as they do for the increasing matrix subalgebras in the paper.

theorem cycle_coefficient_zero (m : ℕ → ℝ)
    (hm : ∀ j, 0 < m j) (hmTop : Tendsto m atTop atTop)
    (k l cycles : ℕ) (a : ℂ) (C : ℝ)
    (hfew : (cycles : ℝ) < 1 + ((k : ℝ) + l) / 2)
    (hbound : ∀ j, ‖a‖ * (m j) ^ (-(cycles : ℝ)) ≤
      C * (m j) ^ (-1 - ((k : ℝ) + l) / 2)) : a = 0 := by
…

theorem OAI.KadisonSimilarity.same_side_pairing_coefficient_zero line 54

Source documentation

Summing orthonormal labels removes a pairing with a source-source or test-test pair: its coefficient grows faster than the product of vector norms.

theorem same_side_pairing_coefficient_zero (a : ℂ) (C : ℝ) (rSource rTest : ℕ)
    (hpair : 0 < rSource + rTest)
    (hbound : ∀ M : ℕ, 0 < M →
      ‖a‖ * (M : ℝ) ^ ((rSource + rTest : ℕ) : ℝ) ≤
        C * (M : ℝ) ^ (((rSource + rTest : ℕ) : ℝ) / 2)) : a = 0 := by
…