Documentation

Mathlib.Analysis.Calculus.TangentCone

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 Fderiv.Basic. Hence, derivatives are not defined yet. The property of uniqueness of the derivative is therefore proved in Fderiv.Basic, but based on the properties of the tangent cone we prove here.

def tangentConeAt (๐•œ : Type u_1) [NontriviallyNormedField ๐•œ] {E : Type u_2} [AddCommMonoid E] [Module ๐•œ E] [TopologicalSpace E] (s : Set E) (x : E) :
Set E

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

Instances For
    theorem uniqueDiffWithinAt_iff (๐•œ : Type u_1) [NontriviallyNormedField ๐•œ] {E : Type u_2} [AddCommMonoid E] [Module ๐•œ E] [TopologicalSpace E] (s : Set E) (x : E) :
    UniqueDiffWithinAt ๐•œ s x โ†” Dense โ†‘(Submodule.span ๐•œ (tangentConeAt ๐•œ s x)) โˆง x โˆˆ closure s
    structure UniqueDiffWithinAt (๐•œ : Type u_1) [NontriviallyNormedField ๐•œ] {E : Type u_2} [AddCommMonoid E] [Module ๐•œ E] [TopologicalSpace E] (s : Set E) (x : E) :

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

    Instances For
      def UniqueDiffOn (๐•œ : Type u_1) [NontriviallyNormedField ๐•œ] {E : Type u_2} [AddCommMonoid E] [Module ๐•œ E] [TopologicalSpace E] (s : Set E) :

      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 Fderiv.Basic.

      Instances For
        theorem mem_tangentConeAt_of_pow_smul {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {x : E} {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
        theorem tangentCone_univ {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {x : E} :
        tangentConeAt ๐•œ Set.univ x = Set.univ
        theorem tangentCone_mono {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {x : E} {s : Set E} {t : Set E} (h : s โŠ† t) :
        tangentConeAt ๐•œ s x โŠ† tangentConeAt ๐•œ t x
        theorem tangentConeAt.lim_zero {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {y : 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)) :

        Auxiliary lemma ensuring that, under the assumptions defining the tangent cone, the sequence d tends to 0 at infinity.

        theorem tangentCone_mono_nhds {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {x : E} {s : Set E} {t : Set E} (h : nhdsWithin x s โ‰ค nhdsWithin x t) :
        tangentConeAt ๐•œ s x โŠ† tangentConeAt ๐•œ t x
        theorem tangentCone_congr {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {x : E} {s : Set E} {t : Set 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.

        theorem tangentCone_inter_nhds {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {x : E} {s : Set E} {t : Set 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.

        theorem subset_tangentCone_prod_left {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] {x : E} {s : Set E} {t : Set F} {y : F} (ht : y โˆˆ closure t) :
        โ†‘(LinearMap.inl ๐•œ E F) '' tangentConeAt ๐•œ s x โŠ† tangentConeAt ๐•œ (s ร—หข t) (x, y)

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

        theorem subset_tangentCone_prod_right {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] {x : E} {s : Set E} {t : Set F} {y : F} (hs : x โˆˆ closure s) :
        โ†‘(LinearMap.inr ๐•œ E F) '' tangentConeAt ๐•œ t y โŠ† tangentConeAt ๐•œ (s ร—หข t) (x, y)

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

        theorem mapsTo_tangentCone_pi {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {ฮน : Type u_5} [DecidableEq ฮน] {E : ฮน โ†’ Type u_6} [(i : ฮน) โ†’ NormedAddCommGroup (E i)] [(i : ฮน) โ†’ NormedSpace ๐•œ (E i)] {s : (i : ฮน) โ†’ Set (E i)} {x : (i : ฮน) โ†’ E i} {i : ฮน} (hi : โˆ€ (j : ฮน), j โ‰  i โ†’ x j โˆˆ closure (s j)) :
        Set.MapsTo (โ†‘(LinearMap.single i)) (tangentConeAt ๐•œ (s i) (x i)) (tangentConeAt ๐•œ (Set.pi Set.univ s) x)

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

        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.

        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 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} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {s : Set E} {x : E} (hs : UniqueDiffOn ๐•œ s) (h : x โˆˆ s) :
        UniqueDiffWithinAt ๐•œ s x
        theorem uniqueDiffWithinAt_univ {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {x : E} :
        UniqueDiffWithinAt ๐•œ Set.univ x
        theorem uniqueDiffOn_univ {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] :
        UniqueDiffOn ๐•œ Set.univ
        theorem uniqueDiffOn_empty {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] :
        theorem UniqueDiffWithinAt.congr_pt {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {x : E} {y : E} {s : Set E} (h : UniqueDiffWithinAt ๐•œ s x) (hy : x = y) :
        UniqueDiffWithinAt ๐•œ s y
        theorem UniqueDiffWithinAt.mono_nhds {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {x : E} {s : Set E} {t : Set 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} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {x : E} {s : Set E} {t : Set E} (h : UniqueDiffWithinAt ๐•œ s x) (st : s โŠ† t) :
        UniqueDiffWithinAt ๐•œ t x
        theorem uniqueDiffWithinAt_congr {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {x : E} {s : Set E} {t : Set 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} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {x : E} {s : Set E} {t : Set E} (ht : t โˆˆ nhds x) :
        UniqueDiffWithinAt ๐•œ (s โˆฉ t) x โ†” UniqueDiffWithinAt ๐•œ s x
        theorem UniqueDiffWithinAt.inter {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {x : E} {s : Set E} {t : Set E} (hs : UniqueDiffWithinAt ๐•œ s x) (ht : t โˆˆ nhds x) :
        UniqueDiffWithinAt ๐•œ (s โˆฉ t) x
        theorem uniqueDiffWithinAt_inter' {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {x : E} {s : Set E} {t : Set E} (ht : t โˆˆ nhdsWithin x s) :
        UniqueDiffWithinAt ๐•œ (s โˆฉ t) x โ†” UniqueDiffWithinAt ๐•œ s x
        theorem UniqueDiffWithinAt.inter' {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {x : E} {s : Set E} {t : Set 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} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {x : E} {s : Set E} (h : s โˆˆ nhds x) :
        UniqueDiffWithinAt ๐•œ s x
        theorem IsOpen.uniqueDiffWithinAt {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {x : E} {s : Set E} (hs : IsOpen s) (xs : x โˆˆ s) :
        UniqueDiffWithinAt ๐•œ s x
        theorem UniqueDiffOn.inter {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {s : Set E} {t : Set E} (hs : UniqueDiffOn ๐•œ s) (ht : IsOpen t) :
        UniqueDiffOn ๐•œ (s โˆฉ t)
        theorem IsOpen.uniqueDiffOn {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {s : Set E} (hs : IsOpen s) :
        UniqueDiffOn ๐•œ s
        theorem UniqueDiffWithinAt.prod {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] {x : E} {s : Set E} {t : Set F} {y : F} (hs : UniqueDiffWithinAt ๐•œ s x) (ht : UniqueDiffWithinAt ๐•œ t y) :
        UniqueDiffWithinAt ๐•œ (s ร—หข t) (x, y)

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

        theorem UniqueDiffWithinAt.univ_pi {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] (ฮน : Type u_5) [Finite ฮน] (E : ฮน โ†’ Type u_6) [(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 Set.univ s) x
        theorem UniqueDiffWithinAt.pi {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] (ฮน : Type u_5) [Finite ฮน] (E : ฮน โ†’ Type u_6) [(i : ฮน) โ†’ NormedAddCommGroup (E i)] [(i : ฮน) โ†’ NormedSpace ๐•œ (E i)] (s : (i : ฮน) โ†’ Set (E i)) (x : (i : ฮน) โ†’ E i) (I : Set ฮน) (h : โˆ€ (i : ฮน), i โˆˆ I โ†’ UniqueDiffWithinAt ๐•œ (s i) (x i)) :
        UniqueDiffWithinAt ๐•œ (Set.pi I s) x
        theorem UniqueDiffOn.prod {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] {s : Set E} {t : Set F} (hs : UniqueDiffOn ๐•œ s) (ht : UniqueDiffOn ๐•œ t) :
        UniqueDiffOn ๐•œ (s ร—หข t)

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

        theorem UniqueDiffOn.pi {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] (ฮน : Type u_5) [Finite ฮน] (E : ฮน โ†’ Type u_6) [(i : ฮน) โ†’ NormedAddCommGroup (E i)] [(i : ฮน) โ†’ NormedSpace ๐•œ (E i)] (s : (i : ฮน) โ†’ Set (E i)) (I : Set ฮน) (h : โˆ€ (i : ฮน), i โˆˆ I โ†’ UniqueDiffOn ๐•œ (s i)) :
        UniqueDiffOn ๐•œ (Set.pi I s)

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

        theorem UniqueDiffOn.univ_pi {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] (ฮน : Type u_5) [Finite ฮน] (E : ฮน โ†’ Type u_6) [(i : ฮน) โ†’ NormedAddCommGroup (E i)] [(i : ฮน) โ†’ NormedSpace ๐•œ (E i)] (s : (i : ฮน) โ†’ Set (E i)) (h : โˆ€ (i : ฮน), UniqueDiffOn ๐•œ (s i)) :
        UniqueDiffOn ๐•œ (Set.pi Set.univ s)

        The finite product of a family of 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 at every point of its closure.

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

        theorem uniqueDiffOn_Icc {a : โ„} {b : โ„} (hab : a < b) :

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