OAI/Analysis/KadisonKastler/CornerStateConjugation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A single state comparison from two corner conjugations

Normalized corner estimates combine under the unitary formed from two complementary corner unitaries. The resulting state comparison is bounded by the sum of the corner errors.

  1. def OAI.KadisonKastler.sandwichFunctional line 21
  2. theorem OAI.KadisonKastler.sandwichFunctional_apply line 25
  3. theorem OAI.KadisonKastler.sandwichFunctional_centralizes line 28
  4. theorem OAI.KadisonKastler.sandwichFunctional_vectorFunctional line 47
  5. theorem OAI.KadisonKastler.cornerFunctional_patched_vector line 54
  6. theorem OAI.KadisonKastler.patched_vector_state_centralizes line 72
  7. theorem OAI.KadisonKastler.patched_vector_state_norm_le line 84

    Source documentation

    Once each corner has a normalized comparison, their sum is the required unitary comparison on the whole algebra.

    theorem patched_vector_state_norm_le (p : AlgebraProjection M)
    (u v : Algebra M) (hu : star u*u=p.val) (hu' : u*star u=p.val)
    (hv : star v*v=1-p.val) (hv' : v*star v=1-p.val) (ξ ζ : H)
    (hξ : Function.Injective (algebraVectorMap M ξ)) (hnξ : ‖ξ‖=1)
    (hζ : Function.Injective (algebraVectorMap M ζ)) (hnζ : ‖ζ‖=1)
    (hp0 : p.val≠0) (hp1 : p.val≠1)
    (hcξ : ∀ x : Algebra M, vectorFunctional ξ (p.val*x)=vectorFunctional ξ (x*p.val))
    (hcζ : ∀ x : Algebra M, vectorFunctional ζ (p.val*x)=vectorFunctional ζ (x*p.val))
    (δ : ℝ)
    (h₀ : ‖(projectionVectorWeight p ξ)⁻¹ • sandwichFunctional (vectorFunctional ξ) u -
      vectorCornerState p ζ‖ ≤ δ)
    (h₁ : ‖(1-projectionVectorWeight p ξ)⁻¹ • sandwichFunctional (vectorFunctional ξ) v -
…

    Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.projectionVectorWeight, OAI.KadisonKastler.sandwichFunctional, OAI.KadisonKastler.vectorCornerState