awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
e_a :
  LSeries (fun (n : ℕ) ↦ (↑((zeta : (a : ℕ) → ℕ) n) : ℂ)) s = LSeries (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s
⊢ riemannZeta s = LSeries (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s

Tactic:
simp_rw [← LSeries_zeta_eq_riemannZeta hs, ← natCoe_apply]

Premises used: ArithmeticFunction.LSeries_zeta_eq_riemannZeta, ArithmeticFunction.natCoe_apply
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
⊢ LSeries (fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) s =
    LSeries (⇑(toArithmeticFunction fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) : (a : ℕ) → ℂ) s

Tactic:
LSeries_congr B.χ.apply_eq_toArithmeticFunction_apply s

Premises used: LSeries_congr, _private.0.DirichletCharacter.BadChar.χ, DirichletCharacter.apply_eq_toArithmeticFunction_apply
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
⊢ LSeries (fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) s =
    LSeries (⇑(toArithmeticFunction fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) : (a : ℕ) → ℂ) s

Tactic:
exact LSeries_congr B.χ.apply_eq_toArithmeticFunction_apply s

Premises used: LSeries_congr, _private.0.DirichletCharacter.BadChar.χ, DirichletCharacter.apply_eq_toArithmeticFunction_apply
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s

Tactic:
LSeriesSummable_zeta_iff.mpr hs

Premises used: Iff.mpr, ArithmeticFunction.LSeriesSummable_zeta_iff
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s

Tactic:
exact LSeriesSummable_zeta_iff.mpr hs

Premises used: Iff.mpr, ArithmeticFunction.LSeriesSummable_zeta_iff
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (⇑(toArithmeticFunction fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) : (a : ℕ) → ℂ) s

Tactic:
(LSeriesSummable_congr _ fun h ↦ (B.χ.apply_eq_toArithmeticFunction_apply h).symm).mpr <|
      ZMod.LSeriesSummable_of_one_lt_re B.χ hs

Premises used: Iff.mpr, LSeriesSummable_congr, _private.0.DirichletCharacter.BadChar.χ, ZMod.LSeriesSummable_of_one_lt_re, DirichletCharacter.apply_eq_toArithmeticFunction_apply, Eq.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (⇑(toArithmeticFunction fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) : (a : ℕ) → ℂ) s

Tactic:
exact (LSeriesSummable_congr _ fun h ↦ (B.χ.apply_eq_toArithmeticFunction_apply h).symm).mpr <|
      ZMod.LSeriesSummable_of_one_lt_re B.χ hs

Premises used: Iff.mpr, LSeriesSummable_congr, _private.0.DirichletCharacter.BadChar.χ, ZMod.LSeriesSummable_of_one_lt_re, DirichletCharacter.apply_eq_toArithmeticFunction_apply, Eq.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
inl : ∀ (hs : s ≠ 1), DifferentiableAt ℂ B.F s
inr : DifferentiableAt ℂ B.F 1
⊢ DifferentiableAt ℂ B.F s

Tactic:
rcases ne_or_eq s 1 with hs | rfl

Premises used: ne_or_eq, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : s ≠ 1
⊢ DifferentiableAt ℂ B.F s

Tactic:
B.F_differentiableAt_of_ne hs

Premises used: _private.0.DirichletCharacter.BadChar.F_differentiableAt_of_ne
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : s ≠ 1
⊢ DifferentiableAt ℂ B.F s

Tactic:
exact B.F_differentiableAt_of_ne hs

Premises used: _private.0.DirichletCharacter.BadChar.F_differentiableAt_of_ne
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
⊢ DifferentiableAt ℂ B.F 1

Tactic:
(analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt ?_ ?_).differentiableAt

Premises used: AnalyticAt.differentiableAt, Complex.analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
inr : ∀ᶠ (z : ℂ) in 𝓝[≠] 1, DifferentiableAt ℂ B.F z
inr₁ : ContinuousAt B.F 1
⊢ DifferentiableAt ℂ B.F 1

Tactic:
refine (analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt ?_ ?_).differentiableAt

Premises used: AnalyticAt.differentiableAt, Complex.analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
h : ∀ (t : ℂ) (ht : Membership.mem (γ := Set ℂ) {1}ᶜ t), DifferentiableAt ℂ B.F t
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] 1, DifferentiableAt ℂ B.F z

Tactic:
filter_upwards [self_mem_nhdsWithin] with t ht

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
t : ℂ
ht : Membership.mem (γ := Set ℂ) {1}ᶜ t
⊢ DifferentiableAt ℂ B.F t

Tactic:
B.F_differentiableAt_of_ne ht

Premises used: _private.0.DirichletCharacter.BadChar.F_differentiableAt_of_ne
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
t : ℂ
ht : Membership.mem (γ := Set ℂ) {1}ᶜ t
⊢ DifferentiableAt ℂ B.F t

Tactic:
exact B.F_differentiableAt_of_ne ht

Premises used: _private.0.DirichletCharacter.BadChar.F_differentiableAt_of_ne
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
G : (a : ℂ) → ℂ := Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) 1 1
H : (a : ℂ) → ℂ :=
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1
    (deriv (LFunction B.χ) 1)
