Tangent cone
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.
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)}
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).
Equations
- unique_diff_within_at ๐ s x = (closure โ(submodule.span ๐ (tangent_cone_at ๐ s x)) = set.univ โง x โ closure s)
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
Auxiliary lemma ensuring that, under the assumptions defining the tangent cone,
the sequence d tends to 0 at infinity.
Tangent cone of s at x depends only on ๐[s] x.
Intersecting with a neighborhood of the point does not change the tangent cone.
The tangent cone of a product contains the tangent cone of its left factor.
The tangent cone of a product contains the tangent cone of its right factor.
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.
The product of two sets of unique differentiability at points x and y has unique
differentiability at (x, y).
The product of two sets of unique differentiability is a set of unique differentiability.
In a real vector space, a convex set with nonempty interior is a set of unique differentiability.
The real interval [0, 1] is a set of unique differentiability.