DelayPrefixBound.lean

1import BFPP.Profiles23/-! # The delay estimate only needs strict predecessors -/45namespace BFPP.Profile67set_option autoImplicit false8open Set910variable {ι : Type*} [LinearOrder ι] [OrderBot ι]1112theorem delayValue_abs_sub_le_of_prefix (a b : Profile ι) (i : ι) (c : ℝ) (hc : 0 ≤ c)13    (h : ∀ j, j < i → |a.val j - b.val j| ≤ c) : |a.delayValue i - b.delayValue i| ≤ c := by14  classical15  by_cases hi : i = ⊥16  · simpa only [hi, delayValue_bot, sub_self, abs_zero] using hc17  · letI : Nonempty (Iio i) := ⟨⟨⊥, lt_of_le_of_ne bot_le (Ne.symm hi)⟩⟩18    rw [delayValue, if_neg hi, delayValue, if_neg hi]19    exact abs_ciSup_sub_ciSup_le _ _ (a.prefix_bddAbove i) (b.prefix_bddAbove i) c20      (fun j => h j.val j.property)2122end BFPP.Profile

SHA-256