English
The tangent cone of a product contains the tangent cone of each factor via coordinate projections.
Русский
Касательный конус произведения содержит касательные конусы каждого фактор через координатные проекции.
LaTeX
$$$\\operatorname{MapsTo}(\\mathrm{single}_{\\mathbb{k}}(i)): \\operatorname{tangentCone}_{\\mathbb{k}}(s_i, x_i) \\to \\operatorname{tangentCone}_{\\mathbb{k}}(\\pi_{univ}(s), x) $$$
Lean4
/-- The tangent cone of a product contains the tangent cone of each factor. -/
theorem mapsTo_tangentConeAt_pi {ι : Type*} [DecidableEq ι] {E : ι → Type*} [∀ i, NormedAddCommGroup (E i)]
[∀ i, NormedSpace 𝕜 (E i)] {s : ∀ i, Set (E i)} {x : ∀ i, E i} {i : ι} (hi : ∀ j ≠ i, x j ∈ closure (s j)) :
MapsTo (LinearMap.single 𝕜 E i) (tangentConeAt 𝕜 (s i) (x i)) (tangentConeAt 𝕜 (Set.pi univ s) x) :=
by
rintro w ⟨c, d, hd, hc, hy⟩
have : ∀ n, ∀ j ≠ i, ∃ d', x j + d' ∈ s j ∧ ‖c n • d'‖ < (1 / 2 : ℝ) ^ n := fun n j hj ↦
by
rcases
mem_closure_iff_nhds.1 (hi j hj) _ (eventually_nhds_norm_smul_sub_lt (c n) (x j) (pow_pos one_half_pos n)) with
⟨z, hz, hzs⟩
exact ⟨z - x j, by simpa using hzs, by simpa using hz⟩
choose! d' hd's hcd' using this
refine ⟨c, fun n => Function.update (d' n) i (d n), hd.mono fun n hn j _ => ?_, hc, tendsto_pi_nhds.2 fun j => ?_⟩
· rcases em (j = i) with (rfl | hj) <;> simp [*]
· rcases em (j = i) with (rfl | hj)
· simp [hy]
· suffices Tendsto (fun n => c n • d' n j) atTop (𝓝 0) by simpa [hj]
refine squeeze_zero_norm (fun n => (hcd' n j hj).le) ?_
exact tendsto_pow_atTop_nhds_zero_of_lt_one one_half_pos.le one_half_lt_one
