OAI/Analysis/KadisonSimilarity/Tracial/SourceMomentConstruction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonSimilarity.source_momentBound_limit line 29

   Source documentation

   Ambient moment bounds persist under trace-norm limits in the source.

   theorem source_momentBound_limit {I : Type*} [Fintype I]
       (F : I → M.toStarSubalgebra) {K N : ℕ} {b : ℝ → ℝ}
       {v : ℕ → PartialUnitary R.toStarSubalgebra} {w : PartialUnitary R.toStarSubalgebra}
       (h : GNSTendsto (vectorPositiveFunctional R υ.vector)
         (fun n => (v n : R.toStarSubalgebra)) atTop (w : R.toStarSubalgebra))
       (hb : ContinuousAt b ((υ.trace (coordinateInclusion hRM w.support)).re))
       (hv : ∀ n, MomentBound F (vectorPositiveFunctional M υ.vector) (K := K) (N := N) b
   …

   Mentions: OAI.KadisonSimilarity.vectorPositiveFunctional

2. theorem OAI.KadisonSimilarity.exists_source_partial_unitary_moments line 54

   Source documentation

   Partial unitaries of every trace below one satisfy prescribed ambient moment bounds. The maximality argument is carried out in the source.

   theorem exists_source_partial_unitary_moments {I : Type*} [Fintype I]
       (F : I → M.toStarSubalgebra)
       (hF : ∀ i, ‖F i‖ ≤ 1) (hFτ : ∀ i, υ.trace (F i) = 0)
       {K N : ℕ} (hK : 0 < K) {δ T : ℝ} (hδ : 0 < δ) (hT0 : 0 ≤ T) (hT : T < 1) :
       ∃ v : PartialUnitary R.toStarSubalgebra,
         (υ.trace (coordinateInclusion hRM v.support)).re = T ∧
         MomentBound F (vectorPositiveFunctional M υ.vector) (K := K) (N := N)
   …

   Mentions: OAI.KadisonSimilarity.vectorPositiveFunctional