[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#19028eric-wieser wants to merge 10 commits intomasterfrom
Conversation
This reverts commit 672c1c4.
|
There is some discussion at #18990 (comment) about proving |
This comment was marked as resolved.
This comment was marked as resolved.
| 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)) : |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
I believe I already addressed this in the subsequent commits; but am happy to wait for @urkud to take another look
| -- 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) := |
There was a problem hiding this comment.
@YaelDillies, any ideas on whether I can make a better generalization that does work here?
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
Not in mathlib :/
Should be easy though. The bound on the set turns into the Lipschitz constant.
There was a problem hiding this comment.
Are you sure this doesn't need the same [isometric_smul E E] argument that I was trying to avoid?
There was a problem hiding this comment.
Don't forget we're in weird normed_group land not normed_add_group.
There was a problem hiding this comment.
Then I'm confused: Isn't isometric_smul E E always true in that context?
There was a problem hiding this comment.
Not without commutativity; only isometric_smul (MulOpposite E) E is true
There was a problem hiding this comment.
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)?
There was a problem hiding this comment.
Do you care about noncommutative settings?
No, but I don't want to un-generalize a lemma solely for the point of a golf.
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
YaelDillies
left a comment
There was a problem hiding this comment.
Thanks, looks good now!
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
Modulo Yuri's comment above LGTM, thanks! bors d+ |
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Thanks! 🎉 |
|
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. |
This was "feat(topology/metric_space): diameter of pointwise zero and addition"
This was "feat(topology/metric_space): diameter of pointwise zero and addition"
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
Split from #18990 as they're orthogonal and I don't need this stuff.