[Merged by Bors] - feat(topology/metric_space): diameter of pointwise zero and addition #19028

eric-wieser · 2023-05-17T14:22:55Z

Split from #18990 as they're orthogonal and I don't need this stuff.

This reverts commit 672c1c4.

eric-wieser · 2023-05-17T14:24:55Z

There is some discussion at #18990 (comment) about proving metric.diam (x * y) ≤ metric.diam x + metric.diam y

urkud · 2023-06-21T17:20:33Z

src/analysis/normed/group/pointwise.lean

@@ -33,6 +34,22 @@ begin
  exact norm_mul_le_of_le (hRs x hx) (hRt y hy),
 end

+@[to_additive] lemma metric.bounded.of_mul [has_isometric_smul E E] (hst : bounded (s * t)) :


I think that we should add a lemma about set.image2 and a map which is antilipschitz in both coordinates. Also, the conclusion seems very weak. If s is nonempty, then t is bounded.

@eric-wieser what do you think of this comment?

I believe I already addressed this in the subsequent commits; but am happy to wait for @urkud to take another look

src/analysis/normed/group/pointwise.lean

src/topology/metric_space/basic.lean

eric-wieser · 2023-07-12T12:07:43Z

src/analysis/normed/group/pointwise.lean

+-- note: we can't use `lipschitz_with.bounded_image2` here without adding `[isometric_smul E E]`
 @[to_additive] lemma metric.bounded.mul (hs : bounded s) (ht : bounded t) : bounded (s * t) :=


@YaelDillies, any ideas on whether I can make a better generalization that does work here?

Yes, I believe you can instead use

lemma bounded_image2 (f : α → β → γ) {K₁ K₂ : ℝ≥0} {s : set α} {t : set β} (hf₁ : ∀ b ∈ t, lipschitz_with K₁ (λ a, f a b) s) (hf₂ : ∀ a ∈ s, lipschitz_on_with K₂ (f a) t) (hs : bounded s) (ht : bounded t) : bounded (set.image2 f s t) := sorry

Then you use the fact that multiplication is Lipschitz on bounded sets.

I'm not sure it results in a shorter proof, but it's at least conceptually more satisfying.

I generalized bounded_image2, but haven't changed this proof

Then you use the fact that multiplication is Lipschitz on bounded sets.

Where is this result?

Not in mathlib :/

Should be easy though. The bound on the set turns into the Lipschitz constant.

Are you sure this doesn't need the same [isometric_smul E E] argument that I was trying to avoid?

Don't forget we're in weird normed_group land not normed_add_group.

Then I'm confused: Isn't isometric_smul E E always true in that context?

Not without commutativity; only isometric_smul (MulOpposite E) E is true

Do you care about noncommutative settings?

Also doesn't that mean you can do the proof along t instead of along s (whatever that means)?

Do you care about noncommutative settings?

No, but I don't want to un-generalize a lemma solely for the point of a golf.

src/topology/metric_space/antilipschitz.lean

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

YaelDillies

Thanks, looks good now!

maintainer merge

github-actions · 2023-07-17T11:21:44Z

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

riccardobrasca · 2023-07-27T13:25:02Z

Modulo Yuri's comment above LGTM, thanks!

bors d+

bors · 2023-07-27T13:25:03Z

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

urkud · 2023-10-09T14:37:38Z

Thanks! 🎉
bors merge

…19028)

bors · 2023-10-09T16:56:45Z

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

This was "feat(topology/metric_space): diameter of pointwise zero and addition"

