[Merged by Bors] - feat(CStarAlgebra): `Ring.inverse` is convex and antitone on strictly positive operators by dupuisf · Pull Request #37009 · leanprover-community/mathlib4

dupuisf · 2026-03-23T00:52:11Z

This PR shows that the inverse is operator convex and operator antitone (we had the latter for inverse of elements in Units, but not for Ring.inverse).

github-actions · 2026-03-23T00:53:26Z

PR summary db1186dd23

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt` (new file)	2308
`Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder` (new file)	2691

Declarations diff

+ Ring.inverse_mul
+ _root_.IsStrictlyPositive.isUnit_cfcSqrt
+ _root_.IsStrictlyPositive.ringInverse
+ _root_.IsUnit.isStrictlyPositive_iff_conjugate_of_isSelfAdjoint
+ _root_.isSelfAdjoint_ringInverse_iff
+ _root_.isStrictlyPositive_ringInverse_iff
+ antitoneOn_ringInverse
+ cfc_rpow
+ commute_of_mul_eq_isSelfAdjoint
+ conjSqrt
+ conjSqrt_apply
+ conjSqrt_conjSqrt_ringInverse
+ conjSqrt_le_conjSqrt
+ conjSqrt_monotone
+ conjSqrt_of_not_nonneg
+ conjSqrt_one
+ conjSqrt_ringInverse_conjSqrt
+ conjSqrt_ringInverse_self
+ conjugate_of_isUnit_of_isSelfAdjoint
+ convexOn_ringInverse
+ inverse_inverse
+ isStrictlyPositive_conjSqrt_iff
+ isUnit_sqrt_iff_isStrictlyPositive
+ mul_left_iff
+ mul_right_iff
+ of_subsingleton
+ ringInverse
+ ringInverse_conjSqrt
+ ringInverse_le_ringInverse
+ ringInverse_nonneg_iff_nonneg_of_isUnit
+ sqrt_of_not_nonneg
+ sqrt_ringInverse
+ toLinearMap_conjSqrt
- Ring.inverse_inverse
- _root_.IsUnit.cfcSqrt

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
6897	1	backward.isDefEq.respectTransparency

Current commit 50e125b400
Reference commit db1186dd23

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

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

themathqueen · 2026-03-23T10:50:38Z

I suspect a lot of these proofs can be golfed a lot. I can give it a shot sometime this week, unless you want to?

dupuisf · 2026-03-23T13:03:45Z

I suspect a lot of these proofs can be golfed a lot. I can give it a shot sometime this week, unless you want to?

Feel free to give it a shot!

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

Co-authored-by: Monica Omar <[email protected]>

j-loreaux

I'll have more to say for the later files, but this is a start. Also, I just sent your ⁻¹ʳ notation PR to bors recently, so you should merge master and use that notation once it's available.

Mathlib/Algebra/Group/Units/Defs.lean

Mathlib/Algebra/GroupWithZero/Units/Basic.lean

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

themathqueen

I'll do the other two files over the weekend.

Mathlib/Algebra/Algebra/StrictPositivity.lean

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

themathqueen

I got bored so here are the rest of my comments

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

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

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

themathqueen

final comments from me

Mathlib/Algebra/Algebra/StrictPositivity.lean

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

Mathlib/Algebra/Algebra/StrictPositivity.lean

themathqueen

Think you need to merge master again? But looks good

j-loreaux

It makes me so happy that all of this now Just Works. 😃

bors d+

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

mathlib-bors · 2026-04-01T04:00:02Z

✌️ dupuisf can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

dupuisf · 2026-04-01T15:52:24Z

bors r+

… positive operators (#37009) This PR shows that the inverse is operator convex and operator antitone (we had the latter for inverse of elements in `Units`, but not for `Ring.inverse`).

mathlib-bors · 2026-04-01T17:00:49Z

Pull request successfully merged into master.

Build succeeded:

… positive operators (leanprover-community#37009) This PR shows that the inverse is operator convex and operator antitone (we had the latter for inverse of elements in `Units`, but not for `Ring.inverse`).

preliminary lemmas, up to conjSqrt

3fb87ff

dupuisf added WIP Work in progress t-analysis Analysis (normed *, calculus) labels Mar 23, 2026

dupuisf added 4 commits March 22, 2026 22:18

add conjSqrt file

39726d3

conjSqrt: cleanup

b47ec80

add RingInverseOrder.lean

77e39c9

add informal proof sketches

d5b76d8

dupuisf removed the WIP Work in progress label Mar 23, 2026

dupuisf requested a review from j-loreaux March 23, 2026 04:24

themathqueen reviewed Mar 23, 2026

View reviewed changes

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/ConjSqrt.lean Outdated Show resolved Hide resolved

themathqueen reviewed Mar 23, 2026

View reviewed changes

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/ConjSqrt.lean Outdated Show resolved Hide resolved

themathqueen reviewed Mar 23, 2026

View reviewed changes

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/ConjSqrt.lean Outdated Show resolved Hide resolved

j-loreaux reviewed Mar 23, 2026

View reviewed changes

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/RingInverseOrder.lean Outdated Show resolved Hide resolved

dupuisf and others added 4 commits March 23, 2026 10:10

Apply suggestions from code review

5fba799

Co-authored-by: Monica Omar <[email protected]>

remove "public" keyword in public section

03dbab9

base antitoneOn_ringInverse on the corresponding lemma for Units

216a09f

namespace: CFC → CStarAlgebra for the convexity result

f7e8340

j-loreaux reviewed Mar 23, 2026

View reviewed changes

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 23, 2026

implement suggestions

7d870d7

github-actions bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 25, 2026

Merge branch 'master' into convexOn_ringInverse

cd11396

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 25, 2026

dupuisf added 3 commits March 24, 2026 22:40

use notation in new code

eeb3ce8

open Ring

e86be45

fix build

08314dd

dupuisf removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 25, 2026

themathqueen reviewed Mar 27, 2026

View reviewed changes

dupuisf added 7 commits March 27, 2026 21:35

fix build

b0afe45

first batch of suggestions

19eef17

suggestions, batch 2

a2e28d4

last batch

b9da5b9

oops, one more

09189a4

a few more grind tags

2ca8c65

fix build

753d44e

themathqueen reviewed Mar 29, 2026

View reviewed changes

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/ConjSqrt.lean Outdated Show resolved Hide resolved

use LinearMap.mulLeftRight

1910597

themathqueen reviewed Mar 29, 2026

View reviewed changes

more suggestions

543714e

themathqueen reviewed Mar 30, 2026

View reviewed changes

Mathlib/Algebra/Algebra/StrictPositivity.lean Show resolved Hide resolved

themathqueen reviewed Mar 30, 2026

View reviewed changes

Mathlib/Algebra/Algebra/StrictPositivity.lean Outdated Show resolved Hide resolved

add isUnit to lemma name

66e90e5

themathqueen approved these changes Mar 31, 2026

View reviewed changes

Merge branch 'master' into convexOn_ringInverse

ed051f4

j-loreaux reviewed Apr 1, 2026

View reviewed changes

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/ConjSqrt.lean Outdated Show resolved Hide resolved

mathlib-triage bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Apr 1, 2026

themathqueen mentioned this pull request Apr 1, 2026

chore: call dsimp in the default tactic of ContinuousLinearMap #37386

Open

move lemmas above variables

50e125b

mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Apr 1, 2026

mathlib-bors bot changed the title ~~feat(CStarAlgebra): Ring.inverse is convex and antitone on strictly positive operators~~ [Merged by Bors] - feat(CStarAlgebra): Ring.inverse is convex and antitone on strictly positive operators Apr 1, 2026

mathlib-bors bot closed this Apr 1, 2026

Conversation

dupuisf commented Mar 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Mar 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary db1186dd23

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

themathqueen commented Mar 23, 2026

Uh oh!

dupuisf commented Mar 23, 2026

Uh oh!

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

themathqueen left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

themathqueen left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

themathqueen left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

themathqueen left a comment

Choose a reason for hiding this comment

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mathlib-bors bot commented Apr 1, 2026

Uh oh!

dupuisf commented Apr 1, 2026

Uh oh!

mathlib-bors bot commented Apr 1, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

dupuisf commented Mar 23, 2026 •

edited

Loading

github-actions bot commented Mar 23, 2026 •

edited

Loading