Tangent cone points as limits of sequences

This file contains a few ways to describe tangentConeAt as the set of limits of certain sequences.

In many cases, one can generalize results about the tangent cone by using mem_tangentConeAt_of_seq and exists_fun_of_mem_tangentConeAt instead of these lemmas.

theorem mem_tangentConeAt_iff_exists_seq {R : Type u_1} {E : Type u_2} [AddCommGroup E] [SMul R E] [TopologicalSpace E] [FirstCountableTopology E] {s : Set E} {x y : E} : y ∈ tangentConeAt R s x ↔ ∃ (c : ℕ → R) (d : ℕ → E), Filter.Tendsto d Filter.atTop (nhds 0) ∧ (∀ᶠ (n : ℕ) in Filter.atTop, x + d n ∈ s) ∧ Filter.Tendsto (fun (n : ℕ) => c n • d n) Filter.atTop (nhds y)

In a vector space with first countable topology, a vector y belongs to tangentConeAt 𝕜 s x if and only if there exist sequences c n and d n such that

• d n tends to zero as n → ∞;
• x + d n ∈ s for sufficiently large n;
• c n • d n tends to y as n → ∞.

See mem_tangentConeAt_of_seq and exists_fun_of_mem_tangentConeAt for versions of two implications of this theorem that don't assume first countable topology.

theorem tangentConeAt.lim_zero {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] {α : Type u_3} (l : Filter α) {c : α → 𝕜} {d : α → E} {y : E} (hc : Filter.Tendsto (fun (n : α) => ‖c n‖) l Filter.atTop) (hd : Filter.Tendsto (fun (n : α) => c n • d n) l (nhds y)) : Filter.Tendsto d l (nhds 0)

Auxiliary lemma ensuring that, under the assumptions from an old definition of the tangent cone, the sequence d tends to 0 at infinity.

theorem mem_tangentConeAt_of_pow_smul {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] {s : Set E} {x y : E} {r : 𝕜} (hr₀ : r ≠ 0) (hr : ‖r‖ < 1) (hs : ∀ᶠ (n : ℕ) in Filter.atTop, x + r ^ n • y ∈ s) : y ∈ tangentConeAt 𝕜 s x

theorem mem_tangentConeAt_iff_exists_seq_norm_tendsto_atTop {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x y : E} : y ∈ tangentConeAt 𝕜 s x ↔ ∃ (c : ℕ → 𝕜) (d : ℕ → E), Filter.Tendsto (fun (x : ℕ) => ‖c x‖) Filter.atTop Filter.atTop ∧ (∀ᶠ (n : ℕ) in Filter.atTop, x + d n ∈ s) ∧ Filter.Tendsto (fun (n : ℕ) => c n • d n) Filter.atTop (nhds y)

In a normed space over a nontrivially normed field, a point y belongs to the tangent cone of a set s at x iff there exists a sequence of scalars c n and a sequence of points d n such that

• ‖c n‖ → ∞ as n → ∞;
• x + d n ∈ s for sufficiently large n;
• c n • d n tends to y.

Before https://github.com/leanprover-community/mathlib4/pull/34127, the right-hand side of this equivalence was the definition of the tangent cone.

In most cases, exists_fun_of_mem_tangentConeAt and/or mem_tangentConeAt_of_seq can be used to generalize a proof using this lemma to topological vector spaces.