monotone_rpow — Mathlib

English

The map a ↦ a^p is operator monotone for p ∈ [0,1] in a C*-algebra.

Русский

Отображение a ↦ a^p операторно монотонно для p ∈ [0,1] в C*-алгебре.

LaTeX

$$$\\forall a\\le b:\\; a^{p} \\le b^{p}$, $p\\in Icc(0,1)$$$

Lean4

/-- `a ↦ a ^ p` is operator monotone for `p ∈ [0,1]`. -/
theorem monotone_rpow {p : ℝ} (hp : p ∈ Icc 0 1) : Monotone (fun a : A => a ^ p) :=
  by
  let q : ℝ≥0 := ⟨p, hp.1⟩
  change Monotone (fun a : A => a ^ (q : ℝ))
  cases (zero_le q).lt_or_eq' with
  | inl hq =>
    simp_rw [← CFC.nnrpow_eq_rpow hq]
    exact monotone_nnrpow hp
  | inr hq =>
    simp only [hq, NNReal.coe_zero]
    intro a b hab
    by_cases ha : 0 ≤ a
    · have hb : 0 ≤ b := ha.trans hab
      simp [CFC.rpow_zero a, CFC.rpow_zero b]
    · have : a ^ (0 : ℝ) = 0 := cfc_apply_of_not_predicate a ha
      simp [this]

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