mathlib3 documentation

analysis.calculus.tangent_cone

Tangent cone #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file, we define two predicates unique_diff_within_at 𝕜 s x and unique_diff_on 𝕜 s ensuring that, if a function has two derivatives, then they have to coincide. As a direct definition of this fact (quantifying on all target types and all functions) would depend on universes, we use a more intrinsic definition: if all the possible tangent directions to the set s at the point x span a dense subset of the whole subset, it is easy to check that the derivative has to be unique.

Therefore, we introduce the set of all tangent directions, named tangent_cone_at, and express unique_diff_within_at and unique_diff_on in terms of it. One should however think of this definition as an implementation detail: the only reason to introduce the predicates unique_diff_within_at and unique_diff_on is to ensure the uniqueness of the derivative. This is why their names reflect their uses, and not how they are defined.

Implementation details #

Note that this file is imported by fderiv.lean. Hence, derivatives are not defined yet. The property of uniqueness of the derivative is therefore proved in fderiv.lean, but based on the properties of the tangent cone we prove here.

def tangent_cone_at (𝕜 : Type u_1) [nontrivially_normed_field 𝕜] {E : Type u_2} [add_comm_monoid E] [module 𝕜 E] [topological_space E] (s : set E) (x : E) :

The set of all tangent directions to the set s at the point x.

Equations

tangent_cone_at 𝕜 s x = {y : E | ∃ (c : ℕ → 𝕜) (d : ℕ → E), (∀ᶠ (n : ℕ) in filter.at_top , x + d n ∈ s) ∧ filter.tendsto (λ (n : ℕ), ‖c n‖) filter.at_top filter.at_top ∧ filter.tendsto (λ (n : ℕ), c n • d n) filter.at_top (nhds y)}

theorem unique_diff_within_at_iff (𝕜 : Type u_1) [nontrivially_normed_field 𝕜] {E : Type u_2} [add_comm_monoid E] [module 𝕜 E] [topological_space E] (s : set E) (x : E) :

unique_diff_within_at 𝕜 s x ↔ dense ↑(submodule.span 𝕜 (tangent_cone_at 𝕜 s x)) ∧ x ∈ closure s

structure unique_diff_within_at (𝕜 : Type u_1) [nontrivially_normed_field 𝕜] {E : Type u_2} [add_comm_monoid E] [module 𝕜 E] [topological_space E] (s : set E) (x : E) :

Prop

dense_tangent_cone : dense ↑(submodule.span 𝕜 (tangent_cone_at 𝕜 s x))
mem_closure : x ∈ closure s

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 unique_diff_within_at.eq in fderiv.lean. 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).

def unique_diff_on (𝕜 : Type u_1) [nontrivially_normed_field 𝕜] {E : Type u_2} [add_comm_monoid E] [module 𝕜 E] [topological_space E] (s : set E) :

Prop

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 unique_diff_on.eq in fderiv.lean.

Equations

unique_diff_on 𝕜 s = ∀ (x : E), x ∈ s → unique_diff_within_at 𝕜 s x

theorem tangent_cone_univ {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} :

tangent_cone_at 𝕜 set.univ x = set.univ

