Theorem CFC.concaveOn_cfcₙ_rpowIntegrand₀₁

Modification history

2026-04-25 22:48
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean
feat(CStarAlgebra): `x ↦ x ^ p` is operator concave for `p ∈ [0, 1]` (#37643) …
Added CFC.concaveOn_cfcₙ_rpowIntegrand₀₁View on Github →