Skip to content

add lemma relating task cost and task rbf

Kimaya Bedarkar requested to merge RTS/internships-2021:task_rbf_lemma into master

Currently, we have lemmas stating that task_rbf at \vareosilon is greater than equal to task cost, and task_rbf is monotone. I combined these two lemmas to state that tsk_rbf at any point greater than 0 is greater than task cost. I find that this fact is regularly required in proofs and therefore, would be good to have in the facts folder.

Merge request reports