phiCostLinearCoeff

formal source

 123  convert h using 1 <;> ext x <;> simp [g, phiCost, Function.comp, Jlog_as_cosh]
 124
 125/-- Linear perturbation coefficient for `phiCost` on `[-A, A]`. -/
 126noncomputable def phiCostLinearCoeff (A : ℝ) : ℝ :=
 127  Real.log phi * Real.sinh (Real.log phi * A)
 128
 129/-- Quadratic perturbation coefficient for `phiCost` on `[-A, A]`. -/
 130noncomputable def phiCostQuadraticCoeff (A : ℝ) : ℝ :=
 131  kappa * Real.exp (Real.log phi * A)
 132
 133/-- On `|x| ≤ 1`, the exponential remainder is quadratically bounded. -/
 134private theorem abs_exp_sub_one_sub_id_le_sq_of_abs_le_one {x : ℝ} (hx : |x| ≤ 1) :
 135    |Real.exp x - 1 - x| ≤ x ^ 2 := by
 136  simpa [Real.norm_eq_abs, sub_eq_add_neg] using
 137    (Real.norm_exp_sub_one_sub_id_le (x := x) (by simpa [Real.norm_eq_abs] using hx))
 138
 139/-- On `|x| ≤ 1`, `cosh x - 1` is quadratically small. -/
 140private theorem cosh_sub_one_le_sq_of_abs_le_one {x : ℝ} (hx : |x| ≤ 1) :
 141    Real.cosh x - 1 ≤ x ^ 2 := by
 142  let A : ℝ := Real.exp x - 1 - x
 143  let B : ℝ := Real.exp (-x) - 1 + x
 144  have hA : |A| ≤ x ^ 2 := by
 145    dsimp [A]
 146    exact abs_exp_sub_one_sub_id_le_sq_of_abs_le_one hx
 147  have hB : |B| ≤ x ^ 2 := by
 148    have hxneg : |-x| ≤ 1 := by simpa using hx
 149    dsimp [B]
 150    simpa using abs_exp_sub_one_sub_id_le_sq_of_abs_le_one hxneg
 151  have hsum : |A + B| ≤ 2 * x ^ 2 := by
 152    calc
 153      |A + B| ≤ |A| + |B| := abs_add_le _ _
 154      _ ≤ x ^ 2 + x ^ 2 := add_le_add hA hB
 155      _ = 2 * x ^ 2 := by ring
 156  have hrewrite : A + B = 2 * (Real.cosh x - 1) := by