l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
⊢ ‖Real.log (↑abs z)‖ ≤ 1 * ‖Real.log (Real.sqrt 2) + Real.log (max z.re (Abs.abs z.im))‖
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
⊢ ‖Real.log (↑abs z)‖ ≤ 1 * ‖Real.log (Real.sqrt 2) + Real.log (max z.re (Abs.abs z.im))‖
have h2 : 0 < Real.sqrt 2 := by simp
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
⊢ ‖Real.log (↑abs z)‖ ≤ 1 * ‖Real.log (Real.sqrt 2) + Real.log (max z.re (Abs.abs z.im))‖
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
⊢ ‖Real.log (↑abs z)‖ ≤ 1 * ‖Real.log (Real.sqrt 2) + Real.log (max z.re (Abs.abs z.im))‖
have hz' : 1 ≤ abs z := hz.trans (re_le_abs z)
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
⊢ ‖Real.log (↑abs z)‖ ≤ 1 * ‖Real.log (Real.sqrt 2) + Real.log (max z.re (Abs.abs z.im))‖
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
⊢ ‖Real.log (↑abs z)‖ ≤ 1 * ‖Real.log (Real.sqrt 2) + Real.log (max z.re (Abs.abs z.im))‖
have _ : 0 < abs z := one_pos.trans_le hz'
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re (Abs.abs z.im)
⊢ ‖Real.log (↑abs z)‖ ≤ 1 * ‖Real.log (Real.sqrt 2) + Real.log (max z.re (Abs.abs z.im))‖
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
⊢ ‖Real.log (↑abs z)‖ ≤ 1 * ‖Real.log (Real.sqrt 2) + Real.log (max z.re (Abs.abs z.im))‖
have hm₀ : 0 < max z.re (|z.im|) := lt_max_iff.2 (Or.inl <| one_pos.trans_le hz)
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re (Abs.abs z.im)
⊢ Real.log (↑abs z) ≤ ‖Real.log (Real.sqrt 2) + Real.log (max z.re (Abs.abs z.im))‖
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re (Abs.abs z.im)
⊢ ‖Real.log (↑abs z)‖ ≤ 1 * ‖Real.log (Real.sqrt 2) + Real.log (max z.re (Abs.abs z.im))‖
rw [one_mul, Real.norm_eq_abs, _root_.abs_of_nonneg (Real.log_nonneg hz')]
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re (Abs.abs z.im)
⊢ Real.log (↑abs z) ≤ Real.log (Real.sqrt 2) + Real.log (max z.re (Abs.abs z.im))
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re (Abs.abs z.im)
⊢ Real.log (↑abs z) ≤ ‖Real.log (Real.sqrt 2) + Real.log (max z.re (Abs.abs z.im))‖
refine' le_trans _ (le_abs_self _)
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re (Abs.abs z.im)
⊢ ↑abs z ≤ Real.sqrt 2 * max (Abs.abs z.re) (Abs.abs z.im)

case h
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re (Abs.abs z.im)
⊢ 0 < ↑abs z

case h₁
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re (Abs.abs z.im)
⊢ 0 < Real.sqrt 2 * max z.re (Abs.abs z.im)

case hx
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re (Abs.abs z.im)
⊢ Real.sqrt 2 ≠ 0

case hy
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re (Abs.abs z.im)
⊢ max z.re (Abs.abs z.im) ≠ 0
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re (Abs.abs z.im)
⊢ Real.log (↑abs z) ≤ Real.log (Real.sqrt 2) + Real.log (max z.re (Abs.abs z.im))
rw [← Real.log_mul, Real.log_le_log, ← _root_.abs_of_nonneg (le_trans zero_le_one hz)]
no goals
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re (Abs.abs z.im)
⊢ ↑abs z ≤ Real.sqrt 2 * max (Abs.abs z.re) (Abs.abs z.im)

case h
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re (Abs.abs z.im)
⊢ 0 < ↑abs z

case h₁
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re (Abs.abs z.im)
⊢ 0 < Real.sqrt 2 * max z.re (Abs.abs z.im)

case hx
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re (Abs.abs z.im)
⊢ Real.sqrt 2 ≠ 0

case hy
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re (Abs.abs z.im)
⊢ max z.re (Abs.abs z.im) ≠ 0
exacts [abs_le_sqrt_two_mul_max z, one_pos.trans_le hz', mul_pos h2 hm₀, h2.ne', hm₀.ne']
no goals
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
⊢ 0 < Real.sqrt 2
simp
case h
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : Abs.abs z.im ^ ↑n ≤ Real.exp z.re
h₁ : 1 < z.re
⊢ ↑n * ‖Real.log (max z.re (Abs.abs z.im))‖ ≤ ‖z.re‖
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ ∀ᶠ (x : ℂ) in l, ↑n * ‖Real.log (max x.re (Abs.abs x.im))‖ ≤ ‖x.re‖
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₁
case h.inl
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : Abs.abs z.im ^ ↑n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : Abs.abs z.im ≤ z.re
⊢ ↑n * ‖Real.log (max z.re (Abs.abs z.im))‖ ≤ ‖z.re‖

case h.inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : Abs.abs z.im ^ ↑n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : z.re ≤ Abs.abs z.im
⊢ ↑n * ‖Real.log (max z.re (Abs.abs z.im))‖ ≤ ‖z.re‖
case h
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : Abs.abs z.im ^ ↑n ≤ Real.exp z.re
h₁ : 1 < z.re
⊢ ↑n * ‖Real.log (max z.re (Abs.abs z.im))‖ ≤ ‖z.re‖
cases' le_total (|z.im|) z.re with hle hle
no goals
case h.inl
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : Abs.abs z.im ^ ↑n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : Abs.abs z.im ≤ z.re
⊢ ↑n * ‖Real.log (max z.re (Abs.abs z.im))‖ ≤ ‖z.re‖
rwa [max_eq_left hle]
case h.inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : Abs.abs z.im ^ ↑n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : z.re ≤ Abs.abs z.im
H : 1 < Abs.abs z.im
⊢ ↑n * ‖Real.log (max z.re (Abs.abs z.im))‖ ≤ ‖z.re‖
case h.inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : Abs.abs z.im ^ ↑n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : z.re ≤ Abs.abs z.im
⊢ ↑n * ‖Real.log (max z.re (Abs.abs z.im))‖ ≤ ‖z.re‖
have H : 1 < |z.im| := h₁.trans_le hle
case h.inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
hle : z.re ≤ Abs.abs z.im
him : Abs.abs z.im ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
H : 1 < Abs.abs z.im
⊢ ↑n * ‖Real.log (max z.re (Abs.abs z.im))‖ ≤ ‖z.re‖
case h.inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : Abs.abs z.im ^ ↑n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : z.re ≤ Abs.abs z.im
H : 1 < Abs.abs z.im
⊢ ↑n * ‖Real.log (max z.re (Abs.abs z.im))‖ ≤ ‖z.re‖
norm_cast at *
no goals
case h.inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
hle : z.re ≤ Abs.abs z.im
him : Abs.abs z.im ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
H : 1 < Abs.abs z.im
⊢ ↑n * ‖Real.log (max z.re (Abs.abs z.im))‖ ≤ ‖z.re‖
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₁)]