Commit 2025-08-21 02:05 dd0685bd

View on Github →

feat(CStarAlgebra): a => a ^ p is operator monotone for p ∈ Icc 0 1 (#27715) This PR shows that a => a ^ p is operator monotone for p ∈ Icc 0 1, i.e. that CFC.nnrpow, CFC.rpow and CFC.sqrt are monotone, using the integral representation for the power function.

Estimated changes

Modified Mathlib/Algebra/Algebra/Spectrum/Quasispectrum.lean

added theorem NonnegSpectrumClass.nonneg_of_mem_quasispectrum

Modified Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean

added theorem CFC.monotoneOn_one_sub_one_add_inv_real

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

added theorem quasispectrum.isCompact_nnreal

added theorem spectrum.isCompact_nnreal

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

added theorem CFC.nnrpow_eq_cfcₙ_real

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

added theorem CFC.cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one

added theorem CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁

added theorem CFC.monotoneOn_cfcₙ_rpowIntegrand₀₁

added theorem CFC.monotone_nnrpow

added theorem CFC.monotone_rpow

added theorem CFC.monotone_sqrt

added theorem CFC.nnrpow_le_nnrpow

added theorem CFC.rpow_le_rpow

added theorem CFC.sqrt_le_sqrt

added theorem Real.continuousOn_rpowIntegrand₀₁_Ici

added theorem Real.continuousOn_rpowIntegrand₀₁_uncurry

added theorem Real.rpowIntegrand₀₁_eqOn_mul_rpowIntegrand₀₁_one

added theorem Real.rpowIntegrand₀₁_monotoneOn

Modified Mathlib/Topology/ContinuousOn.lean

added theorem ContinuousOn.uncurry_left

added theorem ContinuousOn.uncurry_right

Modified Mathlib/Topology/MetricSpace/Bounded.lean

Modified Mathlib/Topology/Separation/Hausdorff.lean