WeightSquareSummable

formal source

  90/-- The bandwidth-derived decay condition on prime weights: the sum
  91    of squared weights is finite.  This is the operator-level analog
  92    of the RS bandwidth constraint. -/
  93def WeightSquareSummable (lamP : Nat.Primes → ℝ) : Prop :=
  94  Summable (fun p : Nat.Primes => (lamP p) ^ 2)
  95
  96/-- The stronger decay condition needed for compact resolvent:
  97    `λ_p = O(1/p^{1+ε})` for some `ε > 0`. -/
  98def WeightDecayPolynomial (lamP : Nat.Primes → ℝ) (ε : ℝ) : Prop :=
  99  ∃ C : ℝ, 0 < C ∧ ∀ p : Nat.Primes, |lamP p| ≤ C / (p.val : ℝ) ^ (1 + ε)
 100
 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 + ε)))) :=