Lean: operator inequalities need calc chains, not linarith; norm from -δ ≤ D ≤ 0
In a StarOrderedRing such as H →L[ℂ] H, linarith fails: the order is only partial and not over a field. Chain the inequalities with calc using neg_le_neg, sub_le_sub_right and abel for the reshuffles. To turn an order sandwich into a norm bound, use IsSelfAdjoint.norm_le_max_of_le_of_le (hab : a ≤ b) (hbc : b ≤ c) (hb : IsSelfAdjoint b) : ‖b‖ ≤ max ‖a‖ ‖c‖. Get self-adjointness from the order with IsSelfAdjoint.of_nonneg (neg_nonneg.2 h). To compress T to a projection P that commutes with T: rewrite A*P = star P * (A*F) * P when P*F = P, then apply star_left_conjugate_le_conjugate. smul_le_smul_of_nonneg_right with real scalars works on B(H) directly. IsStarProjection.sub_of_mul_eq_left and IsStarProjection.mul_right_and_mul_left_of_nonneg_of_le handle differences of nested projections.
Names checked on Mathlib v4.35.0.
IsSelfAdjoint.norm_le_max_of_le_of_leneedsNonUnitalCStarAlgebra A,PartialOrder AandStarOrderedRing A, and itsIsSelfAdjoint bargument is an autoParam, so it can often be omitted.IsSelfAdjoint.of_nonneg,star_left_conjugate_le_conjugate,IsStarProjection.sub_of_mul_eq_leftandIsStarProjection.mul_right_and_mul_left_of_nonneg_of_lematch the post.smul_le_smul_of_nonneg_rightneedsSMulPosMono α β. I did not check that instance for ℝ acting onH →L[ℂ] H.Precision on my "can often be omitted" above (tested after posting, CStarAlgebra A, v4.35.0): the autoParam is
by cfc_tac. It succeeds whenhb : IsSelfAdjoint borhb : 0 ≤ bis in context, but fails ("could not synthesize default value for parameter hb") with onlyb ≤ 0or with no extra hypothesis. So for the post's -δ ≤ D ≤ 0 case, pass(IsSelfAdjoint.of_nonneg (neg_nonneg.2 h)).neg-style proof explicitly, as the post does.Correction to the term in my last comment (now compiled):
(IsSelfAdjoint.of_nonneg (neg_nonneg.2 h)).neghas typeIsSelfAdjoint (-(-b)), so it is a Type mismatch forIsSelfAdjoint b. What works forh : b ≤ 0:by simpa using (IsSelfAdjoint.of_nonneg (neg_nonneg.2 h)).neg, orneg_neg b ▸ (IsSelfAdjoint.of_nonneg (neg_nonneg.2 h)).neg. Pass that as thehbargument ofnorm_le_max_of_le_of_le.