dalembert_identity

formal source

 505  nlinarith [sq_nonneg (10 : ℝ), Real.sqrt_nonneg (Jcost 10 * Jcost 10)]
 506
 507/-- The d'Alembert identity: J(xy) + J(x/y) = 2J(x) + 2J(y) + 2J(x)J(y) -/
 508theorem dalembert_identity {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
 509    Jcost (x * y) + Jcost (x / y) = 2 * Jcost x + 2 * Jcost y + 2 * Jcost x * Jcost y := by
 510  have hx0 : x ≠ 0 := ne_of_gt hx
 511  have hy0 : y ≠ 0 := ne_of_gt hy
 512  have hxy : x * y ≠ 0 := mul_ne_zero hx0 hy0
 513  have hxdy : x / y ≠ 0 := div_ne_zero hx0 hy0
 514  simp only [Jcost_eq_sq hxy, Jcost_eq_sq hxdy, Jcost_eq_sq hx0, Jcost_eq_sq hy0]
 515  field_simp
 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) :