From bd50a166ed90e65d1adca71b16695f14daf388f7 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 4 Feb 2025 18:44:10 +0900 Subject: [PATCH] do not use Coq's MVT --- probability/ln_facts.v | 191 ++++++++++++++++------------------------- 1 file changed, 75 insertions(+), 116 deletions(-) diff --git a/probability/ln_facts.v b/probability/ln_facts.v index 7a1510ba..cba11423 100644 --- a/probability/ln_facts.v +++ b/probability/ln_facts.v @@ -54,85 +54,45 @@ rewrite gerDl//. by rewrite ler_piMr// ltW. Unshelve. all: by end_near. Qed. -(* TODO: clean *) -Lemma MVT_cor1_pderivable_open_continuity {R : realType} (f : R -> R) (a b : R) : - (forall x, a < x < b -> derivable f x 1) -> continuous_at a f -> - continuous_at b f -> - a < b -> - exists c, a < c < b /\ - f b - f a = 'D_1 f c * (b - a) /\ a < c < b. +(* TODO: PR to analysis *) +Lemma ltr0_derive1_decr (R : realType) (f : R -> R) (a b : R) : + (forall x, x \in `]a, b[%R -> derivable f x 1) -> + (forall x, x \in `]a, b[%R -> f^`() x < 0) -> + {within `[a, b], continuous f}%classic -> + forall x y, a <= x -> x < y -> y <= b -> f y < f x. Proof. -move=> H prca prcb ab. -have H1 : (forall x : R^o, x \in `]a, b[ -> is_derive x 1 f ('D_1 f x)). - move=> x. - rewrite in_itv/= => /andP[ax xb]. - apply/derivableP. - apply: H. - by rewrite ax xb. -have H2 : {within `[a, b], continuous f}%classic. - apply/continuous_within_itvP => //. - split. - have : {in `]a, b[, forall x, derivable f x 1}. - move=> w wab. - apply: H. - done. - move/derivable_within_continuous. - rewrite continuous_open_subspace//. - move=> K z zab. - apply: K => //. - by rewrite inE. - by apply: interval_open => //=. - (* TODO: pkoi je peux pas utiliser itv_open?*) - red in prca. - exact: cvg_at_right_filter. - red in prca. - exact: cvg_at_left_filter. -have [c ca fab] := @MVT R f ('D_1 f) _ _ ab H1 H2. -exists c; split. - by move: ca; rewrite in_itv/=. -by rewrite fab. +move=> fdrvbl dflt0 ctsf x y leax ltxy leyb; rewrite -subr_gt0. +case: ltgtP ltxy => // xlty _. +have itvW : {subset `[x, y]%R <= `[a, b]%R}. + by apply/subitvP; rewrite /<=%O /= /<=%O /= leyb leax. +have itvWlt : {subset `]x, y[%R <= `]a, b[%R}. + by apply subitvP; rewrite /<=%O /= /<=%O /= leyb leax. +have fdrv z : z \in `]x, y[%R -> is_derive z 1 f (f^`()z). + rewrite in_itv/= => /andP[xz zy]; apply: DeriveDef; last by rewrite derive1E. + by apply: fdrvbl; rewrite in_itv/= (le_lt_trans _ xz)// (lt_le_trans zy). +have [] := @MVT _ f (f^`()) x y xlty fdrv. + apply: (@continuous_subspaceW _ _ _ `[a, b]); first exact: itvW. + by rewrite continuous_subspace_in. +move=> t /itvWlt dft dftxy; rewrite -oppr_lt0 opprB dftxy. +by rewrite pmulr_llt0 ?subr_gt0// dflt0. Qed. -(* TODO: clean *) -Lemma derive_sincreasing_interv {R : realType} a b (f : R -> R) - (pr : forall x, a < x < b -> derivable f x 1) - (prc : forall x, a <= x <= b -> continuous_at x f) : - a < b -> - ((forall t:R, a < t < b -> derivable f t 1 -> 0 < 'D_1 f t) -> - forall x y:R, a <= x <= b -> a <= y <= b -> x < y -> f x < f y). +(* TODO: PR to analysis *) +Lemma gtr0_derive1_incr (R : realType) (f : R -> R) (a b : R) : + (forall x, x \in `]a, b[%R -> derivable f x 1) -> + (forall x, x \in `]a, b[%R -> 0 < f^`() x) -> + {within `[a, b], continuous f}%classic -> + forall x y, a <= x -> x < y -> y <= b -> f x < f y. Proof. -intros H H0 x y H1 H2 H3. -rewrite -subr_gt0. -have prd' : forall z, x < z < y -> derivable f z 1. - move=> z /= /andP[Hz1 Hz2] ; apply pr. - apply/andP; split. - - apply: (@le_lt_trans _ _ x) => //. - by case/andP : H1. - - apply: (@lt_le_trans _ _ y) => //. - by case/andP : H2. -have H0' : forall t, x < t < y -> 0 < 'D_1 f t. - move=> z /= /andP[Hz0 Hz1]. - apply H0. - apply/andP; split. - - apply: (@le_lt_trans _ _ x) => //. - by case/andP : H1. - - apply: (@lt_le_trans _ _ y) => //. - by case/andP : H2. - apply: pr. - case/andP : H1 => + _. - move=> /le_lt_trans => /(_ _ Hz0) ->/=. - rewrite (lt_le_trans Hz1)//. - by case/andP : H2. -have prcx : continuous_at (x : R^o) f. - by apply: prc. -have prcy : continuous_at (y : R^o) f. - by apply: prc. -have aux : a < b. - done. -case: (MVT_cor1_pderivable_open_continuity prd' prcx prcy H3); intros x0 [x1 [H7 H8]]. -rewrite H7. -apply mulr_gt0; first by apply H0'. -by rewrite subr_gt0. +move=> fdrvbl dfgt0 ctsf x y leax ltxy leyb. +rewrite -ltrN2; apply: (@ltr0_derive1_decr _ (\- f) a b). +- by move=> z zab; apply: derivableN; exact: fdrvbl. +- move=> z zab; rewrite derive1E deriveN; last exact: fdrvbl. + by rewrite ltrNl oppr0 -derive1E dfgt0. +- by move=> z; apply: continuousN; exact: ctsf. +- exact: leax. +- exact: ltxy. +- exact: leyb. Qed. Section xlnx_sect. @@ -433,31 +393,30 @@ rewrite ltr_pM2l ?expR_gt0//. by rewrite ltrBlDl addrC -ltrBlDl subrr. Qed. +Lemma continuous_at_diff_xlnx (r : R) : continuous_at r diff_xlnx. +Proof. +move=> z. +apply: cvgB => //. + apply: cvg_comp; last exact: continuous_at_xlnx. + apply: cvgB => //. + exact: cvg_cst. +by apply: continuous_at_xlnx. +Qed. + Lemma diff_xlnx_sincreasing_0_Rinv_e2 (x y : R) : 0 <= x <= expR (-2) -> 0 <= y <= expR (-2) -> x < y -> diff_xlnx x < diff_xlnx y. Proof. move=> /andP[x0 x2] /andP[y0 y2] xy. -apply (@derive_sincreasing_interv R 0 (expR (-2))) => //. -- move=> x' /= /andP[Hx1 Hx2]. - apply derivable_pt_diff_xlnx. - apply/andP; split => //. - by rewrite (lt_le_trans Hx2)// -[leRHS]exp.expR0 exp.ler_expR lerNl oppr0. -- move=> x' /= /andP[Hx1 Hx2]. - rewrite /diff_xlnx. - apply: cvgB => //. - apply: cvg_comp; last exact: continuous_at_xlnx. - apply: cvgB => //. - exact: cvg_cst. - by apply: continuous_at_xlnx. -- by rewrite exp.expR_gt0. -- move=> x' /= /andP[Hx1 Hx2] K. - rewrite derive_diff_xlnx_gt0//. - rewrite Hx1/=. - rewrite (lt_le_trans Hx2)//. - by rewrite -[leRHS]exp.expR0 exp.ler_expR lerNl oppr0. -- by rewrite x0. -- by rewrite y0. +apply: (@gtr0_derive1_incr _ _ 0 (expR (- 2))) => //. +- move=> z; rewrite in_itv/= => /andP[z0 z2]. + apply: derivable_pt_diff_xlnx. + by rewrite z0/= (lt_le_trans z2)// -[leRHS]expR0 ler_expR lerNl oppr0. +- move=> z; rewrite in_itv/= => /andP[z0 z2]. + rewrite derive1E derive_diff_xlnx_gt0// z0/=. + by rewrite (lt_le_trans z2)// -[leRHS]expR0 ler_expR lerNl oppr0. +- apply: continuous_subspaceT => z. + exact: continuous_at_diff_xlnx. Qed. Lemma xlnx_ineq (x : R) : 0 <= x <= expR (-2) -> xlnx x <= xlnx (1-x). @@ -525,35 +484,35 @@ rewrite derive_id derive_cst addr0 mulr1. by rewrite opprD addrACA subrr addr0. Qed. +Lemma continuous_at_xlnx_delta (r : R) eps : continuous_at r (xlnx_delta eps). +Proof. +move=> z. +apply: cvgB. + apply: cvg_comp; last first. + exact: continuous_at_xlnx. + apply: cvgD. + exact: cvg_id. + exact: cvg_cst. +exact: continuous_at_xlnx. +Qed. + Lemma increasing_xlnx_delta eps (Heps : 0< eps < 1) : forall x y : R, 0 <= x <= 1 - eps -> 0 <= y <= 1 - eps -> x < y -> xlnx_delta eps x < xlnx_delta eps y. Proof. move=> x y /andP[x0 x1] /andP[y0 y1] xy. -apply (@derive_sincreasing_interv R 0 (1 - eps)) => //=. -- move=> z /andP[z0 z1]. +apply: (@gtr0_derive1_incr _ _ 0 (1 - eps)) => //. +- move=> z; rewrite in_itv/= => /andP[z0 z1]. apply: derivable_xlnx_delta => //. by rewrite z0. -- move=> z /andP[z0 z1]. - apply: cvgB. - apply: cvg_comp; last first. - exact: continuous_at_xlnx. - apply: cvgD. - exact: cvg_id. - exact: cvg_cst. - exact: continuous_at_xlnx. -- rewrite subr_gt0. - by case/andP : Heps. -- move=> t /andP[t0 t1] H. - rewrite derive_pt_xlnx_delta//. +- move=> z; rewrite in_itv/= => /andP[z0 z1]. + rewrite derive1E derive_pt_xlnx_delta//. rewrite subr_gt0 ltr_ln ?posrE//. - rewrite ltrDl. - by case/andP: Heps. - rewrite addr_gt0//. - by case/andP: Heps. - by rewrite t0/=. -- by rewrite x0. -- by rewrite y0. + by rewrite ltrDl; case/andP : Heps. + by rewrite addr_gt0//; case/andP : Heps. + by rewrite z0. +- apply: continuous_subspaceT => z. + exact: continuous_at_xlnx_delta. Qed. Lemma xlnx_delta_bound eps : 0 < eps <= expR (-2) ->