h : ∀ (t : ℂ), B.F t = (G * H) t
⊢ B.F = G * H

Tactic:
ext1 t
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
G : (a : ℂ) → ℂ := Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) 1 1
H : (a : ℂ) → ℂ :=
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1
    (deriv (LFunction B.χ) 1)
t : ℂ
h : B.F 1 = (G * H) 1
h₁ : ∀ (ht : t ≠ 1), B.F t = (G * H) t
⊢ B.F t = (G * H) t

Tactic:
rcases eq_or_ne t 1 with rfl | ht

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
G : (a : ℂ) → ℂ := Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) 1 1
H : (a : ℂ) → ℂ :=
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1
    (deriv (LFunction B.χ) 1)
⊢ B.F 1 = (G * H) 1

Tactic:
simp only [F, G, H, Pi.mul_apply, one_mul, Function.update_self]

Premises used: Pi.mul_apply, _private.0.DirichletCharacter.BadChar.F, Function.update_self, one_mul
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
G : (a : ℂ) → ℂ := Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) 1 1
H : (a : ℂ) → ℂ :=
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1
    (deriv (LFunction B.χ) 1)
t : ℂ
ht : t ≠ 1
⊢ B.F t = (G * H) t

Tactic:
simp only [F, G, H, Function.update_of_ne ht, mul_comm _ (riemannZeta _), B.hχ, sub_zero,
      Pi.mul_apply, mul_assoc, mul_div_cancel₀ _ (sub_ne_zero.mpr ht)]

Premises used: Iff.mpr, Pi.mul_apply, riemannZeta, sub_zero, sub_ne_zero, mul_assoc, _private.0.DirichletCharacter.BadChar.F, mul_div_cancel₀, mul_comm, _private.0.DirichletCharacter.BadChar.hχ, Function.update_of_ne
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
G : (a : ℂ) → ℂ := Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) 1 1
H : (a : ℂ) → ℂ :=
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1
    (deriv (LFunction B.χ) 1)
⊢ B.F = G * H

Tactic:
have : B.F = G * H := by
    ext1 t
    rcases eq_or_ne t 1 with rfl | ht
    · simp only [F, G, H, Pi.mul_apply, one_mul, Function.update_self]
    · simp only [F, G, H, Function.update_of_ne ht, mul_comm _ (riemannZeta _), B.hχ, sub_zero,
      Pi.mul_apply, mul_assoc, mul_div_cancel₀ _ (sub_ne_zero.mpr ht)]
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
G : (a : ℂ) → ℂ := Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) 1 1
H : (a : ℂ) → ℂ :=
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1
    (deriv (LFunction B.χ) 1)
this : B.F = G * H
inr : ContinuousAt (G * H) 1
⊢ ContinuousAt B.F 1

Tactic:
rw [this]
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
G : (a : ℂ) → ℂ := Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) 1 1
H : (a : ℂ) → ℂ :=
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1
    (deriv (LFunction B.χ) 1)
