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] - refactor(analysis/analytic/basic): refactor change_origin
#8282
Conversation
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
🎉 Great news! Looks like all the dependencies have been resolved: 💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
…/mathlib into change-origin
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.
bors d+
Thanks!
src/analysis/analytic/basic.lean
Outdated
|
||
variables (p : formal_multilinear_series 𝕜 E F) {x y : E} {r R : ℝ≥0} | ||
|
||
/-- A term of `formal_multilinear_series.change_origin_series`. -/ |
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.
Can you expand the docstring? I.e., recall whay change_origin_series
is gonna be, and what is its role?
src/analysis/analytic/basic.lean
Outdated
apply continuous_multilinear_map.le_op_nnnorm | ||
end | ||
|
||
/-- The power series for `f.change_origin k`. -/ |
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.
Can you explain what f.change_origin k
is in the docstring?
src/analysis/analytic/basic.lean
Outdated
series of terms `B`, and we show that they correspond to each other by reordering to conclude the | ||
proof. -/ | ||
theorem change_origin_eval (h : (∥x∥₊ + ∥y∥₊ : ℝ≥0∞) < p.radius) : | ||
(p.change_origin x).sum y = (p.sum (x + y)) := |
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.
(p.change_origin x).sum y = (p.sum (x + y)) := | |
(p.change_origin x).sum y = (p.sum (x + y)) := |
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
Now each term of `change_origin` is defined as a sum of a formal power series, so it is clear that each term is an analytic function. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Pull request successfully merged into master. Build succeeded: |
change_origin
change_origin
Now each term of `change_origin` is defined as a sum of a formal power series, so it is clear that each term is an analytic function. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Now each term of
change_origin
is defined as a sum of a formal power series, so it is clear that each term is an analytic function.mul_le_mul'
forcanonically_ordered_comm_semiring
#8284