OAI/Analysis/KadisonSimilarity/Tracial/SourceWeakPowers.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Weak powers in a prescribed diffuse source, tested against ambient coefficients. Conditional expectation moves only the coefficients.

  1. def OAI.KadisonSimilarity.sourceExpectation line 23
  2. theorem OAI.KadisonSimilarity.sourceExpectation_pairing line 26
  3. theorem OAI.KadisonSimilarity.exists_source_partial_unitary_weak_powers line 44

    Source documentation

    Every nonzero source corner contains a partial unitary whose prescribed nonzero powers are weakly small against any finite family from the ambient algebra.

    theorem exists_source_partial_unitary_weak_powers
    (hfactor : ∀ c : N.toStarSubalgebra, (∀ a, a * c = c * a) → ∃ z : ℂ, c = z • 1)
    (hdiff : ∀ p : N.toStarSubalgebra, IsStarProjection p → p ≠ 0 →
      ∃ q, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p * q = q ∧ q * p = q)
    (p : N.toStarSubalgebra) (hp : IsStarProjection p) (hp0 : p ≠ 0)
    {I : Type*} [Fintype I] (a : I → M.toStarSubalgebra) (k : I → Bool × ℕ)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ w : PartialUnitary N.toStarSubalgebra, w.support = p ∧
      ∀ i, ‖υ.trace (a i * coordinateInclusion hNM (w.power (k i)))‖ <
        ε * (υ.trace (coordinateInclusion hNM p)).re := by
…