cfc_nnreal — Mathlib

English

Over NNReal base, if a and b commute, then cfc f a commutes with b for any NNReal-valued function f, avoiding star interactions.

Русский

Для NNReal-базы: если a и b коммутируют, тогда cfc f a коммутизирует с b для любой NNReal-функции f без взаимодействия со star.

LaTeX

$$$\forall a,b\in A\, (hb:\ Commute a b) (f: \mathbb{R}_{\ge 0} \to \mathbb{R}_{\ge 0}),\ Commute( cfc\! f\ a, b).$$

Lean4

/-- A version of `Commute.cfc` or `IsSelfAdjoint.commute_cfc` which does not require any interaction
with `star` when the base ring is `ℝ≥0`. -/
@[grind ←]
protected theorem cfc_nnreal {a b : A} (hb : Commute a b) (f : ℝ≥0 → ℝ≥0) : Commute (cfc f a) b :=
  by
  by_cases ha : 0 ≤ a
  · rw [cfc_nnreal_eq_real ..]
    exact hb.cfc_real _
  · simp [cfc_apply_of_not_predicate a ha]

Похожие утверждения