internlm/Lean-Github huggingface dataset:
Theorem: DirichletCharacter.LSeries_eulerProduct'
Proof state before:
case h.e'_3.h.e'_5.h.h.e.h
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
x✝ n : ℕ
⊢ term (fun n => χ ↑n) s n = (dirichletSummandHom χ ⋯) n
Tactic:
rcases eq_or_ne n 0 with rfl | hn
Proof state after:
case h.e'_3.h.e'_5.h.h.e.h.inl
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
x✝ : ℕ
⊢ term (fun n => χ ↑n) s 0 = (dirichletSummandHom χ ⋯) 0

case h.e'_3.h.e'_5.h.h.e.h.inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
x✝ n : ℕ
hn : n ≠ 0
⊢ term (fun n => χ ↑n) s n = (dirichletSummandHom χ ⋯) n
Theorem: DirichletCharacter.LSeries_eulerProduct'
Proof state before:
case h.e'_3.h.e'_5.h.h.e.h.inl
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
x✝ : ℕ
⊢ term (fun n => χ ↑n) s 0 = (dirichletSummandHom χ ⋯) 0
Tactic:
simp only [term_zero, map_zero]
Proof state after:
no goals
Theorem: DirichletCharacter.LSeries_eulerProduct'
Proof state before:
case h.e'_3.h.e'_5.h.h.e.h.inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
x✝ n : ℕ
hn : n ≠ 0
⊢ term (fun n => χ ↑n) s n = (dirichletSummandHom χ ⋯) n
Tactic:
simp [hn, dirichletSummandHom, div_eq_mul_inv, cpow_neg]
Proof state after:
no goals
Theorem: ArithmeticFunction.LSeries_zeta_eulerProduct'
Proof state before:
s : ℂ
hs : 1 < s.re
⊢ cexp (∑' (p : Primes), -(1 - ↑↑p ^ (-s)).log) = L 1 s
Tactic:
convert modOne_eq_one (R := ℂ) ▸ LSeries_eulerProduct' (1 : DirichletCharacter ℂ 1) hs using 7
Proof state after:
case h.e'_2.h.e'_1.h.e'_5.h.h.e'_3.h.e'_1.h.e'_6
s : ℂ
hs : 1 < s.re
x✝ : Primes
⊢ ↑↑x✝ ^ (-s) = 1 ↑↑x✝ * ↑↑x✝ ^ (-s)
Theorem: ArithmeticFunction.LSeries_zeta_eulerProduct'
Proof state before:
case h.e'_2.h.e'_1.h.e'_5.h.h.e'_3.h.e'_1.h.e'_6
s : ℂ
hs : 1 < s.re
x✝ : Primes
⊢ ↑↑x✝ ^ (-s) = 1 ↑↑x✝ * ↑↑x✝ ^ (-s)
Tactic:
rw [MulChar.one_apply <| isUnit_of_subsingleton _, one_mul]
Proof state after:
no goals
Theorem: LSeriesSummable.mul_bounded
Proof state before:
f g : ℕ → ℂ
c : ℝ
s : ℂ
hs : LSeriesSummable f s
hg : ∀ (n : ℕ), ‖g n‖ ≤ c
⊢ LSeriesSummable (f * g) s
Tactic:
refine Summable.of_norm <| (hs.const_smul c).norm.of_nonneg_of_le (fun _ ↦ norm_nonneg _) fun n ↦ ?_
Proof state after:
f g : ℕ → ℂ
c : ℝ
s : ℂ
hs : LSeriesSummable f s
hg : ∀ (n : ℕ), ‖g n‖ ≤ c
n : ℕ
⊢ ‖LSeries.term (f * g) s n‖ ≤ ‖c • LSeries.term f s n‖
Theorem: LSeriesSummable.mul_bounded
Proof state before:
f g : ℕ → ℂ
c : ℝ
s : ℂ
hs : LSeriesSummable f s
hg : ∀ (n : ℕ), ‖g n‖ ≤ c
n : ℕ
⊢ ‖LSeries.term (f * g) s n‖ ≤ ‖c • LSeries.term f s n‖
Tactic:
rw [Complex.real_smul, ← LSeries.term_smul_apply, mul_comm]
Proof state after:
f g : ℕ → ℂ
c : ℝ
s : ℂ
hs : LSeriesSummable f s
hg : ∀ (n : ℕ), ‖g n‖ ≤ c
n : ℕ
⊢ ‖LSeries.term (g * f) s n‖ ≤ ‖LSeries.term (↑c • f) s n‖
Theorem: LSeriesSummable.mul_bounded
Proof state before:
f g : ℕ → ℂ
c : ℝ
s : ℂ
hs : LSeriesSummable f s
hg : ∀ (n : ℕ), ‖g n‖ ≤ c
n : ℕ
⊢ ‖LSeries.term (g * f) s n‖ ≤ ‖LSeries.term (↑c • f) s n‖
Tactic:
refine LSeries.norm_term_le s ?_
Proof state after:
f g : ℕ → ℂ
c : ℝ
s : ℂ
hs : LSeriesSummable f s
hg : ∀ (n : ℕ), ‖g n‖ ≤ c
n : ℕ
⊢ ‖(g * f) n‖ ≤ ‖(↑c • f) n‖
Theorem: LSeriesSummable.mul_bounded
Proof state before:
f g : ℕ → ℂ
c : ℝ
s : ℂ
hs : LSeriesSummable f s
hg : ∀ (n : ℕ), ‖g n‖ ≤ c
n : ℕ
⊢ ‖(g * f) n‖ ≤ ‖(↑c • f) n‖
Tactic:
have hc : ‖(c : ℂ)‖ = c := by
  simp only [Complex.norm_eq_abs, Complex.abs_ofReal, abs_eq_self, (norm_nonneg _).trans (hg 0)]
Proof state after:
f g : ℕ → ℂ
c : ℝ
s : ℂ
hs : LSeriesSummable f s
hg : ∀ (n : ℕ), ‖g n‖ ≤ c
n : ℕ
hc : ‖↑c‖ = c
⊢ ‖(g * f) n‖ ≤ ‖(↑c • f) n‖
Theorem: LSeriesSummable.mul_bounded
Proof state before:
f g : ℕ → ℂ
c : ℝ
s : ℂ
hs : LSeriesSummable f s
hg : ∀ (n : ℕ), ‖g n‖ ≤ c
n : ℕ
hc : ‖↑c‖ = c
⊢ ‖(g * f) n‖ ≤ ‖(↑c • f) n‖
Tactic:
simpa only [Pi.mul_apply, norm_mul, Pi.smul_apply, smul_eq_mul, hc]
  using mul_le_mul_of_nonneg_right (hg n) <| norm_nonneg _
Proof state after:
no goals
Theorem: LSeriesSummable.mul_bounded
Proof state before:
f g : ℕ → ℂ
c : ℝ
s : ℂ
hs : LSeriesSummable f s
hg : ∀ (n : ℕ), ‖g n‖ ≤ c
n : ℕ
⊢ ‖↑c‖ = c
Tactic:
simp only [Complex.norm_eq_abs, Complex.abs_ofReal, abs_eq_self, (norm_nonneg _).trans (hg 0)]
Proof state after:
no goals
Theorem: LSeriesSummable.mul_moebius
Proof state before:
f : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
⊢ LSeriesSummable (f * fun n => ↑(μ n)) s
Tactic:
refine hf.mul_bounded (c := 1) fun n ↦ ?_
Proof state after:
f : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
n : ℕ
⊢ ‖↑(μ n)‖ ≤ 1
Theorem: LSeriesSummable.mul_moebius
Proof state before:
f : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
n : ℕ
⊢ ‖↑(μ n)‖ ≤ 1
Tactic:
simp only [Complex.norm_int]
Proof state after:
f : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
n : ℕ
⊢ |↑(μ n)| ≤ 1
Theorem: LSeriesSummable.mul_moebius
Proof state before:
f : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
n : ℕ
⊢ |↑(μ n)| ≤ 1
Tactic:
exact_mod_cast abs_moebius_le_one
Proof state after:
no goals
Theorem: LSeries.mul_convolution_distrib
Proof state before:
R : Type u_1
inst✝ : CommSemiring R
φ : ℕ → R
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
f g : ℕ → R
⊢ φ * (f ⍟ g) = φ * f ⍟ (φ * g)
Tactic:
ext n
Proof state after:
case h
R : Type u_1
inst✝ : CommSemiring R
φ : ℕ → R
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
f g : ℕ → R
n : ℕ
⊢ (φ * (f ⍟ g)) n = (φ * f ⍟ (φ * g)) n
Theorem: LSeries.mul_convolution_distrib
Proof state before:
case h
R : Type u_1
inst✝ : CommSemiring R
φ : ℕ → R
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
f g : ℕ → R
n : ℕ
⊢ (φ * (f ⍟ g)) n = (φ * f ⍟ (φ * g)) n
Tactic:
simp only [Pi.mul_apply, LSeries.convolution_def, Finset.mul_sum]
Proof state after:
case h
R : Type u_1
inst✝ : CommSemiring R
φ : ℕ → R
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
f g : ℕ → R
n : ℕ
⊢ ∑ i ∈ n.divisorsAntidiagonal, φ n * (f i.1 * g i.2) = ∑ x ∈ n.divisorsAntidiagonal, φ x.1 * f x.1 * (φ x.2 * g x.2)
Theorem: LSeries.mul_convolution_distrib
Proof state before:
case h
R : Type u_1
inst✝ : CommSemiring R
φ : ℕ → R
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
f g : ℕ → R
n : ℕ
⊢ ∑ i ∈ n.divisorsAntidiagonal, φ n * (f i.1 * g i.2) = ∑ x ∈ n.divisorsAntidiagonal, φ x.1 * f x.1 * (φ x.2 * g x.2)
Tactic:
refine Finset.sum_congr rfl fun p hp ↦ ?_
Proof state after:
case h
R : Type u_1
inst✝ : CommSemiring R
φ : ℕ → R
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
f g : ℕ → R
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ φ n * (f p.1 * g p.2) = φ p.1 * f p.1 * (φ p.2 * g p.2)
Theorem: LSeries.mul_convolution_distrib
Proof state before:
case h
R : Type u_1
inst✝ : CommSemiring R
φ : ℕ → R
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
f g : ℕ → R
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ φ n * (f p.1 * g p.2) = φ p.1 * f p.1 * (φ p.2 * g p.2)
Tactic:
rw [(Nat.mem_divisorsAntidiagonal.mp hp).1.symm, hφ]
Proof state after:
case h
R : Type u_1
inst✝ : CommSemiring R
φ : ℕ → R
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
f g : ℕ → R
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ φ p.1 * φ p.2 * (f p.1 * g p.2) = φ p.1 * f p.1 * (φ p.2 * g p.2)
Theorem: LSeries.mul_convolution_distrib
Proof state before:
case h
R : Type u_1
inst✝ : CommSemiring R
φ : ℕ → R
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
f g : ℕ → R
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ φ p.1 * φ p.2 * (f p.1 * g p.2) = φ p.1 * f p.1 * (φ p.2 * g p.2)
Tactic:
exact mul_mul_mul_comm ..
Proof state after:
no goals
Theorem: LSeries.convolution_mul_moebius
Proof state before:
φ : ℕ → ℂ
h₁ : φ 1 = 1
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
this : (1 ⍟ fun x => ↑(μ x)) = δ
⊢ φ ⍟ (φ * fun n => ↑(μ n)) = δ
Tactic:
nth_rewrite 1 [← mul_one φ]
Proof state after:
φ : ℕ → ℂ
h₁ : φ 1 = 1
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
this : (1 ⍟ fun x => ↑(μ x)) = δ
⊢ φ * 1 ⍟ (φ * fun n => ↑(μ n)) = δ
Theorem: LSeries.convolution_mul_moebius
Proof state before:
φ : ℕ → ℂ
h₁ : φ 1 = 1
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
this : (1 ⍟ fun x => ↑(μ x)) = δ
⊢ φ * 1 ⍟ (φ * fun n => ↑(μ n)) = δ
Tactic:
simp only [← mul_convolution_distrib hφ 1 ↗μ, this, mul_delta h₁]
Proof state after:
no goals
Theorem: LSeries.convolution_mul_moebius
Proof state before:
φ : ℕ → ℂ
h₁ : φ 1 = 1
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
⊢ (1 ⍟ fun x => ↑(μ x)) = δ
Tactic:
rw [one_convolution_eq_zeta_convolution, ← one_eq_delta]
Proof state after:
φ : ℕ → ℂ
h₁ : φ 1 = 1
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
⊢ ((fun x => ↑(ζ x)) ⍟ fun x => ↑(μ x)) = fun n => 1 n
Theorem: LSeries.convolution_mul_moebius
Proof state before:
φ : ℕ → ℂ
h₁ : φ 1 = 1
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
⊢ ((fun x => ↑(ζ x)) ⍟ fun x => ↑(μ x)) = fun n => 1 n
Tactic:
change ⇑(ζ : ArithmeticFunction ℂ) ⍟ ⇑(μ : ArithmeticFunction ℂ) = ⇑(1 : ArithmeticFunction ℂ)
Proof state after:
φ : ℕ → ℂ
h₁ : φ 1 = 1
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
⊢ ⇑↑ζ ⍟ ⇑↑μ = ⇑1
Theorem: LSeries.convolution_mul_moebius
Proof state before:
φ : ℕ → ℂ
h₁ : φ 1 = 1
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
⊢ ⇑↑ζ ⍟ ⇑↑μ = ⇑1
Tactic:
simp only [coe_mul, coe_zeta_mul_coe_moebius]
Proof state after:
no goals
Theorem: LSeries.mul_mu_eq_one
Proof state before:
φ : ℕ → ℂ
h₁ : φ 1 = 1
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
s : ℂ
hs : LSeriesSummable φ s
⊢ L φ s * L (φ * fun n => ↑(μ n)) s = 1
Tactic:
rw [← LSeries_convolution' hs ?_, convolution_mul_moebius h₁ hφ, LSeries_delta, Pi.one_apply]
Proof state after:
φ : ℕ → ℂ
h₁ : φ 1 = 1
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
s : ℂ
hs : LSeriesSummable φ s
⊢ LSeriesSummable (φ * fun n => ↑(μ n)) s
Theorem: LSeries.mul_mu_eq_one
Proof state before:
φ : ℕ → ℂ
h₁ : φ 1 = 1
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
s : ℂ
hs : LSeriesSummable φ s
⊢ LSeriesSummable (φ * fun n => ↑(μ n)) s
Tactic:
exact hs.mul_moebius
Proof state after:
no goals
Theorem: ArithmeticFunction.LSeries_zeta_eulerProduct'
Proof state before:
s : ℂ
hs : 1 < s.re
⊢ cexp (∑' (p : Primes), -(1 - ↑↑p ^ (-s)).log) = L 1 s
Tactic:
convert modOne_eq_one (R := ℂ) ▸ LSeries_eulerProduct' χ₁ hs using 7
Proof state after:
case h.e'_2.h.e'_1.h.e'_5.h.h.e'_3.h.e'_1.h.e'_6
s : ℂ
hs : 1 < s.re
x✝ : Primes
⊢ ↑↑x✝ ^ (-s) = 1 ↑↑x✝ * ↑↑x✝ ^ (-s)
Theorem: summable_neg_log_one_sub_char_mul_prime_cpow
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ Summable fun p => -(1 - χ ↑↑p * ↑↑p ^ (-s)).log
Tactic:
have (p : Nat.Primes) : ‖χ p * (p : ℂ) ^ (-s)‖ ≤ (p : ℝ) ^ (-s).re := by
  rw [norm_mul, norm_natCast_cpow_of_re_ne_zero _ <| re_neg_ne_zero_of_one_lt_re hs]
  calc ‖χ p‖ * (p : ℝ) ^ (-s).re
    _ ≤ 1 * (p : ℝ) ^ (-s.re) := by gcongr; exact DirichletCharacter.norm_le_one χ _
    _ = _ := one_mul _
Proof state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
this : ∀ (p : Nat.Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ ≤ ↑↑p ^ (-s).re
⊢ Summable fun p => -(1 - χ ↑↑p * ↑↑p ^ (-s)).log
Theorem: summable_neg_log_one_sub_char_mul_prime_cpow
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
this : ∀ (p : Nat.Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ ≤ ↑↑p ^ (-s).re
⊢ Summable fun p => -(1 - χ ↑↑p * ↑↑p ^ (-s)).log
Tactic:
refine (Nat.Primes.summable_rpow.mpr ?_).of_nonneg_of_le (fun _ ↦ norm_nonneg _) this
  |>.of_norm.neg_clog_one_sub
Proof state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
this : ∀ (p : Nat.Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ ≤ ↑↑p ^ (-s).re
⊢ (-s).re < -1
Theorem: summable_neg_log_one_sub_char_mul_prime_cpow
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
this : ∀ (p : Nat.Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ ≤ ↑↑p ^ (-s).re
⊢ (-s).re < -1
Tactic:
simp only [neg_re, neg_lt_neg_iff, hs]
Proof state after:
no goals
Theorem: summable_neg_log_one_sub_char_mul_prime_cpow
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Nat.Primes
⊢ ‖χ ↑↑p * ↑↑p ^ (-s)‖ ≤ ↑↑p ^ (-s).re
Tactic:
rw [norm_mul, norm_natCast_cpow_of_re_ne_zero _ <| re_neg_ne_zero_of_one_lt_re hs]
Proof state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Nat.Primes
⊢ ‖χ ↑↑p‖ * ↑↑p ^ (-s).re ≤ ↑↑p ^ (-s).re
Theorem: summable_neg_log_one_sub_char_mul_prime_cpow
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Nat.Primes
⊢ ‖χ ↑↑p‖ * ↑↑p ^ (-s).re ≤ ↑↑p ^ (-s).re
Tactic:
calc ‖χ p‖ * (p : ℝ) ^ (-s).re
  _ ≤ 1 * (p : ℝ) ^ (-s.re) := by gcongr; exact DirichletCharacter.norm_le_one χ _
  _ = _ := one_mul _
Proof state after:
no goals
Theorem: summable_neg_log_one_sub_char_mul_prime_cpow
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Nat.Primes
⊢ ‖χ ↑↑p‖ * ↑↑p ^ (-s).re ≤ 1 * ↑↑p ^ (-s.re)
Tactic:
gcongr
Proof state after:
case h
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Nat.Primes
⊢ ‖χ ↑↑p‖ ≤ 1
Theorem: summable_neg_log_one_sub_char_mul_prime_cpow
Proof state before:
case h
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Nat.Primes
⊢ ‖χ ↑↑p‖ ≤ 1
Tactic:
exact DirichletCharacter.norm_le_one χ _
Proof state after:
no goals
Theorem: re_log_comb_nonneg'
Proof state before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re
Tactic:
have hac₀ : ‖(a : ℂ)‖ < 1 := by
  simp only [norm_eq_abs, abs_ofReal, _root_.abs_of_nonneg ha₀, ha₁]
Proof state after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re
Theorem: re_log_comb_nonneg'
Proof state before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re
Tactic:
have hac₁ : ‖a * z‖ < 1 := by rwa [norm_mul, hz, mul_one]
Proof state after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re
Theorem: re_log_comb_nonneg'
Proof state before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re
Tactic:
have hac₂ : ‖a * z ^ 2‖ < 1 := by rwa [norm_mul, norm_pow, hz, one_pow, mul_one]
Proof state after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re
Theorem: re_log_comb_nonneg'
Proof state before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re
Tactic:
have H₀ := (hasSum_re <| hasSum_taylorSeries_neg_log hac₀).mul_left 3
Proof state after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
H₀ : HasSum (fun i => 3 * (↑a ^ i / ↑i).re) (3 * (-(1 - ↑a).log).re)
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re
Theorem: re_log_comb_nonneg'
Proof state before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
H₀ : HasSum (fun i => 3 * (↑a ^ i / ↑i).re) (3 * (-(1 - ↑a).log).re)
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re
Tactic:
have H₁ := (hasSum_re <| hasSum_taylorSeries_neg_log hac₁).mul_left 4
Proof state after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
H₀ : HasSum (fun i => 3 * (↑a ^ i / ↑i).re) (3 * (-(1 - ↑a).log).re)
H₁ : HasSum (fun i => 4 * ((↑a * z) ^ i / ↑i).re) (4 * (-(1 - ↑a * z).log).re)
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re
Theorem: re_log_comb_nonneg'
Proof state before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
H₀ : HasSum (fun i => 3 * (↑a ^ i / ↑i).re) (3 * (-(1 - ↑a).log).re)
H₁ : HasSum (fun i => 4 * ((↑a * z) ^ i / ↑i).re) (4 * (-(1 - ↑a * z).log).re)
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re
Tactic:
have H₂ := hasSum_re <| hasSum_taylorSeries_neg_log hac₂
Proof state after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
H₀ : HasSum (fun i => 3 * (↑a ^ i / ↑i).re) (3 * (-(1 - ↑a).log).re)
H₁ : HasSum (fun i => 4 * ((↑a * z) ^ i / ↑i).re) (4 * (-(1 - ↑a * z).log).re)
H₂ : HasSum (fun x => ((↑a * z ^ 2) ^ x / ↑x).re) (-(1 - ↑a * z ^ 2).log).re
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re
Theorem: re_log_comb_nonneg'
Proof state before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
H₀ : HasSum (fun i => 3 * (↑a ^ i / ↑i).re) (3 * (-(1 - ↑a).log).re)
H₁ : HasSum (fun i => 4 * ((↑a * z) ^ i / ↑i).re) (4 * (-(1 - ↑a * z).log).re)
H₂ : HasSum (fun x => ((↑a * z ^ 2) ^ x / ↑x).re) (-(1 - ↑a * z ^ 2).log).re
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re
Tactic:
rw [← ((H₀.add H₁).add H₂).tsum_eq]
Proof state after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
H₀ : HasSum (fun i => 3 * (↑a ^ i / ↑i).re) (3 * (-(1 - ↑a).log).re)
H₁ : HasSum (fun i => 4 * ((↑a * z) ^ i / ↑i).re) (4 * (-(1 - ↑a * z).log).re)
H₂ : HasSum (fun x => ((↑a * z ^ 2) ^ x / ↑x).re) (-(1 - ↑a * z ^ 2).log).re
⊢ 0 ≤ ∑' (b : ℕ), (3 * (↑a ^ b / ↑b).re + 4 * ((↑a * z) ^ b / ↑b).re + ((↑a * z ^ 2) ^ b / ↑b).re)
Theorem: re_log_comb_nonneg'
Proof state before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
H₀ : HasSum (fun i => 3 * (↑a ^ i / ↑i).re) (3 * (-(1 - ↑a).log).re)
H₁ : HasSum (fun i => 4 * ((↑a * z) ^ i / ↑i).re) (4 * (-(1 - ↑a * z).log).re)
H₂ : HasSum (fun x => ((↑a * z ^ 2) ^ x / ↑x).re) (-(1 - ↑a * z ^ 2).log).re
⊢ 0 ≤ ∑' (b : ℕ), (3 * (↑a ^ b / ↑b).re + 4 * ((↑a * z) ^ b / ↑b).re + ((↑a * z ^ 2) ^ b / ↑b).re)
Tactic:
clear H₀ H₁ H₂
Proof state after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
⊢ 0 ≤ ∑' (b : ℕ), (3 * (↑a ^ b / ↑b).re + 4 * ((↑a * z) ^ b / ↑b).re + ((↑a * z ^ 2) ^ b / ↑b).re)
Theorem: re_log_comb_nonneg'
Proof state before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
⊢ 0 ≤ ∑' (b : ℕ), (3 * (↑a ^ b / ↑b).re + 4 * ((↑a * z) ^ b / ↑b).re + ((↑a * z ^ 2) ^ b / ↑b).re)
Tactic:
refine tsum_nonneg fun n ↦ ?_
Proof state after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
⊢ 0 ≤ 3 * (↑a ^ n / ↑n).re + 4 * ((↑a * z) ^ n / ↑n).re + ((↑a * z ^ 2) ^ n / ↑n).re
Theorem: re_log_comb_nonneg'
Proof state before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
⊢ 0 ≤ 3 * (↑a ^ n / ↑n).re + 4 * ((↑a * z) ^ n / ↑n).re + ((↑a * z ^ 2) ^ n / ↑n).re
Tactic:
simp only [mul_pow, ← ofReal_pow, div_natCast_re, ofReal_re, mul_re, ofReal_im, zero_mul,
  sub_zero]
Proof state after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
⊢ 0 ≤ 3 * (a ^ n / ↑n) + 4 * (a ^ n * (z ^ n).re / ↑n) + a ^ n * ((z ^ 2) ^ n).re / ↑n
Theorem: re_log_comb_nonneg'
Proof state before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
⊢ 0 ≤ 3 * (a ^ n / ↑n) + 4 * (a ^ n * (z ^ n).re / ↑n) + a ^ n * ((z ^ 2) ^ n).re / ↑n
Tactic:
rcases n.eq_zero_or_pos with rfl | hn
Proof state after:
case inl
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
⊢ 0 ≤ 3 * (a ^ 0 / ↑0) + 4 * (a ^ 0 * (z ^ 0).re / ↑0) + a ^ 0 * ((z ^ 2) ^ 0).re / ↑0

case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * (a ^ n / ↑n) + 4 * (a ^ n * (z ^ n).re / ↑n) + a ^ n * ((z ^ 2) ^ n).re / ↑n
Theorem: re_log_comb_nonneg'
Proof state before:
case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * (a ^ n / ↑n) + 4 * (a ^ n * (z ^ n).re / ↑n) + a ^ n * ((z ^ 2) ^ n).re / ↑n
Tactic:
field_simp
Proof state after:
case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ (3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ 2) ^ n).re) / ↑n
Theorem: re_log_comb_nonneg'
Proof state before:
case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ (3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ 2) ^ n).re) / ↑n
Tactic:
refine div_nonneg ?_ n.cast_nonneg
Proof state after:
case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ 2) ^ n).re
Theorem: re_log_comb_nonneg'
Proof state before:
case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ 2) ^ n).re
Tactic:
rw [← pow_mul, pow_mul', sq, mul_re, ← sq, ← sq, ← sq_abs_sub_sq_re, ← norm_eq_abs, norm_pow, hz]
Proof state after:
case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ n).re ^ 2 - ((1 ^ n) ^ 2 - (z ^ n).re ^ 2))
Theorem: re_log_comb_nonneg'
Proof state before:
case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ n).re ^ 2 - ((1 ^ n) ^ 2 - (z ^ n).re ^ 2))
Tactic:
calc
  0 ≤ 2 * a ^ n * ((z ^ n).re + 1) ^ 2 := by positivity
  _ = _  := by ring
