-- Mathlib/NumberTheory/EulerProduct/Basic.lean
/-- We relate a finite product over primes in `s` to an infinite sum over `s`-factored numbers. -/
lemma summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum
    (hsum : ∀ {p : ℕ}, p.Prime → Summable (fun n : ℕ ↦ ‖f (p ^ n)‖)) (s : Finset ℕ) :
    Summable (fun m : factoredNumbers s ↦ ‖f m‖) ∧
      HasSum (fun m : factoredNumbers s ↦ f m)
        (∏ p ∈ s with p.Prime, ∑' n : ℕ, f (p ^ n))

Proof state:
case pos.right
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ filter (fun p => Nat.Prime p) s
this : T3Space R
⊢ Summable fun x => f (p ^ x.1) * f ↑x.2

Tactic:
apply summable_mul_of_summable_norm (hsum hpp) ih.1

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
hpp : ¬Nat.Prime p
⊢ (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ x ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (x ^ n))

Tactic:
rwa [factoredNumbers_insert s hpp]

Result:
no goals

Proof state:
case empty
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖
⊢ (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) ∅, ∑' (n : ℕ), f (p ^ n))

Tactic:
simp only [not_mem_empty, IsEmpty.forall_iff, forall_const, filter_true_of_mem, prod_empty]

Result:
case empty
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖
⊢ (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) 1

Proof state:
case pos.right
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ filter (fun p => Nat.Prime p) s
this : T3Space R
⊢ HasSum (fun x => f (p ^ x.1) * f ↑x.2)
    ((∑' (n : ℕ), f (p ^ n)) * ∏ x ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (x ^ n))

Tactic:
apply (hsum hpp).of_norm.hasSum.mul ih.2

Result:
case pos.right
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ filter (fun p => Nat.Prime p) s
this : T3Space R
⊢ Summable fun x => f (p ^ x.1) * f ↑x.2

Proof state:
case pos.right
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ filter (fun p => Nat.Prime p) s
⊢ HasSum (fun x => f (p ^ x.1) * f ↑x.2)
    ((∑' (n : ℕ), f (p ^ n)) * ∏ x ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (x ^ n))

Tactic:
have : T3Space R := instT3Space

Result:
case pos.right
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ filter (fun p => Nat.Prime p) s
this : T3Space R
⊢ HasSum (fun x => f (p ^ x.1) * f ↑x.2)
    ((∑' (n : ℕ), f (p ^ n)) * ∏ x ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (x ^ n))

Proof state:
case pos.left
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
⊢ Summable fun x => ‖f (p ^ x.1) * f ↑x.2‖

Tactic:
refine Summable.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun _ ↦ norm_mul_le ..) ?_

Result:
case pos.left
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
⊢ Summable fun x => ‖f (p ^ x.1)‖ * ‖f ↑x.2‖

Proof state:
case pos.left
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
⊢ Summable fun x => ‖f (p ^ x.1)‖ * ‖f ↑x.2‖

Tactic:
apply Summable.mul_of_nonneg (hsum hpp) ih.1 <;> exact fun n ↦ norm_nonneg _

Result:
no goals

Proof state:
case pos.left
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
⊢ Summable fun m => ‖f ↑m‖

Tactic:
simp only [← (equivProdNatFactoredNumbers hpp hp).summable_iff, Function.comp_def,
  equivProdNatFactoredNumbers_apply', factoredNumbers.map_prime_pow_mul hmul hpp hp]

Result:
case pos.left
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
⊢ Summable fun x => ‖f (p ^ x.1) * f ↑x.2‖