Skip to content

feat(CStarAlgebra): x ↦ x ^ p is operator concave for p ∈ [0, 1]#37643

Open
dupuisf wants to merge 15 commits intoleanprover-community:masterfrom
dupuisf:concaveOn_cfc_rpow
Open

feat(CStarAlgebra): x ↦ x ^ p is operator concave for p ∈ [0, 1]#37643
dupuisf wants to merge 15 commits intoleanprover-community:masterfrom
dupuisf:concaveOn_cfc_rpow

Commits

Commits on Apr 4, 2026

Commits on Apr 5, 2026

Commits on Apr 15, 2026