* commit '65a1391a0106c9204fe45bc73a039f056558cb83': (12443 commits) feat(data/{list,multiset,finset}/*): `attach` and `filter` lemmas (leanprover-community#18087) feat(combinatorics/simple_graph): More clique lemmas (leanprover-community#19203) feat(measure_theory/order/upper_lower): Order-connected sets in `ℝⁿ` are measurable (leanprover-community#16976) move old README.md to OLD_README.md doc: Add a warning mentioning Lean 4 to the readme (leanprover-community#19243) feat(topology/metric_space): diameter of pointwise zero and addition (leanprover-community#19028) feat(topology/algebra/order/liminf_limsup): Eventual boundedness of neighborhoods (leanprover-community#18629) feat(probability/independence): Independence of singletons (leanprover-community#18506) feat(combinatorics/set_family/ahlswede_zhang): Ahlswede-Zhang identity, part I (leanprover-community#18612) feat(data/finset/lattice): `sup'`/`inf'` lemmas (leanprover-community#18989) chore(order/liminf_limsup): Generalise and move lemmas (leanprover-community#18628) feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for abelian categories (leanprover-community#17926) feat(data/sum/interval): The lexicographic sum of two locally finite orders is locally finite (leanprover-community#11352) feat(analysis/convex/proj_Icc): Extending convex functions (leanprover-community#18797) feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for pseudoabelian categories (leanprover-community#17925) feat(measure_theory/measure/haar_quotient): the Unfolding Trick (leanprover-community#18863) feat(linear_algebra/orientation): add `orientation.reindex` (leanprover-community#19236) feat(combinatorics/quiver/covering): Definition of coverings and unique lifting of paths (leanprover-community#17828) feat(set_theory/game/pgame): small sets of pre-games / games / surreals are bounded (leanprover-community#15260) feat(tactic/positivity): Extension for `ite` (leanprover-community#17650) ... # Conflicts: # README.md

feat(topology/metric_space): diameter of pointwise zero and addition

22717be

This reverts commit 672c1c4.

eric-wieser requested a review from YaelDillies May 17, 2023 14:22

eric-wieser added awaiting-review The author would like community review of the PR t-topology Topological spaces, uniform spaces, metric spaces, filters t-analysis Analysis (normed *, calculus) labels May 17, 2023

github-actions bot added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label May 17, 2023

eric-wieser mentioned this pull request May 17, 2023

[Merged by Bors] - feat(analysis/normed_space/basic): scaling a set scales its diameter, translating it leaves it unchanged #18990

Closed

This comment was marked as resolved.

Sign in to view

eric-wieser added 2 commits May 17, 2023 15:12

progress

d98708e

helper

02bf304

urkud reviewed Jun 21, 2023

View reviewed changes

src/analysis/normed/group/pointwise.lean Show resolved Hide resolved

urkud reviewed Jun 21, 2023

View reviewed changes

src/topology/metric_space/basic.lean Show resolved Hide resolved

urkud added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jun 21, 2023

eric-wieser added 4 commits July 12, 2023 11:13

add ediam_image2_le

54f4671

golf

0efdfb7

fix

316137e

add new results

7b34024

eric-wieser commented Jul 12, 2023

View reviewed changes

eric-wieser added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 12, 2023

eric-wieser requested a review from urkud July 12, 2023 13:44

eric-wieser added 2 commits July 14, 2023 18:10

generalize

4e21956

fix

4065f17

eric-wieser added the not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 label Jul 15, 2023

YaelDillies reviewed Jul 16, 2023

View reviewed changes

src/topology/metric_space/antilipschitz.lean Outdated Show resolved Hide resolved

Update src/topology/metric_space/antilipschitz.lean

23e27a8

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

YaelDillies approved these changes Jul 17, 2023

View reviewed changes

github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Jul 27, 2023

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Oct 9, 2023

bors bot pushed a commit that referenced this pull request Oct 9, 2023

feat(topology/metric_space): diameter of pointwise zero and addition (#…

c8f3055

…19028)

bors bot changed the title ~~feat(topology/metric_space): diameter of pointwise zero and addition~~ [Merged by Bors] - feat(topology/metric_space): diameter of pointwise zero and addition Oct 9, 2023

bors bot closed this Oct 9, 2023

bors bot deleted the eric-wieser/diam-add branch October 9, 2023 16:56

eric-wieser added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 1, 2023

chore: forward-port leanprover-community/mathlib3#19028

83e44eb

This was "feat(topology/metric_space): diameter of pointwise zero and addition"

eric-wieser added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 1, 2023

chore: forward-port leanprover-community/mathlib3#19028

033f394

This was "feat(topology/metric_space): diameter of pointwise zero and addition"

bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Nov 1, 2023

chore: forward-port leanprover-community/mathlib3#19028 (#8083)

5a2b014

This was "feat(topology/metric_space): diameter of pointwise zero and addition"

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(topology/metric_space): diameter of pointwise zero and addition #19028

[Merged by Bors] - feat(topology/metric_space): diameter of pointwise zero and addition #19028

eric-wieser commented May 17, 2023

eric-wieser commented May 17, 2023

This comment was marked as resolved.

urkud Jun 21, 2023

riccardobrasca Jul 27, 2023

eric-wieser Jul 28, 2023

eric-wieser Jul 12, 2023

YaelDillies Jul 14, 2023 •

edited

Loading

eric-wieser Jul 14, 2023

YaelDillies Jul 15, 2023

eric-wieser Jul 15, 2023

eric-wieser Jul 16, 2023

YaelDillies Jul 16, 2023

eric-wieser Jul 16, 2023

YaelDillies Jul 16, 2023 •

edited

Loading

eric-wieser Jul 16, 2023

YaelDillies left a comment

github-actions bot commented Jul 17, 2023

riccardobrasca commented Jul 27, 2023

bors bot commented Jul 27, 2023

urkud commented Oct 9, 2023

bors bot commented Oct 9, 2023

		-- note: we can't use `lipschitz_with.bounded_image2` here without adding `[isometric_smul E E]`
		@[to_additive] lemma metric.bounded.mul (hs : bounded s) (ht : bounded t) : bounded (s * t) :=

[Merged by Bors] - feat(topology/metric_space): diameter of pointwise zero and addition #19028

[Merged by Bors] - feat(topology/metric_space): diameter of pointwise zero and addition #19028

Conversation

eric-wieser commented May 17, 2023

eric-wieser commented May 17, 2023

This comment was marked as resolved.

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

YaelDillies Jul 14, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

YaelDillies Jul 16, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

YaelDillies left a comment

Choose a reason for hiding this comment

github-actions bot commented Jul 17, 2023

riccardobrasca commented Jul 27, 2023

bors bot commented Jul 27, 2023

urkud commented Oct 9, 2023

bors bot commented Oct 9, 2023

YaelDillies Jul 14, 2023 •

edited

Loading

YaelDillies Jul 16, 2023 •

edited

Loading