this : B.F = G * H
inr : ContinuousAt G 1
inr₁ : ContinuousAt H 1
⊢ ContinuousAt (G * H) 1

Tactic:
apply ContinuousAt.mul

Premises used: ContinuousAt.mul
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
G : (a : ℂ) → ℂ := Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) 1 1
H : (a : ℂ) → ℂ :=
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1
    (deriv (LFunction B.χ) 1)
this : B.F = G * H
⊢ ContinuousAt G 1

Tactic:
simpa only [G, continuousAt_update_same] using riemannZeta_residue_one

Premises used: riemannZeta_residue_one, continuousAt_update_same
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
G : (a : ℂ) → ℂ := Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) 1 1
H : (a : ℂ) → ℂ :=
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1
    (deriv (LFunction B.χ) 1)
this : B.F = G * H
⊢ ContinuousAt H 1

Tactic:
(B.χ.differentiableAt_LFunction 1 (.inr B.χ_ne)).hasDerivAt.continuousAt_div

Premises used: DifferentiableAt.hasDerivAt, _private.0.DirichletCharacter.BadChar.χ_ne, DirichletCharacter.differentiableAt_LFunction, _private.0.DirichletCharacter.BadChar.χ, HasDerivAt.continuousAt_div, OfNat.ofNat, Or.inr
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
G : (a : ℂ) → ℂ := Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) 1 1
H : (a : ℂ) → ℂ :=
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1
    (deriv (LFunction B.χ) 1)
this : B.F = G * H
⊢ ContinuousAt H 1

Tactic:
exact (B.χ.differentiableAt_LFunction 1 (.inr B.χ_ne)).hasDerivAt.continuousAt_div

Premises used: DifferentiableAt.hasDerivAt, _private.0.DirichletCharacter.BadChar.χ_ne, DirichletCharacter.differentiableAt_LFunction, _private.0.DirichletCharacter.BadChar.χ, HasDerivAt.continuousAt_div, OfNat.ofNat, Or.inr
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
⊢ riemannZeta (-2 * HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1) = 0

Tactic:
have := riemannZeta_neg_two_mul_nat_add_one 0
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
this : riemannZeta (-2 * HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1) = 0
⊢ riemannZeta (-2) = 0

Tactic:
rw [Nat.cast_zero, zero_add, mul_one] at this

Premises used: zero_add, Nat.cast_zero, mul_one
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
this : riemannZeta (-2) = 0
⊢ Ne (α := ℤ) (-2) 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
this : riemannZeta (-2) = 0
rw :
  Eq (α := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1)
        (↑(-2) : ℂ) :
      ℂ)
    (0 : ℂ)
rw₁ :
  Eq (α := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1)
        (-(↑2 : ℂ)) :
      ℂ)
    (0 : ℂ)
rw₂ :
  Eq (α := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1)
        (-2) :
      ℂ)
    (0 : ℂ)
rw₃ : riemannZeta (-2) * LFunction B.χ (-2) = 0
rw₄ : 0 * LFunction B.χ (-2) = 0
rw₅ rw₆ : Eq (α := ℂ) 0 0
⊢ B.F (↑(-2) : ℂ) = 0

Tactic:
rw [F, ofReal_neg, ofReal_ofNat, Function.update_of_ne (mod_cast (by lia : (-2 : ℤ) ≠ 1)),
    this, zero_mul]

Premises used: MulZeroClass.zero_mul, Complex.ofReal_neg, _private.0.DirichletCharacter.BadChar.F, Complex.ofReal_ofNat, Function.update_of_ne
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
χ_ne : χ ≠ 1
hL : LFunction χ 1 = 0
B : BadChar N := { χ := χ, χ_ne := χ_ne, χ_sq := hχ, hχ := hL }
⊢ False

Tactic:
B.F_neg_two.not_gt ?_

