English
If f and g satisfy exponential bounds and boundary equality in a vertical strip, then they coincide on the closed vertical strip.
Русский
Если f и g удовлетворяют экспоненциальным ограничениям и совпадают на границе в вертикальной полосе, то они совпадают на замкнутой вертикальной полосе.
LaTeX
$$EqOn f g (Set.preimage Complex.re (Set.Icc a b))$$
Lean4
/-- **Phragmen-Lindelöf principle** in a strip `U = {z : ℂ | a < re z < b}`.
Let `f g : ℂ → E` be functions such that
* `f` and `g` are differentiable on `U` and are continuous on its closure;
* `‖f z‖` and `‖g z‖` are bounded from above by `A * exp(B * exp(c * |im z|))` on `U` for some
`c < π / (b - a)`;
* `f z = g z` on the boundary of `U`.
Then `f` is equal to `g` on the closed strip `{z : ℂ | a ≤ re z ≤ b}`.
-/
theorem eqOn_vertical_strip {g : ℂ → E} (hdf : DiffContOnCl ℂ f (re ⁻¹' Ioo a b))
(hBf :
∃ c < π / (b - a),
∃ B, f =O[comap (_root_.abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.im|)))
(hdg : DiffContOnCl ℂ g (re ⁻¹' Ioo a b))
(hBg :
∃ c < π / (b - a),
∃ B, g =O[comap (_root_.abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.im|)))
(ha : ∀ z : ℂ, re z = a → f z = g z) (hb : ∀ z : ℂ, re z = b → f z = g z) : EqOn f g (re ⁻¹' Icc a b) :=
fun _z hz =>
sub_eq_zero.1
(eq_zero_on_vertical_strip (hdf.sub hdg) (isBigO_sub_exp_exp hBf hBg) (fun w hw => sub_eq_zero.2 (ha w hw))
(fun w hw => sub_eq_zero.2 (hb w hw)) hz)
