English
The function a ↦ a^p is monotone for p ∈ [0,1] in a C*-algebra with the square root operation.
Русский
Функция a ↦ a^p монотонна для p ∈ [0,1] в C*-алгебре при оператора sqrt.
LaTeX
$$$\\text{Monotone}\\bigl(\\lambda a:\\, A, a^{p}\\bigr)\\;\\text{for } p\\in Icc[0,1]$$$
Lean4
/-- `rpowIntegrand₀₁ p t` is operator monotone for all `p ∈ Ioo 0 1` and all `t ∈ Ioi 0`. -/
theorem monotoneOn_cfcₙ_rpowIntegrand₀₁ {p : ℝ} {t : ℝ} (hp : p ∈ Ioo 0 1) (ht : 0 < t) :
MonotoneOn (cfcₙ (rpowIntegrand₀₁ p t)) (Ici (0 : A)) :=
by
intro a (ha : 0 ≤ a) b (hb : 0 ≤ b) hab
calc
_ = t ^ ((p : ℝ) - 1) • cfcₙ (rpowIntegrand₀₁ p 1) (t⁻¹ • a) := by
rw [cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one hp ht a ha]
_ ≤ t ^ ((p : ℝ) - 1) • cfcₙ (rpowIntegrand₀₁ p 1) (t⁻¹ • b) :=
by
gcongr
unfold rpowIntegrand₀₁
simp only [Real.one_rpow, one_mul, inv_one]
refine CFC.monotoneOn_one_sub_one_add_inv_real (?_ : 0 ≤ t⁻¹ • a) (?_ : 0 ≤ t⁻¹ • b) (by gcongr)
all_goals positivity
_ = cfcₙ (rpowIntegrand₀₁ p t) b := by rw [cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one hp ht b hb]
