English
Let K be a convex body containing 0 and u_n ≥ 0 with u_n → 0. Then the intersection over n of (1+u_n)·K equals K.
Русский
Пусть K — выпуклое тело, содержащее 0, и последовательность u_n ≥ 0 сходится к 0. Тогда ⋂_n (1+u_n)·K = K.
LaTeX
$$$\\bigcap_{n\\in\\mathbb{N}} (1+u_n)\\cdot K = K.$$$
Lean4
/-- Let `K` be a convex body that contains `0` and let `u n` be a sequence of nonnegative real
numbers that tends to `0`. Then the intersection of the dilated bodies `(1 + u n) • K` is equal
to `K`. -/
theorem iInter_smul_eq_self [T2Space V] {u : ℕ → ℝ≥0} (K : ConvexBody V) (h_zero : 0 ∈ K) (hu : Tendsto u atTop (𝓝 0)) :
⋂ n : ℕ, (1 + (u n : ℝ)) • (K : Set V) = K := by
ext x
refine ⟨fun h => ?_, fun h => ?_⟩
· obtain ⟨C, hC_pos, hC_bdd⟩ := K.isBounded.exists_pos_norm_le
rw [← K.isClosed.closure_eq, SeminormedAddCommGroup.mem_closure_iff]
rw [← NNReal.tendsto_coe, NormedAddCommGroup.tendsto_atTop] at hu
intro ε hε
obtain ⟨n, hn⟩ := hu (ε / C) (div_pos hε hC_pos)
obtain ⟨y, hyK, rfl⟩ := Set.mem_smul_set.mp (Set.mem_iInter.mp h n)
refine ⟨y, hyK, ?_⟩
rw [show (1 + u n : ℝ) • y - y = (u n : ℝ) • y by rw [add_smul, one_smul, add_sub_cancel_left], norm_smul,
Real.norm_eq_abs]
specialize hn n le_rfl
rw [lt_div_iff₀' hC_pos, mul_comm, NNReal.coe_zero, sub_zero, Real.norm_eq_abs] at hn
refine lt_of_le_of_lt ?_ hn
exact mul_le_mul_of_nonneg_left (hC_bdd _ hyK) (abs_nonneg _)
· refine Set.mem_iInter.mpr (fun n => Convex.mem_smul_of_zero_mem K.convex h_zero h ?_)
exact le_add_of_nonneg_right (by positivity)