Premises used: Eq.not_gt, _private.0.DirichletCharacter.BadChar.F_neg_two
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
χ_ne : χ ≠ 1
hL : LFunction χ 1 = 0
B : BadChar N := { χ := χ, χ_ne := χ_ne, χ_sq := hχ, hχ := hL }
refine : 0 < B.F (↑(-2) : ℂ)
⊢ False

Tactic:
refine B.F_neg_two.not_gt ?_

Premises used: Eq.not_gt, _private.0.DirichletCharacter.BadChar.F_neg_two
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
χ_ne : χ ≠ 1
hL : LFunction χ 1 = 0
B : BadChar N := { χ := χ, χ_ne := χ_ne, χ_sq := hχ, hχ := hL }
⊢ 0 < B.F (↑(-2) : ℂ)

Tactic:
ArithmeticFunction.LSeries_positive_of_differentiable_of_eqOn (zetaMul_nonneg hχ)
    (χ.isMultiplicative_zetaMul.map_one ▸ zero_lt_one) B.F_differentiable ?_
    (fun _ ↦ B.F_eq_LSeries) _

Premises used: _private.0.DirichletCharacter.BadChar.F_eq_LSeries, ArithmeticFunction.LSeries_positive_of_differentiable_of_eqOn, Eq.rec, DirichletCharacter.zetaMul_nonneg, _private.0.DirichletCharacter.BadChar.F_differentiable, ArithmeticFunction.IsMultiplicative.map_one, zero_lt_one, DirichletCharacter.isMultiplicative_zetaMul, Eq.symm
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
χ_ne : χ ≠ 1
hL : LFunction χ 1 = 0
B : BadChar N := { χ := χ, χ_ne := χ_ne, χ_sq := hχ, hχ := hL }
refine : LSeries.abscissaOfAbsConv (⇑χ.zetaMul : (a : ℕ) → ℂ) ≤ (↑1 : EReal)
⊢ 0 < B.F (↑(-2) : ℂ)

Tactic:
refine ArithmeticFunction.LSeries_positive_of_differentiable_of_eqOn (zetaMul_nonneg hχ)
    (χ.isMultiplicative_zetaMul.map_one ▸ zero_lt_one) B.F_differentiable ?_
    (fun _ ↦ B.F_eq_LSeries) _

Premises used: _private.0.DirichletCharacter.BadChar.F_eq_LSeries, ArithmeticFunction.LSeries_positive_of_differentiable_of_eqOn, Eq.rec, DirichletCharacter.zetaMul_nonneg, _private.0.DirichletCharacter.BadChar.F_differentiable, ArithmeticFunction.IsMultiplicative.map_one, zero_lt_one, DirichletCharacter.isMultiplicative_zetaMul, Eq.symm
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
χ_ne : χ ≠ 1
hL : LFunction χ 1 = 0
B : BadChar N := { χ := χ, χ_ne := χ_ne, χ_sq := hχ, hχ := hL }
⊢ LSeries.abscissaOfAbsConv (⇑χ.zetaMul : (a : ℕ) → ℂ) ≤ (↑1 : EReal)

Tactic:
LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable
    fun _ a ↦ χ.LSeriesSummable_zetaMul a

Premises used: LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable, DirichletCharacter.LSeriesSummable_zetaMul
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
χ_ne : χ ≠ 1
hL : LFunction χ 1 = 0
B : BadChar N := { χ := χ, χ_ne := χ_ne, χ_sq := hχ, hχ := hL }
⊢ LSeries.abscissaOfAbsConv (⇑χ.zetaMul : (a : ℕ) → ℂ) ≤ (↑1 : EReal)

Tactic:
exact LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable
    fun _ a ↦ χ.LSeriesSummable_zetaMul a

Premises used: LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable, DirichletCharacter.LSeriesSummable_zetaMul
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
⊢ ‖(↑a : ℂ)‖ < 1

Tactic:
simp only [Complex.norm_of_nonneg ha₀, ha₁]

Premises used: Complex.norm_of_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
⊢ ‖(↑a : ℂ)‖ < 1

