cone_bound

formal source

  72        _ = rad x + ((Nat.succ n : ℝ) * U.ell0) := by
  73              simpa [Nat.cast_add, Nat.cast_one]
  74
  75lemma cone_bound
  76  (H : StepBounds K U time rad)
  77  {n x y} (h : Local.ReachN K n x y) :
  78  rad y - rad x ≤ U.c * (time y - time x) := by
  79  have ht := H.reach_time_eq (K:=K) (U:=U) (time:=time) (rad:=rad) h
  80  have hr := H.reach_rad_le  (K:=K) (U:=U) (time:=time) (rad:=rad) h
  81  have hτ : time y - time x = (n : ℝ) * U.tau0 := by
  82    have := congrArg (fun t => t - time x) ht
  83    simpa [sub_eq_add_neg, add_comm, add_left_comm, add_assoc] using this
  84  have hℓ : rad y - rad x ≤ (n : ℝ) * U.ell0 := by
  85    have := hr
  86    -- rearrange ≤ to a difference inequality
  87    have := sub_le_iff_le_add'.mpr this
  88    simpa [sub_eq_add_neg, add_comm, add_left_comm, add_assoc]
  89  -- In minimal RSUnits, ell0 = c * tau0 is available as the supplied field
  90  have hcτ : U.ell0 = U.c * U.tau0 := by simpa using (U.c_ell0_tau0).symm
  91  simpa [hτ, hcτ, mul_left_comm, mul_assoc] using hℓ
  92
  93/-- Saturation lemma restated: equality holds when each step exactly reaches its bounds. -/
  94lemma cone_bound_saturates
  95  (H : StepBounds K U time rad)
  96  (ht : ∀ {y z}, K.step y z → time z = time y + U.tau0)
  97  (hr : ∀ {y z}, K.step y z → rad z = rad y + U.ell0)
  98  {n x y} (h : Local.ReachN K n x y) :
  99  rad y - rad x = U.c * (time y - time x) := by
 100  have hineq := cone_bound (K:=K) (U:=U) (time:=time) (rad:=rad) H h
 101  have ht' : time y - time x = (n : ℝ) * U.tau0 := by
 102    have := H.reach_time_eq (K:=K) (U:=U) (time:=time) (rad:=rad) h
 103    have := congrArg (fun t => t - time x) this
 104    simpa [sub_eq_add_neg, add_comm, add_left_comm, add_assoc] using this
 105  have hr' : rad y - rad x = (n : ℝ) * U.ell0 := by