TomiyamaPositive.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Positivity of unital contractions

This is the first step of the norm-one projection argument. Positivity and adjoint preservation are derived from the norm bound and the unit.

theorem OAI.KadisonKastler.cstar_norm_one_le line 23
theorem OAI.KadisonKastler.norm_imaginary_perturbation_sq line 29

theorem OAI.KadisonKastler.unital_contraction_isSelfAdjoint line 51

Source documentation

A unital complex-linear contraction preserves self-adjointness.

theorem unital_contraction_isSelfAdjoint (P : A →L[ℂ] B)
    (hP : ∀ x, ‖P x‖ ≤ ‖x‖) (h1 : P 1 = 1)
    (x : A) (hx : IsSelfAdjoint x) : IsSelfAdjoint (P x) := by
…

theorem OAI.KadisonKastler.unital_contraction_nonneg line 65

Source documentation

A unital complex-linear contraction is positive.

theorem unital_contraction_nonneg (P : A →L[ℂ] B)
    (hP : ∀ x, ‖P x‖ ≤ ‖x‖) (h1 : P 1 = 1)
    (x : A) (hx : 0 ≤ x) : 0 ≤ P x := by
…

theorem OAI.KadisonKastler.unital_contraction_map_star line 97

Source documentation

Adjoint preservation follows from the same norm-one hypotheses.

theorem unital_contraction_map_star (P : A →L[ℂ] B)
    (hP : ∀ x, ‖P x‖ ≤ ‖x‖) (h1 : P 1 = 1) (x : A) :
    P (star x) = star (P x) := by
…