Theorem: EulerProduct.exp_sum_primes_log_eq_tsum (EulerProducts/Logarithm.lean)

State before:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
⊢ cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log) = ∑' (n : ℕ), f n
Tactic:
have hs {p : ℕ} (hp : 1 < p) : ‖f p‖ < 1 := hsum.of_norm.norm_lt_one (f := f.toMonoidHom) hp
State after:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
⊢ cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log) = ∑' (n : ℕ), f n

State before:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
⊢ cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log) = ∑' (n : ℕ), f n
Tactic:
have H := Complex.exp_tsum_primes hsum.of_norm.neg_clog_one_sub
State after:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
H :
  Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
⊢ cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log) = ∑' (n : ℕ), f n

State before:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
H :
  Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
⊢ cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log) = ∑' (n : ℕ), f n
Tactic:
have help (n : ℕ) : n.primesBelow.prod (fun p ↦ cexp (-log (1 - f p))) =
    n.primesBelow.prod fun p ↦ (1 - f p)⁻¹ := by
  refine Finset.prod_congr rfl (fun p hp ↦ ?_)
  rw [exp_neg, exp_log ?_]
  rw [ne_eq, sub_eq_zero, ← ne_eq]
  exact fun h ↦ (norm_one (α := ℂ) ▸ h.symm ▸ hs (Nat.prime_of_mem_primesBelow hp).one_lt).false
State after:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
H :
  Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
help : ∀ (n : ℕ), ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log) = ∏ p ∈ n.primesBelow, (1 - f p)⁻¹
⊢ cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log) = ∑' (n : ℕ), f n

State before:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
H :
  Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
help : ∀ (n : ℕ), ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log) = ∏ p ∈ n.primesBelow, (1 - f p)⁻¹
⊢ cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log) = ∑' (n : ℕ), f n
Tactic:
simp_rw [help] at H
State after:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
help : ∀ (n : ℕ), ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log) = ∏ p ∈ n.primesBelow, (1 - f p)⁻¹
H : Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - f p)⁻¹) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
⊢ cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log) = ∑' (n : ℕ), f n

State before:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
help : ∀ (n : ℕ), ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log) = ∏ p ∈ n.primesBelow, (1 - f p)⁻¹
H : Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - f p)⁻¹) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
⊢ cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log) = ∑' (n : ℕ), f n
Tactic:
exact tendsto_nhds_unique H <| eulerProduct_completely_multiplicative hsum
State after:
no goals

State before:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
H :
  Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
n : ℕ
⊢ ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log) = ∏ p ∈ n.primesBelow, (1 - f p)⁻¹
Tactic:
refine Finset.prod_congr rfl (fun p hp ↦ ?_)
State after:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
H :
  Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
n p : ℕ
hp : p ∈ n.primesBelow
⊢ cexp (-(1 - f p).log) = (1 - f p)⁻¹

State before:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
H :
  Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
n p : ℕ
hp : p ∈ n.primesBelow
⊢ cexp (-(1 - f p).log) = (1 - f p)⁻¹
Tactic:
rw [exp_neg, exp_log ?_]
State after:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
H :
  Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
n p : ℕ
hp : p ∈ n.primesBelow
⊢ 1 - f p ≠ 0

State before:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
H :
  Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
n p : ℕ
hp : p ∈ n.primesBelow
⊢ 1 - f p ≠ 0
Tactic:
rw [ne_eq, sub_eq_zero, ← ne_eq]
State after:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
H :
  Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
n p : ℕ
hp : p ∈ n.primesBelow
⊢ 1 ≠ f p

State before:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
H :
  Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
n p : ℕ
hp : p ∈ n.primesBelow
⊢ 1 ≠ f p
Tactic:
exact fun h ↦ (norm_one (α := ℂ) ▸ h.symm ▸ hs (Nat.prime_of_mem_primesBelow hp).one_lt).false
State after:
no goals