English
If a map f tends uniformly to g on a set K and the real parts of g are bounded above on K, then exp composed with f also tends uniformly to exp composed with g on K.
Русский
Если f стремится равномерно к g на K и вещественная часть g ограничена сверху на K, то exp ∘ f сходится равномерно к exp ∘ g на K.
LaTeX
$$$TendstoUniformlyOn\\ (cexp \\circ f\\cdot)\\ (cexp \\circ g)\\ p\\ K \\quad\\text{при условии }\\ hf:\\ TendstoUniformlyOn f g p K \\text{ и } hg:\\ BddAbove \\<| (\\lambda x, (g x).re) '' K.$$$
Lean4
theorem comp_cexp {p : Filter ι} {g : α → ℂ} (hf : TendstoUniformlyOn f g p K)
(hg : BddAbove <| (fun x ↦ (g x).re) '' K) : TendstoUniformlyOn (cexp ∘ f ·) (cexp ∘ g) p K :=
by
obtain ⟨v, hv⟩ : ∃ v, ∀ x ∈ K, (g x).re ≤ v := hg.imp <| by simp [mem_upperBounds]
have : ∀ᶠ i in p, ∀ x ∈ K, (f i x).re ≤ v + 1 := hf.re.eventually_forall_le (lt_add_one v) hv
refine (UniformContinuousOn.cexp _).comp_tendstoUniformlyOn_eventually (by simpa) ?_ hf
exact fun x hx ↦ (hv x hx).trans (lt_add_one v).le
