Commit 2026-04-25 22:48 2113b177

View on Github →

feat(CStarAlgebra): x ↦ x ^ p is operator concave for p ∈ [0, 1] (#37643) This PR shows that x ↦ x ^ p is operator concave (i.e. CFC.nnrpow is concave) on positive elements of a C*-algebra for p ∈ [0, 1].

Estimated changes

Modified Mathlib/Algebra/Algebra/Unitization.lean

modified def Unitization.inrHom

added theorem Unitization.inrHom_injective

modified def Unitization.sndHom

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean

added theorem cfcₙ_neg'

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

added theorem CStarAlgebra.concaveOn_cfcₙ_of_concaveOn_cfc

added theorem CStarAlgebra.convexOn_cfcₙ_of_convexOn_cfc

added theorem CStarAlgebra.inr_map_Ici_zero

added theorem Unitization.concaveOn_of_concaveOn_inr_comp

added theorem Unitization.convexOn_of_convexOn_inr_comp

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

added theorem cfc_neg'

modified theorem cfc_ringInverse_id

Modified Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean

added theorem CFC.nnrpow_one_eqOn

added theorem CFC.rpow_zero_eqOn

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean

added theorem CFC.concaveOn_cfc_rpowIntegrand₀₁

added theorem CFC.concaveOn_cfcₙ_rpowIntegrand₀₁

added theorem Real.rpowIntegrand₀₁_eq_sub

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Order.lean

added theorem CFC.concaveOn_nnrpow

added theorem CFC.concaveOn_rpow

added theorem CFC.concaveOn_sqrt

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/RingInverseOrder.lean