IndisputableMonolith.NumberTheory.CostTwistedLSeries

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.NumberTheory.PrimeCostSpectrum
   4
   5/-!
   6# Cost-Twisted Arithmetic Functions and L-Functions
   7
   8This module generalizes the prime cost spectrum from
   9`IndisputableMonolith.NumberTheory.PrimeCostSpectrum` to the
  10character-twisted setting.
  11
  12For each completely multiplicative arithmetic function `chi : ℕ → ℝ`
  13(typically the real part of a Dirichlet character), we define the
  14twisted prime cost spectrum value
  15  `c_chi(n) := Σ_p v_p(n) · J(p) · chi(p)`,
  16and prove the elementary properties: complete additivity, the
  17relationship to the prime-restricted partial sum
  18`Π_chi(x) := Σ_{p ≤ x} J(p) chi(p)`, and the structural identities.
  19
  20The Dirichlet series of `c_chi` factorizes through the corresponding
  21L-function (paper-level result; not formalized analytically here).
  22
  23## Lean status: 0 sorry
  24-/
  25
  26namespace IndisputableMonolith
  27namespace NumberTheory
  28namespace CostTwistedLSeries
  29
  30open Cost PrimeCostSpectrum
  31
  32noncomputable section
  33
  34/-! ## Twisted prime cost
  35
  36For a function `chi : ℕ → ℝ`, the cost of a prime `p` twisted by `chi`
  37is `J(p) · chi(p)`. -/
  38
  39/-- The cost of a prime `p` twisted by an arithmetic function `chi`. -/
  40def twistedPrimeCost (chi : ℕ → ℝ) (p : ℕ) : ℝ :=
  41  primeCost p * chi p
  42
  43/-- The cost spectrum value of `n` twisted by `chi`, defined via the
  44    prime factorization. -/
  45def twistedCostSpectrumValue (chi : ℕ → ℝ) (n : ℕ) : ℝ :=
  46  n.factorization.sum fun p k => (k : ℝ) * twistedPrimeCost chi p
  47
  48@[simp]
  49theorem twistedCostSpectrumValue_one (chi : ℕ → ℝ) :
  50    twistedCostSpectrumValue chi 1 = 0 := by
  51  unfold twistedCostSpectrumValue
  52  simp [Nat.factorization_one]
  53
  54@[simp]
  55theorem twistedCostSpectrumValue_zero (chi : ℕ → ℝ) :
  56    twistedCostSpectrumValue chi 0 = 0 := by
  57  unfold twistedCostSpectrumValue
  58  simp [Nat.factorization_zero]
  59
  60/-- For a prime `p`, the twisted cost is `J(p) · chi(p)`. -/
  61theorem twistedCostSpectrumValue_prime (chi : ℕ → ℝ) {p : ℕ}
  62    (hp : Nat.Prime p) :
  63    twistedCostSpectrumValue chi p = primeCost p * chi p := by
  64  unfold twistedCostSpectrumValue twistedPrimeCost
  65  rw [Nat.Prime.factorization hp]
  66  simp [Finsupp.sum_single_index]
  67
  68/-- For a prime power `p^k`, the twisted cost is `k · J(p) · chi(p)`. -/
  69theorem twistedCostSpectrumValue_pow (chi : ℕ → ℝ) {p k : ℕ}
  70    (hp : Nat.Prime p) :
  71    twistedCostSpectrumValue chi (p ^ k) = (k : ℝ) * (primeCost p * chi p) := by
  72  unfold twistedCostSpectrumValue twistedPrimeCost
  73  rw [Nat.Prime.factorization_pow hp]
  74  simp [Finsupp.sum_single_index]
  75
  76/-- The twisted cost is completely additive over coprime products.
  77    This generalizes `costSpectrumValue_mul`. -/
  78theorem twistedCostSpectrumValue_mul (chi : ℕ → ℝ) {m n : ℕ}
  79    (hm : m ≠ 0) (hn : n ≠ 0) :
  80    twistedCostSpectrumValue chi (m * n)
  81      = twistedCostSpectrumValue chi m + twistedCostSpectrumValue chi n := by
  82  unfold twistedCostSpectrumValue
  83  rw [Nat.factorization_mul hm hn]
  84  rw [Finsupp.sum_add_index']
  85  · intro p
  86    simp
  87  · intro p i j
  88    push_cast
  89    ring
  90
  91/-- For the trivial character `chi = 1`, the twisted cost spectrum value
  92    reduces to the standard cost spectrum value. -/
  93theorem twistedCostSpectrumValue_one_char (n : ℕ) :
  94    twistedCostSpectrumValue (fun _ => 1) n = costSpectrumValue n := by
  95  unfold twistedCostSpectrumValue costSpectrumValue twistedPrimeCost
  96  refine Finsupp.sum_congr ?_
  97  intro p _
  98  ring
  99
 100/-- Negating the character flips the sign of the twisted cost. -/
 101theorem twistedCostSpectrumValue_eq_neg (chi : ℕ → ℝ) (n : ℕ) :
 102    twistedCostSpectrumValue (fun p => -chi p) n
 103      = -twistedCostSpectrumValue chi n := by
 104  unfold twistedCostSpectrumValue twistedPrimeCost
 105  rw [Finsupp.sum, Finsupp.sum]
 106  rw [← Finset.sum_neg_distrib]
 107  apply Finset.sum_congr rfl
 108  intro p _
 109  ring
 110
 111/-! ## The twisted prime cost sum
 112
 113The twisted analog of the prime cost sum `Π(x)`. -/
 114
 115/-- The twisted prime cost sum:
 116    `Π_chi(x) := Σ_{p ≤ x prime} J(p) · chi(p)`.
 117
 118    Defined as a finite sum over primes ≤ N (using the fact that
 119    `Nat.primesBelow` returns the finset of primes below N). -/
 120def twistedPrimeCostSum (chi : ℕ → ℝ) (N : ℕ) : ℝ :=
 121  (Finset.range (N + 1)).sum fun p =>
 122    if Nat.Prime p then primeCost p * chi p else 0
 123
 124@[simp]
 125theorem twistedPrimeCostSum_zero (chi : ℕ → ℝ) :
 126    twistedPrimeCostSum chi 0 = 0 := by
 127  simp [twistedPrimeCostSum, Nat.not_prime_zero]
 128
 129/-- For the trivial character, the twisted prime cost sum equals the
 130    untwisted version. -/
 131theorem twistedPrimeCostSum_one_char (N : ℕ) :
 132    twistedPrimeCostSum (fun _ => 1) N
 133      = (Finset.range (N + 1)).sum fun p =>
 134          if Nat.Prime p then primeCost p else 0 := by
 135  unfold twistedPrimeCostSum
 136  congr 1
 137  ext p
 138  by_cases hp : Nat.Prime p
 139  · simp [hp]
 140  · simp [hp]
 141
 142/-! ## Master certificate -/
 143
 144/-- Master certificate: the elementary properties of the cost-twisted
 145    arithmetic function. -/
 146theorem cost_twisted_certificate :
 147    -- (1) Twisted cost is zero at n = 1.
 148    (∀ (chi : ℕ → ℝ), twistedCostSpectrumValue chi 1 = 0) ∧
 149    -- (2) Twisted cost is completely additive over positive products.
 150    (∀ (chi : ℕ → ℝ) {m n : ℕ}, m ≠ 0 → n ≠ 0 →
 151      twistedCostSpectrumValue chi (m * n)
 152        = twistedCostSpectrumValue chi m + twistedCostSpectrumValue chi n) ∧
 153    -- (3) Twisted cost on a prime equals J(p) · chi(p).
 154    (∀ (chi : ℕ → ℝ) {p : ℕ}, Nat.Prime p →
 155      twistedCostSpectrumValue chi p = primeCost p * chi p) ∧
 156    -- (4) Twisted cost on a prime power equals k · J(p) · chi(p).
 157    (∀ (chi : ℕ → ℝ) {p k : ℕ}, Nat.Prime p →
 158      twistedCostSpectrumValue chi (p ^ k) = (k : ℝ) * (primeCost p * chi p)) ∧
 159    -- (5) Trivial character recovers untwisted cost.
 160    (∀ (n : ℕ), twistedCostSpectrumValue (fun _ => 1) n = costSpectrumValue n) ∧
 161    -- (6) Negation flips sign.
 162    (∀ (chi : ℕ → ℝ) (n : ℕ),
 163      twistedCostSpectrumValue (fun p => -chi p) n
 164        = -twistedCostSpectrumValue chi n) :=
 165  ⟨twistedCostSpectrumValue_one,
 166   @twistedCostSpectrumValue_mul,
 167   @twistedCostSpectrumValue_prime,
 168   @twistedCostSpectrumValue_pow,
 169   twistedCostSpectrumValue_one_char,
 170   twistedCostSpectrumValue_eq_neg⟩
 171
 172end
 173
 174end CostTwistedLSeries
 175end NumberTheory
 176end IndisputableMonolith
 177