[Merged by Bors] - feat(analysis/normed_space/basic): scaling a set scales its diameter, translating it leaves it unchanged #18990
Conversation
eric-wieser
added
easy
github-actions
bot
added
the
modifies-synchronized-file
|
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. |
eric-wieser
removed
the
easy
|
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>
|
🚀 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. |
| @@ -26,6 +26,41 @@ variables {𝕜 E : Type*} [normed_field 𝕜] | |||
| section seminormed_add_comm_group | |||
| 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. |
github-actions
bot
added
ready-to-merge
… 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. |
bors
bot
changed the title
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
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.