theorem scaledRestrictedDualFunction_mem_Icc_of_concaveOn {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {Q : Set E} {F : E → ℝ} (hF : ConcaveOn ℝ Q F) {xBar : E} (hxBar : xBar ∈ Q) {τ : ℝ} (hτ : τ ∈ Set.Icc 0 1) (s : StrongDual ℝ E) : scaledRestrictedDualFunction Q (fun (x : E) => ↑(F x)) ⟨xBar, ⋯⟩ τ s ∈ Set.Icc 0 (↑τ * restrictedDualFunction Q (fun (x : E) => ↑(F x)) ⟨xBar, ⋯⟩ s)

Lemma 6.16: for a concave real-valued function F on Q, the scaled restricted dual function of the canonical WithTop lift of F at (τ, xBar) lies between 0 and τ times the unscaled restricted dual function.