OAI/Analysis/KadisonKastler/ConcreteRecoveryWeakLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.TraceQuotientMap.exists_recovery_weak_scalar line 25

   Source documentation

   Combining the constructed expectation and spectral recovery gives both pieces needed by the randomized-row argument. The recovered scalar has real part at least one half and is the weak limit of the coordinate recovery average.

   theorem TraceQuotientMap.exists_recovery_weak_scalar
       (D : TraceQuotientMap τ σ ω)
       (hτ : FiniteVectorTrace τ) (hσ : FiniteVectorTrace σ)
       {ι : Type*} [Fintype ι] [Nonempty ι]
       (p : ι → Algebra M) (v : ι → unitary (BoundedSequence (Algebra M)))
       (u : ι → unitary (Algebra P))
       (hu : ∀ i, D.quotient (v i : BoundedSequence (Algebra M)) = (u i : Algebra P))
       (hp : ∀ i, IsStarProjection (p i))
       (hfree : ∀ i, FreeHaarMoments σ D.constant.range (u i))
       {n N : ℕ} (hn : 2 ≤ n)
       (hptrace : ∀ i, τ.toLinearMap (p i) = (((n : ℝ)⁻¹ : ℝ) : ℂ))
       (hpavg : finiteAverage p = (((n : ℝ)⁻¹ : ℝ) : ℂ) • (1 : Algebra M))
   …

   Mentions: OAI.KadisonKastler.TraceQuotientMap, OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.finiteAverage