Proof state after:
no goals
Theorem: re_log_comb_nonneg'
Proof state before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
⊢ ‖↑a‖ < 1
Tactic:
simp only [norm_eq_abs, abs_ofReal, _root_.abs_of_nonneg ha₀, ha₁]
Proof state after:
no goals
Theorem: re_log_comb_nonneg'
Proof state before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
⊢ ‖↑a * z‖ < 1
Tactic:
rwa [norm_mul, hz, mul_one]
Proof state after:
no goals
Theorem: re_log_comb_nonneg'
Proof state before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
⊢ ‖↑a * z ^ 2‖ < 1
Tactic:
rwa [norm_mul, norm_pow, hz, one_pow, mul_one]
Proof state after:
no goals
Theorem: re_log_comb_nonneg'
Proof state before:
case inl
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
⊢ 0 ≤ 3 * (a ^ 0 / ↑0) + 4 * (a ^ 0 * (z ^ 0).re / ↑0) + a ^ 0 * ((z ^ 2) ^ 0).re / ↑0
Tactic:
simp
Proof state after:
no goals
Theorem: re_log_comb_nonneg'
Proof state before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 2 * a ^ n * ((z ^ n).re + 1) ^ 2
Tactic:
positivity
Proof state after:
no goals
Theorem: re_log_comb_nonneg'
Proof state before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 2 * a ^ n * ((z ^ n).re + 1) ^ 2 =
    3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ n).re ^ 2 - ((1 ^ n) ^ 2 - (z ^ n).re ^ 2))
Tactic:
ring
Proof state after:
no goals
Theorem: re_log_comb_nonneg_dirichlet
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
⊢ 0 ≤
    3 * (-(1 - 1 ↑n * ↑n ^ (-↑x)).log).re + 4 * (-(1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y))).log).re +
      (-(1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y))).log).re
Tactic:
by_cases hn' : IsUnit (n : ZMod N)
Proof state after:
case pos
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
⊢ 0 ≤
    3 * (-(1 - 1 ↑n * ↑n ^ (-↑x)).log).re + 4 * (-(1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y))).log).re +
      (-(1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y))).log).re

case neg
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : ¬IsUnit ↑n
⊢ 0 ≤
    3 * (-(1 - 1 ↑n * ↑n ^ (-↑x)).log).re + 4 * (-(1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y))).log).re +
      (-(1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y))).log).re