theorem tangent_cone_mono {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {s t : set E} (h : s ⊆ t) :

tangent_cone_at 𝕜 s x ⊆ tangent_cone_at 𝕜 t x

theorem tangent_cone_at.lim_zero {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {y : E} {α : Type u_3} (l : filter α) {c : α → 𝕜} {d : α → E} (hc : filter.tendsto (λ (n : α), ‖c n‖) l filter.at_top) (hd : filter.tendsto (λ (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 tangent_cone_mono_nhds {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {s t : set E} (h : nhds_within x s ≤ nhds_within x t) :

tangent_cone_at 𝕜 s x ⊆ tangent_cone_at 𝕜 t x

theorem tangent_cone_congr {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {s t : set E} (h : nhds_within x s = nhds_within x t) :

tangent_cone_at 𝕜 s x = tangent_cone_at 𝕜 t x

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

theorem tangent_cone_inter_nhds {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {s t : set E} (ht : t ∈ nhds x) :

tangent_cone_at 𝕜 (s ∩ t) x = tangent_cone_at 𝕜 s x

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

theorem subset_tangent_cone_prod_left {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {x : E} {s : set E} {t : set F} {y : F} (ht : y ∈ closure t) :

⇑(linear_map.inl 𝕜 E F) '' tangent_cone_at 𝕜 s x ⊆ tangent_cone_at 𝕜 (s ×ˢ t) (x, y)

The tangent cone of a product contains the tangent cone of its left factor.

theorem subset_tangent_cone_prod_right {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {x : E} {s : set E} {t : set F} {y : F} (hs : x ∈ closure s) :

⇑(linear_map.inr 𝕜 E F) '' tangent_cone_at 𝕜 t y ⊆ tangent_cone_at 𝕜 (s ×ˢ t) (x, y)

The tangent cone of a product contains the tangent cone of its right factor.

theorem maps_to_tangent_cone_pi {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {ι : Type u_2} [decidable_eq ι] {E : ι → Type u_3} [Π (i : ι), normed_add_comm_group (E i)] [Π (i : ι), normed_space 𝕜 (E i)] {s : Π (i : ι), set (E i)} {x : Π (i : ι), E i} {i : ι} (hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)) :

set.maps_to ⇑(linear_map.single i) (tangent_cone_at 𝕜 (s i) (x i)) (tangent_cone_at 𝕜 (set.univ.pi s) x)

The tangent cone of a product contains the tangent cone of each factor.

theorem mem_tangent_cone_of_open_segment_subset {G : Type u_4} [normed_add_comm_group G] [normed_space ℝ G] {s : set G} {x y : G} (h : open_segment ℝ x y ⊆ s) :

y - x ∈ tangent_cone_at ℝ s x

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_tangent_cone_of_segment_subset {G : Type u_4} [normed_add_comm_group G] [normed_space ℝ G] {s : set G} {x y : G} (h : segment ℝ x y ⊆ s) :

y - x ∈ tangent_cone_at ℝ s x

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.

Properties of `unique_diff_within_at` and `unique_diff_on` #

This section is devoted to properties of the predicates unique_diff_within_at and unique_diff_on.

theorem unique_diff_on.unique_diff_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {s : set E} {x : E} (hs : unique_diff_on 𝕜 s) (h : x ∈ s) :

unique_diff_within_at 𝕜 s x

theorem unique_diff_within_at_univ {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} :

unique_diff_within_at 𝕜 set.univ x

theorem unique_diff_on_univ {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] :

unique_diff_on 𝕜 set.univ

theorem unique_diff_on_empty {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] :

unique_diff_on 𝕜 ∅

theorem unique_diff_within_at.mono_nhds {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {s t : set E} (h : unique_diff_within_at 𝕜 s x) (st : nhds_within x s ≤ nhds_within x t) :

unique_diff_within_at 𝕜 t x

theorem unique_diff_within_at.mono {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {s t : set E} (h : unique_diff_within_at 𝕜 s x) (st : s ⊆ t) :

unique_diff_within_at 𝕜 t x

theorem unique_diff_within_at_congr {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {s t : set E} (st : nhds_within x s = nhds_within x t) :

unique_diff_within_at 𝕜 s x ↔ unique_diff_within_at 𝕜 t x

theorem unique_diff_within_at_inter {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {s t : set E} (ht : t ∈ nhds x) :

unique_diff_within_at 𝕜 (s ∩ t) x ↔ unique_diff_within_at 𝕜 s x

theorem unique_diff_within_at.inter {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {s t : set E} (hs : unique_diff_within_at 𝕜 s x) (ht : t ∈ nhds x) :

unique_diff_within_at 𝕜 (s ∩ t) x

theorem unique_diff_within_at_inter' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {s t : set E} (ht : t ∈ nhds_within x s) :

unique_diff_within_at 𝕜 (s ∩ t) x ↔ unique_diff_within_at 𝕜 s x

theorem unique_diff_within_at.inter' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {s t : set E} (hs : unique_diff_within_at 𝕜 s x) (ht : t ∈ nhds_within x s) :

unique_diff_within_at 𝕜 (s ∩ t) x

theorem unique_diff_within_at_of_mem_nhds {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {s : set E} (h : s ∈ nhds x) :

unique_diff_within_at 𝕜 s x

theorem is_open.unique_diff_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {s : set E} (hs : is_open s) (xs : x ∈ s) :

unique_diff_within_at 𝕜 s x

theorem unique_diff_on.inter {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {s t : set E} (hs : unique_diff_on 𝕜 s) (ht : is_open t) :

unique_diff_on 𝕜 (s ∩ t)

theorem is_open.unique_diff_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {s : set E} (hs : is_open s) :

unique_diff_on 𝕜 s

theorem unique_diff_within_at.prod {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {x : E} {s : set E} {t : set F} {y : F} (hs : unique_diff_within_at 𝕜 s x) (ht : unique_diff_within_at 𝕜 t y) :

unique_diff_within_at 𝕜 (s ×ˢ t) (x, y)

The product of two sets of unique differentiability at points x and y has unique differentiability at (x, y).

theorem unique_diff_within_at.univ_pi {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] (ι : Type u_2) [finite ι] (E : ι → Type u_3) [Π (i : ι), normed_add_comm_group (E i)] [Π (i : ι), normed_space 𝕜 (E i)] (s : Π (i : ι), set (E i)) (x : Π (i : ι), E i) (h : ∀ (i : ι), unique_diff_within_at 𝕜 (s i) (x i)) :

unique_diff_within_at 𝕜 (set.univ.pi s) x

theorem unique_diff_within_at.pi {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] (ι : Type u_2) [finite ι] (E : ι → Type u_3) [Π (i : ι), normed_add_comm_group (E i)] [Π (i : ι), normed_space 𝕜 (E i)] (s : Π (i : ι), set (E i)) (x : Π (i : ι), E i) (I : set ι) (h : ∀ (i : ι), i ∈ I → unique_diff_within_at 𝕜 (s i) (x i)) :

unique_diff_within_at 𝕜 (I.pi s) x

theorem unique_diff_on.prod {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {s : set E} {t : set F} (hs : unique_diff_on 𝕜 s) (ht : unique_diff_on 𝕜 t) :

unique_diff_on 𝕜 (s ×ˢ t)

The product of two sets of unique differentiability is a set of unique differentiability.

theorem unique_diff_on.pi {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] (ι : Type u_2) [finite ι] (E : ι → Type u_3) [Π (i : ι), normed_add_comm_group (E i)] [Π (i : ι), normed_space 𝕜 (E i)] (s : Π (i : ι), set (E i)) (I : set ι) (h : ∀ (i : ι), i ∈ I → unique_diff_on 𝕜 (s i)) :

unique_diff_on 𝕜 (I.pi s)

The finite product of a family of sets of unique differentiability is a set of unique differentiability.

theorem unique_diff_on.univ_pi {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] (ι : Type u_2) [finite ι] (E : ι → Type u_3) [Π (i : ι), normed_add_comm_group (E i)] [Π (i : ι), normed_space 𝕜 (E i)] (s : Π (i : ι), set (E i)) (h : ∀ (i : ι), unique_diff_on 𝕜 (s i)) :

unique_diff_on 𝕜 (set.univ.pi s)

The finite product of a family of sets of unique differentiability is a set of unique differentiability.

theorem unique_diff_within_at_convex {G : Type u_4} [normed_add_comm_group G] [normed_space ℝ G] {s : set G} (conv : convex ℝ s) (hs : (interior s).nonempty) {x : G} (hx : x ∈ closure s) :

unique_diff_within_at ℝ s x

In a real vector space, a convex set with nonempty interior is a set of unique differentiability at every point of its closure.

theorem unique_diff_on_convex {G : Type u_4} [normed_add_comm_group G] [normed_space ℝ G] {s : set G} (conv : convex ℝ s) (hs : (interior s).nonempty) :

unique_diff_on ℝ s

In a real vector space, a convex set with nonempty interior is a set of unique differentiability.

theorem unique_diff_on_Ici (a : ℝ) :

unique_diff_on ℝ (set.Ici a)

theorem unique_diff_on_Iic (a : ℝ) :

unique_diff_on ℝ (set.Iic a)

theorem unique_diff_on_Ioi (a : ℝ) :

unique_diff_on ℝ (set.Ioi a)

theorem unique_diff_on_Iio (a : ℝ) :

unique_diff_on ℝ (set.Iio a)

theorem unique_diff_on_Icc {a b : ℝ} (hab : a < b) :

unique_diff_on ℝ (set.Icc a b)

theorem unique_diff_on_Ico (a b : ℝ) :

unique_diff_on ℝ (set.Ico a b)

theorem unique_diff_on_Ioc (a b : ℝ) :

unique_diff_on ℝ (set.Ioc a b)

theorem unique_diff_on_Ioo (a b : ℝ) :

unique_diff_on ℝ (set.Ioo a b)

theorem unique_diff_on_Icc_zero_one :

unique_diff_on ℝ (set.Icc 0 1)

The real interval [0, 1] is a set of unique differentiability.

theorem unique_diff_within_at_Ioo {a b t : ℝ} (ht : t ∈ set.Ioo a b) :

unique_diff_within_at ℝ (set.Ioo a b) t

theorem unique_diff_within_at_Ioi (a : ℝ) :

unique_diff_within_at ℝ (set.Ioi a) a

theorem unique_diff_within_at_Iio (a : ℝ) :

unique_diff_within_at ℝ (set.Iio a) a