[Merged by Bors] - feat(Analysis/Complex/Hadamard): generalize Hadamard's three lines theorem by madeve-unipi · Pull Request #15009 · leanprover-community/mathlib4

madeve-unipi · 2024-07-22T10:14:47Z

Make Hadamard's three lines theorem work on any vertical strip of the complex plane (i.e., the set of complex numbers of real part between l and u, provided l is less than u). Previously, the theorem would only work for l=0 and u=1.

Moves:

norm_le_interp_of_mem_verticalClosedStrip -> norm_le_interp_of_mem_verticalClosedStrip₀₁
norm_le_interp_of_mem_verticalClosedStrip' -> norm_le_interp_of_mem_verticalClosedStrip₀₁'

github-actions · 2024-07-22T10:15:25Z

messageFile.md

dupuisf · 2024-08-19T15:30:07Z

This looks quite good. Can you merge master to get rid of the merge conflict?

madeve-unipi · 2024-08-20T13:28:37Z

@dupuisf I merged master but I'm not sure what went wrong with building mathlib (unsuccessful check)

dupuisf · 2024-08-20T17:41:31Z

If you click on the red X next to the failed commit, you can see which step failed. Here it's the "build" step, and if you
click on "Details", you can see what went wrong. In this case, the issue is that there are several unused arguments.

madeve-unipi · 2024-08-20T18:20:00Z

If you click on the red X next to the failed commit, you can see which step failed. Here it's the "build" step, and if you click on "Details", you can see what went wrong. In this case, the issue is that there are several unused arguments.

I wonder why this wasn't an issue in the original commit, but it's fixed now. Thank you!

dupuisf · 2024-08-20T20:15:22Z

I wonder why this wasn't an issue in the original commit, but it's fixed now. Thank you!

The latest version of Lean includes a change in the variable inclusion mechanism, leading to a lot of breakage like this.

dupuisf

This looks quite good. I have a first round of comments, mostly about coding style and removing lemmas that are a bit out of place in this file. Also, I have one request: could you add back versions of the theorem with the strip from 0 to 1? It's a bit easier to use since there's no division by u-l in the exponents and so on.

Mathlib/Analysis/Complex/Hadamard.lean

madeve-unipi · 2024-09-07T14:15:31Z

Thank you for your comments. I should have fixed everything that was brought up.

Also, I have one request: could you add back versions of the theorem with the strip from 0 to 1? It's a bit easier to use since there's no division by u-l in the exponents and so on.

I am not sure I understand what you mean here. The old versions should still be usable under [theoremname]_{01}, see lines 371 and 385 (I'm sorry but I don't know how to paste them here like you did in the review).

Ah right, never mind, somehow I expected them to be close together -- just disregard what I wrote there!

dupuisf · 2024-09-10T02:12:06Z

Another quick note: to make things easier for reviewers, can you click on "resolve conversation" whenever a comment has been addressed? Also, if you feel like the PR is ready for another round of review, you should remove the "awaiting-author" label, otherwise people will just assume that you are still working on it.

Mathlib/Analysis/Complex/Hadamard.lean

dupuisf · 2024-09-11T02:19:44Z

Mathlib/Analysis/Complex/Hadamard.lean

+/-- The norm of the function `scale f l u` is bounded above on the closed strip `re⁻¹' [0, 1]`-/
+lemma scale_bddAbove {f: ℂ → E} {l u : ℝ} (hul: l< u)


Suggested change

/-- The norm of the function `scale f l u` is bounded above on the closed strip `re⁻¹' [0, 1]`-/

lemma scale_bddAbove {f: ℂ → E} {l u : ℝ} (hul: l< u)

/-- The norm of the function `scale f l u` is bounded above on the closed strip `re⁻¹' [0, 1]`-/

lemma scale_bddAbove {f: ℂ → E} {l u : ℝ} (hul: l < u)

Can you standardize the spacing in the file? Normally things like u-l should really be written as u - l and so on.

I've tried fixing this. I hope nothing slipped past.

Mathlib/Analysis/Complex/Hadamard.lean

madeve-unipi · 2024-10-08T08:40:54Z

Some general remark: Why don't generalise the existing lemmas from the 0-1 strip to a general strip rather than reducing the general case to the 0-1 strip by a transformation?

