SpatialCoefficientEstimate.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The elementary coefficient estimate used to pass from almost central Hilbert--Schmidt vectors to spatial tensor functionals. No multiplicativity of a completely positive map is inferred from centrality.

lemma OAI.WeakPureInfiniteness.norm_inner_left_difference_le line 17
lemma OAI.WeakPureInfiniteness.norm_inner_unit_left_difference_le line 23

lemma OAI.WeakPureInfiniteness.norm_product_coefficient_error_le line 30

Source documentation

The product coefficient error separates into the actual vector intertwining error and the single-operator state error.

lemma norm_product_coefficient_error_le (z : H) (hz : ‖z‖ = 1)
    (L R S : H →L[ℂ] H) (α : ℂ) :
    ‖inner ℂ z ((L * R) z) - α‖ ≤
      ‖L‖ * ‖R z - S z‖ + ‖inner ℂ z ((L * S) z) - α‖ := by
…

lemma OAI.WeakPureInfiniteness.norm_sum_product_coefficient_error_le line 41
lemma OAI.WeakPureInfiniteness.realPart_operator_coefficient line 54
lemma OAI.WeakPureInfiniteness.imaginaryPart_operator_coefficient line 64

lemma OAI.WeakPureInfiniteness.complex_coefficient_error_le line 82

Source documentation

Real and imaginary self-adjoint tests control the complex state value.

lemma complex_coefficient_error_le (f : A →ₗ[ℂ] ℂ)
    (hf : ∀ a, f (star a) = star (f a))
    (π : A →ₗ[ℂ] (H →L[ℂ] H)) (hπ : ∀ a, π (star a) = star (π a))
    (a : A) (z : H) :
    ‖f a - inner ℂ z (π a z)‖ ≤
      |(f (ℜ a)).re - (inner ℂ z (π (ℜ a) z)).re| +
      |(f (ℑ a)).re - (inner ℂ z (π (ℑ a) z)).re| := by
…