Tactic:
have hac₀ : ‖(a : ℂ)‖ < 1 := by
    simp only [Complex.norm_of_nonneg ha₀, ha₁]
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
rwa : ‖(↑a : ℂ)‖ * ‖z‖ < 1
rwa₁ : ‖(↑a : ℂ)‖ * 1 < 1
rwa₂ rwa₃ rwa₄ rwa₅ : ‖(↑a : ℂ)‖ < 1
⊢ ‖(↑a : ℂ) * z‖ < 1

Tactic:
rwa [norm_mul, hz, mul_one]

Premises used: norm_mul, mul_one
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
⊢ ‖(↑a : ℂ) * z‖ < 1

Tactic:
have hac₁ : ‖a * z‖ < 1 := by rwa [norm_mul, hz, mul_one]
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
rwa : ‖(↑a : ℂ)‖ * ‖HPow.hPow (β := ℕ) z 2‖ < 1
rwa₁ : ‖(↑a : ℂ)‖ * HPow.hPow (β := ℕ) ‖z‖ 2 < 1
rwa₂ : ‖(↑a : ℂ)‖ * HPow.hPow (α := ℝ) (β := ℕ) 1 2 < 1
rwa₃ : ‖(↑a : ℂ)‖ * 1 < 1
rwa₄ rwa₅ rwa₆ rwa₇ : ‖(↑a : ℂ)‖ < 1
⊢ ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1

Tactic:
rwa [norm_mul, norm_pow, hz, one_pow, mul_one]

Premises used: one_pow, norm_pow, norm_mul, mul_one
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
⊢ ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1

Tactic:
have hac₂ : ‖a * z ^ 2‖ < 1 := by rwa [norm_mul, norm_pow, hz, one_pow, mul_one]
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
hac₂ : ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1
rw :
  LE.le (α := ℝ) 0
    (∑' (b : ℕ),
      (3 * ((↑a : ℂ) ^ b / (↑b : ℂ)).re + 4 * (((↑a : ℂ) * z) ^ b / (↑b : ℂ)).re +
        (((↑a : ℂ) * HPow.hPow (β := ℕ) z 2) ^ b / (↑b : ℂ)).re))
⊢ 0 ≤
    3 * (-log (1 - (↑a : ℂ))).re + 4 * (-log (1 - (↑a : ℂ) * z)).re + (-log (1 - (↑a : ℂ) * HPow.hPow (β := ℕ) z 2)).re

Tactic:
rw [← ((hasSum_re <| hasSum_taylorSeries_neg_log hac₀).mul_left 3).add
    ((hasSum_re <| hasSum_taylorSeries_neg_log hac₁).mul_left 4) |>.add
    (hasSum_re <| hasSum_taylorSeries_neg_log hac₂) |>.tsum_eq]

Premises used: HasSum.add, HasSum.mul_left, Complex.hasSum_re, HasSum.tsum_eq, Complex.hasSum_taylorSeries_neg_log, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
hac₂ : ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1
⊢ LE.le (α := ℝ) 0
    (∑' (b : ℕ),
      (3 * ((↑a : ℂ) ^ b / (↑b : ℂ)).re + 4 * (((↑a : ℂ) * z) ^ b / (↑b : ℂ)).re +
        (((↑a : ℂ) * HPow.hPow (β := ℕ) z 2) ^ b / (↑b : ℂ)).re))

Tactic:
tsum_nonneg fun n ↦ ?_

Premises used: tsum_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
hac₂ : ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1
refine :
  ∀ (n : ℕ),
    0 ≤
      3 * ((↑a : ℂ) ^ n / (↑n : ℂ)).re + 4 * (((↑a : ℂ) * z) ^ n / (↑n : ℂ)).re +
        (((↑a : ℂ) * HPow.hPow (β := ℕ) z 2) ^ n / (↑n : ℂ)).re
⊢ LE.le (α := ℝ) 0
    (∑' (b : ℕ),
      (3 * ((↑a : ℂ) ^ b / (↑b : ℂ)).re + 4 * (((↑a : ℂ) * z) ^ b / (↑b : ℂ)).re +
        (((↑a : ℂ) * HPow.hPow (β := ℕ) z 2) ^ b / (↑b : ℂ)).re))