This is essentially because I had proved the result from scratch for a university course (https://florisvandoorn.com/BonnAnalysis/) and then we realized the 0-1 strip case was already here. My proof was the one in Stein-Shakarchi's Functional Analysis book. It was very convenient to have 0 and 1 and then I obtained the rest via a transformation, so I just adapted that part to commit here. I haven't really studied the details of how the current mathlib proof actually works. I can try to go through it if it's better to prove the general case first, but I don't think I will have enough time for that in the next couple of weeks.

YaelDillies · 2024-10-08T14:48:27Z

Okay, fair enough. I think mathlib's proof could be easy to adapt by applying the transformation earlier (although I'm not sure). If you don't have time for now, this can be left as a TODO.

Please address my comments above, however.

madeve-unipi · 2025-01-31T13:53:44Z

I am sorry I completely forgot to do this. I removed the unnecessary brackets around verticalClosedStrip 0 1 and sSupNormIm throughout the document. It is not entirely clear to me whether or not more brackets can be removed. For example, why is f '' VerticalClosedStrip 0 1 perfectly fine, but f ' ' (re ⁻¹' {x}) requires bracketing?

YaelDillies · 2025-01-31T15:48:59Z

why is f '' VerticalClosedStrip 0 1 perfectly fine, but f ' ' (re ⁻¹' {x}) requires bracketing?

Because precedences are wrong. Feel free to open an issue for that on this repo!

YaelDillies

Thanks! Maybe merge master once to make sure everything still works.

maintainer delegate

Mathlib/Analysis/Complex/Hadamard.lean

github-actions · 2025-01-31T16:05:32Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

jcommelin

bors d+

mathlib-bors · 2025-01-31T16:40:13Z

✌️ madeve-unipi can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

github-actions · 2025-01-31T17:00:13Z

PR summary 5e6f98d675

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ interpStrip'
+ interpStrip_scale
+ mem_verticalClosedStrip_of_scale_id_mem_verticalClosedStrip
+ norm_le_interpStrip_of_mem_verticalClosedStrip₀₁
+ norm_le_interp_of_mem_verticalClosedStrip₀₁'
+ sSupNormIm_scale_left
+ sSupNormIm_scale_right
+ scale
+ scale_bddAbove
+ scale_bound_left
+ scale_bound_right
+ scale_diffContOnCl
+ scale_id_mem_verticalClosedStrip_of_mem_verticalClosedStrip
+ scale_id_mem_verticalStrip_of_mem_verticalStrip

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.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

spacing fix Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

spacing fix #2 Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

madeve-unipi · 2025-01-31T17:27:17Z

I merged master and committed your spacing fix, everything looks fine to me

YaelDillies · 2025-01-31T17:28:37Z

Feel free to reply bors merge then 😄

madeve-unipi · 2025-01-31T17:36:20Z

Because precedences are wrong. Feel free to open an issue for that on this repo!

Do you mean that f '' (re ⁻¹' {x}) should not require brackets and this is a Lean issue I should open?
Does this look right?

Title: Notation precedence issue with ' '
Description: The expression f '' (re ⁻¹' {x}) requires brackets when it should not. See for example Mathlib/Analysis/Complex/Hadamard.lean

madeve-unipi · 2025-01-31T17:38:14Z

bors merge

…eorem (#15009) Make Hadamard's three lines theorem work on any vertical strip of the complex plane (i.e., the set of complex numbers of real part between `l` and `u`, provided l is less than u). Previously, the theorem would only work for `l=0` and `u=1`. Moves: - norm_le_interp_of_mem_verticalClosedStrip -> norm_le_interp_of_mem_verticalClosedStrip₀₁ - norm_le_interp_of_mem_verticalClosedStrip' -> norm_le_interp_of_mem_verticalClosedStrip₀₁' Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: madeve-unipi <56154049+madeve-unipi@users.noreply.github.com>

YaelDillies · 2025-01-31T17:44:58Z

Do you mean that f '' (re ⁻¹' {x}) should not require brackets and this is a Lean issue I should open?
Does this look right?

It's not a Lean issue, it's a Mathlib issue

mathlib-bors · 2025-01-31T18:03:25Z

Pull request successfully merged into master.

Build succeeded:

* factorial-dvd-int: (143 commits) Apply suggestions from code review feat(Factorial): k! divides the product of any k successive integers feat(CategoryTheory): creation of finite limits (#21320) chore: update Mathlib dependencies 2025-02-01 (#21328) chore(GroupTheory/SpecificGroups/Alternating.lean): follow last minute review of JX (#21314) feat: `‖x‖ₑ.toNNReal = ‖x‖₊` (#21306) chore: cleanup imports in Archive/IfNormalization (#21318) doc: fix several typos (#21315) feat(CategoryTheory): transfer being iso along an iso in the arrow category (#21310) chore: delete declarations deprecated between 2024-01 and 2024-07 (#21271) feat(Analysis/Normed/Module/Dual): polar in a normed space as a submodule (#20084) chore(Data/ZMod/Basic): split `ZMod.valMinAbs` off (#21308) feat(GroupTheory/Perm/Centralizer): study the centralizer of a permutation (#17522) feat(RingTheory/LocalRing): `IsLocalRing` for subrings (#21168) chore: update Mathlib dependencies 2025-02-01 (#21312) chore: update Mathlib dependencies 2025-01-31 (#21311) feat: generalize `mem_dite` to `Membership α β` (#21262) feat: Lemmas for some monomial orders (#16177) feat(CategoryTheory): the localized category is monoidal (#12728) feat: add function log⁺ (=positive part of the logarithm) and prove standard estimates (#21289) feat(RingTheory/WittVector): ring of Witt vectors is p-adically complete (#21295) feat(GroupTheory/GroupAction/Blocks): more on blocks (#21284) fix(FieldTheory/KrullTopology): make `krullTopology_discreteTopology_of_finiteDimensional` universe polymorphic (#21299) feat(RingTheory/Artinian): integral non-zero-divisors are units over artinian rings (#21199) refactor(Topology/Gluing): simplify definition of `TopCat.GlueData.Rel` (#20653) feat(RingTheory/PowerSeries): binomial series (#20192) chore(Mathlib/RingTheory/MvPolynomial): rename MonomiaOrder.lCoeff to MonomialOrder.leadingCoeff (#21290) chore (RingTheory/HahnSeries): fix names that use coeff (#21279) feat: let `notation3` distinguish `Prop` vs `Type _ ` vs `Sort _` (#21233) chore(MeasureTheory/Function/StronglyMeasurable): split Basic into Basic and AEStronglyMeasurable (#21273) feat(CategoryTheory): the monoidal category structure on a localization (#20951) feat(Analysis/Complex/Hadamard): generalize Hadamard's three lines theorem (#15009) feat(Order/CompleteBooleanAlgebra): Himp in terms of sSup (#20328) feat(ENNReal/Basic): add `ofNat_ne_top` and `top_ne_ofNat` (#14486) feat: Function.const as a PartialEquiv (#21137) chore(NonZeroDivisors): don't import rings (#20871) feat(Data/Set/Lattice): insert distributivity with iUnion/iInter (#21267) feat(GroupTheory/SpecificGroups/AlternatingGroup): subgroups of index 2 of Equiv.Perm (#21190) feat(GroupTheory/GroupAction/Transitive): basic results on transitive actions (#21285) perf(MeasureTheory/Function/LpSpace.lean): speed up (#21179) feat(Order): order isomorphisms from `Fin n` for small `n` (#21120) refactor(Topology/Group): turn morphisms in ProfiniteGrp into one field structures (#20740) feat: Sylow's first theorem for elementary `p`-groups (#21072) chore(Submonoid/Membership): don't import `MonoidWithZero` (#20748) refactor(Algebra/Algebra/Pi): cleanup and renaming (#21213) feat(GroupTheory/IndexNormal): subgroups of small index are normal (#21186) feat(Algebra/Group/Action): add definition of equidecomposition (#16936) feat(CategoryTheory/Subpresheaf): equalizer (#21096) feat: add lemmas about products of `Matrix.stdBasisMatrix` (#21204) chore: update Mathlib dependencies 2025-01-31 (#21282) ...

…eorem (#15009) Make Hadamard's three lines theorem work on any vertical strip of the complex plane (i.e., the set of complex numbers of real part between `l` and `u`, provided l is less than u). Previously, the theorem would only work for `l=0` and `u=1`. Moves: - norm_le_interp_of_mem_verticalClosedStrip -> norm_le_interp_of_mem_verticalClosedStrip₀₁ - norm_le_interp_of_mem_verticalClosedStrip' -> norm_le_interp_of_mem_verticalClosedStrip₀₁' Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: madeve-unipi <56154049+madeve-unipi@users.noreply.github.com>

generalized three lines lemma

3227f13

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jul 22, 2024

grunweg added the t-analysis Analysis (normed *, calculus) label Jul 22, 2024

grunweg changed the title ~~feat (Analysis/Complex/Hadamard): generalize previous version of Hadamard's three lines theorem/lemma~~ feat(Analysis/Complex/Hadamard): generalize previous version of Hadamard's three lines theorem/lemma Jul 22, 2024

grunweg changed the title ~~feat(Analysis/Complex/Hadamard): generalize previous version of Hadamard's three lines theorem/lemma~~ feat(Analysis/Complex/Hadamard): generalize Hadamard's three lines theorem Jul 22, 2024

ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 25, 2024

dupuisf self-assigned this Aug 19, 2024

Merge remote-tracking branch 'origin' into madeve-unipi_hadamard

3deaad6

ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 20, 2024

fix unused variable issue

4886c43

dupuisf reviewed Sep 6, 2024

View reviewed changes

dupuisf added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 6, 2024

Comment fixes

0fb8533

madeve-unipi removed the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 10, 2024

dupuisf reviewed Sep 11, 2024

View reviewed changes

dupuisf added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 11, 2024

madeve-unipi added 2 commits September 11, 2024 10:51

fixes

d9fe862

scale_mem to scale_id_mem

255f91f

madeve-unipi removed the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 13, 2024

jcommelin requested a review from dupuisf September 24, 2024 14:29

YaelDillies reviewed Sep 24, 2024

View reviewed changes

dupuisf added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 27, 2024

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 2, 2024

removed unnecessary bracketing

d760a22

madeve-unipi removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 31, 2025

YaelDillies approved these changes Jan 31, 2025

View reviewed changes

Mathlib/Analysis/Complex/Hadamard.lean Outdated Show resolved Hide resolved

Mathlib/Analysis/Complex/Hadamard.lean Outdated Show resolved Hide resolved

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 31, 2025

jcommelin reviewed Jan 31, 2025

View reviewed changes

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jan 31, 2025

merge master

cfe43a7

madeve-unipi and others added 2 commits January 31, 2025 18:16

Update Mathlib/Analysis/Complex/Hadamard.lean

116d2b3

spacing fix Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/Analysis/Complex/Hadamard.lean

5e6f98d

spacing fix #2 Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

mathlib-bors bot changed the title ~~feat(Analysis/Complex/Hadamard): generalize Hadamard's three lines theorem~~ [Merged by Bors] - feat(Analysis/Complex/Hadamard): generalize Hadamard's three lines theorem Jan 31, 2025

mathlib-bors bot closed this Jan 31, 2025

mathlib-bors bot deleted the madeve-unipi_hadamard branch January 31, 2025 18:03

		/-- The norm of the function `scale f l u` is bounded above on the closed strip `re⁻¹' [0, 1]`-/
		lemma scale_bddAbove {f: ℂ → E} {l u : ℝ} (hul: l< u)

Conversation

madeve-unipi commented Jul 22, 2024 • edited by grunweg Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jul 22, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

dupuisf commented Aug 19, 2024

Uh oh!

madeve-unipi commented Aug 20, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

dupuisf commented Aug 20, 2024

Uh oh!

madeve-unipi commented Aug 20, 2024

Uh oh!

dupuisf commented Aug 20, 2024

Uh oh!

dupuisf left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

madeve-unipi commented Sep 7, 2024 • edited by dupuisf Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

dupuisf commented Sep 10, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

dupuisf Sep 11, 2024

Choose a reason for hiding this comment

Uh oh!

madeve-unipi Sep 11, 2024

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

madeve-unipi commented Oct 8, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

YaelDillies commented Oct 8, 2024

Uh oh!

madeve-unipi commented Jan 31, 2025

Uh oh!

YaelDillies commented Jan 31, 2025

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented Jan 31, 2025

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jan 31, 2025

Uh oh!

github-actions bot commented Jan 31, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 5e6f98d675

Import changes for modified files

Declarations diff

Uh oh!

madeve-unipi commented Jan 31, 2025

Uh oh!

YaelDillies commented Jan 31, 2025

madeve-unipi commented Jul 22, 2024 •

edited by grunweg

Loading

github-actions bot commented Jul 22, 2024 •

edited

Loading

madeve-unipi commented Aug 20, 2024 •

edited

Loading

madeve-unipi commented Sep 7, 2024 •

edited by dupuisf

Loading

dupuisf commented Sep 10, 2024 •

edited

Loading

madeve-unipi commented Oct 8, 2024 •

edited

Loading

github-actions bot commented Jan 31, 2025 •

edited

Loading