PrimeNormStructure

formal source

  67    norm `‖·‖ > 1` on each element.  This abstracts away from the
  68    specific arithmetic structure (integer primes, monic irreducible
  69    polynomials, prime ideals in number fields, etc.). -/
  70class PrimeNormStructure (P : Type*) where
  71  norm : P → ℝ
  72  norm_gt_one : ∀ p : P, 1 < norm p
  73
  74variable {P : Type*} [PrimeNormStructure P]
  75
  76/-- The cost of an abstract prime: `J(‖p‖)`. -/
  77def primeJcost (p : P) : ℝ := Jcost (PrimeNormStructure.norm p)
  78
  79/-- The cost of any prime is strictly positive. -/
  80theorem primeJcost_pos (p : P) : 0 < primeJcost p := by
  81  unfold primeJcost
  82  apply Jcost_pos_of_ne_one
  83  · linarith [PrimeNormStructure.norm_gt_one p]
  84  · linarith [PrimeNormStructure.norm_gt_one p]
  85
  86theorem primeJcost_nonneg (p : P) : 0 ≤ primeJcost p :=
  87  le_of_lt (primeJcost_pos p)
  88
  89/-! ## The universal cost spectrum value -/
  90
  91variable [DecidableEq P]
  92
  93/-- The universal cost spectrum value on `f : P →₀ ℕ`.
  94
  95    Interpreting `f` as the multiplicity vector of an element of the
  96    multiplicative monoid generated by `P`, this is the cost-weighted
  97    sum `Σ_p f(p) · J(‖p‖)`. -/
  98def universalCost (f : P →₀ ℕ) : ℝ :=
  99  f.sum (fun p k => (k : ℝ) * primeJcost p)
 100