[Merged by Bors] - feat(analysis/normed_space/basic): scaling a set scales its diameter, translating it leaves it unchanged#18990
[Merged by Bors] - feat(analysis/normed_space/basic): scaling a set scales its diameter, translating it leaves it unchanged#18990eric-wieser wants to merge 21 commits intomasterfrom
Conversation
|
Let me mention that I think I have those results and a bit more on branch https://github.com/leanprover-community/mathlib/tree/geometric-group-theory, if you want to compare. |
|
Could you add to this PR the lemmas I proved on |
|
I'd rather keep this one small so the forward-port is manageable. I also don't really fancy trawling though the 25 files in that branch to find the lemmas in question! |
|
I just mean the two or three |
|
I don't think those lemmas fit the theme of this PR; they're not about Edit: I've moved all the non-smul stuff to #19028. |
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
YaelDillies
left a comment
There was a problem hiding this comment.
Thanks!
maintainer merge
YaelDillies
left a comment
There was a problem hiding this comment.
Thanks!
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
1 similar comment
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
| variables [seminormed_add_comm_group E] [normed_space 𝕜 E] | ||
|
|
||
| lemma ediam_smul₀ (c : 𝕜) (s : set E) : | ||
| emetric.diam (c • s) = ‖c‖₊ • emetric.diam s := |
There was a problem hiding this comment.
I thought about that too, but I only really need the versions for the "canonical" dilation by c. It's in an isolated file, so we still have plenty of time to consider it before the port is over.
| simp [zero_smul_set hs, ←set.singleton_zero], }, | ||
| refine le_antisymm _ _, | ||
| { exact (lipschitz_with_smul c).ediam_image_le s }, | ||
| { have := (lipschitz_with_smul c⁻¹).ediam_image_le (c • s), |
There was a problem hiding this comment.
There was a problem hiding this comment.
I think I tried that and it didn't make it easier. Feel free to try again.
There was a problem hiding this comment.
I'll try in a few hours. Please don't merge before that. Let's say that this lock auto expires in 4h from now.
There was a problem hiding this comment.
I can get there with something like
rw ←ennreal.le_inv_smul_iff (nnnorm_ne_zero_iff.mpr hc),
apply antilipschitz_with.le_mul_ediam_image,
intros x hx,
rw [← smul_eq_mul, ←ennreal.smul_def, edist_smul₀, inv_smul_smul₀ (nnnorm_ne_zero_iff.mpr hc) _],
exact le_rfl,
but it's not great
| by simp_rw [diam, ediam_smul₀, ennreal.to_real_smul, nnreal.smul_def, coe_nnnorm, smul_eq_mul] | ||
|
|
||
| lemma inf_edist_smul₀ {c : 𝕜} (hc : c ≠ 0) (s : set E) (x : E) : | ||
| emetric.inf_edist (c • x) (c • s) = ‖c‖₊ • emetric.inf_edist x s := |
There was a problem hiding this comment.
I think that we should have inequalities for lipschitz_with and antilipschitz_with functions, then just use le_antisymm here.
|
bors merge I need the ennreal results in another PR. |
… translating it leaves it unchanged (#18990)
|
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. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Forward-port of leanprover-community/mathlib3#18990 Original title: feat(analysis/normed_space/basic): scaling a set scales its diameter, translating it leaves it unchanged
Forward-port of leanprover-community/mathlib3#18990 Original title: feat(analysis/normed_space/basic): scaling a set scales its diameter, translating it leaves it unchanged
This is pre-work for showing that
μH[d] (c • s) = c^d • μH[d] s.