CostPotentialLinearGrowth

formal source

  81    `c(v) = Σ_p v_p J(p) ≥ Σ_p v_p · J(2)` when all `v_p ≥ 0`.  The
  82    general case (allowing negative `v_p`) requires the symmetry
  83    `J(1/p) = J(p)`. -/
  84def CostPotentialLinearGrowth : Prop :=
  85  ∃ R : ℝ, 0 < R ∧ ∀ v : MultIndex,
  86    R * (v.support.sum (fun p => |(v p : ℝ)|)) ≤ costAt v
  87
  88/-! ## Weight decay condition -/
  89
  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