-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
/-- The function `n ↦ Λ n / n`, restricted to non-primes in a residue class, is summable.
This is used to convert results on `ArithmeticFunction.vonMangoldt.residueClass` to results
on primes in an arithmetic progression. -/
lemma summable_residueClass_non_primes_div :
    Summable fun n : ℕ ↦ (if n.Prime then 0 else residueClass a n) / n

Proof state:
case refine_1
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
⊢ Summable (ArithmeticFunction.vonMangoldt.F₀ ∘ Subtype.val)

Tactic:
have hFF' :
    F₀ ∘ Subtype.val (p := fun n ↦ n ∈ {n | IsPrimePow n}) = F' ∘ ⇑prodNatEquiv.symm := by
  refine (Equiv.eq_comp_symm prodNatEquiv (F₀ ∘ Subtype.val) F').mpr ?_
  ext1 n
  simp only [Function.comp_apply, F']
  congr

Result:
case refine_1
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
hFF' : ArithmeticFunction.vonMangoldt.F₀ ∘ Subtype.val = ArithmeticFunction.vonMangoldt.F' ∘ ⇑prodNatEquiv.symm
⊢ Summable (ArithmeticFunction.vonMangoldt.F₀ ∘ Subtype.val)

Proof state:
case refine_1
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
hFF' : ArithmeticFunction.vonMangoldt.F₀ ∘ Subtype.val = ArithmeticFunction.vonMangoldt.F' ∘ ⇑prodNatEquiv.symm
⊢ Summable ArithmeticFunction.vonMangoldt.F'

Tactic:
have hF'₀ (p : Nat.Primes) : F' (p, 0) = 0 := by simp only [zero_add, pow_one, hF₀, F']

Result:
case refine_1
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
hFF' : ArithmeticFunction.vonMangoldt.F₀ ∘ Subtype.val = ArithmeticFunction.vonMangoldt.F' ∘ ⇑prodNatEquiv.symm
hF'₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F' (p, 0) = 0
⊢ Summable ArithmeticFunction.vonMangoldt.F'

Proof state:
case refine_2
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
n : ℕ
hn : ¬IsPrimePow n
⊢ ArithmeticFunction.vonMangoldt.F₀ n = 0

Tactic:
simp +contextual only [div_eq_zero_iff, ite_eq_left_iff, vonMangoldt_eq_zero_iff, hn,
  not_false_eq_true, implies_true, Nat.cast_eq_zero, true_or, F₀]

Result:
no goals

Proof state:
case h
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
hFF' : ArithmeticFunction.vonMangoldt.F₀ ∘ Subtype.val = ArithmeticFunction.vonMangoldt.F' ∘ ⇑prodNatEquiv.symm
hF'₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F' (p, 0) = 0
x✝ : Nat.Primes × ℕ
⊢ ArithmeticFunction.vonMangoldt.F'' x✝ = (ArithmeticFunction.vonMangoldt.F' ∘ Prod.map _root_.id fun x => x + 1) x✝

Tactic:
simp only [Function.comp_apply, Prod.map_fst, id_eq, Prod.map_snd, F'', F']

Result:
no goals

Proof state:
case refine_1.refine_2
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
hFF' : ArithmeticFunction.vonMangoldt.F₀ ∘ Subtype.val = ArithmeticFunction.vonMangoldt.F' ∘ ⇑prodNatEquiv.symm
hF'₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F' (p, 0) = 0
hF'₁ : ArithmeticFunction.vonMangoldt.F'' = ArithmeticFunction.vonMangoldt.F' ∘ Prod.map _root_.id fun x => x + 1
u : Nat.Primes × ℕ
hu : u.2 = 0
⊢ ArithmeticFunction.vonMangoldt.F' u = 0

Tactic:
rw [← hF'₀ u.1, ← hu]

Result:
no goals

Proof state:
case pos
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
n : ℕ
h✝ : Nat.Prime n
⊢ 0 ≤ 0

case neg
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
n : ℕ
h✝ : ¬Nat.Prime n
⊢ residueClass a n ≤ Λ n

Tactic:
exacts [le_rfl, residueClass_le a n]

Result:
no goals

Proof state:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
⊢ ArithmeticFunction.vonMangoldt.F₀ ∘ Subtype.val = ArithmeticFunction.vonMangoldt.F' ∘ ⇑prodNatEquiv.symm

Tactic:
refine (Equiv.eq_comp_symm prodNatEquiv (F₀ ∘ Subtype.val) F').mpr ?_

Result:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
⊢ (ArithmeticFunction.vonMangoldt.F₀ ∘ Subtype.val) ∘ ⇑prodNatEquiv = ArithmeticFunction.vonMangoldt.F'

Proof state:
case h
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
n : Nat.Primes × ℕ
⊢ ((ArithmeticFunction.vonMangoldt.F₀ ∘ Subtype.val) ∘ ⇑prodNatEquiv) n = ArithmeticFunction.vonMangoldt.F' n

Tactic:
simp only [Function.comp_apply, F']

Result:
case h
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
n : Nat.Primes × ℕ
⊢ ArithmeticFunction.vonMangoldt.F₀ ↑(prodNatEquiv n) = ArithmeticFunction.vonMangoldt.F₀ (↑n.1 ^ (n.2 + 1))

Proof state:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ ArithmeticFunction.vonMangoldt.F₀ n
⊢ Summable fun n => (if Nat.Prime n then 0 else residueClass a n) / ↑n

Tactic:
refine Summable.of_nonneg_of_le h₀ hleF₀ ?_

Result:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ ArithmeticFunction.vonMangoldt.F₀ n
⊢ Summable ArithmeticFunction.vonMangoldt.F₀

Proof state:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
n : ℕ
⊢ (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ ArithmeticFunction.vonMangoldt.F₀ n

Tactic:
refine div_le_div_of_nonneg_right ?_ n.cast_nonneg

Result:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
n : ℕ
⊢ (if Nat.Prime n then 0 else residueClass a n) ≤ if Nat.Prime n then 0 else Λ n