English
If f and g have the same boundary values in the open second quadrant and obey the same growth bound, then f ≡ g on the closed second quadrant.
Русский
Если f и g совпадают на границе открытой второй четверти и подчиняются той же ростовой границе, то f ≡ g на всей закрытой второй четверти.
LaTeX
$$$$\\forall z \\in \\{\\Re z \\le 0, \\Im z \\ge 0\\}, \\ f(z) = g(z).$$$$
Lean4
/-- **Phragmen-Lindelöf principle** in the second quadrant. Let `f : ℂ → E` be a function such that
* `f` is differentiable in the open second quadrant and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open second quadrant
for some `A`, `B`, and `c < 2`;
* `f` is equal to zero on the boundary of the second quadrant.
Then `f` is equal to zero on the closed second quadrant. -/
theorem eq_zero_on_quadrant_II (hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0))
(hB : ∃ c < (2 : ℝ), ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * ‖z‖ ^ c))
(hre : ∀ x : ℝ, x ≤ 0 → f x = 0) (him : ∀ x : ℝ, 0 ≤ x → f (x * I) = 0) : EqOn f 0 {z | z.re ≤ 0 ∧ 0 ≤ z.im} :=
fun _z hz =>
norm_le_zero_iff.1 <|
quadrant_II 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
