proposition: Lemma concavity_of_entropy_x_le_y x y (t : {prob R}) : x \in open_unit_interval -> y \in open_unit_interval -> x < y -> concave_function_at H2 x y t.
proof: Proof. rewrite !classical_sets.in_setE => -[H0x Hx1] [H0y Hy1] Hxy. apply RNconcave_function_at. set Df := fun z : R => log z - log (1 - z). have @f_derive : pderivable (fun x0 => - H2 x0) (fun z => x <= z <= y). move => z Hz. exact/derivable_pt_opp/pderivable_H2/(@expand_interval_closed_to_open 0 x y 1). have @derive_pt_f : forall z (Hz : x <= z <= y), Df z = derive_pt (fun x1 => - H2 x1) _ (f_derive _ Hz). move => z Hz. rewrite derive_pt_opp. set H := expand_interval_closed_to_open _ _ _ _. rewrite /pderivable_H2. case H => [H0z Hz1]. rewrite derive_pt_plus. rewrite 2!derive_pt_opp. rewrite 2!derive_pt_mult. rewrite derive_pt_id derive_pt_comp 2!derive_pt_Log /=. rewrite mul1R mulN1R mulRN1. rewrite [X in z * X]mulRC [X in (1 - z) * - X]mulRC mulRN 2!mulRA. rewrite !mulRV ?gtR_eqF // ?subR_gt0 // mul1R -2!oppRD oppRK. by rewrite [X in X + - _]addRC oppRD addRA addRC !addRA Rplus_opp_l add0R addR_opp. have @pderivable_Df : pderivable Df (fun z => x <= z <= y). move => z [Hxz Hzy]. apply derivable_pt_minus. apply derivable_pt_Log. apply (ltR_leR_trans H0x Hxz). apply derivable_pt_comp. apply derivable_pt_Rminus. apply derivable_pt_Log. apply subR_gt0. exact: leR_ltR_trans Hzy Hy1. set DDf := fun z => / (z * (1 - z) * ln 2). have derive_pt_Df : forall z (Hz : x <= z <= y), DDf z = derive_pt Df z (pderivable_Df z Hz). rewrite -/Df => z [Hxz Hzy]. rewrite derive_pt_minus derive_pt_comp 2!derive_pt_Log /=. rewrite mulRN1 -[X in _ = X]addR_opp oppRK. rewrite -mulRDr [X in _ = X]mulRC. have Hzn0 : z != 0 by apply/gtR_eqF/(ltR_leR_trans H0x Hxz). have H1zn0 : 1 - z != 0. by rewrite subR_eq0' ?gtR_eqF //; apply/leR_ltR_trans; [exact Hzy| exact Hy1]. have Hzn0' : z <> 0 by move : Hzn0 => /eqP. have H1zn0' : 1 - z <> 0 by move : H1zn0 => /eqP. have /eqP Hz1zn0 : z * (1 - z) <> 0 by rewrite mulR_neq0. have -> : / z = (1 - z) / (z * (1 - z)). change (/ z = (1 - z) * / (z * (1 - z))). by rewrite invRM // [X in _ = _ * X]mulRC mulRA mulRV // mul1R. have -> : / (1 - z) = z / (z * (1 - z)). change (/ (1 - z) = z * / (z * (1 - z))). by rewrite invRM // mulRA mulRV // mul1R. by rewrite -Rdiv_plus_distr -addRA Rplus_opp_l addR0 div1R -invRM // ln2_neq0. have DDf_nonneg : forall z, x <= z <= y -> 0 <= DDf z. move => z [Hxz Hzy]. have Hz : 0 < z by apply /ltR_leR_trans; [exact H0x| exact Hxz]. have H1z : 0 < 1 - z by apply /subR_gt0 /leR_ltR_trans; [exact Hzy| exact Hy1]. by apply/or_introl/invR_gt0/mulR_gt0; [exact/mulR_gt0 | exact/ln2_gt0]. exact: (@second_derivative_convexf_pt _ _ _ _ Df _ _ DDf). Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(mathcomp_extra Rstruct reals) Reals Ranalysis_ext Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist jfdist_cond entropy convex binary_entropy_function log_sum divergence