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

universalCost_pos

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)

 128theorem universalCost_pos {f : P →₀ ℕ} (hf : f ≠ 0) : 0 < universalCost f := by

proof body

Tactic-mode proof.

 129  obtain ⟨p, hp_mem⟩ := Finsupp.support_nonempty_iff.mpr hf
 130  have hk_pos : 0 < f p := by
 131    have := Finsupp.mem_support_iff.mp hp_mem
 132    exact Nat.pos_of_ne_zero this
 133  have hJ_pos : 0 < primeJcost p := primeJcost_pos p
 134  have hsummand_pos : 0 < (f p : ℝ) * primeJcost p := by
 135    have hk_real : (0 : ℝ) < (f p : ℝ) := by exact_mod_cast hk_pos
 136    exact mul_pos hk_real hJ_pos
 137  unfold universalCost
 138  rw [Finsupp.sum, ← Finset.sum_erase_add _ _ hp_mem]
 139  apply add_pos_of_nonneg_of_pos
 140  · apply Finset.sum_nonneg
 141    intro q _
 142    apply mul_nonneg
 143    · exact_mod_cast Nat.zero_le _
 144    · exact primeJcost_nonneg q
 145  · exact hsummand_pos
 146
 147/-! ## Power and multiplicative structure -/
 148
 149/-- The cost of a power `n · single p 1`: `c(n · single p 1) = n · J(‖p‖)`.
 150    More generally, scaling a single-prime Finsupp scales the cost. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (16)

Lean names referenced from this declaration's body.