feat(Data/IsROrC/Basic): add a `StarOrderedRing` instance by MohanadAhmed · Pull Request #6210 · leanprover-community/mathlib4

MohanadAhmed · 2023-07-28T11:10:59Z

This PR implements a suggestion by @urkud on Zulip thread on how to get a StarOrderedRing on the IsROrC class. In that discussion the suggested step were:

Add PartialOrder K to the list of extends and add le_iff_re_im : z ≤ w ↔ re z ≤ re w ∧ im z = im w to the list of axioms.
Prove StarOrderedRing instance for any IsROrC.
Add (almost trivial) le_iff_re_im proofs to IsROrC instances for real and complex numbers.

This PR does exactly these three steps

eric-wieser

Prove StarOrderedRing instance for any IsROrC.

I don't see this step in this PR; which is the titular one!

eric-wieser

You should also probably delete these lines:

mathlib4/Mathlib/Data/Real/Sqrt.lean

Lines 467 to 471 in e266a1e

    
           instance : StarOrderedRing ℝ := 
        
             StarOrderedRing.ofNonnegIff' add_le_add_left fun r => by 
        
               refine ⟨fun hr => ⟨sqrt r, (mul_self_sqrt hr).symm⟩, ?_⟩ 
        
               rintro ⟨s, rfl⟩ 
        
               exact mul_self_nonneg s

mathlib4/Mathlib/Data/Complex/Basic.lean

Lines 1242 to 1261 in e266a1e

    
           /-- With `z ≤ w` iff `w - z` is real and nonnegative, `ℂ` is a star ordered ring. 
        
           (That is, a star ring in which the nonnegative elements are those of the form `star z * z`.) 
        
           -/ 
        
           protected def starOrderedRing : StarOrderedRing ℂ := 
        
             StarOrderedRing.ofNonnegIff' add_le_add_left fun r => by 
        
               refine' ⟨fun hr => ⟨Real.sqrt r.re, _⟩, fun h => _⟩ 
        
               · have h₁ : 0 ≤ r.re := by 
        
                   rw [le_def] at hr 
        
                   exact hr.1 
        
                 have h₂ : r.im = 0 := by 
        
                   rw [le_def] at hr 
        
                   exact hr.2.symm 
        
                 ext 
        
                 · simp only [ofReal_im, star_def, ofReal_re, sub_zero, conj_re, mul_re, mul_zero, 
        
                     ← Real.sqrt_mul h₁ r.re, Real.sqrt_mul_self h₁] 
        
                 · simp only [h₂, add_zero, ofReal_im, star_def, zero_mul, conj_im, mul_im, mul_zero, 
        
                     neg_zero] 
        
               · obtain ⟨s, rfl⟩ := h 
        
                 simp only [← normSq_eq_conj_mul_self, normSq_nonneg, zero_le_real, star_def] 
        
           #align complex.star_ordered_ring Complex.starOrderedRing

Mathlib/Analysis/Complex/Basic.lean

Mathlib/Data/IsROrC/Basic.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Data/Complex/Basic.lean

Mathlib/Data/IsROrC/Basic.lean

Mathlib/Analysis/Complex/Basic.lean

…ty/mathlib4 into IsROrCStarOrderedRing

eric-wieser · 2023-08-02T10:08:42Z

(Sometimes github makes a mess of the history after a merge; switching the base branch to something else and back fixed it)

MohanadAhmed · 2023-08-02T10:13:01Z

(Sometimes github makes a mess of the history after a merge; switching the base branch to something else and back fixed it)

Is there a way for me to reset it and just start from the current master? @eric-wieser

MohanadAhmed added 6 commits July 27, 2023 18:57

some work on IsRORC StarOrdereRing

39db9d1

more steps

0b58842

Remove sorries

90d4ad7

ugly proof

23a12a5

More human readable proof

5fd81b4

Remove wierd comment

dce8aee

eric-wieser reviewed Jul 28, 2023

View reviewed changes

eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes. t-analysis Analysis (normed *, calculus) t-algebra Algebra (groups, rings, fields, etc) labels Jul 28, 2023

MohanadAhmed added 2 commits July 28, 2023 17:02

The Missing Title

f1f3488

Delete the other StarOrderedRing instances as suggesetd by @eric-wieser

aede694

MohanadAhmed added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jul 28, 2023

eric-wieser reviewed Jul 28, 2023

View reviewed changes

Mathlib/Analysis/Complex/Basic.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jul 28, 2023

View reviewed changes

Mathlib/Data/IsROrC/Basic.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jul 28, 2023

View reviewed changes

Mathlib/Data/IsROrC/Basic.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jul 28, 2023

View reviewed changes

Mathlib/Data/IsROrC/Basic.lean Outdated Show resolved Hide resolved

