Jcost_one_plus_eps

formal source

  69
  70This is an exact algebraic identity from [P2]. -/
  71
  72theorem Jcost_one_plus_eps {eps : ℝ} (heps : 0 ≤ eps) :
  73    Jcost (1 + eps) = eps ^ 2 / (2 * (1 + eps)) := by
  74  unfold Jcost
  75  have hne : (1 : ℝ) + eps ≠ 0 := by linarith
  76  field_simp [hne]; ring
  77
  78/-- J(1+eps) <= eps^2/2 for eps >= 0.
  79
  80Proof: eps^2/(2*(1+eps)) <= eps^2/2 because 1+eps >= 1 and the numerator
  81is nonneg. -/
  82theorem Jcost_one_plus_eps_le_sq {eps : ℝ} (heps : 0 ≤ eps) :
  83    Jcost (1 + eps) ≤ eps ^ 2 / 2 := by
  84  rw [Jcost_one_plus_eps heps]
  85  have h1eps : (0 : ℝ) < 1 + eps := by linarith
  86  have h2eps : (0 : ℝ) < 2 * (1 + eps) := by linarith
  87  have h2 : (0 : ℝ) < 2 := by norm_num
  88  exact div_le_div_of_nonneg_left (sq_nonneg eps) h2 (by linarith)
  89
  90/-- The factored RCL pair budget at one site: 2*(J(a)+1)*J(lam).
  91With lam = 1 + d and d >= 0, the bound J(1+d) <= d^2/2 gives:
  92
  93  pairwiseStretchingChange(a, 1+d) = 2*(J(a)+1)*J(1+d) <= (J(a)+1)*d^2 -/
  94theorem pair_budget_factored_bound {a d : ℝ}
  95    (ha : 0 < a) (hd : 0 ≤ d) :
  96    pairwiseStretchingChange a (1 + d) ≤ (Jcost a + 1) * d ^ 2 := by
  97  have hlam : 0 < 1 + d := by linarith
  98  rw [pairwise_RCL_balance_factored ha hlam]
  99  have hJa : 0 ≤ Jcost a := Jcost_nonneg ha
 100  have hJlam_le : Jcost (1 + d) ≤ d ^ 2 / 2 := Jcost_one_plus_eps_le_sq hd
 101  nlinarith [Jcost_nonneg hlam]
 102