English
Llog of the norm is little-o of Re z along the filter.
Русский
Логарифм нормы есть маленькое o по отношению к Re z вдоль фильтра.
LaTeX
$$$\\forall l:\\,\\mathsf{IsExpCmpFilter}\\ l \\to (\\lambda z: \\log \\|z\\|) =_o_l (\\operatorname{re})$$$
Lean4
/-- If `l : Filter ℂ` is an "exponential comparison filter", then $\log |z| =o(ℜ z)$ along `l`.
This is the main lemma in the proof of `Complex.IsExpCmpFilter.isLittleO_cpow_exp` below.
-/
theorem isLittleO_log_norm_re (hl : IsExpCmpFilter l) : (fun z => Real.log ‖z‖) =o[l] re :=
calc
(fun z => Real.log ‖z‖) =O[l] fun z => Real.log (√2) + Real.log (max z.re |z.im|) :=
.of_norm_eventuallyLE <|
(hl.tendsto_re.eventually_ge_atTop 1).mono fun z hz =>
by
have h2 : 0 < √2 := by simp
have hz' : 1 ≤ ‖z‖ := hz.trans (re_le_norm z)
have hm₀ : 0 < max z.re |z.im| := lt_max_iff.2 (Or.inl <| one_pos.trans_le hz)
simp only [Real.norm_of_nonneg (Real.log_nonneg hz')]
rw [← Real.log_mul, Real.log_le_log_iff, ← abs_of_nonneg (le_trans zero_le_one hz)]
exacts [norm_le_sqrt_two_mul_max z, one_pos.trans_le hz', mul_pos h2 hm₀, h2.ne', hm₀.ne']
_ =o[l] re :=
IsLittleO.add (isLittleO_const_left.2 <| Or.inr <| hl.tendsto_abs_re) <|
isLittleO_iff_nat_mul_le.2 fun n =>
by
filter_upwards [isLittleO_iff_nat_mul_le'.1 hl.isLittleO_log_re_re n, hl.abs_im_pow_eventuallyLE_exp_re n,
hl.tendsto_re.eventually_gt_atTop 1] with z hre him h₁
rcases le_total |z.im| z.re with hle | hle
· rwa [max_eq_left hle]
· have H : 1 < |z.im| := h₁.trans_le hle
norm_cast at *
rwa [max_eq_right hle, Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (Real.log_pos H), ← Real.log_pow,
Real.log_le_iff_le_exp (pow_pos (one_pos.trans H) _), abs_of_pos (one_pos.trans h₁)]
