-
Notifications
You must be signed in to change notification settings - Fork 299
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
[Merged by Bors] - feat(analysis/normed_space/exponential): exponentials of negations, scalar actions, and sums #13036
Conversation
These live in their respective namespaces for now to match `list.prod_commute` and `multiset.prod_commute`. This also renames the existing additive versions to `sum_add_commute`, to avoid confusion.
These live in their respective namespaces for now to match `list.prod_commute` and `multiset.prod_commute`. This also renames the existing additive versions to `sum_add_commute`, to avoid confusion.
This PR/issue depends on: |
noncomputable def invertible_exp [char_zero 𝕂] (x : 𝔸) : invertible (exp 𝕂 𝔸 x) := | ||
invertible_exp_of_mem_ball $ (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _ |
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.
noncomputable def invertible_exp [char_zero 𝕂] (x : 𝔸) : invertible (exp 𝕂 𝔸 x) := | |
invertible_exp_of_mem_ball $ (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _ | |
noncomputable def invertible_exp (x : 𝔸) : invertible (exp 𝕂 𝔸 x) := | |
invertible_exp_of_mem_ball $ (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _ |
Same with the rest of this section, we have this instance for is_R_or_C 𝕂
. Also, how about making this an instance and removing this awkward requirement from inv_of_exp
?
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.
It seems we don't tend to make invertible
declarations actually instance
s, as this easily leads to diamonds. The awkward requirement in inv_of_exp
is deliberate, as it makes this lemma immune to diamond problems.
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.
Fair enough. Let's just remove the [char_zero 𝕂]
assumptions and merge this.
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.
Yep, I agree I should do that.
bors r+ |
…calar actions, and sums (#13036) The new lemmas are: * `exp_invertible_of_mem_ball` * `exp_invertible` * `is_unit_exp_of_mem_ball` * `is_unit_exp` * `ring.inverse_exp` * `exp_neg_of_mem_ball` * `exp_neg` * `exp_sum_of_commute` * `exp_sum` * `exp_nsmul` * `exp_zsmul` I don't know enough about the radius of convergence of `exp` to know if `exp_nsmul` holds more generally under extra conditions.
Pull request successfully merged into master. Build succeeded: |
The new lemmas are:
exp_invertible_of_mem_ball
exp_invertible
is_unit_exp_of_mem_ball
is_unit_exp
ring.inverse_exp
exp_neg_of_mem_ball
exp_neg
exp_sum_of_commute
exp_sum
exp_nsmul
exp_zsmul
I don't know enough about the radius of convergence of
exp
to know ifexp_nsmul
holds more generally under extra conditions.commute.*_sum_{left,right}
lemmas #13035