Theorem CFC.monotone_sqrt

Modification history

2025-12-03 03:21

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

chore: split operator monotonicity results to privately import integration results (#32329) …

Modified CFC.monotone_sqrt View on Github →

2025-08-21 02:05

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

feat(CStarAlgebra): `a => a ^ p` is operator monotone for `p ∈ Icc 0 1` (#27715) …

Added CFC.monotone_sqrt View on Github →