English
Let E be a normed additive group equipped with a complex‑vector space structure. Let f: C → E be differentiable on the open first quadrant and continuous on its closure; suppose there exist A > 0, B > 0 and c < 2 such that ∥f(z)∥ ≤ A e^{B ∥z∥^c} for z in the open first quadrant, and f vanishes on the boundary of the first quadrant. Then f vanishes on the closed first quadrant, i.e. f(z) = 0 for all z with Re z ≥ 0 and Im z ≥ 0.
Русский
Пусть E — нормированная аддитивная группа с комплексным векторным пространством; пусть f: C → E дифференцируема на открытой первой четверти и непрерывна на её замыкании; существует A > 0, B > 0 и c < 2 такие, что ∥f(z)∥ ≤ A e^{B ∥z∥^c} на открытой первой четверти, и f = 0 на границе этой четверти. Тогда f = 0 на всей замкнутой первой четверти, т.е. f(z) = 0 для всех z с Re z ≥ 0 и Im z ≥ 0.
LaTeX
$$$$\\forall z \\in \\{w \\in \\mathbb{C} : \\Re w \\ge 0, \\Im w \\ge 0\\}, \\ f(z) = 0.$$$$
Lean4
/-- **Phragmen-Lindelöf principle** in the first quadrant. Let `f : ℂ → E` be a function such that
* `f` is differentiable in the open first quadrant and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open first quadrant
for some `A`, `B`, and `c < 2`;
* `f` is equal to zero on the boundary of the first quadrant.
Then `f` is equal to zero on the closed first quadrant. -/
theorem eq_zero_on_quadrant_I (hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0))
(hB : ∃ c < (2 : ℝ), ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z => expR (B * ‖z‖ ^ c))
(hre : ∀ x : ℝ, 0 ≤ x → f x = 0) (him : ∀ x : ℝ, 0 ≤ x → f (x * I) = 0) : EqOn f 0 {z | 0 ≤ z.re ∧ 0 ≤ z.im} :=
fun _z hz =>
norm_le_zero_iff.1 <|
quadrant_I hd hB (fun x hx => norm_le_zero_iff.2 <| hre x hx) (fun x hx => norm_le_zero_iff.2 <| him x hx) hz.1 hz.2
