English
Under the hypotheses of the fourth-quadrant P-L principle, f vanishes on the closed fourth quadrant if it vanishes on the boundary and satisfies the growth bound.
Русский
При условии принципа Прагмeн-Линдельоф в IV квадранте, если f=0 на границе и удовлетворяет ростовой границе, то f=0 и на всей закрытой четвертой четверти.
LaTeX
$$$$ \\forall z \\in \\{ \\Re z \\ge 0, \\Im z \\le 0 \\}, \\ f(z) = 0.$$$$
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 → 0` as `x : ℝ` tends to infinity.
Then `‖f z‖` is bounded from above by the same constant on the closed right half-plane.
See also `PhragmenLindelof.right_half_plane_of_bounded_on_real` for a stronger version. -/
theorem right_half_plane_of_tendsto_zero_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 : Tendsto (fun x : ℝ => f x) atTop (𝓝 0)) (him : ∀ x : ℝ, ‖f (x * I)‖ ≤ C) (hz : 0 ≤ z.re) : ‖f z‖ ≤ C := by
/- We are going to apply the Phragmen-Lindelöf principle in the first and fourth quadrants.
The lemmas immediately imply that for any upper estimate `C'` on `‖f x‖`, `x : ℝ`, `0 ≤ x`,
the number `max C C'` is an upper estimate on `f` in the whole right half-plane. -/
revert z
have hle : ∀ C', (∀ x : ℝ, 0 ≤ x → ‖f x‖ ≤ C') → ∀ z : ℂ, 0 ≤ z.re → ‖f z‖ ≤ max C C' := fun C' hC' z hz ↦
by
rcases hexp with ⟨c, hc, B, hO⟩
rcases le_total z.im 0 with h | h
· refine
quadrant_IV (hd.mono fun _ => And.left) ⟨c, hc, B, ?_⟩ (fun x hx => (hC' x hx).trans <| le_max_right _ _)
(fun x _ => (him x).trans (le_max_left _ _)) hz h
exact hO.mono (inf_le_inf_left _ <| principal_mono.2 fun _ => And.left)
· refine
quadrant_I (hd.mono fun _ => And.left) ⟨c, hc, B, ?_⟩ (fun x hx => (hC' x hx).trans <| le_max_right _ _)
(fun x _ => (him x).trans (le_max_left _ _)) hz h
exact
hO.mono
(inf_le_inf_left _ <| principal_mono.2 fun _ => And.left)
-- Since `f` is continuous on `Ici 0` and `‖f x‖` tends to zero as `x → ∞`,
-- the norm `‖f x‖` takes its maximum value at some `x₀ : ℝ`.
obtain ⟨x₀, hx₀, hmax⟩ : ∃ x : ℝ, 0 ≤ x ∧ ∀ y : ℝ, 0 ≤ y → ‖f y‖ ≤ ‖f x‖ :=
by
have hfc : ContinuousOn (fun x : ℝ => f x) (Ici 0) :=
by
refine hd.continuousOn.comp continuous_ofReal.continuousOn fun x hx => ?_
rwa [closure_setOf_lt_re]
by_cases h₀ : ∀ x : ℝ, 0 ≤ x → f x = 0
· refine ⟨0, le_rfl, fun y hy => ?_⟩; rw [h₀ y hy, h₀ 0 le_rfl]
push_neg at h₀
rcases h₀ with ⟨x₀, hx₀, hne⟩
have hlt : ‖(0 : E)‖ < ‖f x₀‖ := by rwa [norm_zero, norm_pos_iff]
suffices ∀ᶠ x : ℝ in cocompact ℝ ⊓ 𝓟 (Ici 0), ‖f x‖ ≤ ‖f x₀‖ by
simpa only [exists_prop] using hfc.norm.exists_isMaxOn' isClosed_Ici hx₀ this
rw [cocompact_eq_atBot_atTop, inf_sup_right, (disjoint_atBot_principal_Ici (0 : ℝ)).eq_bot, bot_sup_eq]
exact (hre.norm.eventually <| ge_mem_nhds hlt).filter_mono inf_le_left
rcases le_or_gt ‖f x₀‖ C with h | h
· -- If `‖f x₀‖ ≤ C`, then `hle` implies the required estimate
simpa only [max_eq_left h] using hle _ hmax
· -- Otherwise, `‖f z‖ ≤ ‖f x₀‖` for all `z` in the right half-plane due to `hle`.
replace hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} x₀ :=
by
rintro z (hz : 0 < z.re)
simpa [max_eq_right h.le] using hle _ hmax _ hz.le
have : ‖f 0‖ = ‖f x₀‖ := by
apply norm_eq_norm_of_isMaxOn_of_ball_subset hd hmax
intro z hz
rw [mem_ball, dist_zero_left, dist_eq, Complex.norm_of_nonneg hx₀] at hz
rw [mem_setOf_eq]
contrapose! hz
calc
x₀ ≤ x₀ - z.re := (le_sub_self_iff _).2 hz
_ ≤ |x₀ - z.re| := (le_abs_self _)
_ = |(z - x₀).re| := by rw [sub_re, ofReal_re, _root_.abs_sub_comm]
_ ≤ ‖z - x₀‖ :=
abs_re_le_norm
_
-- Thus we have `C < ‖f x₀‖ = ‖f 0‖ ≤ C`. Contradiction completes the proof.
refine (h.not_ge <| this ▸ ?_).elim
simpa using him 0
