Lean4
/-- **Phragmen-Lindelöf principle** in the first quadrant. Let `f : ℂ → E` be a function such that
* `f` is differentiable in the open first quadrant and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open first quadrant
for some `c < 2`;
* `‖f z‖` is bounded from above by a constant `C` on the boundary of the first quadrant.
Then `‖f z‖` is bounded from above by the same constant on the closed first quadrant. -/
nonrec theorem quadrant_I (hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0))
(hB : ∃ c < (2 : ℝ), ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z => expR (B * ‖z‖ ^ c))
(hre : ∀ x : ℝ, 0 ≤ x → ‖f x‖ ≤ C) (him : ∀ x : ℝ, 0 ≤ x → ‖f (x * I)‖ ≤ C) (hz_re : 0 ≤ z.re) (hz_im : 0 ≤ z.im) :
‖f z‖ ≤ C := by
-- The case `z = 0` is trivial.
rcases eq_or_ne z 0 with (rfl | hzne)
· exact hre 0 le_rfl
obtain ⟨ζ, hζ, rfl⟩ : ∃ ζ : ℂ, ζ.im ∈ Icc 0 (π / 2) ∧ exp ζ = z :=
by
refine ⟨log z, ?_, exp_log hzne⟩
rw [log_im]
exact
⟨arg_nonneg_iff.2 hz_im, arg_le_pi_div_two_iff.2 (Or.inl hz_re)⟩
-- We are going to apply `PhragmenLindelof.horizontal_strip` to `f ∘ Complex.exp` and `ζ`.
change ‖(f ∘ exp) ζ‖ ≤ C
have H : MapsTo exp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0) := fun z hz ↦
by
rw [mem_reProdIm, exp_re, exp_im, mem_Ioi, mem_Ioi]
have : 0 < Real.cos z.im := Real.cos_pos_of_mem_Ioo ⟨by linarith [hz.1, hz.2], hz.2⟩
have : 0 < Real.sin z.im := Real.sin_pos_of_mem_Ioo ⟨hz.1, hz.2.trans (half_lt_self Real.pi_pos)⟩
constructor <;> positivity
refine horizontal_strip (hd.comp differentiable_exp.diffContOnCl H) ?_ ?_ ?_ hζ.1 hζ.2
· -- The estimate `hB` on `f` implies the required estimate on
-- `f ∘ exp` with the same `c` and `B' = max B 0`.
rw [sub_zero, div_div_cancel₀ Real.pi_pos.ne']
rcases hB with ⟨c, hc, B, hO⟩
refine ⟨c, hc, max B 0, ?_⟩
rw [← comap_comap, comap_abs_atTop, comap_sup, inf_sup_right]
-- We prove separately the estimates as `ζ.re → ∞` and as `ζ.re → -∞`
refine
IsBigO.sup ?_ <| (hO.comp_tendsto <| tendsto_exp_comap_re_atTop.inf H.tendsto).trans <| .of_norm_eventuallyLE ?_
· -- For the estimate as `ζ.re → -∞`, note that `f` is continuous within the first quadrant at
-- zero, hence `f (exp ζ)` has a limit as `ζ.re → -∞`, `0 < ζ.im < π / 2`.
have hc : ContinuousWithinAt f (Ioi 0 ×ℂ Ioi 0) 0 :=
by
refine (hd.continuousOn _ ?_).mono subset_closure
simp [closure_reProdIm, mem_reProdIm]
refine
((hc.tendsto.comp <| tendsto_exp_comap_re_atBot.inf H.tendsto).isBigO_one ℝ).trans (isBigO_of_le _ fun w => ?_)
rw [norm_one, Real.norm_of_nonneg (Real.exp_pos _).le, Real.one_le_exp_iff]
positivity
· -- For the estimate as `ζ.re → ∞`, we reuse the upper estimate on `f`
simp only [EventuallyLE, eventually_inf_principal, eventually_comap, comp_apply,
Real.norm_of_nonneg (Real.exp_pos _).le, norm_exp, ← Real.exp_mul, Real.exp_le_exp]
filter_upwards [eventually_ge_atTop 0] with x hx z hz _
rw [hz, abs_of_nonneg hx, mul_comm _ c]
gcongr; apply le_max_left
· -- If `ζ.im = 0`, then `Complex.exp ζ` is a positive real number
intro ζ hζ; lift ζ to ℝ using hζ
rw [comp_apply, ← ofReal_exp]
exact hre _ (Real.exp_pos _).le
· -- If `ζ.im = π / 2`, then `Complex.exp ζ` is a purely imaginary number with positive `im`
intro ζ hζ
rw [← re_add_im ζ, hζ, comp_apply, exp_add_mul_I, ← ofReal_cos, ← ofReal_sin, Real.cos_pi_div_two,
Real.sin_pi_div_two, ofReal_zero, ofReal_one, one_mul, zero_add, ← ofReal_exp]
exact him _ (Real.exp_pos _).le
