English
For any g, if f and g satisfy a right-half-plane P-L bound and f−g decays superexponentially, then f ≡ g on the right half-plane boundary, hence on the closure.
Русский
Если f и g удовлетворяют правой полуплоскости ограничению Прагмена-Линдельоф и разность f−g исчезает суперэкспоненциально, то f≡g на границе правой полуплоскости и, следовательно, на всей её замыкании.
LaTeX
$$$$ \\text{If } f-g \\text{ decays superexponentially and bounds hold, then } f \equiv g \\text{ on } \\{ z : \\Re z \\ge 0 \\}. $$$$
Lean4
/-- **Phragmen-Lindelöf principle** in the right half-plane. Let `f g : ℂ → E` be functions such
that
* `f` and `g` are differentiable in the open right half-plane and are continuous on its closure;
* `‖f z‖` and `‖g z‖` are bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open right
half-plane for some `c < 2`;
* `‖f z‖` and `‖g z‖` are bounded from above by constants on the imaginary axis;
* `f x - g x`, `x : ℝ`, tends to zero superexponentially fast as `x → ∞`:
for any natural `n`, `exp (n * x) * ‖f x - g x‖` tends to zero as `x → ∞`.
Then `f` is equal to `g` on the closed right half-plane. -/
theorem eqOn_right_half_plane_of_superexponential_decay {g : ℂ → E} (hfd : DiffContOnCl ℂ f {z | 0 < z.re})
(hgd : DiffContOnCl ℂ g {z | 0 < z.re})
(hfexp : ∃ c < (2 : ℝ), ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c))
(hgexp : ∃ c < (2 : ℝ), ∃ B, g =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c))
(hre : SuperpolynomialDecay atTop expR fun x => ‖f x - g x‖) (hfim : ∃ C, ∀ x : ℝ, ‖f (x * I)‖ ≤ C)
(hgim : ∃ C, ∀ x : ℝ, ‖g (x * I)‖ ≤ C) : EqOn f g {z : ℂ | 0 ≤ z.re} :=
by
suffices EqOn (f - g) 0 {z : ℂ | 0 ≤ z.re} by simpa only [EqOn, Pi.sub_apply, Pi.zero_apply, sub_eq_zero] using this
refine eq_zero_on_right_half_plane_of_superexponential_decay (hfd.sub hgd) ?_ hre ?_
· exact isBigO_sub_exp_rpow hfexp hgexp
· rcases hfim with ⟨Cf, hCf⟩; rcases hgim with ⟨Cg, hCg⟩
exact ⟨Cf + Cg, fun x => norm_sub_le_of_le (hCf x) (hCg x)⟩
