-- Mathlib/NumberTheory/EulerProduct/Basic.lean
/-- Given a (completely) multiplicative function `f : ℕ → F`, where `F` is a normed field,
such that `‖f p‖ < 1` for all primes `p`, we can express the sum of `f n` over all `s`-factored
positive integers `n` as a product of `(1 - f p)⁻¹` over the primes `p ∈ s`. At the same time,
we show that the sum involved converges absolutely. -/
lemma summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric {f : ℕ →* F}
    (h : ∀ {p : ℕ}, p.Prime → ‖f p‖ < 1) (s : Finset ℕ) :
    Summable (fun m : factoredNumbers s ↦ ‖f m‖) ∧
      HasSum (fun m : factoredNumbers s ↦ f m) (∏ p ∈ s with p.Prime, (1 - f p)⁻¹)

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
p : ℕ
hp : p ∈ filter (fun p => Nat.Prime p) s
⊢ ∑' (n : ℕ), f p ^ n = (1 - f p)⁻¹

Tactic:
exact tsum_geometric_of_norm_lt_one <| h (mem_filter.mp hp).2

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
H₁ : ∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n) = ∏ p ∈ filter (fun p => Nat.Prime p) s, (1 - f p)⁻¹
⊢ (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, (1 - f p)⁻¹)

Tactic:
have H₂ : ∀ {p : ℕ}, p.Prime → Summable fun n ↦ ‖f (p ^ n)‖ := by
  intro p hp
  simp only [map_pow]
  refine Summable.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun _ ↦ norm_pow_le ..) ?_
  exact summable_geometric_iff_norm_lt_one.mpr <| (norm_norm (f p)).symm ▸ h hp

Result:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
H₁ : ∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n) = ∏ p ∈ filter (fun p => Nat.Prime p) s, (1 - f p)⁻¹
H₂ : ∀ {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) s, (1 - f p)⁻¹)

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
⊢ (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, (1 - f p)⁻¹)

Tactic:
have H₁ :
    ∏ p ∈ s with p.Prime, ∑' n : ℕ, f (p ^ n) = ∏ p ∈ s with p.Prime, (1 - f p)⁻¹ := by
  refine prod_congr rfl fun p hp ↦ ?_
  simp only [map_pow]
  exact tsum_geometric_of_norm_lt_one <| h (mem_filter.mp hp).2

Result:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
H₁ : ∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n) = ∏ p ∈ filter (fun p => Nat.Prime p) s, (1 - f p)⁻¹
⊢ (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, (1 - f p)⁻¹)

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
⊢ ∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n) = ∏ p ∈ filter (fun p => Nat.Prime p) s, (1 - f p)⁻¹

Tactic:
refine prod_congr rfl fun p hp ↦ ?_

Result:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
p : ℕ
hp : p ∈ filter (fun p => Nat.Prime p) s
⊢ ∑' (n : ℕ), f (p ^ n) = (1 - f p)⁻¹

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
H₁ : ∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n) = ∏ p ∈ filter (fun p => Nat.Prime p) s, (1 - f p)⁻¹
p : ℕ
hp : Nat.Prime p
⊢ Summable fun n => ‖f (p ^ n)‖

Tactic:
simp only [map_pow]

Result:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
H₁ : ∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n) = ∏ p ∈ filter (fun p => Nat.Prime p) s, (1 - f p)⁻¹
p : ℕ
hp : Nat.Prime p
⊢ Summable fun n => ‖f p ^ n‖

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
p : ℕ
hp : p ∈ filter (fun p => Nat.Prime p) s
⊢ ∑' (n : ℕ), f (p ^ n) = (1 - f p)⁻¹

Tactic:
simp only [map_pow]

Result:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
p : ℕ
hp : p ∈ filter (fun p => Nat.Prime p) s
⊢ ∑' (n : ℕ), f p ^ n = (1 - f p)⁻¹

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
⊢ (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, (1 - f p)⁻¹)

Tactic:
have hmul {m n} (_ : Nat.Coprime m n) := f.map_mul m n

Result:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
⊢ (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, (1 - f p)⁻¹)

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
H₁ : ∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n) = ∏ p ∈ filter (fun p => Nat.Prime p) s, (1 - f p)⁻¹
p : ℕ
hp : Nat.Prime p
⊢ Summable fun n => ‖f p ^ n‖

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

Result:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
H₁ : ∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n) = ∏ p ∈ filter (fun p => Nat.Prime p) s, (1 - f p)⁻¹
p : ℕ
hp : Nat.Prime p
⊢ Summable (HPow.hPow ‖f p‖)

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
H₁ : ∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n) = ∏ p ∈ filter (fun p => Nat.Prime p) s, (1 - f p)⁻¹
H₂ : ∀ {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) s, (1 - f p)⁻¹)

Tactic:
exact H₁ ▸ summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum f.map_one hmul H₂ s

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
H₁ : ∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n) = ∏ p ∈ filter (fun p => Nat.Prime p) s, (1 - f p)⁻¹
p : ℕ
hp : Nat.Prime p
⊢ Summable (HPow.hPow ‖f p‖)

Tactic:
exact summable_geometric_iff_norm_lt_one.mpr <| (norm_norm (f p)).symm ▸ h hp

Result:
no goals