Asymptotic cone of a set

This file defines the asymptotic cone of a set in a topological affine space.

Implementation details

The asymptotic cone of a set $A$ is usually defined as the set of points $v$ for which there exist sequences $t_n > 0$ and $x_n \in A$ such that $t_n \to 0$ and $t_n x_n \to v$. We take a different approach here using filters: we define the asymptotic cone of s as the set of vectors v such that ∃ᶠ p in Filter.atTop • 𝓝 v, p ∈ s holds.

Main definitions

• AffineSpace.asymptoticNhds: the filter of neighborhoods at infinity in some direction.
• asymptoticCone: the asymptotic cone of a subset of a topological affine space.

Main statements

• Convex.smul_vadd_mem_of_isClosed_of_mem_asymptoticCone: if v is in the asymptotic cone of a closed convex set s, then every ray of direction v starting from s is contained in s.
• Convex.smul_vadd_mem_of_mem_nhds_of_mem_asymptoticCone: if v is in the asymptotic cone of a convex set s, then every ray of direction v starting from the interior of s is contained in s.

@[irreducible]

def AffineSpace.asymptoticNhds (k : Type u_1) {V : Type u_2} (P : Type u_3) [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] (v : V) : Filter P

In a topological affine space P over k, AffineSpace.asymptoticNhds k P v is the filter of neighborhoods at infinity in directions near v. In a topological vector space, this is the filter Filter.atTop • 𝓝 v. To support affine spaces, the actual definition is different and should be considered an implementation detail. Use AffineSpace.asymptoticNhds_eq_smul or AffineSpace.asymptoticNhds_eq_smul_vadd for unfolding.

theorem AffineSpace.asymptoticNhds_vadd_pure {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] (v : V) (p : P) : asymptoticNhds k V v +ᵥ pure p = asymptoticNhds k P v

theorem AffineSpace.vadd_asymptoticNhds {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] (u v : V) : u +ᵥ asymptoticNhds k P v = asymptoticNhds k P v

theorem Filter.Tendsto.asymptoticNhds_vadd_const {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] {α : Type u_4} {l : Filter α} {f : α → V} {v : V} (p : P) (hf : Tendsto f l (AffineSpace.asymptoticNhds k V v)) : Tendsto (fun (x : α) => f x +ᵥ p) l (AffineSpace.asymptoticNhds k P v)

theorem Filter.Tendsto.const_vadd_asymptoticNhds {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] {α : Type u_4} {l : Filter α} {f : α → P} {v : V} (u : V) (hf : Tendsto f l (AffineSpace.asymptoticNhds k P v)) : Tendsto (fun (x : α) => u +ᵥ f x) l (AffineSpace.asymptoticNhds k P v)

theorem AffineSpace.asymptoticNhds_eq_smul {k : Type u_1} {V : Type u_2} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [TopologicalSpace V] [TopologicalSpace k] [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] (v : V) : asymptoticNhds k V v = Filter.atTop • nhds v

theorem AffineSpace.asymptoticNhds_eq_smul_vadd {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] [TopologicalSpace k] [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] (v : V) (p : P) : asymptoticNhds k P v = Filter.atTop • nhds v +ᵥ pure p

instance AffineSpace.instNeBotAsymptoticNhds {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] [TopologicalSpace k] [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] {v : V} : (asymptoticNhds k P v).NeBot

@[simp]

theorem AffineSpace.asymptoticNhds_zero {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] [TopologicalSpace k] [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] : asymptoticNhds k P 0 = ⊤

theorem Filter.Tendsto.atTop_smul_nhds_tendsto_asymptoticNhds {k : Type u_1} {V : Type u_2} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [TopologicalSpace V] {α : Type u_4} {l : Filter α} [TopologicalSpace k] [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] {f : α → k} {g : α → V} {v : V} (hf : Tendsto f l atTop) (hg : Tendsto g l (nhds v)) : Tendsto (fun (x : α) => f x • g x) l (AffineSpace.asymptoticNhds k V v)

theorem Filter.Tendsto.atTop_smul_const_tendsto_asymptoticNhds {k : Type u_1} {V : Type u_2} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [TopologicalSpace V] {α : Type u_4} {l : Filter α} [TopologicalSpace k] [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] {f : α → k} (v : V) (hf : Tendsto f l atTop) : Tendsto (fun (x : α) => f x • v) l (AffineSpace.asymptoticNhds k V v)

theorem AffineSpace.asymptoticNhds_smul {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] [TopologicalSpace k] [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] (v : V) {c : k} (hc : 0 < c) : asymptoticNhds k P (c • v) = asymptoticNhds k P v

@[simp]

theorem AffineSpace.nhds_bind_asymptoticNhds {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] [TopologicalSpace k] [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] (v : V) : (nhds v).bind (asymptoticNhds k P) = asymptoticNhds k P v

@[simp]

theorem AffineSpace.asymptoticNhds_bind_nhds {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] [TopologicalSpace k] [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] [TopologicalSpace P] [IsTopologicalAddTorsor P] (v : V) : (asymptoticNhds k P v).bind nhds = asymptoticNhds k P v

@[simp]

theorem AffineSpace.asymptoticNhds_bind_asymptoticNhds {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] [TopologicalSpace k] [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] (v : V) : (asymptoticNhds k V v).bind (asymptoticNhds k P) = asymptoticNhds k P v

def asymptoticCone (k : Type u_1) {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] (s : Set P) : Set V

The set of directions v for which the set has points arbitrarily far in directions near v.

theorem mem_asymptoticCone_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] {v : V} {s : Set P} : v ∈ asymptoticCone k s ↔ ∃ᶠ (p : P) in AffineSpace.asymptoticNhds k P v, p ∈ s

