Skip to content

[Merged by Bors] - chore(Analysis/InnerProductSpace): weaken assumptions to SeminormedAddCommGroup#17007

Closed
yoh-tanimoto wants to merge 9 commits intomasterfrom
yoh-tanimoto-innerproductspace-semi
Closed

[Merged by Bors] - chore(Analysis/InnerProductSpace): weaken assumptions to SeminormedAddCommGroup#17007
yoh-tanimoto wants to merge 9 commits intomasterfrom
yoh-tanimoto-innerproductspace-semi

Conversation

@yoh-tanimoto
Copy link
Copy Markdown
Collaborator

@yoh-tanimoto yoh-tanimoto commented Sep 21, 2024 •
edited by eric-wieser
Loading

replace the assumption NormedAddCommGroup to SemiNormedAddCommGroup in various places.

motivation: with the weakened assumption the results apply to InnerProductSpace without definite assumption.

This is suggested in #16707, and continues from #14024.

I think it should be possible to do the same with IsSymmetric.restrictScalars but CompatibleSMul E E ℝ 𝕜 cannot be synthesized. Can anyone help?

Are there other things that work with SemiNormedAddCommGroup?

I noticed that in InnerProductSpace.Basic there are two instances of InnerProductSpace ℝ ℂ. Should I remove the latter?

@yoh-tanimoto yoh-tanimoto added help-wanted The author needs attention to resolve issues t-analysis Analysis (normed *, calculus) labels Sep 21, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Sep 21, 2024 •
edited
Loading

PR summary 0f88afc31f

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

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

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

@yoh-tanimoto yoh-tanimoto mentioned this pull request Sep 21, 2024
Closed
3 tasks
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Sep 22, 2024

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Sep 22, 2024

Here are the benchmark results for commit 94fe59e.
There were no significant changes against commit 831db37.

@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Sep 22, 2024

I span off #17011 from this; I think that in turn will make some sections more generalizable.

eric-wieser
eric-wieser reviewed Sep 22, 2024
View reviewed changes
@yoh-tanimoto yoh-tanimoto changed the title refactor(Analysis/InnerProductSpace/Dual): weaken the assumption to SemiNormedAddCommGroup chore:(Analysis/InnerProductSpace/Dual): weaken the assumption to SemiNormedAddCommGroup Sep 22, 2024
@yoh-tanimoto yoh-tanimoto changed the title chore:(Analysis/InnerProductSpace/Dual): weaken the assumption to SemiNormedAddCommGroup chore:(Analysis/InnerProductSpace/Symmetric): weaken the assumption to SemiNormedAddCommGroup Sep 22, 2024
eric-wieser
eric-wieser reviewed Sep 23, 2024
View reviewed changes
Mathlib/Analysis/Normed/Module/Completion.lean
namespace Completion

variable (𝕜 E : Type*) [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
variable (𝕜 E : Type*) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser Sep 23, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've done a much more thorough version of this in #17059, but they can be merged in either order.

@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Sep 23, 2024

this is suggested in #16707. I think it should be possible to do the same with IsSymmetric.restrictScalars but CompatibleSMul E E ℝ 𝕜 cannot be synthesized. Can anyone help?

I managed to solve this for you with a letI.

@eric-wieser eric-wieser changed the title chore:(Analysis/InnerProductSpace/Symmetric): weaken the assumption to SemiNormedAddCommGroup chore:(Analysis/InnerProductSpace): weaken assumptions to SeminormedAddCommGroup Sep 24, 2024
eric-wieser
eric-wieser approved these changes Sep 24, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This now looks good to me; I think there are probably more generalizations possible elsewhere, but this already hits quite a lot of them!

Were there any more you wanted help with, or can the help-wanted label go?

@yoh-tanimoto yoh-tanimoto removed the help-wanted The author needs attention to resolve issues label Sep 24, 2024
@yoh-tanimoto
Copy link
Copy Markdown
Collaborator Author

yoh-tanimoto commented Sep 24, 2024

Yes, I only checked Basic, Symmetric and Dual. I will see whether more generalizations are possible in other files when I will use them. Thank you very much for your help!

Could you please tell me why #synth CompatibleSMul E E ℝ 𝕜 cannot be synthesized, yet the previous code worked with NormedAddCommGroup?

@eric-wieser eric-wieser changed the title chore:(Analysis/InnerProductSpace): weaken assumptions to SeminormedAddCommGroup chore(Analysis/InnerProductSpace): weaken assumptions to SeminormedAddCommGroup Sep 24, 2024
@j-loreaux
Copy link
Copy Markdown
Contributor

j-loreaux commented Sep 25, 2024

@yoh-tanimoto I think Eric already explained this above. The issue is that the instance it was trying to use required T2Space, which doesn't hold in seminormed spaces, only normed ones. So it needed explicit help.

@j-loreaux
Copy link
Copy Markdown
Contributor

j-loreaux commented Sep 25, 2024

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Sep 25, 2024
mathlib-bors bot pushed a commit that referenced this pull request Sep 25, 2024
@yoh-tanimoto @eric-wieser
chore(Analysis/InnerProductSpace): weaken assumptions to `SeminormedA…
691fdda 
…ddCommGroup` (#17007)

replace the assumption `NormedAddCommGroup` to `SemiNormedAddCommGroup` in various places.

motivation: with the weakened assumption the results apply to `InnerProductSpace` without `definite` assumption.

This is suggested in #16707, and continues from #14024.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Sep 25, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Analysis/InnerProductSpace): weaken assumptions to SeminormedAddCommGroup [Merged by Bors] - chore(Analysis/InnerProductSpace): weaken assumptions to SeminormedAddCommGroup Sep 25, 2024
@mathlib-bors mathlib-bors bot closed this Sep 25, 2024
@mathlib-bors mathlib-bors bot deleted the yoh-tanimoto-innerproductspace-semi branch September 25, 2024 21:08
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Sep 25, 2024

@yoh-tanimoto I think Eric already explained this above. The issue is that the instance it was trying to use required T2Space, which doesn't hold in seminormed spaces, only normed ones. So it needed explicit help.

Actually the issue here was more subtle; the lemma was about a non-instance typeclass argument provided through a messy @ _ _ _ invocation. I switched this to use letI for clarify, but you would need the same letI in the #synth for it to work.

@yoh-tanimoto
Copy link
Copy Markdown
Collaborator Author

yoh-tanimoto commented Sep 26, 2024

Yes, I meant that. Even with NormedAddCommGroup, I got #synth error (as in my question above).

fbarroero pushed a commit that referenced this pull request Oct 2, 2024
@yoh-tanimoto @eric-wieser @fbarroero
chore(Analysis/InnerProductSpace): weaken assumptions to `SeminormedA…
69bc19e 
…ddCommGroup` (#17007)

replace the assumption `NormedAddCommGroup` to `SemiNormedAddCommGroup` in various places.

motivation: with the weakened assumption the results apply to `InnerProductSpace` without `definite` assumption.

This is suggested in #16707, and continues from #14024.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser approved these changes

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@yoh-tanimoto @eric-wieser @leanprover-bot @j-loreaux