-
Notifications
You must be signed in to change notification settings - Fork 297
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
feat(measure_theory/integral/circle_transform): Circle transform results pt2 #15356
Conversation
…esults needed for the uniform lim of holo result
…esults needed for the uniform lim of holo result
Could you split this PR into two, one doing the renaming, and the other one adding the new content? This would make it easier to review. |
Ok I changed the name here: #16387 |
Please add an empty line before the dashed line. Also you have to merge master and fix the merge conflicts (you can do that in github). |
apply add_nonneg, | ||
apply (finset.sum_nonneg ), | ||
intros a b, | ||
apply absolute_value.nonneg, | ||
apply add_nonneg, | ||
apply absolute_value.nonneg, | ||
apply absolute_value.nonneg, |
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.
Looks like you didn't enclose subgoals in braces here. And can't you use the positivity
tactic?
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've made some remarks. Please look through the whole PR and do the corresponding changes.
Also I think you should add docstrings to almost all new lemmas, they are not easy to read.
def circle_integral_form [complete_space E] (R : ℝ) (z : ℂ) (f : ℂ → E) : (ℂ → E) := | ||
λ w, (2 * π * I : ℂ)⁻¹ • (∮ z in C(z, R), (z - w)⁻¹ • f z) |
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.
def circle_integral_form [complete_space E] (R : ℝ) (z : ℂ) (f : ℂ → E) : (ℂ → E) := | |
λ w, (2 * π * I : ℂ)⁻¹ • (∮ z in C(z, R), (z - w)⁻¹ • f z) | |
def circle_integral_form [complete_space E] (R : ℝ) (z : ℂ) (f : ℂ → E) (w : ℂ) : E := | |
(2 * π * I : ℂ)⁻¹ • (∮ z in C(z, R), (z - w)⁻¹ • f z) |
The contains the next set of results needed for #13500 . Note also the change of file name from pt1 since the name
circle_integral_transform
is no longer used (so the first 175 lines are not new).