Jcost_submult

formal source

 516  ring
 517
 518/-- From d'Alembert: J(xy) ≤ 2J(x) + 2J(y) + 2J(x)J(y) since J(x/y) ≥ 0 -/
 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
 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) -/
 527lemma Jcost_prod_bound {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
 528    Jcost (x * y) ≤ 2 * (1 + Jcost x) * (1 + Jcost y) - 2 := by
 529  have h := Jcost_submult hx hy
 530  -- 2*(1+J(x))*(1+J(y)) - 2 = 2*(1 + J(x) + J(y) + J(x)*J(y)) - 2
 531  --                        = 2 + 2*J(x) + 2*J(y) + 2*J(x)*J(y) - 2
 532  --                        = 2*J(x) + 2*J(y) + 2*J(x)*J(y)
 533  calc Jcost (x * y) ≤ 2 * Jcost x + 2 * Jcost y + 2 * Jcost x * Jcost y := h
 534    _ = 2 * (1 + Jcost x) * (1 + Jcost y) - 2 := by ring
 535
 536/-! ## Small-strain Taylor expansion -/
 537
 538lemma Jcost_one_plus_eps_quadratic (ε : ℝ) (hε : |ε| ≤ (1 : ℝ) / 2) :
 539    ∃ (c : ℝ), Jcost (1 + ε) = ε ^ 2 / 2 + c * ε ^ 3 ∧ |c| ≤ 2 := by
 540  classical
 541  have hbounds := abs_le.mp hε
 542  have hpos : 0 < 1 + ε := by
 543    have : -(1 : ℝ) / 2 ≤ ε := by simpa [neg_div] using hbounds.1
 544    linarith
 545  have hne : 1 + ε ≠ 0 := ne_of_gt hpos
 546  have hcalc : Jcost (1 + ε) = ε ^ 2 / (2 * (1 + ε)) := by
 547    simpa [pow_two, add_comm, add_left_comm, add_assoc, sub_eq_add_neg]
 548      using (Jcost_eq_sq hne)
 549  let c : ℝ := -1 / (2 * (1 + ε))