Tangent cone

In this file, we define two predicates UniqueDiffWithinAt 𝕜 s x and UniqueDiffOn 𝕜 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 tangentConeAt, and express UniqueDiffWithinAt and UniqueDiffOn in terms of it. One should however think of this definition as an implementation detail: the only reason to introduce the predicates UniqueDiffWithinAt and UniqueDiffOn 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 Mathlib/Analysis/Calculus/FDeriv/Basic.lean. Hence, derivatives are not defined yet. The property of uniqueness of the derivative is therefore proved in Mathlib/Analysis/Calculus/FDeriv/Basic.lean, but based on the properties of the tangent cone we prove here.

@[irreducible]

def tangentConeAt (R : Type u_1) {E : Type u_2} [AddCommGroup E] [SMul R E] [TopologicalSpace E] (s : Set E) (x : E) : Set E

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

A point y belongs to the tangent cone of s at x iff there exist a family of scalars c n, a family of vectors d n, and a nontrivial filter in the index type such that

• d n → 0 along the filter;
• x + d n ∈ s eventually along the filter;
• c n • d n → y along the filter,

The actual definition is given in terms of cluster points of a filter, see mem_tangentConeAt_of_seq and exists_fun_of_mem_tangentConeAt for the two implications unfolding this definition in more convenient way.

In a space with first countable topology, one can assume that the index type is ℕ and the filter is atTop, but the definition we use is more useful without that assumption.

Equations

• tangentConeAt R s x = {y : E | ClusterPt y (⊤ • nhdsWithin 0 ((fun (x_1 : E) => x + x_1) ⁻¹' s))}

theorem tangentConeAt_def (R : Type u_1) {E : Type u_2} [AddCommGroup E] [SMul R E] [TopologicalSpace E] (s : Set E) (x : E) : tangentConeAt R s x = {y : E | ClusterPt y (⊤ • nhdsWithin 0 ((fun (x_1 : E) => x + x_1) ⁻¹' s))}

theorem mem_tangentConeAt_of_frequently {R : Type u} {E : Type v} [AddCommGroup E] [SMul R E] [TopologicalSpace E] {s : Set E} {x y : E} {α : Type u_1} (l : Filter α) (c : α → R) (d : α → E) (hd₀ : Filter.Tendsto d l (nhds 0)) (hds : ∃ᶠ (n : α) in l, x + d n ∈ s) (hcd : Filter.Tendsto (fun (n : α) => c n • d n) l (nhds y)) : y ∈ tangentConeAt R s x

Let c n be a family of scalars, d n be a family of vectors, and l be a filter such that

• d n → 0 along l;
• x + d n ∈ s frequently along l;
• c n • d n → y along l.

Then y belongs to the tangent cone of s at x. See also

• mem_tangentConeAt_of_seq for a version assuming that x + d n ∈ s eventually along l.
• exists_fun_of_mem_tangentConeAt for the other implication.

theorem mem_tangentConeAt_of_seq {R : Type u} {E : Type v} [AddCommGroup E] [SMul R E] [TopologicalSpace E] {s : Set E} {x y : E} {α : Type u_1} (l : Filter α) [l.NeBot] (c : α → R) (d : α → E) (hd₀ : Filter.Tendsto d l (nhds 0)) (hds : ∀ᶠ (n : α) in l, x + d n ∈ s) (hcd : Filter.Tendsto (fun (n : α) => c n • d n) l (nhds y)) : y ∈ tangentConeAt R s x

A special case of mem_tangentConeAt_of_frequently, which avoids Filter.Frequently.

theorem exists_fun_of_mem_tangentConeAt {R : Type u} {E : Type v} [AddCommGroup E] [SMul R E] [TopologicalSpace E] {s : Set E} {x y : E} (h : y ∈ tangentConeAt R s x) : ∃ (α : Type (max u v)) (l : Filter α) (_ : l.NeBot) (c : α → R) (d : α → E), Filter.Tendsto d l (nhds 0) ∧ (∀ᶠ (n : α) in l, x + d n ∈ s) ∧ Filter.Tendsto (fun (n : α) => c n • d n) l (nhds y)

If y belongs to the tangent cone of s at x, then there exist

• an index type α and a nontrivial filter l on α;
• a family of scalars c n, n : α, and a family of vectors d n, n : α such that
• d n → 0 along l;
• x + d n ∈ s eventually along l;
• c n • d n → y along l.

In fact, one can take α = R × E, c = Prod.fst, and d = Prod.snd, but this is not important, so the lemma statement hides these details.

This lemma provides a convenient way to unfold the definition of tangentConeAt.

@[reducible, inline]

abbrev posTangentConeAt {E : Type v} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] (s : Set E) (x : E) : Set E

"Positive" tangent cone to s at x.

Equations

• posTangentConeAt s x = tangentConeAt NNReal s x

structure UniqueDiffWithinAt (R : Type u) {E : Type v} [Semiring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] (s : Set E) (x : E) : Prop

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.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).

• dense_tangentConeAt : Dense ↑(Submodule.span R (tangentConeAt R s x))
• mem_closure : x ∈ closure s

theorem uniqueDiffWithinAt_iff (R : Type u) {E : Type v} [Semiring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] (s : Set E) (x : E) : UniqueDiffWithinAt R s x ↔ Dense ↑(Submodule.span R (tangentConeAt R s x)) ∧ x ∈ closure s

def UniqueDiffOn (R : Type u) {E : Type v} [Semiring R] [AddCommGroup E] [Module R E] [TopologicalSpace 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 UniqueDiffOn.eq in Mathlib/Analysis/Calculus/FDeriv/Basic.lean.

Equations

• UniqueDiffOn R s = ∀ x ∈ s, UniqueDiffWithinAt R s x

theorem UniqueDiffOn.uniqueDiffWithinAt {R : Type u} {E : Type v} [Semiring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] {s : Set E} {x : E} (hs : UniqueDiffOn R s) (h : x ∈ s) : UniqueDiffWithinAt R s x