English
In quadrant IV, the P-L principle gives the same bound ∥f(z)∥ ≤ C for all z with Re z ≥ 0, Im z ≤ 0, provided boundary bound holds.
Русский
Во IV квадранте принцип Прагмeн-Линдельоф сохраняет верхнюю границу ∥f(z)∥ ≤ C для всех z с Re z ≥ 0, Im z ≤ 0, при условии границы.
LaTeX
$$$$ \\forall z \\text{ with } \\Re z \\ge 0, \\Im z \\le 0, \\ ∥f(z)∥ \\le C.$$$$
Lean4
/-- **Phragmen-Lindelöf principle** in the right half-plane. Let `f : ℂ → E` be a function such that
* `f` is differentiable in the open right half-plane and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open right half-plane
for some `c < 2`;
* `‖f z‖` is bounded from above by a constant `C` on the imaginary axis;
* `‖f x‖` is bounded from above by a constant for large real values of `x`.
Then `‖f z‖` is bounded from above by `C` on the closed right half-plane.
See also `PhragmenLindelof.right_half_plane_of_tendsto_zero_on_real` for a weaker version. -/
theorem right_half_plane_of_bounded_on_real (hd : DiffContOnCl ℂ f {z | 0 < z.re})
(hexp : ∃ c < (2 : ℝ), ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c))
(hre : IsBoundedUnder (· ≤ ·) atTop fun x : ℝ => ‖f x‖) (him : ∀ x : ℝ, ‖f (x * I)‖ ≤ C) (hz : 0 ≤ z.re) :
‖f z‖ ≤ C := by
-- For each `ε < 0`, the function `fun z ↦ exp (ε * z) • f z` satisfies assumptions of
-- `right_half_plane_of_tendsto_zero_on_real`, hence `‖exp (ε * z) • f z‖ ≤ C` for all `ε < 0`.
-- Taking the limit as `ε → 0`, we obtain the required inequality.
suffices ∀ᶠ ε : ℝ in 𝓝[<] 0, ‖exp (ε * z) • f z‖ ≤ C
by
refine le_of_tendsto (Tendsto.mono_left ?_ nhdsWithin_le_nhds) this
apply ((continuous_ofReal.mul continuous_const).cexp.smul continuous_const).norm.tendsto'
simp
filter_upwards [self_mem_nhdsWithin] with ε ε₀; change ε < 0 at ε₀
set g : ℂ → E := fun z => exp (ε * z) • f z; change ‖g z‖ ≤ C
replace hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re} := (differentiable_id.const_mul _).cexp.diffContOnCl.smul hd
have hgn : ∀ z, ‖g z‖ = expR (ε * z.re) * ‖f z‖ := fun z ↦ by rw [norm_smul, norm_exp, re_ofReal_mul]
refine right_half_plane_of_tendsto_zero_on_real hd ?_ ?_ (fun y => ?_) hz
· rcases hexp with ⟨c, hc, B, hO⟩
refine ⟨c, hc, B, .trans (.of_bound' ?_) hO⟩
refine eventually_inf_principal.2 <| Eventually.of_forall fun z hz => ?_
rw [hgn]
refine mul_le_of_le_one_left (norm_nonneg _) (Real.exp_le_one_iff.2 ?_)
exact mul_nonpos_of_nonpos_of_nonneg ε₀.le (le_of_lt hz)
· simp_rw [g, ← ofReal_mul, ← ofReal_exp, coe_smul]
have h₀ : Tendsto (fun x : ℝ => expR (ε * x)) atTop (𝓝 0) :=
Real.tendsto_exp_atBot.comp (tendsto_const_nhds.neg_mul_atTop ε₀ tendsto_id)
exact h₀.zero_smul_isBoundedUnder_le hre
· rw [hgn, re_ofReal_mul, I_re, mul_zero, mul_zero, Real.exp_zero, one_mul]
exact him y
