English
Let f satisfy a P-L growth bound in the open fourth quadrant and be bounded on its boundary; then ∥f(z)∥ ≤ C on the closed fourth quadrant.
Русский
Пусть f удовлетворяет ростовому ограничению в открытом четвертом квадранте и ограничено на границе; тогда ∥f(z)∥ ≤ C на всей закрытой четвертой четверти.
LaTeX
$$$$\\forall z \\in \\{ \\Re z \\ge 0, \\Im z \\le 0 \\}, \\ ∥f(z)∥ ≤ C.$$$$
Lean4
/-- **Phragmen-Lindelöf principle** in the fourth quadrant. Let `f : ℂ → E` be a function such that
* `f` is differentiable in the open fourth quadrant and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open fourth quadrant
for some `c < 2`;
* `‖f z‖` is bounded from above by a constant `C` on the boundary of the fourth quadrant.
Then `‖f z‖` is bounded from above by the same constant on the closed fourth quadrant. -/
theorem quadrant_IV (hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Iio 0))
(hB : ∃ c < (2 : ℝ), ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)] fun z => expR (B * ‖z‖ ^ c))
(hre : ∀ x : ℝ, 0 ≤ x → ‖f x‖ ≤ C) (him : ∀ x : ℝ, x ≤ 0 → ‖f (x * I)‖ ≤ C) (hz_re : 0 ≤ z.re) (hz_im : z.im ≤ 0) :
‖f z‖ ≤ C := by
obtain ⟨z, rfl⟩ : ∃ z', -z' = z := ⟨-z, neg_neg z⟩
simp only [neg_re, neg_im, neg_nonpos, neg_nonneg] at hz_re hz_im
change ‖(f ∘ Neg.neg) z‖ ≤ C
have H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0) := fun w hw ↦ by
simpa only [mem_reProdIm, neg_re, neg_im, neg_lt_zero, neg_pos, mem_Ioi, mem_Iio] using hw
refine quadrant_II (hd.comp differentiable_neg.diffContOnCl H) ?_ (fun x hx => ?_) (fun x hx => ?_) hz_re hz_im
· rcases hB with ⟨c, hc, B, hO⟩
refine ⟨c, hc, B, ?_⟩
simpa only [Function.comp_def, norm_neg] using hO.comp_tendsto (tendsto_neg_cobounded.inf H.tendsto)
· rw [comp_apply, ← ofReal_neg]
exact hre (-x) (neg_nonneg.2 hx)
· rw [comp_apply, ← neg_mul, ← ofReal_neg]
exact him (-x) (neg_nonpos.2 hx)