weight_polynomial_decay_summable

formal source

 101/-- Polynomial decay (with exponent at least `1`, i.e., `ε ≥ 0`) implies
 102    square-summability.  We need `2 * (1 + ε) > 1` which holds for any
 103    `ε > -1/2`; in particular for any `ε ≥ 0`. -/
 104theorem weight_polynomial_decay_summable {lamP : Nat.Primes → ℝ}
 105    {ε : ℝ} (hε : 0 ≤ ε) (h : WeightDecayPolynomial lamP ε) :
 106    WeightSquareSummable lamP := by
 107  obtain ⟨C, hC_pos, hC⟩ := h
 108  -- Define the comparison function on Nat.Primes.
 109  set g : Nat.Primes → ℝ := fun p => (C / (p.val : ℝ) ^ (1 + ε)) ^ 2 with hg_def
 110  -- Step 1: g is summable.
 111  have h_g_sum : Summable g := by
 112    have h_exp : (1 : ℝ) < 2 * (1 + ε) := by linarith
 113    have h_nat_sum : Summable (fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ (2 * (1 + ε))) := by
 114      simpa using Real.summable_one_div_nat_rpow.mpr h_exp
 115    have h_inj : Function.Injective (fun p : Nat.Primes => p.val) := fun _ _ hpq => Subtype.ext hpq
 116    -- Comparison: (C / p^(1+ε))^2 = C^2 / p^(2(1+ε))
 117    -- Pull back to primes.
 118    have h_pulled : Summable (fun p : Nat.Primes =>
 119        (1 : ℝ) / ((p.val : ℝ)) ^ (2 * (1 + ε))) := by
 120      have := h_nat_sum.comp_injective h_inj
 121      simpa [Function.comp] using this
 122    have h_scaled : Summable (fun p : Nat.Primes =>
 123        C^2 * ((1 : ℝ) / ((p.val : ℝ)) ^ (2 * (1 + ε)))) :=
 124      h_pulled.mul_left (C^2)
 125    -- Now: g p = C^2 * (1 / p^(2(1+ε))).
 126    have h_g_eq : ∀ p : Nat.Primes,
 127        g p = C^2 * ((1 : ℝ) / ((p.val : ℝ)) ^ (2 * (1 + ε))) := by
 128      intro p
 129      have hpval : (0 : ℝ) < (p.val : ℝ) := by exact_mod_cast p.prop.pos
 130      have h_pow_split : ((p.val : ℝ)) ^ (2 * (1 + ε)) =
 131                       (((p.val : ℝ)) ^ (1 + ε)) ^ 2 := by
 132        rw [show (2 * (1 + ε) : ℝ) = (1 + ε) + (1 + ε) from by ring]
 133        rw [Real.rpow_add hpval]
 134        ring