OAI/Analysis/KadisonSimilarity/Derivation/QuadraticSandwich.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The separation step in Haagerup's cyclic-similarity argument. Equal finite square sums with comparable orbit norms give a positive functional between the corresponding quadratic forms.

  1. def OAI.KadisonSimilarity.listSquareSum line 18
  2. def OAI.KadisonSimilarity.listOrbitSum line 21
  3. theorem OAI.KadisonSimilarity.listSquareSum_nil line 24
  4. theorem OAI.KadisonSimilarity.listSquareSum_singleton_coe line 25
  5. theorem OAI.KadisonSimilarity.listOrbitSum_nil line 28
  6. theorem OAI.KadisonSimilarity.listSquareSum_append line 31
  7. theorem OAI.KadisonSimilarity.listOrbitSum_append line 36
  8. theorem OAI.KadisonSimilarity.listSquareSum_scale line 40
  9. theorem OAI.KadisonSimilarity.listOrbitSum_scale line 53
  10. def OAI.KadisonSimilarity.orbitSandwichCone line 65
  11. theorem OAI.KadisonSimilarity.exists_positive_orbit_sandwich line 86

    Source documentation

    The only hypothesis is the finite quadratic comparison.

    theorem exists_positive_orbit_sandwich (π : BoundedUnitalHom A H) (ξ : H) (K : ℝ)
    (hcompare : ∀ a b : List A, listSquareSum a = listSquareSum b →
      listOrbitSum π ξ a ≤ K * listOrbitSum π ξ b) :
    ∃ ω : A →ₚ[ℂ] ℂ, ∀ a : A,
      ‖π.1 a ξ‖ ^ 2 ≤ (ω (star a * a)).re ∧
        (ω (star a * a)).re ≤ K * ‖π.1 a ξ‖ ^ 2 := by
…

    Mentions: OAI.KadisonSimilarity.BoundedUnitalHom, OAI.KadisonSimilarity.listSquareSum, OAI.KadisonSimilarity.listOrbitSum