-- 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.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 ∉ Set.range (Prod.map _root_.id fun x => x + 1)
⊢ ArithmeticFunction.vonMangoldt.F' u = 0

Tactic:
simp only [Set.range_prod_map, Set.range_id, Set.mem_prod, Set.mem_univ, Set.mem_range,
  Nat.exists_add_one_eq, true_and, not_lt, nonpos_iff_eq_zero] at hu

Result:
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

Proof state:
q : ℕ
a : ZMod q
n : ℕ
this : 0 ≤ residueClass a n
⊢ 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n

Tactic:
positivity

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
p : Nat.Primes
⊢ ArithmeticFunction.vonMangoldt.F₀ ↑p = 0

Tactic:
simp only [p.prop, ↓reduceIte, zero_div, F₀]

Result:
no goals

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) ≤ if Nat.Prime n then 0 else Λ n

Tactic:
split_ifs

Result:
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

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₀ ∘ Subtype.val)

Tactic:
rw [hFF']

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' ∘ ⇑prodNatEquiv.symm)

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' ∘ ⇑prodNatEquiv.symm)

Tactic:
refine (Nat.Primes.prodNatEquiv.symm.summable_iff (f := F')).mpr ?_

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'

Proof state:
case refine_1.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
hF'₁ : ArithmeticFunction.vonMangoldt.F'' = ArithmeticFunction.vonMangoldt.F' ∘ Prod.map _root_.id fun x => x + 1
⊢ Function.Injective (Prod.map _root_.id fun x => x + 1)

Tactic:
exact Function.Injective.prodMap (fun ⦃a₁ a₂⦄ a ↦ a) <| add_left_injective 1

Result:
no goals

Proof state:
q : ℕ
a : ZMod q
⊢ Summable fun n => (if Nat.Prime n then 0 else residueClass a n) / ↑n

Tactic:
have h₀ (n : ℕ) : 0 ≤ (if n.Prime then 0 else residueClass a n) / n := by
  have := residueClass_nonneg a n
  positivity

Result:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
⊢ Summable fun n => (if Nat.Prime n 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)

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:
swap

Result:
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

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)

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
hFF' : ArithmeticFunction.vonMangoldt.F₀ ∘ Subtype.val = ArithmeticFunction.vonMangoldt.F' ∘ ⇑prodNatEquiv.symm
p : Nat.Primes
⊢ ArithmeticFunction.vonMangoldt.F' (p, 0) = 0

Tactic:
simp only [zero_add, pow_one, hF₀, F']

Result:
no goals