English
The tangent cone at a non-isolated point always contains 0.
Русский
Касательный конус в точке неизолированной всегда содержит 0.
LaTeX
$$$0 \\in \\operatorname{tangentCone}_{\\mathbb{k}}(s, x)$$$
Lean4
/-- The tangent cone at a non-isolated point contains `0`. -/
theorem zero_mem_tangentCone {s : Set E} {x : E} (hx : x ∈ closure s) : 0 ∈ tangentConeAt 𝕜 s x := by
/- Take a sequence `d n` tending to `0` such that `x + d n ∈ s`. Taking `c n` of the order
of `1 / (d n) ^ (1/2)`, then `c n` tends to infinity, but `c n • d n` tends to `0`. By definition,
this shows that `0` belongs to the tangent cone. -/
obtain ⟨u, -, hu, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n ∧ u n < 1) ∧ Tendsto u atTop (𝓝 (0 : ℝ)) :=
exists_seq_strictAnti_tendsto' one_pos
choose u_pos u_lt_one using hu
choose v hvs hvu using fun n ↦ Metric.mem_closure_iff.mp hx _ (mul_pos (u_pos n) (u_pos n))
let d n := v n - x
let ⟨r, hr⟩ := exists_one_lt_norm 𝕜
have A n := exists_nat_pow_near (one_le_inv_iff₀.mpr ⟨u_pos n, (u_lt_one n).le⟩) hr
choose m hm_le hlt_m using A
set c := fun n ↦ r ^ (m n + 1)
have c_lim : Tendsto (fun n ↦ ‖c n‖) atTop atTop :=
by
simp only [c, norm_pow]
refine tendsto_atTop_mono (fun n ↦ (hlt_m n).le) <| .inv_tendsto_nhdsGT_zero ?_
exact tendsto_nhdsWithin_iff.mpr ⟨u_lim, .of_forall u_pos⟩
refine ⟨c, d, .of_forall <| by simpa [d], c_lim, ?_⟩
have Hle n : ‖c n • d n‖ ≤ ‖r‖ * u n := by
specialize u_pos n
calc
‖c n • d n‖ ≤ (u n)⁻¹ * ‖r‖ * (u n * u n) :=
by
simp only [c, norm_smul, norm_pow, pow_succ, norm_mul, d, ← dist_eq_norm']
gcongr
exacts [hm_le n, (hvu n).le]
_ = ‖r‖ * u n := by field_simp
refine squeeze_zero_norm Hle ?_
simpa using tendsto_const_nhds.mul u_lim
