Commit 2024-09-04 22:22 5ba359da

View on Github →

feat: H →L[ℂ] H is a StarOrderedRing when H is a Hilbert space (#16462)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean

added theorem ContinuousLinearMap.antilipschitz_of_forall_le_inner_map

added theorem ContinuousLinearMap.isUnit_of_forall_le_norm_inner_map

Created Mathlib/Analysis/InnerProductSpace/StarOrder.lean

added theorem ContinuousLinearMap.IsPositive.spectrumRestricts

added theorem ContinuousLinearMap.instStarOrderedRingRCLike