proposition: Lemma second_derivative_convex (t : {i01 R}) : a <= b -> f (a <| t |> b) <= f a <| t |> f b.
proof: Proof. rewrite le_eqVlt => /predU1P[<-|/[dup] ab]; first by rewrite !convmm. move/convexf_ptP; apply => x /andP[]. rewrite le_eqVlt => /predU1P[<-|ax]. by rewrite /L factorl mul0r addr0 subrr. rewrite le_eqVlt => /predU1P[->|xb]. by rewrite /L factorr ?lt_eqF// mul1r addrAC addrA subrK subrr. have [c2 Ic2 Hc2] : exists2 c2, x < c2 < b & (f b - f x) / (b - x) = 'D_1 f c2. have xbf : {in `]x, b[, forall z, derivable f z 1} := in1_subset_itv (subset_itvW _ _ (ltW ax) (lexx b)) HDf. have derivef z : z \in `]x, b[ -> is_derive z 1 f ('D_1 f z). by move=> zxb; apply/derivableP/xbf; exact: zxb. have [|z zxb fbfx] := MVT xb derivef. apply/(derivable_oo_continuous_bnd_within (And3 xbf _ cvg_left))/cvg_at_right_filter. have := derivable_within_continuous HDf. rewrite continuous_open_subspace//; last exact: interval_open. by apply; rewrite inE/= in_itv/= ax. by exists z => //; rewrite fbfx -mulrA divff ?mulr1// subr_eq0 gt_eqF. have [c1 Ic1 Hc1] : exists2 c1, a < c1 < x & (f x - f a) / (x - a) = 'D_1 f c1. have axf : {in `]a, x[, forall z, derivable f z 1} := in1_subset_itv (subset_itvW _ _ (lexx a) (ltW xb)) HDf. have derivef z : z \in `]a, x[ -> is_derive z 1 f ('D_1 f z). by move=> zax; apply /derivableP/axf. have [|z zax fxfa] := MVT ax derivef. apply/(derivable_oo_continuous_bnd_within (And3 axf cvg_right _))/cvg_at_left_filter. have := derivable_within_continuous HDf. rewrite continuous_open_subspace//; last exact: interval_open. by apply; rewrite inE/= in_itv/= ax. by exists z => //; rewrite fxfa -mulrA divff ?mulr1// subr_eq0 gt_eqF. have c1c2 : c1 < c2. by move: Ic2 Ic1 => /andP[+ _] => /[swap] /andP[_] /lt_trans; apply. have [d Id h] : exists2 d, c1 < d < c2 & ('D_1 f c2 - 'D_1 f c1) / (c2 - c1) = DDf d. have h : {in `]c1, c2[, forall z, derivable Df z 1}. apply: (in1_subset_itv (subset_itvW _ _ (ltW (andP Ic1).1) (lexx _))). apply: (in1_subset_itv (subset_itvW _ _ (lexx _) (ltW (andP Ic2).2))). exact: HDDf. have derivef z : z \in `]c1, c2[ -> is_derive z 1 Df ('D_1 Df z). by move=> zc1c2; apply/derivableP/h. have [|z zc1c2 {}h] := MVT c1c2 derivef. apply: (derivable_oo_continuous_bnd_within (And3 h _ _)). + apply: cvg_at_right_filter. move: cDf; rewrite continuous_open_subspace//; last exact: interval_open. by apply; rewrite inE/= in_itv/= (andP Ic1).1 (lt_trans _ (andP Ic2).2). + apply: cvg_at_left_filter. move: cDf; rewrite continuous_open_subspace//; last exact: interval_open. by apply; rewrite inE/= in_itv/= (andP Ic2).2 (lt_trans (andP Ic1).1). by exists z => //; rewrite h -mulrA divff ?mulr1// subr_eq0 gt_eqF. have LfE : L x - f x = ((x - a) * (b - x)) / (b - a) * ((f b - f x) / (b - x)) - ((b - x) * factor a b x) * ((f x - f a) / (x - a)). rewrite !mulrA -(mulrC (b - x)) -(mulrC (b - x)^-1) !mulrA. rewrite mulVf ?mul1r ?subr_eq0 ?gt_eqF//. rewrite -(mulrC (x - a)) -(mulrC (x - a)^-1) !mulrA. rewrite mulVf ?mul1r ?subr_eq0 ?gt_eqF//. rewrite -/(factor a b x). rewrite -(opprB a b) -(opprB x b) invrN mulrNN -/(factor b a x). rewrite -(@onem_factor _ a) ?lt_eqF//. rewrite /onem mulrBl mul1r opprB addrA -mulrDr addrA subrK. by rewrite /L -addrA addrC opprB -addrA (addrC (f a)). have {Hc1 Hc2} -> : L x - f x = (b - x) * (x - a) * (c2 - c1) / (b - a) * (('D_1 f c2 - 'D_1 f c1) / (c2 - c1)). rewrite LfE Hc2 Hc1. rewrite -(mulrC (b - x)) mulrA -mulrBr. rewrite (mulrC ('D_1 f c2 - _)) ![in RHS]mulrA; congr *%R. rewrite -2!mulrA; congr *%R. by rewrite mulrCA divff ?mulr1// subr_eq0 gt_eqF. rewrite {}h mulr_ge0//; last first. rewrite DDf_ge0//; apply/andP; split. by rewrite (lt_trans (andP Ic1).1)//; case/andP : Id. by rewrite (lt_trans (andP Id).2)//; case/andP : Ic2. rewrite mulr_ge0// ?invr_ge0 ?subr_ge0 ?(ltW ab)//. rewrite mulr_ge0// ?subr_ge0 ?(ltW c1c2)//. by rewrite mulr_ge0// subr_ge0 ltW. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) mathcomp(functions cardinality) ereal reals signed topology prodnormedzmodule normedtype derive realfun itv HB(structures)