monotone_nnrpow — Mathlib

English

For p ∈ [0,1], the map a ↦ a^p is monotone on a C*-algebra with the NNReal exponents.

Русский

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

LaTeX

$$$\\text{Monotone}(a \\mapsto a^{p})$ для $p\\in Icc(0,1)$$$

Lean4

/-- `a ↦ a ^ p` is operator monotone for `p ∈ [0,1]`. -/
theorem monotone_nnrpow {p : ℝ≥0} (hp : p ∈ Icc 0 1) : Monotone (fun a : A => a ^ p) :=
  by
  intro a b hab
  by_cases ha : 0 ≤ a
  · have hb : 0 ≤ b := ha.trans hab
    have hIcc : Icc (0 : ℝ≥0) 1 = Ioo 0 1 ∪ {0} ∪ { 1 } := by ext; simp
    rw [hIcc] at hp
    obtain (hp | hp) | hp := hp
    · exact monotoneOn_nnrpow_Ioo hp ha hb hab
    · simp_all [mem_singleton_iff]
    · simp_all [mem_singleton_iff, nnrpow_one a, nnrpow_one b]
  · have : a ^ p = 0 := cfcₙ_apply_of_not_predicate a ha
    simp [this]

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