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
proof body
Tactic-mode proof.
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. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.