Basic properties of tangent cones and sets with unique differentiability property

In this file we prove basic lemmas about tangentConeAt, UniqueDiffWithinAt, and UniqueDiffOn.

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

@[simp]

theorem tangentConeAt_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} : tangentConeAt 𝕜 Set.univ x = Set.univ

@[deprecated tangentConeAt_univ (since := "2025-04-27")]

theorem tangentCone_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} : tangentConeAt 𝕜 Set.univ x = Set.univ

Alias of tangentConeAt_univ.

theorem tangentConeAt_mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s t : Set E} (h : s ⊆ t) : tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x

@[deprecated tangentConeAt_mono (since := "2025-04-27")]

theorem tangentCone_mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s t : Set E} (h : s ⊆ t) : tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x

Alias of tangentConeAt_mono.

theorem tangentConeAt_mono_field {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s : Set E} {𝕜' : Type u_5} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [Module 𝕜' E] [IsScalarTower 𝕜 𝕜' E] : tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜' s x

Given x ∈ s and a field extension 𝕜 ⊆ 𝕜', the tangent cone of s at x with respect to 𝕜 is contained in the tangent cone of s at x with respect to 𝕜'.

theorem tangentConeAt.lim_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {y : E} [ContinuousSMul 𝕜 E] {α : Type u_5} (l : Filter α) {c : α → 𝕜} {d : α → 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 defining the tangent cone, the sequence d tends to 0 at infinity.

theorem tangentConeAt_mono_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s t : Set E} [ContinuousSMul 𝕜 E] [ContinuousAdd E] (h : nhdsWithin x s ≤ nhdsWithin x t) : tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x

@[deprecated tangentConeAt_mono_nhds (since := "2025-04-27")]

theorem tangentCone_mono_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s t : Set E} [ContinuousSMul 𝕜 E] [ContinuousAdd E] (h : nhdsWithin x s ≤ nhdsWithin x t) : tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x

Alias of tangentConeAt_mono_nhds.

theorem tangentConeAt_congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s t : Set E} [ContinuousSMul 𝕜 E] [ContinuousAdd E] (h : nhdsWithin x s = nhdsWithin x t) : tangentConeAt 𝕜 s x = tangentConeAt 𝕜 t x

Tangent cone of s at x depends only on 𝓝[s] x.

@[deprecated tangentConeAt_congr (since := "2025-04-27")]

theorem tangentCone_congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s t : Set E} [ContinuousSMul 𝕜 E] [ContinuousAdd E] (h : nhdsWithin x s = nhdsWithin x t) : tangentConeAt 𝕜 s x = tangentConeAt 𝕜 t x

Alias of tangentConeAt_congr.

---

Tangent cone of s at x depends only on 𝓝[s] x.

theorem tangentConeAt_inter_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s t : Set E} [ContinuousSMul 𝕜 E] [ContinuousAdd E] (ht : t ∈ nhds x) : tangentConeAt 𝕜 (s ∩ t) x = tangentConeAt 𝕜 s x

Intersecting with a neighborhood of the point does not change the tangent cone.

@[deprecated tangentConeAt_inter_nhds (since := "2025-04-27")]

theorem tangentCone_inter_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s t : Set E} [ContinuousSMul 𝕜 E] [ContinuousAdd E] (ht : t ∈ nhds x) : tangentConeAt 𝕜 (s ∩ t) x = tangentConeAt 𝕜 s x

Alias of tangentConeAt_inter_nhds.

---

Intersecting with a neighborhood of the point does not change the tangent cone.

@[simp]

theorem tangentConeAt_closure {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} : tangentConeAt 𝕜 (closure s) x = tangentConeAt 𝕜 s x

theorem zero_mem_tangentCone {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x : E} (hx : x ∈ closure s) : 0 ∈ tangentConeAt 𝕜 s x

The tangent cone at a non-isolated point contains 0.

theorem tangentConeAt_subset_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} (hx : ¬AccPt x (Filter.principal s)) : tangentConeAt 𝕜 s x ⊆ 0

If x is not an accumulation point of s, then the tangent cone of s at x is a subset of {0}.

theorem UniqueDiffWithinAt.accPt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} [Nontrivial E] (h : UniqueDiffWithinAt 𝕜 s x) : AccPt x (Filter.principal s)

Properties of UniqueDiffWithinAt and UniqueDiffOn

This section is devoted to properties of the predicates UniqueDiffWithinAt and UniqueDiffOn.

theorem UniqueDiffOn.uniqueDiffWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {s : Set E} {x : E} (hs : UniqueDiffOn 𝕜 s) (h : x ∈ s) : UniqueDiffWithinAt 𝕜 s x

@[simp]

theorem uniqueDiffWithinAt_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} : UniqueDiffWithinAt 𝕜 Set.univ x

@[simp]

theorem uniqueDiffOn_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] : UniqueDiffOn 𝕜 Set.univ

theorem uniqueDiffOn_empty {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] : UniqueDiffOn 𝕜 ∅

theorem UniqueDiffWithinAt.congr_pt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x y : E} {s : Set E} (h : UniqueDiffWithinAt 𝕜 s x) (hy : x = y) : UniqueDiffWithinAt 𝕜 s y

theorem UniqueDiffWithinAt.mono_field {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s : Set E} {𝕜' : Type u_5} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [Module 𝕜' E] [IsScalarTower 𝕜 𝕜' E] (h₂s : UniqueDiffWithinAt 𝕜 s x) : UniqueDiffWithinAt 𝕜' s x

Assume that E is a normed vector space over normed fields 𝕜 ⊆ 𝕜' and that x ∈ s is a point of unique differentiability with respect to the set s and the smaller field 𝕜, then x is also a point of unique differentiability with respect to the set s and the larger field 𝕜'.

theorem UniqueDiffOn.mono_field {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {s : Set E} {𝕜' : Type u_5} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [Module 𝕜' E] [IsScalarTower 𝕜 𝕜' E] (h₂s : UniqueDiffOn 𝕜 s) : UniqueDiffOn 𝕜' s

Assume that E is a normed vector space over normed fields 𝕜 ⊆ 𝕜' and all points of s are points of unique differentiability with respect to the smaller field 𝕜, then they are also points of unique differentiability with respect to the larger field 𝕜.

theorem UniqueDiffWithinAt.mono_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s t : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] (h : UniqueDiffWithinAt 𝕜 s x) (st : nhdsWithin x s ≤ nhdsWithin x t) : UniqueDiffWithinAt 𝕜 t x

theorem UniqueDiffWithinAt.mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s t : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] (h : UniqueDiffWithinAt 𝕜 s x) (st : s ⊆ t) : UniqueDiffWithinAt 𝕜 t x

theorem uniqueDiffWithinAt_congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s t : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] (st : nhdsWithin x s = nhdsWithin x t) : UniqueDiffWithinAt 𝕜 s x ↔ UniqueDiffWithinAt 𝕜 t x

theorem uniqueDiffWithinAt_inter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s t : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] (ht : t ∈ nhds x) : UniqueDiffWithinAt 𝕜 (s ∩ t) x ↔ UniqueDiffWithinAt 𝕜 s x

theorem UniqueDiffWithinAt.inter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s t : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] (hs : UniqueDiffWithinAt 𝕜 s x) (ht : t ∈ nhds x) : UniqueDiffWithinAt 𝕜 (s ∩ t) x

theorem uniqueDiffWithinAt_inter' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s t : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] (ht : t ∈ nhdsWithin x s) : UniqueDiffWithinAt 𝕜 (s ∩ t) x ↔ UniqueDiffWithinAt 𝕜 s x

theorem UniqueDiffWithinAt.inter' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s t : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] (hs : UniqueDiffWithinAt 𝕜 s x) (ht : t ∈ nhdsWithin x s) : UniqueDiffWithinAt 𝕜 (s ∩ t) x

theorem uniqueDiffWithinAt_of_mem_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] (h : s ∈ nhds x) : UniqueDiffWithinAt 𝕜 s x

theorem IsOpen.uniqueDiffWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] (hs : IsOpen s) (xs : x ∈ s) : UniqueDiffWithinAt 𝕜 s x

theorem UniqueDiffOn.inter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {s t : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] (hs : UniqueDiffOn 𝕜 s) (ht : IsOpen t) : UniqueDiffOn 𝕜 (s ∩ t)

theorem IsOpen.uniqueDiffOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {s : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] (hs : IsOpen s) : UniqueDiffOn 𝕜 s

@[simp]

theorem uniqueDiffWithinAt_closure {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} : UniqueDiffWithinAt 𝕜 (closure s) x ↔ UniqueDiffWithinAt 𝕜 s x

theorem UniqueDiffWithinAt.of_closure {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} : UniqueDiffWithinAt 𝕜 (closure s) x → UniqueDiffWithinAt 𝕜 s x

Alias of the forward direction of uniqueDiffWithinAt_closure.

theorem UniqueDiffWithinAt.closure {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} : UniqueDiffWithinAt 𝕜 s x → UniqueDiffWithinAt 𝕜 (closure s) x

Alias of the reverse direction of uniqueDiffWithinAt_closure.

theorem UniqueDiffWithinAt.mono_closure {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s t : Set E} (h : UniqueDiffWithinAt 𝕜 s x) (st : s ⊆ closure t) : UniqueDiffWithinAt 𝕜 t x