English
Let s > 0. There exist positive numbers M and ε such that for every complex number z with Re z > 1 − ε and z in the Stolz cone with parameter s, one has z ∈ StolzSet(M).
Русский
Пусть s > 0. Существуют положительные M и ε, такие что для каждого z ∈ ℂ, если Re z > 1 − ε и z ∈ stolzCone(s), то z ∈ stolzSet(M).
LaTeX
$$$\\\\exists M>0, \\\\exists \\varepsilon>0: \\\\{ z \in \\mathbb{C} : 1-\\\\varepsilon < \\operatorname{Re} z \\\\} \\cap \\\\operatorname{stolzCone}(s) \\\\subseteq \\\\operatorname{stolzSet}(M).$$$
Lean4
theorem stolzCone_subset_stolzSet_aux {s : ℝ} (hs : 0 < s) :
∃ M ε, 0 < M ∧ 0 < ε ∧ {z : ℂ | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M :=
by
peel stolzCone_subset_stolzSet_aux' s with M ε hM hε H
rintro z ⟨hzl, hzr⟩
rw [Set.mem_setOf_eq, sub_lt_comm, ← one_re, ← sub_re] at hzl
rw [stolzCone, Set.mem_setOf_eq, ← one_re, ← sub_re] at hzr
replace H := H (1 - z).re z.im ((mul_pos_iff_of_pos_left hs).mp <| (abs_nonneg z.im).trans_lt hzr) hzl hzr
have h : z.im ^ 2 = (1 - z).im ^ 2 := by simp only [sub_im, one_im, zero_sub, neg_sq]
rw [h, ← norm_eq_sqrt_sq_add_sq, ← h, sub_re, one_re, sub_sub_cancel, ← norm_eq_sqrt_sq_add_sq] at H
exact ⟨sub_pos.mp <| (mul_pos_iff_of_pos_left hM).mp <| (norm_nonneg _).trans_lt H, H⟩
