-
Notifications
You must be signed in to change notification settings - Fork 891
refactor(Analysis/NormedSpace/Exponential): remove the 𝕂 argument from exp
#8370
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: master
Are you sure you want to change the base?
Conversation
…ditive monoids While many of the lemmas cease to apply, the definitions of sequences and their sums are still perfectly well-behaved in additive monoids; no negation is needed. We could use this to generalize `NormedSpace.exp` such that it works with `NNReal`, but unless leanprover-community/mathlib3#16554 or similar lands and provides a `DivisionSemiring.nnqsmul` field, that would conflict with #8370.
girving
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm curious if 𝕂 can be stripped from more of the lemmas, using the fact that any normed algebra is a real normed algebra. But possibly that would interfere with inference in practice?
| analyticAt_exp_of_mem_ball x ((expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _) | ||
| #align exp_analytic NormedSpace.exp_analytic | ||
|
|
||
| variable (𝕂) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why do we need this? If it's so that we pull in a NormedAlgebra assumption, couldn't we always do that over the reals (since complex normed algebras are real normed algebras)?
| [∀ i, NormedAlgebra 𝕂 (𝔸 i)] [∀ i, CompleteSpace (𝔸 i)] (x : ∀ i, 𝔸 i) (i : ι) : | ||
| exp 𝕂 x i = exp 𝕂 (x i) := | ||
| map_exp _ (Pi.evalRingHom 𝔸 i) (continuous_apply _) x | ||
| [∀ i, Algebra ℚ (𝔸 i)] [∀ i, NormedAlgebra 𝕂 (𝔸 i)] [∀ i, CompleteSpace (𝔸 i)] (x : ∀ i, 𝔸 i) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could we switched the normed algebra to be always over the reals, as complex normed algebras are real normed algebras (resp. below)?
PR summary 36187df13dImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
I agree with this in theory; I guess the question is whether this ends up in annoying situations where |
j-loreaux
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not sure about this. The addition of Algebra ℚ A assumptions is unpleasant, along with needing to remember to supply the 𝕜 argument to lemmas because it can't determine it from the type.
| variable {A : Type*} [NormedRing A] [StarRing A] | ||
| [IsTopologicalRing A] [NormedAlgebra ℝ A] [CompleteSpace A] | ||
| [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] | ||
| [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [Algebra ℚ A] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah, yeah, I was worried about this kind of thing. It's going to be really annoying if, whenever we want to talk about the exponential in a C⋆-algebra, we have to add an Algebra ℚ A assumption.
|
Can you explain in the PR description why mathematically you can remove the field argument? |
|
This pull request has conflicts, please merge |
Thanks for the question! It motivated me to find ratCast_smul_eq. This means that we can define the exponent using something like |
This argument is still needed for almost all the lemmas, which means it can longer be found by unification.
We keep around
expSeries 𝕂 A, as it's needed for talking about the radius of convergence over different base fields.This is a prerequisite for #8372, as we can't merge the functions until they have the same interface.\
Zulip thread: #mathlib4 > Real.exp @ 💬
This is started from the mathport output on leanprover-community/mathlib3#19244