English
In the first quadrant, a differentiable function with appropriate exponential bounds is bounded by C.
Русский
В первой четверти функция, дифференцируема и удовлетворяет экспоненциальным ограничениям, ограничена константой C.
LaTeX
$$Quadrant_I statement: differentiable f on Ioi 0 ×ℂ Ioi 0 with exponential bounds implies ‖f z‖ ≤ C in first quadrant$$
Lean4
/-- **Phragmen-Lindelöf principle** in a strip `U = {z : ℂ | a < im z < b}`.
Let `f : ℂ → E` be a function such that
* `f` is differentiable on `U` and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * exp(c * |re z|))` on `U` for some `c < π / (b - a)`;
* `f z = 0` on the boundary of `U`.
Then `f` is equal to zero on the closed strip `{z : ℂ | a ≤ im z ≤ b}`.
-/
theorem eq_zero_on_horizontal_strip (hd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b))
(hB :
∃ c < π / (b - a),
∃ B, f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.re|)))
(ha : ∀ z : ℂ, z.im = a → f z = 0) (hb : ∀ z : ℂ, z.im = b → f z = 0) : EqOn f 0 (im ⁻¹' Icc a b) := fun _z hz =>
norm_le_zero_iff.1 <|
horizontal_strip hd hB (fun z hz => (ha z hz).symm ▸ norm_zero.le) (fun z hz => (hb z hz).symm ▸ norm_zero.le) hz.1
hz.2
