FiniteStandardEstimate.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Finite standard multiplicities from the centered free-corner test

This is a reduction theorem. Its centered-symmetry premise is an explicit local conclusion to be supplied by the free-corner argument, and is not a published-input predicate. Haar averaging, multiplicity padding, matrix GNS transport, symmetry dilation, and restoring the original operator are all performed by proved lemmas.

theorem OAI.KadisonSimilarity.finite_standard_estimate_of_centered_tests line 29

Source documentation

The centered-symmetry bound c * (3δ) for operators commuting with the finite matrix tower gives the complete finite-standard bound (3c+2) * δ. The only unproved premise in this reduction is the displayed centered test itself; the initial perturbation is constructed by Haar averaging rather than assumed.

theorem finite_standard_estimate_of_centered_tests
    (τ : A →ₚ[ℂ] ℂ)
    (F : ∀ j, Matrix (I j) (I j) ℂ →⋆ₐ[ℂ] A)
    (transition : ∀ j k, j ≤ k →
      Matrix (I j) (I j) ℂ →⋆ₐ[ℂ] Matrix (I k) (I k) ℂ)
    (hcompat : ∀ j k h a, F k (transition j k h a) = F j a)
    {c : ℝ} (hc : 0 ≤ c)
    (hcentered : ∀ (m : ℕ) [NeZero m]
      (Y₀ : HilbertCopies τ.GNS (4 * m) →L[ℂ] HilbertCopies τ.GNS (4 * m))
      (δ : ℝ), 0 ≤ δ →
      (∀ a, ‖commutator Y₀ (amplify (τ.gnsStarAlgHom a) (4 * m))‖ ≤
        (3 * δ) * ‖a‖) →
…

Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify