CostPotentialBound

formal source

  67/-- A growth bound for the cost potential at a multiplicative index `v`
  68    with respect to a chosen norm `‖v‖`.  We state the abstract bound
  69    rather than fixing a specific norm. -/
  70structure CostPotentialBound (norm : MultIndex → ℝ) (R : ℝ) (α : ℝ) : Prop where
  71  growth : ∀ v : MultIndex, R * norm v ^ α ≤ costAt v
  72
  73/-- Sub-conjecture C.2 (precondition): the cost potential grows linearly
  74    in the L¹-norm of the multiplicative index.
  75
  76    Specifically: there exists `R > 0` such that
  77    `costAt v ≥ R * Σ_p |v_p|`
  78    for every `v : MultIndex`.
  79
  80    This holds because `J(p) ≥ J(2) = 1/4` for all primes `p ≥ 2`, so
  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