Theorem: Summable.neg_clog_one_sub (EulerProducts/Logarithm.lean)

State before:
α : Type u_1
f : α → ℂ
hsum : Summable f
⊢ Summable fun n => -(1 - f n).log
Tactic:
let g (z : ℂ) : ℂ := -log (1 - z)
State after:
α : Type u_1
f : α → ℂ
hsum : Summable f
g : ℂ → ℂ := fun z => -(1 - z).log
⊢ Summable fun n => -(1 - f n).log

State before:
α : Type u_1
f : α → ℂ
hsum : Summable f
g : ℂ → ℂ := fun z => -(1 - z).log
⊢ Summable fun n => -(1 - f n).log
Tactic:
have hg : DifferentiableAt ℂ g 0 :=
  DifferentiableAt.neg <| ((differentiableAt_const 1).sub differentiableAt_id').clog <|
    by simp only [sub_zero, one_mem_slitPlane]
State after:
α : Type u_1
f : α → ℂ
hsum : Summable f
g : ℂ → ℂ := fun z => -(1 - z).log
hg : DifferentiableAt ℂ g 0
⊢ Summable fun n => -(1 - f n).log

State before:
α : Type u_1
f : α → ℂ
hsum : Summable f
g : ℂ → ℂ := fun z => -(1 - z).log
hg : DifferentiableAt ℂ g 0
⊢ Summable fun n => -(1 - f n).log
Tactic:
have : g =O[𝓝 0] id := by
  simpa only [g, sub_zero, log_one, neg_zero] using DifferentiableAt.isBigO_sub hg
State after:
α : Type u_1
f : α → ℂ
hsum : Summable f
g : ℂ → ℂ := fun z => -(1 - z).log
hg : DifferentiableAt ℂ g 0
this : g =O[𝓝 0] id
⊢ Summable fun n => -(1 - f n).log

State before:
α : Type u_1
f : α → ℂ
hsum : Summable f
g : ℂ → ℂ := fun z => -(1 - z).log
hg : DifferentiableAt ℂ g 0
this : g =O[𝓝 0] id
⊢ Summable fun n => -(1 - f n).log
Tactic:
exact Asymptotics.IsBigO.comp_summable this hsum
State after:
no goals

State before:
α : Type u_1
f : α → ℂ
hsum : Summable f
g : ℂ → ℂ := fun z => -(1 - z).log
⊢ 1 - 0 ∈ slitPlane
Tactic:
simp only [sub_zero, one_mem_slitPlane]
State after:
no goals

State before:
α : Type u_1
f : α → ℂ
hsum : Summable f
g : ℂ → ℂ := fun z => -(1 - z).log
hg : DifferentiableAt ℂ g 0
⊢ g =O[𝓝 0] id
Tactic:
simpa only [g, sub_zero, log_one, neg_zero] using DifferentiableAt.isBigO_sub hg
State after:
no goals