proposition: Lemma second_derivative_convexf_pt : forall t : {prob R}, convex_function_at f a b t.
proof: Proof. have note1 : forall x, R1 = ((x - a) / (b - a) + (b - x) / (b - a))%coqR. move=> x; rewrite -mulRDl addRC addRA subRK addR_opp mulRV // subR_eq0'. exact/gtR_eqF. have step1 : forall x, f x = ((x - a) / (b - a) * f x + (b - x) / (b - a) * f x)%coqR. by move=> x; rewrite -mulRDl -note1 mul1R. apply convexf_ptP => // x axb. rewrite /L. case: axb. rewrite leR_eqVlt => -[-> _|]. by rewrite /L subRR div0R mul0R addR0 subRR. move=> ax. rewrite leR_eqVlt => -[->|xb]. rewrite /L /Rdiv mulRV ?mul1R; last by rewrite subR_eq0'; exact/gtR_eqF. by rewrite addRC subRK subRR. have {step1}step2 : (L x - f x = (x - a) * (b - x) / (b - a) * ((f b - f x) / (b - x)) - (b - x) * (x - a) / (b - a) * ((f x - f a) / (x - a)))%coqR. rewrite {1}step1 {step1}. rewrite -addR_opp oppRD addRA addRC addRA. rewrite LE //. rewrite {1}/Rdiv -(mulRN _ (f x)) -/(Rdiv _ _). rewrite addRA -mulRDr (addRC _ (f a)) (addR_opp (f a)). rewrite -mulRN -addRA -mulRDr (addR_opp (f b)). rewrite addRC. rewrite -(oppRK (f a - f x)) mulRN addR_opp oppRB. congr (_ + _)%coqR. - rewrite {1}/Rdiv -!mulRA; congr (_ * _)%coqR; rewrite mulRCA; congr (_ * _)%coqR. rewrite mulRCA mulRV ?mulR1 // subR_eq0'; exact/gtR_eqF. - rewrite -!mulNR -!mulRA; congr (_ * _)%coqR; rewrite mulRCA; congr (_ * _)%coqR. rewrite mulRCA mulRV ?mulR1 // subR_eq0'; exact/gtR_eqF. have [c2 [Ic2 Hc2]] : exists c2, (x < c2 < b /\ (f b - f x) / (b - x) = Df c2)%coqR. have H : pderivable f (fun x0 => x <= x0 <= b)%coqR. move=> z [z1 z2]; apply HDf; split => //. apply (@leR_trans x) => //; exact: ltRW. case: (@MVT_cor1_pderivable x b f H xb) => c2 [Ic2 [H1 H2]]. exists c2; split => //. rewrite H1 /Rdiv -mulRA mulRV ?mulR1; last first. by rewrite subR_eq0'; exact/gtR_eqF. rewrite DfE; last by move=> ?; exact: proof_derive_irrelevance. split. apply (@leR_trans x); [exact/ltRW | by case: Ic2 H1]. by case: H2 => _ /ltRW. have [c1 [Ic1 Hc1]] : exists c1, (a < c1 < x /\ (f x - f a) / (x - a) = Df c1)%coqR. have H : pderivable f (fun x0 => a <= x0 <= x)%coqR. move=> z [z1 z2]; apply HDf; split => //. apply (@leR_trans x) => //; exact: ltRW. case: (@MVT_cor1_pderivable a x f H ax) => c1 [Ic1 [H1 H2]]. exists c1; split => //. rewrite H1 /Rdiv -mulRA mulRV ?mulR1; last first. by rewrite subR_eq0'; exact/gtR_eqF. rewrite DfE; last by move=> ?; exact: proof_derive_irrelevance. split. - by case: H2 => /ltRW. - apply (@leR_trans x). by case: H2 => _ /ltRW. apply (@leR_trans c2); apply/ltRW; by case: Ic2. have c1c2 : (c1 < c2)%coqR by apply (@ltR_trans x); [case: Ic1 | case: Ic2]. have {step2 Hc1 Hc2}step3 : (L x - f x = (b - x) * (x - a) * (c2 - c1) / (b - a) * ((Df c2 - Df c1) / (c2 - c1)))%coqR. rewrite {}step2 Hc2 Hc1 (mulRC (x - a)%coqR) -mulRBr {1}/Rdiv -!mulRA. congr (_ * (_ * _))%coqR; rewrite mulRCA; congr (_ * _)%coqR. rewrite mulRCA mulRV ?mulR1 // subR_eq0'; by move/gtR_eqF : c1c2. have [d [Id H]] : exists d, (c1 < d < c2 /\ (Df c2 - Df c1) / (c2 - c1) = DDf d)%coqR. have H : pderivable Df (fun x0 => c1 <= x0 <= c2)%coqR. move=> z [z1 z2]; apply HDDf; split => //. - apply (@leR_trans c1) => //; by case: Ic1 => /ltRW. - apply (@leR_trans c2) => //; by case: Ic2 => _ /ltRW. case: (@MVT_cor1_pderivable c1 c2 Df H c1c2) => d [Id [H1 H2]]. exists d; split => //. rewrite H1 /Rdiv -mulRA mulRV ?mulR1; last first. by rewrite subR_eq0'; exact/gtR_eqF. rewrite DDfE; last by move=> ?; exact: proof_derive_irrelevance. split. - apply (@leR_trans c1); last by case: Id H1. by apply/ltRW; case: Ic1. - apply (@leR_trans c2); last by case: Ic2 => _ /ltRW. by case: H2 => _ /ltRW. rewrite {}step3 {}H. apply/mulR_ge0; last first. apply: DDf_ge0; split. apply (@leR_trans c1). apply/ltRW; by case: Ic1. by case: Id => /ltRW. apply (@leR_trans c2). by case: Id => _ /ltRW. apply/ltRW; by case: Ic2. apply/mulR_ge0; last by apply/invR_ge0; rewrite subR_gt0. apply/mulR_ge0; last first. by rewrite subR_ge0; case: Id => Id1 Id2; apply (@leR_trans d); exact/ltRW. by apply/mulR_ge0; rewrite subR_ge0; exact/ltRW. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist