Mathlib.Analysis.Calculus.TangentCone

tangentConeAt definition

(s : Set E) (x : E) : Set E

Full source

/-- The set of all tangent directions to the set `s` at the point `x`. -/
def tangentConeAt (s : Set E) (x : E) : Set E :=
  { y : E | ∃ (c : ℕ → 𝕜) (d : ℕ → E),
    (∀ᶠ n in atTop, x + d n ∈ s) ∧
    Tendsto (fun n => ‖c n‖) atTop atTop ∧
    Tendsto (fun n => c n • d n) atTop (𝓝 y) }

Tangent cone to a set at a point

Informal description

The tangent cone to a set $ s $ at a point $ x $ in a vector space $ E $ over a field $ \mathbb{K} $ is the set of all vectors $ y \in E $ for which there exist sequences $ (c_n) $ in $ \mathbb{K} $ and $ (d_n) $ in $ E $ such that: 1. For all sufficiently large $ n $, the point $ x + d_n $ belongs to $ s $, 2. The norm $ \|c_n\| $ tends to infinity as $ n $ tends to infinity, 3. The sequence $ c_n \cdot d_n $ converges to $ y $ as $ n $ tends to infinity.

UniqueDiffWithinAt structure

(s : Set E) (x : E)

Full source

/-- A property ensuring that the tangent cone to `s` at `x` spans a dense subset of the whole space.
The main role of this property is to ensure that the differential within `s` at `x` is unique,
hence this name. The uniqueness it asserts is proved in `UniqueDiffWithinAt.eq` in
`Mathlib.Analysis.Calculus.FDeriv.Basic`.
To avoid pathologies in dimension 0, we also require that `x` belongs to the closure of `s` (which
is automatic when `E` is not `0`-dimensional). -/
@[mk_iff]
structure UniqueDiffWithinAt (s : Set E) (x : E) : Prop where
  dense_tangentConeAt : Dense (Submodule.span 𝕜 (tangentConeAt 𝕜 s x) : Set E)
  mem_closure : x ∈ closure s

Uniqueness of derivative within a set at a point

Informal description

A property of a set $ s $ at a point $ x $ in a topological vector space $ E $ over a field $ \mathbb{K} $, ensuring that the tangent cone to $ s $ at $ x $ spans a dense subspace of $ E $. This guarantees the uniqueness of the derivative of functions defined on $ s $ at $ x $. Additionally, to avoid pathological cases in zero-dimensional spaces, $ x $ is required to be in the closure of $ s $.

UniqueDiffOn definition

(s : Set E) : Prop

Full source

/-- A property ensuring that the tangent cone to `s` at any of its points spans a dense subset of
the whole space. The main role of this property is to ensure that the differential along `s` is
unique, hence this name. The uniqueness it asserts is proved in `UniqueDiffOn.eq` in
`Mathlib.Analysis.Calculus.FDeriv.Basic`. -/
def UniqueDiffOn (s : Set E) : Prop :=
  ∀ x ∈ s, UniqueDiffWithinAt 𝕜 s x

Uniqueness of derivative on a set

Informal description

A property of a set $ s $ in a topological vector space $ E $ over a field $ \mathbb{K} $, ensuring that at every point $ x $ in $ s $, the tangent cone to $ s $ at $ x $ spans a dense subspace of $ E $. This guarantees the uniqueness of the derivative of functions defined on $ s $ at every point in $ s $.

mem_tangentConeAt_of_pow_smul theorem

 {r : 𝕜} (hr₀ : r ≠ 0) (hr : ‖r‖ < 1) (hs : ∀ᶠ n : ℕ in atTop, x + r ^ n • y ∈ s) : y ∈ tangentConeAt 𝕜 s x

Full source

theorem mem_tangentConeAt_of_pow_smul {r : 𝕜} (hr₀ : r ≠ 0) (hr : ‖r‖ < 1)
    (hs : ∀ᶠ n : ℕ in atTop, x + r ^ n • y ∈ s) : y ∈ tangentConeAt 𝕜 s x := by
  refine ⟨fun n ↦ (r ^ n)⁻¹, fun n ↦ r ^ n • y, hs, ?_, ?_⟩
  · simp only [norm_inv, norm_pow, ← inv_pow]
    exact tendsto_pow_atTop_atTop_of_one_lt <| (one_lt_inv₀ (norm_pos_iff.2 hr₀)).2 hr
  · simp only [inv_smul_smul₀ (pow_ne_zero _ hr₀), tendsto_const_nhds]

Characterization of Tangent Cone via Power Scaling: $y \in \text{tangentConeAt}_{\mathbb{K}} s x$ under power scaling condition

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a topological vector space over $\mathbb{K}$, $s \subseteq E$, and $x \in E$. For any $r \in \mathbb{K}$ with $r \neq 0$ and $\|r\| < 1$, if there exists a sequence of natural numbers $n \to \infty$ such that $x + r^n \cdot y \in s$ for all sufficiently large $n$, then $y$ belongs to the tangent cone of $s$ at $x$.

tangentConeAt_univ theorem

: tangentConeAt 𝕜 univ x = univ

Full source

@[simp]
theorem tangentConeAt_univ : tangentConeAt 𝕜 univ x = univ :=
  let ⟨_r, hr₀, hr⟩ := exists_norm_lt_one 𝕜
  eq_univ_of_forall fun _ ↦ mem_tangentConeAt_of_pow_smul (norm_pos_iff.1 hr₀) hr <|
    Eventually.of_forall fun _ ↦ mem_univ _

Tangent Cone of Universal Set Equals Whole Space

Informal description

For any nontrivially normed field $\mathbb{K}$, topological vector space $E$ over $\mathbb{K}$, and point $x \in E$, the tangent cone to the universal set $\text{univ} = E$ at $x$ is equal to $E$ itself. In other words, $\text{tangentConeAt}_{\mathbb{K}} E x = E$.

tangentConeAt_mono theorem

(h : s ⊆ t) : tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x

Full source

@[gcongr]
theorem tangentConeAt_mono (h : s ⊆ t) : tangentConeAttangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x := by
  rintro y ⟨c, d, ds, ctop, clim⟩
  exact ⟨c, d, mem_of_superset ds fun n hn => h hn, ctop, clim⟩

Monotonicity of Tangent Cone with Respect to Set Inclusion

Informal description

For any subsets $s$ and $t$ of a vector space $E$ over a field $\mathbb{K}$ with $s \subseteq t$, the tangent cone to $s$ at a point $x \in E$ is contained in the tangent cone to $t$ at $x$. In other words, if $y \in \text{tangentConeAt}_{\mathbb{K}} s x$, then $y \in \text{tangentConeAt}_{\mathbb{K}} t x$.

tangentConeAt_closure theorem

: tangentConeAt 𝕜 (closure s) x = tangentConeAt 𝕜 s x

Full source

@[simp]
theorem tangentConeAt_closure : tangentConeAt 𝕜 (closure s) x = tangentConeAt 𝕜 s x := by
  refine Subset.antisymm ?_ (tangentConeAt_mono subset_closure)
  rintro y ⟨c, d, ds, ctop, clim⟩
  obtain ⟨u, -, u_pos, u_lim⟩ :
      ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 (0 : ℝ)) :=
    exists_seq_strictAnti_tendsto (0 : ℝ)
  have : ∀ᶠ n in atTop, ∃ d', x + d' ∈ s ∧ dist (c n • d n) (c n • d') < u n := by
    filter_upwards [ctop.eventually_gt_atTop 0, ds] with n hn hns
    rcases Metric.mem_closure_iff.mp hns (u n / ‖c n‖) (div_pos (u_pos n) hn) with ⟨y, hys, hy⟩
    refine ⟨y - x, by simpa, ?_⟩
    rwa [dist_smul₀, ← dist_add_left x, add_sub_cancel, ← lt_div_iff₀' hn]
  simp only [Filter.skolem, eventually_and] at this
  rcases this with ⟨d', hd's, hd'⟩
  exact ⟨c, d', hd's, ctop, clim.congr_dist
    (squeeze_zero' (.of_forall fun _ ↦ dist_nonneg) (hd'.mono fun _ ↦ le_of_lt) u_lim)⟩

Tangent Cone at Closure Equals Tangent Cone at Original Set

Informal description

For any subset $s$ of a vector space $E$ over a field $\mathbb{K}$ and any point $x \in E$, the tangent cone to the closure of $s$ at $x$ is equal to the tangent cone to $s$ at $x$. In other words, \[ \text{tangentConeAt}_{\mathbb{K}} (\overline{s}) x = \text{tangentConeAt}_{\mathbb{K}} s x. \]

tangentConeAt.lim_zero theorem

 {α : Type*} (l : Filter α) {c : α → 𝕜} {d : α → E} (hc : Tendsto (fun n => ‖c n‖) l atTop)
  (hd : Tendsto (fun n => c n • d n) l (𝓝 y)) : Tendsto d l (𝓝 0)

Full source

/-- Auxiliary lemma ensuring that, under the assumptions defining the tangent cone,
the sequence `d` tends to 0 at infinity. -/
theorem tangentConeAt.lim_zero {α : Type*} (l : Filter α) {c : α → 𝕜} {d : α → E}
    (hc : Tendsto (fun n => ‖c n‖) l atTop) (hd : Tendsto (fun n => c n • d n) l (𝓝 y)) :
    Tendsto d l (𝓝 0) := by
  have A : Tendsto (fun n => ‖c n‖‖c n‖⁻¹) l (𝓝 0) := tendsto_inv_atTop_zero.comp hc
  have B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖) := (continuous_norm.tendsto _).comp hd
  have C : Tendsto (fun n => ‖c n‖‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 (0 * ‖y‖)) := A.mul B
  rw [zero_mul] at C
  have : ∀ᶠ n in l, ‖c n‖⁻¹ * ‖c n • d n‖ = ‖d n‖ := by
    refine (eventually_ne_of_tendsto_norm_atTop hc 0).mono fun n hn => ?_
    rw [norm_smul, ← mul_assoc, inv_mul_cancel₀, one_mul]
    rwa [Ne, norm_eq_zero]
  have D : Tendsto (fun n => ‖d n‖) l (𝓝 0) := Tendsto.congr' this C
  rw [tendsto_zero_iff_norm_tendsto_zero]
  exact D

Convergence to Zero in Tangent Cone Construction

Informal description

Let $\alpha$ be a type, $l$ a filter on $\alpha$, and consider sequences $c : \alpha \to \mathbb{K}$ and $d : \alpha \to E$ where $\mathbb{K}$ is a normed field and $E$ is a normed space over $\mathbb{K}$. If the sequence $\|c_n\|$ tends to infinity under $l$ and the sequence $c_n \cdot d_n$ tends to $y$ under $l$, then the sequence $d_n$ tends to $0$ under $l$.

tangentConeAt_mono_nhds theorem

(h : 𝓝[s] x ≤ 𝓝[t] x) : tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x

Full source

theorem tangentConeAt_mono_nhds (h : 𝓝[s] x ≤ 𝓝[t] x) :
    tangentConeAttangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x := by
  rintro y ⟨c, d, ds, ctop, clim⟩
  refine ⟨c, d, ?_, ctop, clim⟩
  suffices Tendsto (fun n => x + d n) atTop (𝓝[t] x) from
    tendsto_principal.1 (tendsto_inf.1 this).2
  refine (tendsto_inf.2 ⟨?_, tendsto_principal.2 ds⟩).mono_right h
  simpa only [add_zero] using tendsto_const_nhds.add (tangentConeAt.lim_zero atTop ctop clim)

Monotonicity of Tangent Cone with Respect to Neighborhood Filter Inclusion

Informal description

Let $E$ be a normed space over a field $\mathbb{K}$, and let $s$ and $t$ be subsets of $E$ containing a point $x$. If the neighborhood filter of $x$ within $s$ is finer than the neighborhood filter of $x$ within $t$ (i.e., $\mathcal{N}_s(x) \leq \mathcal{N}_t(x)$), then the tangent cone to $s$ at $x$ is contained in the tangent cone to $t$ at $x$. In other words, \[ \text{tangentConeAt}_{\mathbb{K}} s x \subseteq \text{tangentConeAt}_{\mathbb{K}} t x. \]

tangentConeAt_congr theorem

(h : 𝓝[s] x = 𝓝[t] x) : tangentConeAt 𝕜 s x = tangentConeAt 𝕜 t x

Full source

/-- Tangent cone of `s` at `x` depends only on `𝓝[s] x`. -/
theorem tangentConeAt_congr (h : 𝓝[s] x = 𝓝[t] x) : tangentConeAt 𝕜 s x = tangentConeAt 𝕜 t x :=
  Subset.antisymm (tangentConeAt_mono_nhds h.le) (tangentConeAt_mono_nhds h.ge)

Equality of Tangent Cones for Sets with Equal Neighborhood Filters

Informal description

Let $E$ be a normed space over a field $\mathbb{K}$, and let $s$ and $t$ be subsets of $E$ containing a point $x$. If the neighborhood filters of $x$ within $s$ and $t$ are equal (i.e., $\mathcal{N}_s(x) = \mathcal{N}_t(x)$), then the tangent cones to $s$ and $t$ at $x$ are equal. In other words, \[ \text{tangentConeAt}_{\mathbb{K}} s x = \text{tangentConeAt}_{\mathbb{K}} t x. \]

tangentConeAt_inter_nhds theorem

(ht : t ∈ 𝓝 x) : tangentConeAt 𝕜 (s ∩ t) x = tangentConeAt 𝕜 s x

Full source

/-- Intersecting with a neighborhood of the point does not change the tangent cone. -/
theorem tangentConeAt_inter_nhds (ht : t ∈ 𝓝 x) : tangentConeAt 𝕜 (s ∩ t) x = tangentConeAt 𝕜 s x :=
  tangentConeAt_congr (nhdsWithin_restrict' _ ht).symm

Tangent Cone at Intersection with Neighborhood Equals Original Tangent Cone

Informal description

Let $E$ be a normed space over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ a subset, and $x \in E$ a point. If $t$ is a neighborhood of $x$ (i.e., $t \in \mathcal{N}(x)$), then the tangent cone to $s \cap t$ at $x$ is equal to the tangent cone to $s$ at $x$. In other words, \[ \text{tangentConeAt}_{\mathbb{K}} (s \cap t) x = \text{tangentConeAt}_{\mathbb{K}} s x. \]

subset_tangentConeAt_prod_left theorem

 {t : Set F} {y : F} (ht : y ∈ closure t) : LinearMap.inl 𝕜 E F '' tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y)

Full source

/-- The tangent cone of a product contains the tangent cone of its left factor. -/
theorem subset_tangentConeAt_prod_left {t : Set F} {y : F} (ht : y ∈ closure t) :
    LinearMap.inlLinearMap.inl 𝕜 E F '' tangentConeAt 𝕜 s xLinearMap.inl 𝕜 E F '' tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y) := by
  rintro _ ⟨v, ⟨c, d, hd, hc, hy⟩, rfl⟩
  have : ∀ n, ∃ d', y + d' ∈ t ∧ ‖c n • d'‖ < ((1 : ℝ) / 2) ^ n := by
    intro n
    rcases mem_closure_iff_nhds.1 ht _
        (eventually_nhds_norm_smul_sub_lt (c n) y (pow_pos one_half_pos n)) with
      ⟨z, hz, hzt⟩
    exact ⟨z - y, by simpa using hzt, by simpa using hz⟩
  choose d' hd' using this
  refine ⟨c, fun n => (d n, d' n), ?_, hc, ?_⟩
  · show ∀ᶠ n in atTop, (x, y) + (d n, d' n) ∈ s ×ˢ t
    filter_upwards [hd] with n hn
    simp [hn, (hd' n).1]
  · apply Tendsto.prodMk_nhds hy _
    refine squeeze_zero_norm (fun n => (hd' n).2.le) ?_
    exact tendsto_pow_atTop_nhds_zero_of_lt_one one_half_pos.le one_half_lt_one

Inclusion of Left Tangent Cone in Product Tangent Cone

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, $s \subseteq E$ a subset, $x \in E$ a point, $t \subseteq F$ a subset, and $y \in \overline{t}$ a point in the closure of $t$. Then the image of the tangent cone $\text{tangentConeAt}_{\mathbb{K}}(s, x)$ under the left injection linear map $\text{inl}_{\mathbb{K},E,F} : E \to E \times F$ is contained in the tangent cone at $(x,y)$ of the product set $s \times t$, i.e., \[ \text{inl}_{\mathbb{K},E,F}(\text{tangentConeAt}_{\mathbb{K}}(s, x)) \subseteq \text{tangentConeAt}_{\mathbb{K}}(s \times t, (x,y)). \]

subset_tangentConeAt_prod_right theorem

 {t : Set F} {y : F} (hs : x ∈ closure s) : LinearMap.inr 𝕜 E F '' tangentConeAt 𝕜 t y ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y)

Full source

/-- The tangent cone of a product contains the tangent cone of its right factor. -/
theorem subset_tangentConeAt_prod_right {t : Set F} {y : F} (hs : x ∈ closure s) :
    LinearMap.inrLinearMap.inr 𝕜 E F '' tangentConeAt 𝕜 t yLinearMap.inr 𝕜 E F '' tangentConeAt 𝕜 t y ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y) := by
  rintro _ ⟨w, ⟨c, d, hd, hc, hy⟩, rfl⟩
  have : ∀ n, ∃ d', x + d' ∈ s ∧ ‖c n • d'‖ < ((1 : ℝ) / 2) ^ n := by
    intro n
    rcases mem_closure_iff_nhds.1 hs _
        (eventually_nhds_norm_smul_sub_lt (c n) x (pow_pos one_half_pos n)) with
      ⟨z, hz, hzs⟩
    exact ⟨z - x, by simpa using hzs, by simpa using hz⟩
  choose d' hd' using this
  refine ⟨c, fun n => (d' n, d n), ?_, hc, ?_⟩
  · show ∀ᶠ n in atTop, (x, y) + (d' n, d n) ∈ s ×ˢ t
    filter_upwards [hd] with n hn
    simp [hn, (hd' n).1]
  · apply Tendsto.prodMk_nhds _ hy
    refine squeeze_zero_norm (fun n => (hd' n).2.le) ?_
    exact tendsto_pow_atTop_nhds_zero_of_lt_one one_half_pos.le one_half_lt_one

Inclusion of Right Tangent Cone in Product Tangent Cone

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, $s \subseteq E$ and $t \subseteq F$ be subsets, and $x \in \overline{s}$, $y \in F$. Then the image of the tangent cone to $t$ at $y$ under the right injection linear map $\text{inr} : F \to E \times F$ is contained in the tangent cone to the product set $s \times t$ at the point $(x, y)$. In other words, if $v$ is a tangent vector to $t$ at $y$, then $(0, v)$ is a tangent vector to $s \times t$ at $(x, y)$.

mapsTo_tangentConeAt_pi theorem

 {ι : Type*} [DecidableEq ι] {E : ι → Type*} [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)]
  {s : ∀ i, Set (E i)} {x : ∀ i, E i} {i : ι} (hi : ∀ j ≠ i, x j ∈ closure (s j)) :
  MapsTo (LinearMap.single 𝕜 E i) (tangentConeAt 𝕜 (s i) (x i)) (tangentConeAt 𝕜 (Set.pi univ s) x)

Full source

/-- The tangent cone of a product contains the tangent cone of each factor. -/
theorem mapsTo_tangentConeAt_pi {ι : Type*} [DecidableEq ι] {E : ι → Type*}
    [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)] {s : ∀ i, Set (E i)} {x : ∀ i, E i}
    {i : ι} (hi : ∀ j ≠ i, x j ∈ closure (s j)) :
    MapsTo (LinearMap.single 𝕜 E i) (tangentConeAt 𝕜 (s i) (x i))
      (tangentConeAt 𝕜 (Set.pi univ s) x) := by
  rintro w ⟨c, d, hd, hc, hy⟩
  have : ∀ n, ∀ j ≠ i, ∃ d', x j + d' ∈ s j ∧ ‖c n • d'‖ < (1 / 2 : ℝ) ^ n := fun n j hj ↦ by
    rcases mem_closure_iff_nhds.1 (hi j hj) _
        (eventually_nhds_norm_smul_sub_lt (c n) (x j) (pow_pos one_half_pos n)) with
      ⟨z, hz, hzs⟩
    exact ⟨z - x j, by simpa using hzs, by simpa using hz⟩
  choose! d' hd's hcd' using this
  refine ⟨c, fun n => Function.update (d' n) i (d n), hd.mono fun n hn j _ => ?_, hc,
      tendsto_pi_nhds.2 fun j => ?_⟩
  · rcases em (j = i) with (rfl | hj) <;> simp [*]
  · rcases em (j = i) with (rfl | hj)
    · simp [hy]
    · suffices Tendsto (fun n => c n • d' n j) atTop (𝓝 0) by simpa [hj]
      refine squeeze_zero_norm (fun n => (hcd' n j hj).le) ?_
      exact tendsto_pow_atTop_nhds_zero_of_lt_one one_half_pos.le one_half_lt_one

Inclusion of Tangent Cone under Componentwise Embedding in Product Space

Informal description

Let $\{E_i\}_{i \in \iota}$ be a family of normed additive commutative groups over a nontrivially normed field $\mathbb{K}$, each equipped with a normed space structure. For each $i \in \iota$, let $s_i \subseteq E_i$ be a subset and $x_i \in E_i$ a point such that for all $j \neq i$, the point $x_j$ lies in the closure of $s_j$. Then, the linear map $\text{single}_i : E_i \to \prod_{j \in \iota} E_j$ (which embeds $E_i$ into the product space by placing zero in all other components) maps the tangent cone of $s_i$ at $x_i$ into the tangent cone of the product set $\prod_{j \in \iota} s_j$ at the point $x = (x_j)_{j \in \iota}$.

mem_tangentConeAt_of_openSegment_subset theorem

{s : Set G} {x y : G} (h : openSegment ℝ x y ⊆ s) : y - x ∈ tangentConeAt ℝ s x

Full source

/-- If a subset of a real vector space contains an open segment, then the direction of this
segment belongs to the tangent cone at its endpoints. -/
theorem mem_tangentConeAt_of_openSegment_subset {s : Set G} {x y : G} (h : openSegmentopenSegment ℝ x y ⊆ s) :
    y - x ∈ tangentConeAt ℝ s x := by
  refine mem_tangentConeAt_of_pow_smul one_half_pos.ne' (by norm_num) ?_
  refine (eventually_ne_atTop 0).mono fun n hn ↦ (h ?_)
  rw [openSegment_eq_image]
  refine ⟨(1 / 2) ^ n, ⟨?_, ?_⟩, ?_⟩
  · exact pow_pos one_half_pos _
  · exact pow_lt_one₀ one_half_pos.le one_half_lt_one hn
  · simp only [sub_smul, one_smul, smul_sub]; abel

Tangent Cone Contains Direction of Open Segment

Informal description

Let $G$ be a real vector space and $s \subseteq G$ a subset. For any two points $x, y \in G$, if the open segment between $x$ and $y$ is contained in $s$, then the difference vector $y - x$ belongs to the tangent cone of $s$ at $x$.

mem_tangentConeAt_of_segment_subset theorem

{s : Set G} {x y : G} (h : segment ℝ x y ⊆ s) : y - x ∈ tangentConeAt ℝ s x

Full source

/-- If a subset of a real vector space contains a segment, then the direction of this
segment belongs to the tangent cone at its endpoints. -/
theorem mem_tangentConeAt_of_segment_subset {s : Set G} {x y : G} (h : segmentsegment ℝ x y ⊆ s) :
    y - x ∈ tangentConeAt ℝ s x :=
  mem_tangentConeAt_of_openSegment_subset ((openSegment_subset_segment ℝ x y).trans h)

Tangent Cone Contains Direction of Closed Segment

Informal description

Let $G$ be a real vector space and $s \subseteq G$ a subset. For any two points $x, y \in G$, if the closed segment between $x$ and $y$ is contained in $s$, then the difference vector $y - x$ belongs to the tangent cone of $s$ at $x$.

zero_mem_tangentCone theorem

{s : Set E} {x : E} (hx : x ∈ closure s) : 0 ∈ tangentConeAt 𝕜 s x

Full source

/-- The tangent cone at a non-isolated point contains `0`. -/
theorem zero_mem_tangentCone {s : Set E} {x : E} (hx : x ∈ closure s) :
    0 ∈ tangentConeAt 𝕜 s x := by
  /- Take a sequence `d n` tending to `0` such that `x + d n ∈ s`. Taking `c n` of the order
  of `1 / (d n) ^ (1/2)`, then `c n` tends to infinity, but `c n • d n` tends to `0`. By definition,
  this shows that `0` belongs to the tangent cone. -/
  obtain ⟨u, -, hu, u_lim⟩ :
      ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n ∧ u n < 1) ∧ Tendsto u atTop (𝓝 (0 : ℝ)) :=
    exists_seq_strictAnti_tendsto' one_pos
  choose u_pos u_lt_one using hu
  choose v hvs hvu using fun n ↦ Metric.mem_closure_iff.mp hx _ (mul_pos (u_pos n) (u_pos n))
  let d n := v n - x
  let ⟨r, hr⟩ := exists_one_lt_norm 𝕜
  have A n := exists_nat_pow_near (one_le_inv_iff₀.mpr ⟨u_pos n, (u_lt_one n).le⟩) hr
  choose m hm_le hlt_m using A
  set c := fun n ↦ r ^ (m n + 1)
  have c_lim : Tendsto (fun n ↦ ‖c n‖) atTop atTop := by
    simp only [c, norm_pow]
    refine tendsto_atTop_mono (fun n ↦ (hlt_m n).le) <| .inv_tendsto_nhdsGT_zero ?_
    exact tendsto_nhdsWithin_iff.mpr ⟨u_lim, .of_forall u_pos⟩
  refine ⟨c, d, .of_forall <| by simpa [d], c_lim, ?_⟩
  have Hle n : ‖c n • d n‖ ≤ ‖r‖ * u n := by
    specialize u_pos n
    calc
      ‖c n • d n‖ ≤ (u n)⁻¹ * ‖r‖ * (u n * u n) := by
        simp only [c, norm_smul, norm_pow, pow_succ, norm_mul, d, ← dist_eq_norm']
        gcongr
        exacts [hm_le n, (hvu n).le]
      _ = ‖r‖ * u n := by field_simp [mul_assoc]
  refine squeeze_zero_norm Hle ?_
  simpa using tendsto_const_nhds.mul u_lim

Zero Vector in Tangent Cone at Points of Closure

Informal description

For any subset $s$ of a vector space $E$ over a field $\mathbb{K}$ and any point $x$ in the closure of $s$, the zero vector $0$ belongs to the tangent cone of $s$ at $x$.

tangentConeAt_subset_zero theorem

(hx : ¬AccPt x (𝓟 s)) : tangentConeAt 𝕜 s x ⊆ 0

Full source

/-- If `x` is not an accumulation point of `s, then the tangent cone of `s` at `x`
is a subset of `{0}`. -/
theorem tangentConeAt_subset_zero (hx : ¬AccPt x (𝓟 s)) : tangentConeAttangentConeAt 𝕜 s x ⊆ 0 := by
  rintro y ⟨c, d, hds, hc, hcd⟩
  suffices ∀ᶠ n in .atTop, d n = 0 from
    tendsto_nhds_unique hcd <| tendsto_const_nhds.congr' <| this.mono fun n hn ↦ by simp [hn]
  simp only [accPt_iff_frequently, not_frequently, not_and', ne_eq, not_not] at hx
  have : Tendsto (x + d ·) atTop (𝓝 x) := by
    simpa using tendsto_const_nhds.add (tangentConeAt.lim_zero _ hc hcd)
  filter_upwards [this.eventually hx, hds] with n h₁ h₂
  simpa using h₁ h₂

Tangent cone at non-accumulation point is trivial

Informal description

Let $E$ be a normed space over a field $\mathbb{K}$, $s \subseteq E$ a subset, and $x \in E$. If $x$ is not an accumulation point of $s$ (i.e., $\neg \text{AccPt}(x, \mathcal{P}(s))$), then the tangent cone to $s$ at $x$ is contained in the zero subspace, i.e., $\text{tangentConeAt}_{\mathbb{K}}(s, x) \subseteq \{0\}$.

UniqueDiffWithinAt.accPt theorem

[Nontrivial E] (h : UniqueDiffWithinAt 𝕜 s x) : AccPt x (𝓟 s)

Full source

theorem UniqueDiffWithinAt.accPt [Nontrivial E] (h : UniqueDiffWithinAt 𝕜 s x) : AccPt x (𝓟 s) := by
  by_contra! h'
  have : Dense (Submodule.span 𝕜 (0 : Set E) : Set E) :=
    h.1.mono <| by gcongr; exact tangentConeAt_subset_zero h'
  simp [dense_iff_closure_eq] at this

Accumulation point condition for uniqueness of derivatives

Informal description

Let $E$ be a nontrivial normed space over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset with $x \in E$. If the tangent cone to $s$ at $x$ spans a dense subspace of $E$ (i.e., $\text{UniqueDiffWithinAt}_{\mathbb{K}}(s, x)$ holds), then $x$ is an accumulation point of $s$.

tangentConeAt_nonempty_of_properSpace theorem

[ProperSpace E] {s : Set E} {x : E} (hx : AccPt x (𝓟 s)) : (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty

Full source

/-- In a proper space, the tangent cone at a non-isolated point is nontrivial. -/
theorem tangentConeAt_nonempty_of_properSpace [ProperSpace E]
    {s : Set E} {x : E} (hx : AccPt x (𝓟 s)) :
    (tangentConeAttangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty := by
  /- Take a sequence `d n` tending to `0` such that `x + d n ∈ s`. Taking `c n` of the order
  of `1 / d n`. Then `c n • d n` belongs to a fixed annulus. By compactness, one can extract
  a subsequence converging to a limit `l`. Then `l` is nonzero, and by definition it belongs to
  the tangent cone. -/
  obtain ⟨u, -, u_pos, u_lim⟩ :
      ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 (0 : ℝ)) :=
    exists_seq_strictAnti_tendsto (0 : ℝ)
  have A n : ∃ y ∈ closedBall x (u n) ∩ s, y ≠ x :=
    (accPt_iff_nhds).mp hx _ (closedBall_mem_nhds _ (u_pos n))
  choose v hv hvx using A
  choose hvu hvs using hv
  let d := fun n ↦ v n - x
  have M n : x + d n ∈ s \ {x} := by simp [d, hvs, hvx]
  let ⟨r, hr⟩ := exists_one_lt_norm 𝕜
  have W n := rescale_to_shell hr zero_lt_one (x := d n) (by simpa using (M n).2)
  choose c c_ne c_le le_c hc using W
  have c_lim : Tendsto (fun n ↦ ‖c n‖) atTop atTop := by
    suffices Tendsto (fun n ↦ ‖c n‖‖c n‖⁻¹‖c n‖⁻¹ ⁻¹ ) atTop atTop by simpa
    apply tendsto_inv_nhdsGT_zero.comp
    simp only [nhdsWithin, tendsto_inf, tendsto_principal, mem_Ioi, norm_pos_iff, ne_eq,
      eventually_atTop, ge_iff_le]
    have B (n : ℕ) : ‖c n‖‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * u n := by
      apply (hc n).trans
      gcongr
      simpa [d, dist_eq_norm] using hvu n
    refine ⟨?_, 0, fun n hn ↦ by simpa using c_ne n⟩
    apply squeeze_zero (fun n ↦ by positivity) B
    simpa using u_lim.const_mul _
  obtain ⟨l, l_mem, φ, φ_strict, hφ⟩ :
      ∃ l ∈ Metric.closedBall (0 : E) 1 \ Metric.ball (0 : E) (1 / ‖r‖),
      ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto ((fun n ↦ c n • d n) ∘ φ) atTop (𝓝 l) := by
    apply IsCompact.tendsto_subseq _ (fun n ↦ ?_)
    · exact (isCompact_closedBall 0 1).diff Metric.isOpen_ball
    simp only [mem_diff, Metric.mem_closedBall, dist_zero_right, (c_le n).le,
      Metric.mem_ball, not_lt, true_and, le_c n]
  refine ⟨l, ?_, ?_⟩; swap
  · simp only [mem_compl_iff, mem_singleton_iff]
    contrapose! l_mem
    simp only [one_div, l_mem, mem_diff, Metric.mem_closedBall, dist_self, zero_le_one,
      Metric.mem_ball, inv_pos, norm_pos_iff, ne_eq, not_not, true_and]
    contrapose! hr
    simp [hr]
  refine ⟨c ∘ φ, d ∘ φ, .of_forall fun n ↦ ?_, ?_, hφ⟩
  · simpa [d] using hvs (φ n)
  · exact c_lim.comp φ_strict.tendsto_atTop

Nonemptiness of Tangent Cone at Accumulation Points in Proper Spaces

Informal description

Let $E$ be a proper space (i.e., a metric space where all closed balls are compact) and $s \subseteq E$ a subset. For any point $x \in E$ that is an accumulation point of $s$, the tangent cone to $s$ at $x$ contains a nonzero vector. In other words, the intersection of the tangent cone $\text{tangentConeAt}_{\mathbb{K}}(s, x)$ with the complement of $\{0\}$ is nonempty.

tangentConeAt_eq_univ theorem

{s : Set 𝕜} {x : 𝕜} (hx : AccPt x (𝓟 s)) : tangentConeAt 𝕜 s x = univ

Full source

/-- The tangent cone at a non-isolated point in dimension 1 is the whole space. -/
theorem tangentConeAt_eq_univ {s : Set 𝕜} {x : 𝕜} (hx : AccPt x (𝓟 s)) :
    tangentConeAt 𝕜 s x = univ := by
  apply eq_univ_iff_forall.2 (fun y ↦ ?_)
  -- first deal with the case of `0`, which has to be handled separately.
  rcases eq_or_ne y 0 with rfl | hy
  · exact zero_mem_tangentCone (mem_closure_iff_clusterPt.mpr hx.clusterPt)
  /- Assume now `y` is a fixed nonzero scalar. Take a sequence `d n` tending to `0` such
  that `x + d n ∈ s`. Let `c n = y / d n`. Then `‖c n‖` tends to infinity, and `c n • d n`
  converges to `y` (as it is equal to `y`). By definition, this shows that `y` belongs to the
  tangent cone. -/
  obtain ⟨u, -, u_pos, u_lim⟩ :
      ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 (0 : ℝ)) :=
    exists_seq_strictAnti_tendsto (0 : ℝ)
  have A n : ∃ y ∈ closedBall x (u n) ∩ s, y ≠ x :=
    accPt_iff_nhds.mp hx _ (closedBall_mem_nhds _ (u_pos n))
  choose v hv hvx using A
  choose hvu hvs using hv
  let d := fun n ↦ v n - x
  have d_ne n : d n ≠ 0 := by simpa [d, sub_eq_zero] using hvx n
  refine ⟨fun n ↦ y * (d n)⁻¹, d, .of_forall ?_, ?_, ?_⟩
  · simpa [d] using hvs
  · simp only [norm_mul, norm_inv]
    apply (tendsto_const_mul_atTop_of_pos (by simpa using hy)).2
    apply tendsto_inv_nhdsGT_zero.comp
    simp only [nhdsWithin, tendsto_inf, tendsto_principal, mem_Ioi, norm_pos_iff, ne_eq,
      eventually_atTop, ge_iff_le]
    have B (n : ℕ) : ‖d n‖ ≤ u n := by simpa [dist_eq_norm] using hvu n
    refine ⟨?_, 0, fun n hn ↦ by simpa using d_ne n⟩
    exact squeeze_zero (fun n ↦ by positivity) B u_lim
  · convert tendsto_const_nhds (α := ℕ) (x := y) with n
    simp [mul_assoc, inv_mul_cancel₀ (d_ne n)]

Tangent cone at accumulation point in 1D is the whole space

Informal description

For any subset $s$ of a nontrivially normed field $\mathbb{K}$ and any point $x \in \mathbb{K}$ that is an accumulation point of $s$, the tangent cone to $s$ at $x$ is equal to the entire space $\mathbb{K}$.

UniqueDiffOn.uniqueDiffWithinAt theorem

{s : Set E} {x} (hs : UniqueDiffOn 𝕜 s) (h : x ∈ s) : UniqueDiffWithinAt 𝕜 s x

Full source

theorem UniqueDiffOn.uniqueDiffWithinAt {s : Set E} {x} (hs : UniqueDiffOn 𝕜 s) (h : x ∈ s) :
    UniqueDiffWithinAt 𝕜 s x :=
  hs x h

Uniqueness of Derivative on a Set Implies Uniqueness at Each Point

Informal description

For any set $s$ in a topological vector space $E$ over a nontrivially normed field $\mathbb{K}$, if $s$ has the property `UniqueDiffOn` (i.e., the tangent cone at every point of $s$ spans a dense subspace of $E$), then for any point $x \in s$, the set $s$ also has the property `UniqueDiffWithinAt` at $x$ (i.e., the tangent cone to $s$ at $x$ spans a dense subspace of $E$).

uniqueDiffWithinAt_univ theorem

: UniqueDiffWithinAt 𝕜 univ x

Full source

theorem uniqueDiffWithinAt_univ : UniqueDiffWithinAt 𝕜 univ x := by
  rw [uniqueDiffWithinAt_iff, tangentConeAt_univ]
  simp

Universal Set Has Unique Differentiability at Every Point

Informal description

For any nontrivially normed field $\mathbb{K}$ and any topological vector space $E$ over $\mathbb{K}$, the universal set $E$ satisfies the property of unique differentiability at every point $x \in E$. That is, the tangent cone to $E$ at $x$ spans a dense subspace of $E$, ensuring the uniqueness of derivatives of functions defined on $E$ at $x$.

uniqueDiffOn_univ theorem

: UniqueDiffOn 𝕜 (univ : Set E)

Full source

theorem uniqueDiffOn_univ : UniqueDiffOn 𝕜 (univ : Set E) :=
  fun _ _ => uniqueDiffWithinAt_univ

Universal Set Satisfies Unique Differentiability Property

Informal description

For any nontrivially normed field $\mathbb{K}$ and any topological vector space $E$ over $\mathbb{K}$, the universal set $\text{univ} = E$ satisfies the property of unique differentiability. That is, at every point $x \in E$, the tangent cone to $E$ at $x$ spans a dense subspace of $E$, ensuring the uniqueness of derivatives of functions defined on $E$.

uniqueDiffOn_empty theorem

: UniqueDiffOn 𝕜 (∅ : Set E)

Full source

theorem uniqueDiffOn_empty : UniqueDiffOn 𝕜 (∅ : Set E) :=
  fun _ hx => hx.elim

Empty Set Satisfies Unique Differentiability Property

Informal description

For any nontrivially normed field $\mathbb{K}$ and any topological vector space $E$ over $\mathbb{K}$, the empty set $\emptyset$ satisfies the property of unique differentiability on $E$. That is, the derivative of any function defined on $\emptyset$ is unique at every point in $\emptyset$.

UniqueDiffWithinAt.congr_pt theorem

(h : UniqueDiffWithinAt 𝕜 s x) (hy : x = y) : UniqueDiffWithinAt 𝕜 s y

Full source

theorem UniqueDiffWithinAt.congr_pt (h : UniqueDiffWithinAt 𝕜 s x) (hy : x = y) :
    UniqueDiffWithinAt 𝕜 s y := hy ▸ h

Preservation of Unique Differentiability Under Point Equality

Informal description

Let $E$ be a topological vector space over a nontrivially normed field $\mathbb{K}$, and let $s$ be a subset of $E$. If the property of unique differentiability holds within $s$ at a point $x \in E$, and $x = y$, then the property of unique differentiability also holds within $s$ at the point $y$.

uniqueDiffWithinAt_closure theorem

: UniqueDiffWithinAt 𝕜 (closure s) x ↔ UniqueDiffWithinAt 𝕜 s x

Full source

@[simp]
theorem uniqueDiffWithinAt_closure :
    UniqueDiffWithinAtUniqueDiffWithinAt 𝕜 (closure s) x ↔ UniqueDiffWithinAt 𝕜 s x := by
  simp [uniqueDiffWithinAt_iff]

Unique Differentiability at Closure Equals Unique Differentiability at Original Set

Informal description

For a subset $s$ of a topological vector space $E$ over a nontrivially normed field $\mathbb{K}$ and a point $x \in E$, the property of unique differentiability within $s$ at $x$ holds if and only if it holds within the closure of $s$ at $x$. In other words, \[ \text{UniqueDiffWithinAt}_{\mathbb{K}} (\overline{s}) x \leftrightarrow \text{UniqueDiffWithinAt}_{\mathbb{K}} s x. \]

UniqueDiffWithinAt.mono_nhds theorem

(h : UniqueDiffWithinAt 𝕜 s x) (st : 𝓝[s] x ≤ 𝓝[t] x) : UniqueDiffWithinAt 𝕜 t x

Full source

theorem UniqueDiffWithinAt.mono_nhds (h : UniqueDiffWithinAt 𝕜 s x) (st : 𝓝[s] x ≤ 𝓝[t] x) :
    UniqueDiffWithinAt 𝕜 t x := by
  simp only [uniqueDiffWithinAt_iff] at *
  rw [mem_closure_iff_nhdsWithin_neBot] at h ⊢
  exact ⟨h.1.mono <| Submodule.span_mono <| tangentConeAt_mono_nhds st, h.2.mono st⟩

Preservation of Unique Differentiability Under Neighborhood Filter Coarsening

Informal description

Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, and let $s, t$ be subsets of $E$ containing a point $x$. If the property of unique differentiability holds within $s$ at $x$, and the neighborhood filter of $x$ within $s$ is finer than the neighborhood filter of $x$ within $t$ (i.e., $\mathcal{N}_s(x) \leq \mathcal{N}_t(x)$), then the property of unique differentiability also holds within $t$ at $x$.

UniqueDiffWithinAt.mono theorem

(h : UniqueDiffWithinAt 𝕜 s x) (st : s ⊆ t) : UniqueDiffWithinAt 𝕜 t x

Full source

theorem UniqueDiffWithinAt.mono (h : UniqueDiffWithinAt 𝕜 s x) (st : s ⊆ t) :
    UniqueDiffWithinAt 𝕜 t x :=
  h.mono_nhds <| nhdsWithin_mono _ st

Unique Differentiability is Monotone with Respect to Subset Inclusion

Informal description

Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, and let $s, t$ be subsets of $E$ containing a point $x$. If the property of unique differentiability holds within $s$ at $x$, and $s$ is a subset of $t$, then the property of unique differentiability also holds within $t$ at $x$.

UniqueDiffWithinAt.mono_closure theorem

(h : UniqueDiffWithinAt 𝕜 s x) (st : s ⊆ closure t) : UniqueDiffWithinAt 𝕜 t x

Full source

theorem UniqueDiffWithinAt.mono_closure (h : UniqueDiffWithinAt 𝕜 s x) (st : s ⊆ closure t) :
    UniqueDiffWithinAt 𝕜 t x :=
  (h.mono st).of_closure

Preservation of Unique Differentiability Under Closure Inclusion

Informal description

Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, and let $s, t$ be subsets of $E$ containing a point $x$. If the property of unique differentiability holds within $s$ at $x$, and $s$ is a subset of the closure of $t$, then the property of unique differentiability also holds within $t$ at $x$.

uniqueDiffWithinAt_congr theorem

(st : 𝓝[s] x = 𝓝[t] x) : UniqueDiffWithinAt 𝕜 s x ↔ UniqueDiffWithinAt 𝕜 t x

Full source

theorem uniqueDiffWithinAt_congr (st : 𝓝[s] x = 𝓝[t] x) :
    UniqueDiffWithinAtUniqueDiffWithinAt 𝕜 s x ↔ UniqueDiffWithinAt 𝕜 t x :=
  ⟨fun h => h.mono_nhds <| le_of_eq st, fun h => h.mono_nhds <| le_of_eq st.symm⟩

Equivalence of Unique Differentiability Under Equal Neighborhood Filters

Informal description

Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, and let $s, t$ be subsets of $E$ containing a point $x$. If the neighborhood filters of $x$ within $s$ and $t$ are equal (i.e., $\mathcal{N}_s(x) = \mathcal{N}_t(x)$), then the property of unique differentiability holds within $s$ at $x$ if and only if it holds within $t$ at $x$.

uniqueDiffWithinAt_inter theorem

(ht : t ∈ 𝓝 x) : UniqueDiffWithinAt 𝕜 (s ∩ t) x ↔ UniqueDiffWithinAt 𝕜 s x

Full source

theorem uniqueDiffWithinAt_inter (ht : t ∈ 𝓝 x) :
    UniqueDiffWithinAtUniqueDiffWithinAt 𝕜 (s ∩ t) x ↔ UniqueDiffWithinAt 𝕜 s x :=
  uniqueDiffWithinAt_congr <| (nhdsWithin_restrict' _ ht).symm

Unique Differentiability at a Point is Preserved Under Intersection with Neighborhood

Informal description

Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, let $s$ be a subset of $E$, and let $x \in E$. For any subset $t \subseteq E$ that is a neighborhood of $x$, the property of unique differentiability holds within $s \cap t$ at $x$ if and only if it holds within $s$ at $x$.

UniqueDiffWithinAt.inter theorem

(hs : UniqueDiffWithinAt 𝕜 s x) (ht : t ∈ 𝓝 x) : UniqueDiffWithinAt 𝕜 (s ∩ t) x

Full source

theorem UniqueDiffWithinAt.inter (hs : UniqueDiffWithinAt 𝕜 s x) (ht : t ∈ 𝓝 x) :
    UniqueDiffWithinAt 𝕜 (s ∩ t) x :=
  (uniqueDiffWithinAt_inter ht).2 hs

Preservation of Unique Differentiability Under Intersection with Neighborhood

Informal description

Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, and let $s$ be a subset of $E$ such that the property of unique differentiability holds within $s$ at a point $x \in E$. If $t$ is a neighborhood of $x$ in $E$, then the property of unique differentiability also holds within the intersection $s \cap t$ at $x$.

uniqueDiffWithinAt_inter' theorem

(ht : t ∈ 𝓝[s] x) : UniqueDiffWithinAt 𝕜 (s ∩ t) x ↔ UniqueDiffWithinAt 𝕜 s x

Full source

theorem uniqueDiffWithinAt_inter' (ht : t ∈ 𝓝[s] x) :
    UniqueDiffWithinAtUniqueDiffWithinAt 𝕜 (s ∩ t) x ↔ UniqueDiffWithinAt 𝕜 s x :=
  uniqueDiffWithinAt_congr <| (nhdsWithin_restrict'' _ ht).symm

Equivalence of Unique Differentiability Under Neighborhood Intersection

Informal description

Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, and let $s, t$ be subsets of $E$ containing a point $x$. If $t$ is a neighborhood of $x$ within $s$ (i.e., $t \in \mathcal{N}_s(x)$), then the property of unique differentiability holds within the intersection $s \cap t$ at $x$ if and only if it holds within $s$ at $x$.

UniqueDiffWithinAt.inter' theorem

(hs : UniqueDiffWithinAt 𝕜 s x) (ht : t ∈ 𝓝[s] x) : UniqueDiffWithinAt 𝕜 (s ∩ t) x

Full source

theorem UniqueDiffWithinAt.inter' (hs : UniqueDiffWithinAt 𝕜 s x) (ht : t ∈ 𝓝[s] x) :
    UniqueDiffWithinAt 𝕜 (s ∩ t) x :=
  (uniqueDiffWithinAt_inter' ht).2 hs

Preservation of Unique Differentiability Under Intersection with Neighborhood within a Set

Informal description

Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, and let $s, t$ be subsets of $E$ containing a point $x$. If the property of unique differentiability holds within $s$ at $x$, and $t$ is a neighborhood of $x$ within $s$, then the property of unique differentiability also holds within the intersection $s \cap t$ at $x$.

uniqueDiffWithinAt_of_mem_nhds theorem

(h : s ∈ 𝓝 x) : UniqueDiffWithinAt 𝕜 s x

Full source

theorem uniqueDiffWithinAt_of_mem_nhds (h : s ∈ 𝓝 x) : UniqueDiffWithinAt 𝕜 s x := by
  simpa only [univ_inter] using uniqueDiffWithinAt_univ.inter h

Neighborhood Implies Unique Differentiability Within Set at Point

Informal description

Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, and let $s$ be a subset of $E$. If $s$ is a neighborhood of a point $x \in E$, then the property of unique differentiability holds within $s$ at $x$.

IsOpen.uniqueDiffWithinAt theorem

(hs : IsOpen s) (xs : x ∈ s) : UniqueDiffWithinAt 𝕜 s x

Full source

theorem IsOpen.uniqueDiffWithinAt (hs : IsOpen s) (xs : x ∈ s) : UniqueDiffWithinAt 𝕜 s x :=
  uniqueDiffWithinAt_of_mem_nhds (IsOpen.mem_nhds hs xs)

Open Sets Have Unique Differentiability at Interior Points

Informal description

Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be an open set. For any point $x \in s$, the property of unique differentiability holds within $s$ at $x$.

UniqueDiffOn.inter theorem

(hs : UniqueDiffOn 𝕜 s) (ht : IsOpen t) : UniqueDiffOn 𝕜 (s ∩ t)

Full source

theorem UniqueDiffOn.inter (hs : UniqueDiffOn 𝕜 s) (ht : IsOpen t) : UniqueDiffOn 𝕜 (s ∩ t) :=
  fun x hx => (hs x hx.1).inter (IsOpen.mem_nhds ht hx.2)

Preservation of Unique Differentiability Under Intersection with Open Set

Informal description

Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a set on which derivatives are unique (i.e., $s$ satisfies `UniqueDiffOn 𝕜 s`). If $t \subseteq E$ is an open set, then the intersection $s \cap t$ also satisfies `UniqueDiffOn 𝕜 (s \cap t)`, meaning derivatives are unique on $s \cap t$.

IsOpen.uniqueDiffOn theorem

(hs : IsOpen s) : UniqueDiffOn 𝕜 s

Full source

theorem IsOpen.uniqueDiffOn (hs : IsOpen s) : UniqueDiffOn 𝕜 s :=
  fun _ hx => IsOpen.uniqueDiffWithinAt hs hx

Open Sets Have Unique Differentiability Property

Informal description

Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$. If $s \subseteq E$ is an open set, then the property of unique differentiability holds on $s$, meaning that for every point $x \in s$, the tangent cone to $s$ at $x$ spans a dense subspace of $E$.

UniqueDiffWithinAt.prod theorem

 {t : Set F} {y : F} (hs : UniqueDiffWithinAt 𝕜 s x) (ht : UniqueDiffWithinAt 𝕜 t y) :
  UniqueDiffWithinAt 𝕜 (s ×ˢ t) (x, y)

Full source

/-- The product of two sets of unique differentiability at points `x` and `y` has unique
differentiability at `(x, y)`. -/
theorem UniqueDiffWithinAt.prod {t : Set F} {y : F} (hs : UniqueDiffWithinAt 𝕜 s x)
    (ht : UniqueDiffWithinAt 𝕜 t y) : UniqueDiffWithinAt 𝕜 (s ×ˢ t) (x, y) := by
  rw [uniqueDiffWithinAt_iff] at hs ht ⊢
  rw [closure_prod_eq]
  refine ⟨?_, hs.2, ht.2⟩
  have : _ ≤ Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y)) := Submodule.span_mono
    (union_subset (subset_tangentConeAt_prod_left ht.2) (subset_tangentConeAt_prod_right hs.2))
  rw [LinearMap.span_inl_union_inr, SetLike.le_def] at this
  exact (hs.1.prod ht.1).mono this

Unique Differentiability is Preserved Under Products

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, $s \subseteq E$ and $t \subseteq F$ be subsets, and $x \in E$, $y \in F$ be points. If $s$ has unique differentiability at $x$ and $t$ has unique differentiability at $y$, then the product set $s \times t$ has unique differentiability at the point $(x, y)$.

UniqueDiffWithinAt.univ_pi theorem

 (ι : Type*) [Finite ι] (E : ι → Type*) [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)] (s : ∀ i, Set (E i))
  (x : ∀ i, E i) (h : ∀ i, UniqueDiffWithinAt 𝕜 (s i) (x i)) : UniqueDiffWithinAt 𝕜 (Set.pi univ s) x

Full source

theorem UniqueDiffWithinAt.univ_pi (ι : Type*) [Finite ι] (E : ι → Type*)
    [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)] (s : ∀ i, Set (E i)) (x : ∀ i, E i)
    (h : ∀ i, UniqueDiffWithinAt 𝕜 (s i) (x i)) : UniqueDiffWithinAt 𝕜 (Set.pi univ s) x := by
  classical
  simp only [uniqueDiffWithinAt_iff, closure_pi_set] at h ⊢
  refine ⟨(dense_pi univ fun i _ => (h i).1).mono ?_, fun i _ => (h i).2⟩
  norm_cast
  simp only [← Submodule.iSup_map_single, iSup_le_iff, LinearMap.map_span, Submodule.span_le,
    ← mapsTo']
  exact fun i => (mapsTo_tangentConeAt_pi fun j _ => (h j).2).mono Subset.rfl Submodule.subset_span

Unique Differentiability of Product Sets at Points with Componentwise Unique Differentiability

Informal description

Let $\iota$ be a finite index type, and for each $i \in \iota$, let $E_i$ be a normed additive commutative group over a nontrivially normed field $\mathbb{K}$, equipped with a normed space structure. Let $s_i \subseteq E_i$ be subsets and $x_i \in E_i$ points such that for each $i$, the set $s_i$ has unique differentiability at $x_i$. Then the product set $\prod_{i \in \iota} s_i$ has unique differentiability at the point $(x_i)_{i \in \iota}$ in the product space $\prod_{i \in \iota} E_i$.

UniqueDiffWithinAt.pi theorem

 (ι : Type*) [Finite ι] (E : ι → Type*) [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)] (s : ∀ i, Set (E i))
  (x : ∀ i, E i) (I : Set ι) (h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)) : UniqueDiffWithinAt 𝕜 (Set.pi I s) x

Full source

theorem UniqueDiffWithinAt.pi (ι : Type*) [Finite ι] (E : ι → Type*)
    [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)] (s : ∀ i, Set (E i)) (x : ∀ i, E i)
    (I : Set ι) (h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)) :
    UniqueDiffWithinAt 𝕜 (Set.pi I s) x := by
  classical
  rw [← Set.univ_pi_piecewise_univ]
  refine UniqueDiffWithinAt.univ_pi ι E _ _ fun i => ?_
  by_cases hi : i ∈ I <;> simp [*, uniqueDiffWithinAt_univ]

Unique Differentiability of Partial Product Sets at Points with Componentwise Unique Differentiability

Informal description

Let $\iota$ be a finite index type, and for each $i \in \iota$, let $E_i$ be a normed additive commutative group over a nontrivially normed field $\mathbb{K}$, equipped with a normed space structure. Let $s_i \subseteq E_i$ be subsets and $x_i \in E_i$ points such that for each $i \in I$, the set $s_i$ has unique differentiability at $x_i$. Then the product set $\prod_{i \in I} s_i$ has unique differentiability at the point $(x_i)_{i \in I}$ in the product space $\prod_{i \in I} E_i$.

UniqueDiffOn.prod theorem

{t : Set F} (hs : UniqueDiffOn 𝕜 s) (ht : UniqueDiffOn 𝕜 t) : UniqueDiffOn 𝕜 (s ×ˢ t)

Full source

/-- The product of two sets of unique differentiability is a set of unique differentiability. -/
theorem UniqueDiffOn.prod {t : Set F} (hs : UniqueDiffOn 𝕜 s) (ht : UniqueDiffOn 𝕜 t) :
    UniqueDiffOn 𝕜 (s ×ˢ t) :=
  fun ⟨x, y⟩ h => UniqueDiffWithinAt.prod (hs x h.1) (ht y h.2)

Product of Sets with Unique Differentiability Has Unique Differentiability

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ and $t \subseteq F$ be sets. If $s$ has unique differentiability on all its points and $t$ has unique differentiability on all its points, then the product set $s \times t \subseteq E \times F$ also has unique differentiability on all its points.

UniqueDiffOn.pi theorem

 (ι : Type*) [Finite ι] (E : ι → Type*) [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)] (s : ∀ i, Set (E i))
  (I : Set ι) (h : ∀ i ∈ I, UniqueDiffOn 𝕜 (s i)) : UniqueDiffOn 𝕜 (Set.pi I s)

Full source

/-- The finite product of a family of sets of unique differentiability is a set of unique
differentiability. -/
theorem UniqueDiffOn.pi (ι : Type*) [Finite ι] (E : ι → Type*) [∀ i, NormedAddCommGroup (E i)]
    [∀ i, NormedSpace 𝕜 (E i)] (s : ∀ i, Set (E i)) (I : Set ι)
    (h : ∀ i ∈ I, UniqueDiffOn 𝕜 (s i)) : UniqueDiffOn 𝕜 (Set.pi I s) :=
  fun x hx => UniqueDiffWithinAt.pi _ _ _ _ _ fun i hi => h i hi (x i) (hx i hi)

Unique Differentiability of Product Sets with Componentwise Unique Differentiability

Informal description

Let $\iota$ be a finite index set, and for each $i \in \iota$, let $E_i$ be a normed additive commutative group over a nontrivially normed field $\mathbb{K}$, equipped with a normed space structure. Let $s_i \subseteq E_i$ be subsets such that for each $i \in I \subseteq \iota$, the set $s_i$ has the property of unique differentiability on all its points. Then the product set $\prod_{i \in I} s_i$ has the property of unique differentiability on all its points in the product space $\prod_{i \in I} E_i$.

UniqueDiffOn.univ_pi theorem

 (ι : Type*) [Finite ι] (E : ι → Type*) [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)] (s : ∀ i, Set (E i))
  (h : ∀ i, UniqueDiffOn 𝕜 (s i)) : UniqueDiffOn 𝕜 (Set.pi univ s)

Full source

/-- The finite product of a family of sets of unique differentiability is a set of unique
differentiability. -/
theorem UniqueDiffOn.univ_pi (ι : Type*) [Finite ι] (E : ι → Type*)
    [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)] (s : ∀ i, Set (E i))
    (h : ∀ i, UniqueDiffOn 𝕜 (s i)) : UniqueDiffOn 𝕜 (Set.pi univ s) :=
  UniqueDiffOn.pi _ _ _ _ fun i _ => h i

Unique Differentiability of Full Product of Uniquely Differentiable Sets

Informal description

Let $\iota$ be a finite index set, and for each $i \in \iota$, let $E_i$ be a normed additive commutative group over a nontrivially normed field $\mathbb{K}$, equipped with a normed space structure. Let $s_i \subseteq E_i$ be subsets such that for each $i \in \iota$, the set $s_i$ has the property of unique differentiability on all its points. Then the product set $\prod_{i \in \iota} s_i$ has the property of unique differentiability on all its points in the product space $\prod_{i \in \iota} E_i$.

uniqueDiffWithinAt_convex theorem

 {s : Set G} (conv : Convex ℝ s) (hs : (interior s).Nonempty) {x : G} (hx : x ∈ closure s) : UniqueDiffWithinAt ℝ s x

Full source

/-- In a real vector space, a convex set with nonempty interior is a set of unique
differentiability at every point of its closure. -/
theorem uniqueDiffWithinAt_convex {s : Set G} (conv : Convex ℝ s) (hs : (interior s).Nonempty)
    {x : G} (hx : x ∈ closure s) : UniqueDiffWithinAt ℝ s x := by
  rcases hs with ⟨y, hy⟩
  suffices y - x ∈ interior (tangentConeAt ℝ s x) by
    refine ⟨Dense.of_closure ?_, hx⟩
    simp [(Submodule.span ℝ (tangentConeAt ℝ s x)).eq_top_of_nonempty_interior'
        ⟨y - x, interior_mono Submodule.subset_span this⟩]
  rw [mem_interior_iff_mem_nhds]
  replace hy : interiorinterior s ∈ 𝓝 y := IsOpen.mem_nhds isOpen_interior hy
  apply mem_of_superset ((isOpenMap_sub_right x).image_mem_nhds hy)
  rintro _ ⟨z, zs, rfl⟩
  refine mem_tangentConeAt_of_openSegment_subset (Subset.trans ?_ interior_subset)
  exact conv.openSegment_closure_interior_subset_interior hx zs

Unique Differentiability on Closure of Convex Sets with Nonempty Interior

Informal description

Let $G$ be a real normed vector space and $s \subseteq G$ a convex set with nonempty interior. For any point $x$ in the closure of $s$, the set $s$ has the property of unique differentiability at $x$. This means that the tangent cone to $s$ at $x$ spans a dense subspace of $G$, ensuring the uniqueness of derivatives of functions defined on $s$ at $x$.

uniqueDiffOn_convex theorem

{s : Set G} (conv : Convex ℝ s) (hs : (interior s).Nonempty) : UniqueDiffOn ℝ s

Full source

/-- In a real vector space, a convex set with nonempty interior is a set of unique
differentiability. -/
theorem uniqueDiffOn_convex {s : Set G} (conv : Convex ℝ s) (hs : (interior s).Nonempty) :
    UniqueDiffOn ℝ s :=
  fun _ xs => uniqueDiffWithinAt_convex conv hs (subset_closure xs)

Unique Differentiability of Convex Sets with Nonempty Interior

Informal description

Let $G$ be a real normed vector space and $s \subseteq G$ a convex set with nonempty interior. Then $s$ has the property of unique differentiability, meaning that at every point $x \in s$, the tangent cone to $s$ at $x$ spans a dense subspace of $G$, ensuring the uniqueness of derivatives of functions defined on $s$.

uniqueDiffOn_Ici theorem

(a : ℝ) : UniqueDiffOn ℝ (Ici a)

Full source

theorem uniqueDiffOn_Ici (a : ℝ) : UniqueDiffOn ℝ (Ici a) :=
  uniqueDiffOn_convex (convex_Ici a) <| by simp only [interior_Ici, nonempty_Ioi]

Unique Differentiability of Right-Infinite Left-Closed Interval $[a, \infty)$ in $\mathbb{R}$

Informal description

For any real number $a$, the right-infinite left-closed interval $[a, \infty)$ has the property of unique differentiability on $\mathbb{R}$. This means that at every point $x \in [a, \infty)$, the tangent cone to $[a, \infty)$ at $x$ spans a dense subspace of $\mathbb{R}$, ensuring the uniqueness of derivatives of functions defined on $[a, \infty)$.

uniqueDiffOn_Iic theorem

(a : ℝ) : UniqueDiffOn ℝ (Iic a)

Full source

theorem uniqueDiffOn_Iic (a : ℝ) : UniqueDiffOn ℝ (Iic a) :=
  uniqueDiffOn_convex (convex_Iic a) <| by simp only [interior_Iic, nonempty_Iio]

Unique Differentiability of Left-Infinite Right-Closed Intervals in $\mathbb{R}$

Informal description

For any real number $a$, the left-infinite right-closed interval $(-\infty, a]$ has the property of unique differentiability. This means that at every point $x \in (-\infty, a]$, the tangent cone to the interval at $x$ spans a dense subspace of $\mathbb{R}$, ensuring the uniqueness of derivatives of functions defined on this interval.

uniqueDiffOn_Ioi theorem

(a : ℝ) : UniqueDiffOn ℝ (Ioi a)

Full source

theorem uniqueDiffOn_Ioi (a : ℝ) : UniqueDiffOn ℝ (Ioi a) :=
  isOpen_Ioi.uniqueDiffOn

Unique Differentiability of Left-Open Right-Infinite Intervals in $\mathbb{R}$

Informal description

For any real number $a$, the left-open right-infinite interval $(a, \infty)$ has the property of unique differentiability on $\mathbb{R}$. This means that at every point $x \in (a, \infty)$, the tangent cone to $(a, \infty)$ at $x$ spans a dense subspace of $\mathbb{R}$, ensuring the uniqueness of derivatives of functions defined on $(a, \infty)$.

uniqueDiffOn_Iio theorem

(a : ℝ) : UniqueDiffOn ℝ (Iio a)

Full source

theorem uniqueDiffOn_Iio (a : ℝ) : UniqueDiffOn ℝ (Iio a) :=
  isOpen_Iio.uniqueDiffOn

Unique Differentiability of Left-Infinite Right-Open Intervals in $\mathbb{R}$

Informal description

For any real number $a$, the left-infinite right-open interval $(-\infty, a)$ has the property of unique differentiability. This means that at every point $x \in (-\infty, a)$, the tangent cone to the interval at $x$ spans a dense subspace of $\mathbb{R}$, ensuring the uniqueness of derivatives of functions defined on this interval.

uniqueDiffOn_Icc theorem

{a b : ℝ} (hab : a < b) : UniqueDiffOn ℝ (Icc a b)

Full source

theorem uniqueDiffOn_Icc {a b : ℝ} (hab : a < b) : UniqueDiffOn ℝ (Icc a b) :=
  uniqueDiffOn_convex (convex_Icc a b) <| by simp only [interior_Icc, nonempty_Ioo, hab]

Unique Differentiability of Closed Intervals in $\mathbb{R}$

Informal description

For any real numbers $a$ and $b$ with $a < b$, the closed interval $[a, b]$ has the property of unique differentiability. This means that at every point $x \in [a, b]$, the tangent cone to $[a, b]$ at $x$ spans a dense subspace of $\mathbb{R}$, ensuring the uniqueness of derivatives of functions defined on $[a, b]$.

uniqueDiffOn_Ico theorem

(a b : ℝ) : UniqueDiffOn ℝ (Ico a b)

Full source

theorem uniqueDiffOn_Ico (a b : ℝ) : UniqueDiffOn ℝ (Ico a b) :=
  if hab : a < b then
    uniqueDiffOn_convex (convex_Ico a b) <| by simp only [interior_Ico, nonempty_Ioo, hab]
  else by simp only [Ico_eq_empty hab, uniqueDiffOn_empty]

Unique Differentiability of Left-Closed Right-Open Interval $[a, b)$ in Real Numbers

Informal description

For any real numbers $a$ and $b$, the left-closed right-open interval $[a, b) = \{x \in \mathbb{R} \mid a \leq x < b\}$ has the property of unique differentiability. This means that at every point $x \in [a, b)$, the tangent cone to $[a, b)$ at $x$ spans a dense subspace of $\mathbb{R}$, ensuring the uniqueness of derivatives of functions defined on $[a, b)$.

uniqueDiffOn_Ioc theorem

(a b : ℝ) : UniqueDiffOn ℝ (Ioc a b)

Full source

theorem uniqueDiffOn_Ioc (a b : ℝ) : UniqueDiffOn ℝ (Ioc a b) :=
  if hab : a < b then
    uniqueDiffOn_convex (convex_Ioc a b) <| by simp only [interior_Ioc, nonempty_Ioo, hab]
  else by simp only [Ioc_eq_empty hab, uniqueDiffOn_empty]

Unique Differentiability of Left-Open Right-Closed Intervals in $\mathbb{R}$

Informal description

For any real numbers $a$ and $b$, the left-open right-closed interval $(a, b]$ has the property of unique differentiability. That is, at every point $x \in (a, b]$, the tangent cone to $(a, b]$ at $x$ spans a dense subspace of $\mathbb{R}$, ensuring the uniqueness of derivatives of functions defined on $(a, b]$.

uniqueDiffOn_Ioo theorem

(a b : ℝ) : UniqueDiffOn ℝ (Ioo a b)

Full source

theorem uniqueDiffOn_Ioo (a b : ℝ) : UniqueDiffOn ℝ (Ioo a b) :=
  isOpen_Ioo.uniqueDiffOn

Unique Differentiability of Open Intervals in $\mathbb{R}$

Informal description

For any real numbers $a$ and $b$, the open interval $(a, b) = \{x \in \mathbb{R} \mid a < x < b\}$ has the property of unique differentiability. That is, at every point $x \in (a, b)$, the tangent cone to $(a, b)$ at $x$ spans a dense subspace of $\mathbb{R}$, ensuring the uniqueness of derivatives of functions defined on $(a, b)$.

uniqueDiffOn_Icc_zero_one theorem

: UniqueDiffOn ℝ (Icc (0 : ℝ) 1)

Full source

/-- The real interval `[0, 1]` is a set of unique differentiability. -/
theorem uniqueDiffOn_Icc_zero_one : UniqueDiffOn ℝ (Icc (0 : ℝ) 1) :=
  uniqueDiffOn_Icc zero_lt_one

Unique Differentiability of the Unit Interval $[0,1]$ in $\mathbb{R}$

Informal description

The closed interval $[0, 1]$ in the real numbers has the property of unique differentiability. That is, at every point $x \in [0, 1]$, the tangent cone to $[0, 1]$ at $x$ spans a dense subspace of $\mathbb{R}$, ensuring the uniqueness of derivatives of functions defined on $[0, 1]$.

uniqueDiffWithinAt_Ioo theorem

{a b t : ℝ} (ht : t ∈ Set.Ioo a b) : UniqueDiffWithinAt ℝ (Set.Ioo a b) t

Full source

theorem uniqueDiffWithinAt_Ioo {a b t : ℝ} (ht : t ∈ Set.Ioo a b) :
    UniqueDiffWithinAt ℝ (Set.Ioo a b) t :=
  IsOpen.uniqueDiffWithinAt isOpen_Ioo ht

Unique Differentiability at Interior Points of Open Intervals in $\mathbb{R}$

Informal description

For any real numbers $a < t < b$, the open interval $(a, b)$ has the property of unique differentiability at the point $t$. This means that the tangent cone to $(a, b)$ at $t$ spans a dense subspace of $\mathbb{R}$, ensuring the uniqueness of derivatives of functions defined on $(a, b)$ at $t$.

uniqueDiffWithinAt_Ioi theorem

(a : ℝ) : UniqueDiffWithinAt ℝ (Ioi a) a

Full source

theorem uniqueDiffWithinAt_Ioi (a : ℝ) : UniqueDiffWithinAt ℝ (Ioi a) a :=
  uniqueDiffWithinAt_convex (convex_Ioi a) (by simp) (by simp)

Unique Differentiability at Left Endpoint of Right-Infinite Interval

Informal description

For any real number $a$, the open right-infinite interval $(a, \infty)$ has the property of unique differentiability at the point $a$. This means that the tangent cone to $(a, \infty)$ at $a$ spans a dense subspace of $\mathbb{R}$, ensuring the uniqueness of derivatives of functions defined on $(a, \infty)$ at $a$.

uniqueDiffWithinAt_Iio theorem

(a : ℝ) : UniqueDiffWithinAt ℝ (Iio a) a

Full source

theorem uniqueDiffWithinAt_Iio (a : ℝ) : UniqueDiffWithinAt ℝ (Iio a) a :=
  uniqueDiffWithinAt_convex (convex_Iio a) (by simp) (by simp)

Unique Differentiability at Left Endpoint of $(-\infty, a)$

Informal description

For any real number $a$, the left-infinite right-open interval $(-\infty, a)$ has the property of unique differentiability at the point $a$. This means that the tangent cone to $(-\infty, a)$ at $a$ spans a dense subspace of $\mathbb{R}$, ensuring the uniqueness of derivatives of functions defined on $(-\infty, a)$ at $a$.

uniqueDiffWithinAt_iff_accPt theorem

{s : Set 𝕜} {x : 𝕜} : UniqueDiffWithinAt 𝕜 s x ↔ AccPt x (𝓟 s)

Full source

/-- In one dimension, a point is a point of unique differentiability of a set
iff it is an accumulation point of the set. -/
theorem uniqueDiffWithinAt_iff_accPt {s : Set 𝕜} {x : 𝕜} :
    UniqueDiffWithinAtUniqueDiffWithinAt 𝕜 s x ↔ AccPt x (𝓟 s) :=
  ⟨UniqueDiffWithinAt.accPt, fun h ↦
    ⟨by simp [tangentConeAt_eq_univ h], mem_closure_iff_clusterPt.mpr h.clusterPt⟩⟩

Characterization of Unique Differentiability via Accumulation Points in Normed Fields

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $s \subseteq \mathbb{K}$ a subset, and $x \in \mathbb{K}$. Then $x$ is a point of unique differentiability within $s$ if and only if $x$ is an accumulation point of $s$.

uniqueDiffWithinAt_or_nhdsWithin_eq_bot theorem

(s : Set 𝕜) (x : 𝕜) : UniqueDiffWithinAt 𝕜 s x ∨ 𝓝[s \ { x }] x = ⊥

Full source

/-- In one dimension, every point is either a point of unique differentiability, or isolated. -/
@[deprecated uniqueDiffWithinAt_iff_accPt (since := "2025-04-20")]
theorem uniqueDiffWithinAt_or_nhdsWithin_eq_bot (s : Set 𝕜) (x : 𝕜) :
    UniqueDiffWithinAtUniqueDiffWithinAt 𝕜 s x ∨ 𝓝[s \ {x}] x = ⊥ :=
  (em (AccPt x (𝓟 s))).imp AccPt.uniqueDiffWithinAt fun h ↦ by
    rwa [accPt_principal_iff_nhdsWithin, not_neBot] at h

Dichotomy for Unique Differentiability or Isolation in Normed Fields

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $s \subseteq \mathbb{K}$ a subset, and $x \in \mathbb{K}$. Then either $x$ is a point of unique differentiability within $s$, or the neighborhood filter of $x$ restricted to $s \setminus \{x\}$ is trivial (i.e., $x$ is isolated in $s$).

Implementation details