feat: generalize tangentConeAt.lim_zero to TVS#21065
feat: generalize tangentConeAt.lim_zero to TVS#21065eric-wieser wants to merge 9 commits intomasterfrom
tangentConeAt.lim_zero to TVS#21065Conversation
Without any changes to the proofs, these lemmas do not need a normed space.
PR summary 6cca842c82Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 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 No changes to technical debt.You can run this locally as
|
| variable {x y : E} {s t : Set E} | ||
|
|
||
| /-- The tangent cone of a product contains the tangent cone of its left factor. -/ | ||
| theorem subset_tangentCone_prod_left {t : Set F} {y : F} (ht : y ∈ closure t) : |
There was a problem hiding this comment.
This then becomes the last generalization to resolve in this file. The obvious start to the proof is
theorem subset_tangentCone_prod_left {t : Set F} {y : F} (ht : y ∈ closure t) :
LinearMap.inl 𝕜 E F '' tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y) := by
rintro _ ⟨v, ⟨c, d, hd, hc, hy⟩, rfl⟩
suffices ∃ d' : ℕ → F, (∀ᶠ n in atTop, y + d' n ∈ t) ∧ Tendsto (fun n => c n • d' n) atTop (𝓝 0) by
choose d' hd'1 hd'2 using this
exact ⟨c, fun n => (d n, d' n), hd.and hd'1, hc, hy.prod_mk_nhds hd'2⟩
sorrywhich I think follows immediately just by restructureing the previous proof.
There was a problem hiding this comment.
This (the rest of the proof, not what you've written) does not seem obvious to me. I need to think about it. One issue is the hardcoded countability in the definition of the tangent code.
There was a problem hiding this comment.
Note that I'd be very happy to postpone generalizing this lemma to a later PR; I think the generalization you helped with with that's already in this diff is enough to unlock a lot of basic deriv results.
|
This PR/issue depends on:
|
Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
| variable [NormedAddCommGroup G] [NormedSpace ℝ G] | ||
| variable {x y : E} {s t : Set E} | ||
| /-- The tangent cone at a non-isolated point contains `0`. -/ | ||
| theorem zero_mem_tangentCone {s : Set E} {x : E} (hx : (𝓝[s \ {x}] x).NeBot) : |
There was a problem hiding this comment.
This is the other proof which I skipped generalizing.
There was a problem hiding this comment.
I haven't looked carefully, but again it doesn't seem obvious.
|
If you want to add it somewhere (maybe in an issue?), I would expect the following definition to at least eliminate the countability issues: open scoped Pointwise in
open Bornology in
def tangentConeAt' (s : Set E) (x : E) : Set E :=
let 𝓓 : Filter E := 𝓟 ((x + ·) ⁻¹' s)
let 𝓒 : Filter 𝕜 := Bornology.cobounded 𝕜
{ y : E | ClusterPt y (𝓒 • 𝓓) }The right question I think is: does this work nicely for polynormed spaces, that is spaces whose topology is defined by a family of seminorms (in the real or complex case this is the same as locally convex, but it also covers a bunch of important things about the p-adic case). The reason polynormed spaces are important is that in that case I expect most of the theory to extend, while for general TVSs I don't think we will be able to go that far. |
|
That definition looks very similar to the one that @urkud sent to me in a Zulip message last night! |
|
It's exactly the same definition. The only difference is that I inlined |
|
UPD: I'm thinking about some other definitions that may play better in case of a TVS without a first countable topology. I'm trying to find the weakest definition (with the largest answer) that still guarantees equality of derivatives. def tangentConeAt (s : Set E) (x : E) : Set E :=
{ y : E | MapClusterPt y ((⊤ : Filter 𝕜) ×ˢ 𝓝[insert x s] x) fun (c, d) ↦ c • (d - x) }I'm not 100% sure whether |
|
What's the current status of this PR @eric-wieser and @urkud ? It seems like it shouldn't be on the queue. |
|
I'm working on redefining the tangent cone when I have time. This one shouldn't be on the queue. |
|
This pull request has conflicts, please merge |
... and then adjust the
variables down the rest of the file to make use of the generality.There are two key lemmas that this does not generalize, which would probably unlock the rest of the file:
subset_tangentCone_prod_left(and_right)zero_mem_tangentCone