-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
private lemma summable_F'' : Summable F''

Proof state:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ Summable ArithmeticFunction.vonMangoldt.F''

Tactic:
suffices Summable fun (pk : Nat.Primes × ℕ) ↦ (pk.1 : ℝ)⁻¹ ^ (pk.2 + 3 / 2 : ℝ) by
  refine (Summable.mul_left 2 this).of_nonneg_of_le (fun pk ↦ ?_) (fun pk ↦ F''_le pk.1 pk.2)
  simp only [F'', Function.comp_apply, F', F₀, Prod.map_fst, id_eq, Prod.map_snd, Nat.cast_pow]
  have := vonMangoldt_nonneg (n := (pk.1 : ℕ) ^ (pk.2 + 2))
  positivity

Result:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ Summable fun pk => (↑↑pk.1)⁻¹ ^ (↑pk.2 + 3 / 2)

Proof state:
case refine_2.refine_2.h
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ (1 - (↑↑p)⁻¹)⁻¹ ≤ 2

Tactic:
rw [inv_le_comm₀ (sub_pos.mpr (hp₁ p)) zero_lt_two, le_sub_comm,
  show (1 : ℝ) - 2⁻¹ = 2⁻¹ by norm_num, inv_le_inv₀ (mod_cast p.prop.pos) zero_lt_two]

Result:
case refine_2.refine_2.h
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ 2 ≤ ↑↑p

Proof state:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ Summable fun pk => (↑↑pk.1)⁻¹ ^ pk.2 * (↑↑pk.1)⁻¹ ^ (3 / 2)

Tactic:
refine (summable_prod_of_nonneg (fun _ ↦ by positivity)).mpr ⟨(fun p ↦ ?_), ?_⟩

Result:
case refine_1
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ Summable fun y => (↑↑(p, y).1)⁻¹ ^ (p, y).2 * (↑↑(p, y).1)⁻¹ ^ (3 / 2)

case refine_2
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ Summable fun x => ∑' (y : ℕ), (↑↑(x, y).1)⁻¹ ^ (x, y).2 * (↑↑(x, y).1)⁻¹ ^ (3 / 2)

Proof state:
⊢ Summable ArithmeticFunction.vonMangoldt.F''

Tactic:
have hp₀ (p : Nat.Primes) : 0 < (p : ℝ)⁻¹ := inv_pos_of_pos (Nat.cast_pos.mpr p.prop.pos)

Result:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
⊢ Summable ArithmeticFunction.vonMangoldt.F''

Proof state:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ Summable fun pk => (↑↑pk.1)⁻¹ ^ (↑pk.2 + 3 / 2)

Tactic:
conv => enter [1, pk]; rw [Real.rpow_add <| hp₀ pk.1, Real.rpow_natCast]

Result:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ Summable fun pk => (↑↑pk.1)⁻¹ ^ pk.2 * (↑↑pk.1)⁻¹ ^ (3 / 2)

Proof state:
case refine_2.refine_2
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ (1 - (↑↑p)⁻¹)⁻¹ * (↑↑p ^ (3 / 2))⁻¹ ≤ 2 * (↑↑p ^ (3 / 2))⁻¹

Tactic:
gcongr

Result:
case refine_2.refine_2.h
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ (1 - (↑↑p)⁻¹)⁻¹ ≤ 2

Proof state:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
this : Summable fun pk => (↑↑pk.1)⁻¹ ^ (↑pk.2 + 3 / 2)
pk : Nat.Primes × ℕ
⊢ 0 ≤ ArithmeticFunction.vonMangoldt.F'' pk

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

Result:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
this : Summable fun pk => (↑↑pk.1)⁻¹ ^ (↑pk.2 + 3 / 2)
pk : Nat.Primes × ℕ
⊢ 0 ≤ (if Nat.Prime (↑pk.1 ^ (pk.2 + 1 + 1)) then 0 else Λ (↑pk.1 ^ (pk.2 + 1 + 1))) / ↑↑pk.1 ^ (pk.2 + 1 + 1)

Proof state:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
this✝ : Summable fun pk => (↑↑pk.1)⁻¹ ^ (↑pk.2 + 3 / 2)
pk : Nat.Primes × ℕ
this : 0 ≤ Λ (↑pk.1 ^ (pk.2 + 2))
⊢ 0 ≤ (if Nat.Prime (↑pk.1 ^ (pk.2 + 1 + 1)) then 0 else Λ (↑pk.1 ^ (pk.2 + 1 + 1))) / ↑↑pk.1 ^ (pk.2 + 1 + 1)

Tactic:
positivity

Result:
no goals

Proof state:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ -(3 / 2) < -1

Tactic:
norm_num

Result:
no goals

Proof state:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
this : Summable fun pk => (↑↑pk.1)⁻¹ ^ (↑pk.2 + 3 / 2)
⊢ Summable ArithmeticFunction.vonMangoldt.F''

Tactic:
refine (Summable.mul_left 2 this).of_nonneg_of_le (fun pk ↦ ?_) (fun pk ↦ F''_le pk.1 pk.2)

Result:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
this : Summable fun pk => (↑↑pk.1)⁻¹ ^ (↑pk.2 + 3 / 2)
pk : Nat.Primes × ℕ
⊢ 0 ≤ ArithmeticFunction.vonMangoldt.F'' pk

Proof state:
case refine_2
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ Summable fun x => ∑' (y : ℕ), (↑↑(x, y).1)⁻¹ ^ (x, y).2 * (↑↑(x, y).1)⁻¹ ^ (3 / 2)

Tactic:
dsimp only

Result:
case refine_2
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ Summable fun x => ∑' (y : ℕ), (↑↑x)⁻¹ ^ y * (↑↑x)⁻¹ ^ (3 / 2)

Proof state:
case refine_2.refine_1
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
this : 0 < 1 - (↑↑p)⁻¹
⊢ 0 ≤ (1 - (↑↑p)⁻¹)⁻¹ * (↑↑p)⁻¹ ^ (3 / 2)

Tactic:
positivity

Result:
no goals

Proof state:
case refine_2.refine_2.h
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ 2 ≤ ↑↑p

Tactic:
exact Nat.ofNat_le_cast.mpr p.prop.two_le

Result:
no goals

Proof state:
case refine_2.refine_1
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ 0 ≤ (1 - (↑↑p)⁻¹)⁻¹ * (↑↑p)⁻¹ ^ (3 / 2)

Tactic:
have := sub_pos.mpr (hp₁ p)

Result:
case refine_2.refine_1
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
this : 0 < 1 - (↑↑p)⁻¹
⊢ 0 ≤ (1 - (↑↑p)⁻¹)⁻¹ * (↑↑p)⁻¹ ^ (3 / 2)

Proof state:
case refine_2
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ Summable fun p => (1 - (↑↑p)⁻¹)⁻¹ * (↑↑p)⁻¹ ^ (3 / 2)

Tactic:
refine (summable_rpow.mpr (by norm_num : -(3 / 2 : ℝ) < -1)).mul_left 2
  |>.of_nonneg_of_le (fun p ↦ ?_) (fun p ↦ ?_)

Result:
case refine_2.refine_1
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ 0 ≤ (1 - (↑↑p)⁻¹)⁻¹ * (↑↑p)⁻¹ ^ (3 / 2)

case refine_2.refine_2
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ (1 - (↑↑p)⁻¹)⁻¹ * (↑↑p)⁻¹ ^ (3 / 2) ≤ 2 * ↑↑p ^ (-(3 / 2))

Proof state:
case refine_2
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ Summable fun x => ∑' (y : ℕ), (↑↑x)⁻¹ ^ y * (↑↑x)⁻¹ ^ (3 / 2)

Tactic:
conv => enter [1, p]; rw [tsum_mul_right, tsum_geometric_of_lt_one (hp₀ p).le (hp₁ p)]

Result:
case refine_2
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ Summable fun p => (1 - (↑↑p)⁻¹)⁻¹ * (↑↑p)⁻¹ ^ (3 / 2)

Proof state:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
⊢ Summable ArithmeticFunction.vonMangoldt.F''

Tactic:
have hp₁ (p : Nat.Primes) : (p : ℝ)⁻¹ < 1 :=
  (inv_lt_one₀ <| mod_cast p.prop.pos).mpr <| Nat.one_lt_cast.mpr <| p.prop.one_lt

Result:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ Summable ArithmeticFunction.vonMangoldt.F''

Proof state:
case refine_2.refine_2
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ (1 - (↑↑p)⁻¹)⁻¹ * (↑↑p)⁻¹ ^ (3 / 2) ≤ 2 * ↑↑p ^ (-(3 / 2))

Tactic:
rw [Real.inv_rpow p.val.cast_nonneg, Real.rpow_neg p.val.cast_nonneg]

Result:
case refine_2.refine_2
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ (1 - (↑↑p)⁻¹)⁻¹ * (↑↑p ^ (3 / 2))⁻¹ ≤ 2 * (↑↑p ^ (3 / 2))⁻¹

Proof state:
case refine_1
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ Summable fun y => (↑↑(p, y).1)⁻¹ ^ (p, y).2 * (↑↑(p, y).1)⁻¹ ^ (3 / 2)

Tactic:
dsimp only

Result:
case refine_1
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ Summable fun y => (↑↑p)⁻¹ ^ y * (↑↑p)⁻¹ ^ (3 / 2)