pith. machine review for the scientific record. sign in
theorem proved term proof

universal_cost_certificate

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 163theorem universal_cost_certificate :
 164    -- (1) Every prime cost is strictly positive.
 165    (∀ (p : P), 0 < primeJcost p) ∧
 166    -- (2) Cost is zero at the trivial Finsupp (the unit element).
 167    (universalCost (0 : P →₀ ℕ) = 0) ∧
 168    -- (3) Cost is additive.
 169    (∀ (f g : P →₀ ℕ),
 170      universalCost (f + g) = universalCost f + universalCost g) ∧
 171    -- (4) Cost on a singleton: c(single p k) = k · J(‖p‖).
 172    (∀ (p : P) (k : ℕ),
 173      universalCost (Finsupp.single p k) = (k : ℝ) * primeJcost p) ∧
 174    -- (5) Cost is nonneg.
 175    (∀ (f : P →₀ ℕ), 0 ≤ universalCost f) ∧
 176    -- (6) Cost is strictly positive on non-trivial Finsupps.
 177    (∀ {f : P →₀ ℕ}, f ≠ 0 → 0 < universalCost f) :=

proof body

Term-mode proof.

 178  ⟨primeJcost_pos,
 179   universalCost_zero,
 180   universalCost_add,
 181   universalCost_single,
 182   universalCost_nonneg,
 183   @universalCost_pos P _ _⟩
 184
 185/-! ## Instance: Integer primes -/
 186

depends on (17)

Lean names referenced from this declaration's body.