English
Let f satisfy a P-L growth bound in the open second quadrant, and assume ∥f(z)∥ ≤ C on the boundary of the second quadrant. Then ∥f(z)∥ ≤ C on the closed second quadrant.
Русский
Пусть f удовлетворяет ростовой условиП Линдельф в открытой второй четверти, а на границе второй четверти имеет верхнюю границу ∥f(z)∥ ≤ C. Тогда ∥f(z)∥ ≤ C на всей закрытой второй четверти.
LaTeX
$$$$\\forall z: \\Re z \\le 0, \\Im z \\ge 0, \\ ‖f(z)‖ ≤ C.$$$$
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 `c < 2`;
* `‖f z‖` is bounded from above by a constant `C` on the boundary of the second quadrant.
Then `‖f z‖` is bounded from above by the same constant on the closed second quadrant. -/
theorem 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‖ ≤ C) (him : ∀ x : ℝ, 0 ≤ x → ‖f (x * I)‖ ≤ C) (hz_re : z.re ≤ 0) (hz_im : 0 ≤ z.im) :
‖f z‖ ≤ C := by
obtain ⟨z, rfl⟩ : ∃ z', z' * I = z := ⟨z / I, div_mul_cancel₀ _ I_ne_zero⟩
simp only [mul_I_re, mul_I_im, neg_nonpos] at hz_re hz_im
change ‖(f ∘ (· * I)) z‖ ≤ C
have H : MapsTo (· * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0) := fun w hw ↦ by
simpa only [mem_reProdIm, mul_I_re, mul_I_im, neg_lt_zero, mem_Iio] using hw.symm
rcases hB with ⟨c, hc, B, hO⟩
refine
quadrant_I (hd.comp (differentiable_id.mul_const _).diffContOnCl H) ⟨c, hc, B, ?_⟩ him (fun x hx => ?_) hz_im hz_re
·
simpa only [Function.comp_def, norm_mul, norm_I, mul_one] using
hO.comp_tendsto ((tendsto_mul_right_cobounded I_ne_zero).inf H.tendsto)
· rw [comp_apply, mul_assoc, I_mul_I, mul_neg_one, ← ofReal_neg]
exact hre _ (neg_nonpos.2 hx)