theorem parametricValueFunction_strict_lt_right_and_secant_lower_bound {Index : Type u} {Param : Type v} {Decision : Type w} (Q : Set Decision) (hatFn checkFn : Index → Param → Decision → ℝ) (k : Index) (X : Param) {t0 t1 τ : ℝ} (ht0_lt_t1 : t0 < t1) (ht1_le_right : t1 ≤ τ) (hpos : 0 < extendedRealRealPart (parametricValueFunction Q (hatFn k X) (checkFn k X)) t1) (hτ_dom : τ ∈ extendedRealEffectiveDomain (parametricValueFunction Q (hatFn k X) (checkFn k X))) (hright_nonpos : parametricValueFunction Q (hatFn k X) (checkFn k X) τ ≤ 0) (hconvex : ConvexOn ℝ (Set.Iic τ) (extendedRealRealPart (parametricValueFunction Q (hatFn k X) (checkFn k X)))) : t1 < τ ∧ extendedRealRealPart (parametricValueFunction Q (hatFn k X) (checkFn k X)) t0 ≥ extendedRealRealPart (parametricValueFunction Q (hatFn k X) (checkFn k X)) t1 + (t1 - t0) / (τ - t1) * extendedRealRealPart (parametricValueFunction Q (hatFn k X) (checkFn k X)) t1

Lemma 3.3.5: if the finite real-part view of the complete-data owner value parametricValueFunction Q (hatFn k X) (checkFn k X) t₁ is positive for some t₀ < t₁ ≤ τ, the owner value at τ is finite and nonpositive, and the scalar slice is convex on (-∞, τ], then τ lies strictly to the right of t₁ and the displayed secant lower bound holds.