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

summand_decomposition

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)

 245private lemma summand_decomposition (p k : ℕ) (hp : Nat.Prime p) :
 246    (k : ℝ) * primeCost p =
 247      (1/2) * ((k : ℝ) * (p : ℝ))
 248      + (1/2) * ((k : ℝ) / (p : ℝ)) - (k : ℝ) := by

proof body

Tactic-mode proof.

 249  unfold primeCost Jcost
 250  have hp_pos : (0 : ℝ) < (p : ℝ) := by exact_mod_cast hp.pos
 251  have hp_ne : (p : ℝ) ≠ 0 := ne_of_gt hp_pos
 252  field_simp
 253
 254/-! ## Power formula and Omega bound -/
 255
 256/-- For any positive integer `n` and any natural `k`,
 257    `c(n^k) = k · c(n)`.  This is the complete-additivity of `c`
 258    extended to repeated multiplication. -/

depends on (15)

Lean names referenced from this declaration's body.