Tactic:
refine tsum_nonneg fun n ↦ ?_

Premises used: tsum_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
hac₂ : ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1
n : ℕ
simp :
  0 ≤ 3 * (a ^ n / (↑n : ℝ)) + 4 * (a ^ n * (z ^ n).re / (↑n : ℝ)) + a ^ n * (HPow.hPow (β := ℕ) z 2 ^ n).re / (↑n : ℝ)
⊢ 0 ≤
    3 * ((↑a : ℂ) ^ n / (↑n : ℂ)).re + 4 * (((↑a : ℂ) * z) ^ n / (↑n : ℂ)).re +
      (((↑a : ℂ) * HPow.hPow (β := ℕ) z 2) ^ n / (↑n : ℂ)).re

Tactic:
simp only [← ofReal_pow, div_natCast_re, ofReal_re, mul_pow, mul_re, ofReal_im, zero_mul,
    sub_zero]

Premises used: Complex.mul_re, sub_zero, MulZeroClass.zero_mul, Complex.ofReal_re, Complex.ofReal_im, mul_pow, Complex.ofReal_pow, Complex.div_natCast_re
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
hac₂ : ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1
n : ℕ
inl :
  0 ≤
    3 * (HPow.hPow (β := ℕ) a 0 / (↑0 : ℝ)) + 4 * (HPow.hPow (β := ℕ) a 0 * (HPow.hPow (β := ℕ) z 0).re / (↑0 : ℝ)) +
      HPow.hPow (β := ℕ) a 0 * (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) z 2) 0).re / (↑0 : ℝ)
inr :
  ∀ (hn : n > 0),
    0 ≤
      3 * (a ^ n / (↑n : ℝ)) + 4 * (a ^ n * (z ^ n).re / (↑n : ℝ)) + a ^ n * (HPow.hPow (β := ℕ) z 2 ^ n).re / (↑n : ℝ)
⊢ 0 ≤ 3 * (a ^ n / (↑n : ℝ)) + 4 * (a ^ n * (z ^ n).re / (↑n : ℝ)) + a ^ n * (HPow.hPow (β := ℕ) z 2 ^ n).re / (↑n : ℝ)

Tactic:
rcases n.eq_zero_or_pos with rfl | hn

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
hac₂ : ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1
⊢ 0 ≤
    3 * (HPow.hPow (β := ℕ) a 0 / (↑0 : ℝ)) + 4 * (HPow.hPow (β := ℕ) a 0 * (HPow.hPow (β := ℕ) z 0).re / (↑0 : ℝ)) +
      HPow.hPow (β := ℕ) a 0 * (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) z 2) 0).re / (↑0 : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
hac₂ : ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1
n : ℕ
hn : n > 0
inr : 0 ≤ (3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * (HPow.hPow (β := ℕ) z 2 ^ n).re) / (↑n : ℝ)
⊢ 0 ≤ 3 * (a ^ n / (↑n : ℝ)) + 4 * (a ^ n * (z ^ n).re / (↑n : ℝ)) + a ^ n * (HPow.hPow (β := ℕ) z 2 ^ n).re / (↑n : ℝ)

Tactic:
simp only [← mul_div_assoc, ← add_div]

Premises used: mul_div_assoc, add_div
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
hac₂ : ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ (3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * (HPow.hPow (β := ℕ) z 2 ^ n).re) / (↑n : ℝ)

Tactic:
div_nonneg ?_ n.cast_nonneg

Premises used: Nat.cast_nonneg, div_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
hac₂ : ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1
n : ℕ
hn : n > 0
inr : 0 ≤ 3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * (HPow.hPow (β := ℕ) z 2 ^ n).re
⊢ 0 ≤ (3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * (HPow.hPow (β := ℕ) z 2 ^ n).re) / (↑n : ℝ)

Tactic:
refine div_nonneg ?_ n.cast_nonneg

Premises used: div_nonneg