lemma
proved
term proof
Jcost_submult
show as:
view Lean formalization →
formal statement (Lean)
519lemma Jcost_submult {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
520 Jcost (x * y) ≤ 2 * Jcost x + 2 * Jcost y + 2 * Jcost x * Jcost y := by
proof body
Term-mode proof.
521 have h := dalembert_identity hx hy
522 have hnonneg : 0 ≤ Jcost (x / y) := Jcost_nonneg (div_pos hx hy)
523 linarith
524
525/-- Bound on J product: J(xy) ≤ 2*(1 + J(x))*(1 + J(y)) - 2
526 This follows from d'Alembert since (1+J(x))(1+J(y)) = 1 + J(x) + J(y) + J(x)J(y) -/