Jcost_small_strain_bound

proof body

Tactic-mode proof.

  84  classical
  85  have hbounds := abs_le.mp hε
  86  have hpos : 0 < 1 + ε := by
  87    have : -(1 : ℝ) / 10 ≤ ε := by simpa [neg_div] using hbounds.1
  88    linarith
  89  have hne : 1 + ε ≠ 0 := ne_of_gt hpos
  90  have hform : Jcost (1 + ε) = ε ^ 2 / (2 * (1 + ε)) := by
  91    simpa [pow_two, add_comm, add_left_comm, add_assoc, sub_eq_add_neg]
  92      using (Jcost_eq_sq (x := 1 + ε) hne)
  93  have hden_pos : 0 < 2 * (1 + ε) := by nlinarith [hpos]
  94  -- Exact difference and absolute value
  95  have h1 : Jcost (1 + ε) - ε ^ 2 / 2
  96      = ε ^ 2 / (2 * (1 + ε)) - ε ^ 2 / 2 := by
  97    simpa [hform]
  98  have hx : (2 : ℝ) * (1 + ε) ≠ 0 := mul_ne_zero two_ne_zero hne
  99  have h2 : ε ^ 2 / (2 * (1 + ε)) - ε ^ 2 / 2 = -ε ^ 3 / (2 * (1 + ε)) := by
 100    field_simp [hx]
 101    ring
 102  have hdiff : Jcost (1 + ε) - ε ^ 2 / 2 = -ε ^ 3 / (2 * (1 + ε)) := h1.trans h2
 103  have habs : |Jcost (1 + ε) - ε ^ 2 / 2| = |ε| ^ 3 / (2 * (1 + ε)) := by
 104    have hposden : 0 < 2 * (1 + ε) := hden_pos
 105    simpa [abs_div, abs_neg, abs_pow, abs_of_pos hposden] using
 106      congrArg (fun z => |z|) hdiff
 107  -- Now bound using |ε|/(2(1+ε)) ≤ 1/18 from below
 108  have hx_lower : (9 : ℝ) / 10 ≤ 1 + ε := by linarith [show -(1 : ℝ) / 10 ≤ ε from by simpa [neg_div] using hbounds.1]
 109  have hx_pos : 0 < (9 : ℝ) / 10 := by norm_num
 110  have hx_inv : 1 / (1 + ε) ≤ (10 : ℝ) / 9 := by
 111    have := one_div_le_one_div_of_le hx_pos hx_lower
 112    simpa using this
 113  have hrec_bound : 1 / (2 * (1 + ε)) ≤ (5 : ℝ) / 9 := by
 114    have hmul : (1 / 2 : ℝ) * (1 / (1 + ε)) ≤ (1 / 2) * ((10 : ℝ) / 9) :=
 115      mul_le_mul_of_nonneg_left hx_inv (by norm_num)
 116    have hleft : 1 / (2 * (1 + ε)) = (1 / 2) * (1 / (1 + ε)) := by
 117      simp [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc]
 118    have hright : (5 : ℝ) / 9 = (1 / 2) * ((10 : ℝ) / 9) := by norm_num
 119    simpa [hleft, hright] using hmul
 120  have hrec_nonneg : 0 ≤ 1 / (2 * (1 + ε)) := by
 121    have : 0 ≤ 2 * (1 + ε) := le_of_lt (by nlinarith [hpos])
 122    exact one_div_nonneg.mpr this
 123  have hA : |ε| / (2 * (1 + ε)) ≤ (1 : ℝ) / 10 * (1 / (2 * (1 + ε))) := by
 124    simpa [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc]
 125      using mul_le_mul_of_nonneg_right hε hrec_nonneg
 126  have hB : (1 : ℝ) / 10 * (1 / (2 * (1 + ε))) ≤ (1 : ℝ) / 18 := by
 127    have hmul := mul_le_mul_of_nonneg_left hrec_bound (by norm_num : (0 : ℝ) ≤ (1 : ℝ) / 10)
 128    have hright : (1 : ℝ) / 18 = (1 : ℝ) / 10 * ((5 : ℝ) / 9) := by norm_num
 129    simpa [hright] using hmul
 130  have hfrac : |ε| / (2 * (1 + ε)) ≤ (1 : ℝ) / 18 := hA.trans hB
 131  -- Conclude
 132  have hineq : |Jcost (1 + ε) - ε ^ 2 / 2| ≤ |ε| ^ 2 / 18 := by
 133    have hnn : 0 ≤ |ε| ^ 2 := by
 134      have := sq_nonneg (|ε|); simpa [pow_two] using this
 135    have hmul := mul_le_mul_of_nonneg_left hfrac hnn
 136    calc
 137      |Jcost (1 + ε) - ε ^ 2 / 2| = |ε| ^ 3 / (2 * (1 + ε)) := by simpa [habs]
 138      _ ≤ |ε| ^ 2 * (1 / 18) := by
 139        simpa [pow_succ, pow_two, mul_comm, mul_left_comm, mul_assoc, div_eq_mul_inv] using hmul
 140      _ = |ε| ^ 2 / 18 := by simp [div_eq_mul_inv]
 141  have hratio : (1 : ℝ) / 18 ≤ 1 / 10 := by norm_num
 142  have hsq : |ε| ^ 2 = ε ^ 2 := by
 143    have h1 : |ε| * |ε| = |ε * ε| := by simpa [abs_mul]
 144    calc
 145      |ε| ^ 2 = |ε| * |ε| := by simpa [pow_two]
 146      _ = |ε * ε| := h1
 147      _ = |ε ^ 2| := by simpa [pow_two]
 148      _ = ε ^ 2 := by simpa [abs_of_nonneg (sq_nonneg ε)]
 149  have hcompare : |ε| ^ 2 / 18 ≤ ε ^ 2 / 10 := by
 150    have := mul_le_mul_of_nonneg_left hratio (by exact sq_nonneg ε)
 151    simpa [hsq, pow_two] using this
 152  exact (hineq.trans hcompare)
 153