@[simp]

theorem asymptoticCone_empty {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] : asymptoticCone k ∅ = ∅

theorem asymptoticCone_mono {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] {s t : Set P} (h : s ⊆ t) : asymptoticCone k s ⊆ asymptoticCone k t

theorem asymptoticCone_union {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] {s t : Set P} : asymptoticCone k (s ∪ t) = asymptoticCone k s ∪ asymptoticCone k t

theorem asymptoticCone_biUnion {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] {ι : Type u_4} {s : Set ι} (hs : s.Finite) (f : ι → Set P) : asymptoticCone k (⋃ i ∈ s, f i) = ⋃ i ∈ s, asymptoticCone k (f i)

theorem asymptoticCone_sUnion {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] {S : Set (Set P)} (hS : S.Finite) : asymptoticCone k (⋃₀ S) = ⋃ s ∈ S, asymptoticCone k s

theorem Finset.asymptoticCone_biUnion {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] {ι : Type u_4} (s : Finset ι) (f : ι → Set P) : asymptoticCone k (⋃ i ∈ s, f i) = ⋃ i ∈ s, asymptoticCone k (f i)

theorem asymptoticCone_iUnion_of_finite {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] {ι : Type u_4} [Finite ι] (f : ι → Set P) : asymptoticCone k (⋃ (i : ι), f i) = ⋃ (i : ι), asymptoticCone k (f i)

theorem zero_mem_asymptoticCone {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] [TopologicalSpace k] [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : Set P} : 0 ∈ asymptoticCone k s ↔ s.Nonempty

theorem asymptoticCone_nonempty {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] [TopologicalSpace k] [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : Set P} : (asymptoticCone k s).Nonempty ↔ s.Nonempty

@[simp]

theorem smul_mem_asymptoticCone_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] [TopologicalSpace k] [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : Set P} {c : k} {v : V} (hc : 0 < c) : c • v ∈ asymptoticCone k s ↔ v ∈ asymptoticCone k s

theorem smul_mem_asymptoticCone {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] [TopologicalSpace k] [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : Set P} {c : k} {v : V} (hc : 0 ≤ c) (h : v ∈ asymptoticCone k s) : c • v ∈ asymptoticCone k s

theorem asymptoticCone_eq_closure_of_forall_smul_mem {k : Type u_1} {V : Type u_2} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [TopologicalSpace V] [TopologicalSpace k] [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : Set V} (hs : ∀ (c : k), 0 < c → ∀ x ∈ s, c • x ∈ s) : asymptoticCone k s = closure s

theorem asymptoticCone_submodule {k : Type u_1} {V : Type u_2} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [TopologicalSpace V] [TopologicalSpace k] [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : Submodule k V} : asymptoticCone k ↑s = closure ↑s

theorem asymptoticCone_affineSubspace {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] [TopologicalSpace k] [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : AffineSubspace k P} (hs : (↑s).Nonempty) : asymptoticCone k ↑s = closure ↑s.direction

@[simp]

theorem asymptoticCone_univ {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] [TopologicalSpace k] [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] : asymptoticCone k Set.univ = Set.univ

theorem asymptoticCone_closure {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] [TopologicalSpace k] [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] [TopologicalSpace P] [IsTopologicalAddTorsor P] (s : Set P) : asymptoticCone k (closure s) = asymptoticCone k s

theorem isClosed_asymptoticCone {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] [TopologicalSpace k] [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : Set P} : IsClosed (asymptoticCone k s)

@[simp]

theorem asymptoticCone_asymptoticCone {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [TopologicalSpace V] [TopologicalSpace k] [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] (s : Set P) : asymptoticCone k (asymptoticCone k s) = asymptoticCone k s

theorem StarConvex.smul_vadd_mem_of_isClosed_of_mem_asymptoticCone {k : Type u_1} {V : Type u_2} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [TopologicalSpace k] [OrderTopology k] [AddCommGroup V] [Module k V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : Set V} {c : k} {v p : V} (hs₁ : StarConvex k p s) (hs₂ : IsClosed s) (hc : 0 ≤ c) (hv : v ∈ asymptoticCone k s) : c • v +ᵥ p ∈ s

If a closed set s is star-convex at p and v is in the asymptotic cone of s, then the ray of direction v starting from p is contained in s.

theorem Convex.smul_vadd_mem_of_isClosed_of_mem_asymptoticCone {k : Type u_1} {V : Type u_2} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [TopologicalSpace k] [OrderTopology k] [AddCommGroup V] [Module k V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : Set V} {c : k} {v p : V} (hs₁ : Convex k s) (hs₂ : IsClosed s) (hc : 0 ≤ c) (hv : v ∈ asymptoticCone k s) (hp : p ∈ s) : c • v +ᵥ p ∈ s

If v is in the asymptotic cone of a closed convex set s, then for every p ∈ s, the ray of direction v starting from p is contained in s.

theorem Convex.asymptoticCone {k : Type u_1} {V : Type u_2} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [TopologicalSpace k] [OrderTopology k] [AddCommGroup V] [Module k V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : Set V} (hs : Convex k s) : Convex k (asymptoticCone k s)

theorem Convex.smul_vadd_mem_of_mem_nhds_of_mem_asymptoticCone {k : Type u_1} {V : Type u_2} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [TopologicalSpace k] [OrderTopology k] [AddCommGroup V] [Module k V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : Set V} {c : k} {v p : V} (hs : Convex k s) (hc : 0 ≤ c) (hp : s ∈ nhds p) (hv : v ∈ asymptoticCone k s) : c • v +ᵥ p ∈ s

If v is in the asymptotic cone of a convex set s, then for every interior point p, the ray of direction v starting from p is contained in s.