English
The posPart behaves well with scalar multiplication: (r a)⁺ = r a⁺ for nonnegative reals r ≥ 0 (in the appropriate scalar context).
Русский
Положительная часть сохраняет скаляры: (r a)⁺ = r a⁺ при r ≥ 0.
LaTeX
$$$ (r \cdot a)^+ = r \cdot a^+ $$$
Lean4
@[simp]
theorem posPart_smul {r : ℝ≥0} {a : A} : (r • a)⁺ = r • a⁺ :=
by
by_cases ha : IsSelfAdjoint a
· simp only [CFC.posPart_def, NNReal.smul_def]
rw [← cfcₙ_comp_smul .., ← cfcₙ_smul ..]
refine cfcₙ_congr fun x hx ↦ ?_
simp [_root_.posPart_def, mul_max_of_nonneg]
· obtain (rfl | hr) := eq_or_ne r 0
· simp
· have := (not_iff_not.mpr <| (IsSelfAdjoint.all r).smul_iff hr.isUnit (x := a)) |>.mpr ha
simp [CFC.posPart_def, cfcₙ_apply_of_not_predicate a ha, cfcₙ_apply_of_not_predicate _ this]