English
If f and g satisfy the same growth bounds and agree on the boundary, they are equal on the horizontal strip closure.
Русский
Если f и g удовлетворяют одинаковым экспоненциальным ограничениям и совпадают на границе, они равны на замкнутой горизонтальной полосе.
LaTeX
$$EqOn f g (im ⁻¹' Icc a b)$$
Lean4
/-- **Phragmen-Lindelöf principle** in a strip `U = {z : ℂ | a < re 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 * |im z|))` on `U` for some `c < π / (b - a)`;
* `‖f z‖` is bounded from above by a constant `C` on the boundary of `U`.
Then `‖f z‖` is bounded by the same constant on the closed strip
`{z : ℂ | a ≤ re z ≤ b}`. Moreover, it suffices to verify the second assumption
only for sufficiently large values of `|im z|`.
-/
theorem vertical_strip (hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b))
(hB :
∃ c < π / (b - a),
∃ B, f =O[comap (_root_.abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.im|)))
(hle_a : ∀ z : ℂ, re z = a → ‖f z‖ ≤ C) (hle_b : ∀ z, re z = b → ‖f z‖ ≤ C) (hza : a ≤ re z) (hzb : re z ≤ b) :
‖f z‖ ≤ C := by
suffices ‖f (z * I * -I)‖ ≤ C by simpa [mul_assoc] using this
have H : MapsTo (· * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b) := fun z hz ↦ by simpa using hz
refine
horizontal_strip (f := fun z ↦ f (z * -I)) (hfd.comp (differentiable_id.mul_const _).diffContOnCl H) ?_
(fun z hz => hle_a _ ?_) (fun z hz => hle_b _ ?_) ?_ ?_
· rcases hB with ⟨c, hc, B, hO⟩
refine ⟨c, hc, B, ?_⟩
have : Tendsto (· * -I) (comap (|re ·|) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) (comap (|im ·|) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) :=
by
refine (tendsto_comap_iff.2 ?_).inf H.tendsto
simpa [Function.comp_def] using tendsto_comap
simpa [Function.comp_def] using hO.comp_tendsto this
all_goals simpa