MohanadAhmed and others added 2 commits July 28, 2023 18:06

Leave the real StarOrderedRing alone

6cc1291

Update Mathlib/Data/IsROrC/Basic.lean

536dc78

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

j-loreaux reviewed Jul 28, 2023

View reviewed changes

Mathlib/Data/Complex/Basic.lean Show resolved Hide resolved

j-loreaux reviewed Jul 28, 2023

View reviewed changes

Mathlib/Data/IsROrC/Basic.lean Outdated Show resolved Hide resolved

remove manual isROrC on Complex type and unnecessary n Fintype

f50eb4b

eric-wieser reviewed Jul 28, 2023

View reviewed changes

Mathlib/Data/IsROrC/Basic.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jul 28, 2023

View reviewed changes

Mathlib/Analysis/Complex/Basic.lean Outdated Show resolved Hide resolved

MohanadAhmed removed the awaiting-review label Jul 28, 2023

MohanadAhmed and others added 3 commits July 28, 2023 20:29

some modifications

bb46899

Merge remote-tracking branch 'origin/master' into IsROrCStarOrderedRing

33fbe9d

golf

946f784

eric-wieser and others added 7 commits July 30, 2023 13:44

golf

82e09bd

very slight golf

efbf8e0

Move inside the namespace

083680a

fix timeout

a6e6907

remove the import

31ffe5f

tweak priority

9638ceb

Merge branch 'IsROrCStarOrderedRing' of github.com:leanprover-communi…

2cb37d7

…ty/mathlib4 into IsROrCStarOrderedRing

eric-wieser changed the base branch from master to staging August 2, 2023 10:07

eric-wieser changed the base branch from staging to master August 2, 2023 10:08

eric-wieser changed the title ~~IsROrC StarOrdered Ring~~ feat(Data/IsROrC/Basic): add a StarOrderedRing instance Aug 2, 2023

eric-wieser mentioned this pull request Aug 6, 2023

[Merged by Bors] - feat: IsROrC.toStarOrderedRing as a scoped instance #6391

Closed

1 task

ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 9, 2023

MohanadAhmed added the WIP Work in progress label Aug 15, 2023

bors bot changed the base branch from master to ScottCarnahan/BinomialRing2 September 17, 2023 03:25

kim-em changed the base branch from ScottCarnahan/BinomialRing2 to master September 17, 2023 12:14

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(Data/IsROrC/Basic): add a `StarOrderedRing` instance#6210

feat(Data/IsROrC/Basic): add a `StarOrderedRing` instance#6210
MohanadAhmed wants to merge 21 commits intomasterfrom
IsROrCStarOrderedRing

MohanadAhmed commented Jul 28, 2023

Uh oh!

eric-wieser left a comment •

edited

Loading

Uh oh!

eric-wieser left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

eric-wieser commented Aug 2, 2023

Uh oh!

MohanadAhmed commented Aug 2, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

	instance : StarOrderedRing ℝ :=
	StarOrderedRing.ofNonnegIff' add_le_add_left fun r => by
	refine ⟨fun hr => ⟨sqrt r, (mul_self_sqrt hr).symm⟩, ?_⟩
	rintro ⟨s, rfl⟩
	exact mul_self_nonneg s

	/-- With `z ≤ w` iff `w - z` is real and nonnegative, `ℂ` is a star ordered ring.
	(That is, a star ring in which the nonnegative elements are those of the form `star z * z`.)
	-/
	protected def starOrderedRing : StarOrderedRing ℂ :=
	StarOrderedRing.ofNonnegIff' add_le_add_left fun r => by
	refine' ⟨fun hr => ⟨Real.sqrt r.re, _⟩, fun h => _⟩
	· have h₁ : 0 ≤ r.re := by
	rw [le_def] at hr
	exact hr.1
	have h₂ : r.im = 0 := by
	rw [le_def] at hr
	exact hr.2.symm
	ext
	· simp only [ofReal_im, star_def, ofReal_re, sub_zero, conj_re, mul_re, mul_zero,
	← Real.sqrt_mul h₁ r.re, Real.sqrt_mul_self h₁]
	· simp only [h₂, add_zero, ofReal_im, star_def, zero_mul, conj_im, mul_im, mul_zero,
	neg_zero]
	· obtain ⟨s, rfl⟩ := h
	simp only [← normSq_eq_conj_mul_self, normSq_nonneg, zero_le_real, star_def]
	#align complex.star_ordered_ring Complex.starOrderedRing

Conversation

MohanadAhmed commented Jul 28, 2023

Uh oh!

eric-wieser left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

eric-wieser 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!

eric-wieser commented Aug 2, 2023

Uh oh!

MohanadAhmed commented Aug 2, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

eric-wieser left a comment •

edited

Loading