OAI/Analysis/FactorGeneration/HaarIndependence.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Two-norm continuity of ordered moments along uniformly operator-bounded representatives. No topological-ring structure on the two-norm quotient is used.

  1. theorem OAI.Generator.Tracial.quotient_bounded_mul_norm line 18
  2. theorem OAI.Generator.Tracial.quotient_mul_bounded_norm line 29
  3. theorem OAI.Generator.Tracial.quotient_fixed_right_tendsto line 43
  4. theorem OAI.Generator.Tracial.quotient_bounded_mul_tendsto line 54
  5. theorem OAI.Generator.Tracial.quotient_fixed_left_tendsto line 72
  6. theorem OAI.Generator.Tracial.quotient_star_tendsto line 78
  7. theorem OAI.Generator.Tracial.quotient_partial_signed_tendsto line 83
  8. theorem OAI.Generator.Tracial.quotient_partial_core_tendsto line 91
  9. theorem OAI.Generator.Tracial.quotient_trace_tendsto line 119
  10. theorem OAI.Generator.Tracial.exactOrderedMoments_partial_limit line 127
  11. theorem OAI.Generator.Tracial.exactOrderedMoments_zero line 154
  12. theorem OAI.Generator.Tracial.exists_full_support_ordered_independence line 174
  13. theorem OAI.Generator.Tracial.exists_included_ordered_unitary line 202

    Source documentation

    Membership is witnessed by the actual inclusion homomorphism of quotients.

    theorem exists_included_ordered_unitary
    (ω : Ultrafilter ℕ) (hω : (ω : Filter ℕ) ≤ atTop)
    (x : ℕ → Q τ ω) (hx : ∀ i,quotientTrace τ ω (x i)=0) :
    ∃ t : Q τ ω,
      (∃ q : TracialQuotient (restrictedTrace τ hNM) (ω : Filter ℕ),
        quotientInclusion τ hNM (ω : Filter ℕ) q=t) ∧
      star t*t=1 ∧ t*star t=1 ∧ ExactOrderedMoments τ ω t x := by
…

    Mentions: OAI.Generator.Tracial.Q, OAI.Generator.Tracial.restrictedTrace, OAI.Generator.Tracial.quotientInclusion, OAI.Generator.Tracial.ExactOrderedMoments

  14. theorem OAI.Generator.Tracial.exists_included_reduced_unitary line 236