From a46d7fd51b5377d2ef65eb3257670ee73b066d15 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 1 Jun 2023 10:58:07 +0900 Subject: [PATCH] powere_pos lemmas - refactoring by Cyril Co-authored-by: Alessandro Bruni Co-authored-by: Cyril Cohen --- CHANGELOG_UNRELEASED.md | 17 ++++ theories/exp.v | 219 ++++++++++++++++++++-------------------- theories/itv.v | 2 +- 3 files changed, 127 insertions(+), 111 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c646e45a7d..769ed4782b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -41,6 +41,13 @@ - in `lebesgue_measure.v`: + lemmas `measurable_fun_ltr`, `measurable_minr` +- in `exp.v`: + + notation `` e `^?(r +? s) `` + + lemmas `expR_eq0`, `power_posN` + + definition `powere_posD_def` + + lemmas `powere_posD_defE`, `powere_posB_defE`, `add_neq0_powere_posD_def`, + `add_neq0_powere_posB_def`, `nneg_neq0_powere_posD_def`, `nneg_neq0_powere_posB_def` + ### Changed - moved from `lebesgue_measure.v` to `real_interval.v`: @@ -49,14 +56,24 @@ - moved from `functions.v` to `classical_sets.v`: `subsetP`. +- in `exp.v`: + + lemmas `power_pos_eq0`, `powere_pos_eq0` + + lemmas `power_posD`, `power_posB` + ### Renamed - in `boolp.v`: + `mextentionality` -> `mextensionality` + `extentionality` -> `extensionality` + - in `exp.v`: + `expK` -> `expRK` +- in `exp.v`: + + `power_pos_eq0` -> `power_pos_eq0_eq0` + + `power_pos_inv` -> `power_pos_invn` + + `powere_pos_eq0` -> `powere_pos_eq0_eq0` + ### Generalized - in `exp.v`: diff --git a/theories/exp.v b/theories/exp.v index 4a2948c064..a693e01ff2 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -24,6 +24,8 @@ Require Import itv convex. (* e `^ r == power function, in ereal_scope (assumes e >= 0) *) (* riemannR a == sequence n |-> 1 / (n.+1) `^ a where a has a type *) (* of type realType *) +(* e `^?(r +? s) == validity condition for the distributivity of *) +(* the power of the addition, in ereal_scope *) (* *) (******************************************************************************) @@ -36,6 +38,9 @@ Import numFieldNormedType.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. +Reserved Notation "x `^?( r +? s )" + (format "x `^?( r +? s )", r at next level, at level 11) . + (* PR to mathcomp in progress *) Lemma normr_nneg (R : numDomainType) (x : R) : `|x| \is Num.nneg. Proof. by rewrite qualifE. Qed. @@ -385,6 +390,9 @@ Qed. Lemma expR_ge0 x : 0 <= expR x. Proof. by rewrite ltW// expR_gt0. Qed. +Lemma expR_eq0 x : (expR x == 0) = false. +Proof. by rewrite gt_eqF ?expR_gt0. Qed. + Lemma expRN x : expR (- x) = (expR x)^-1. Proof. apply: (mulfI (lt0r_neq0 (expR_gt0 x))). @@ -494,7 +502,7 @@ Implicit Types x : R. Notation exp := (@expR R). -Definition ln x : R := xget 0 [set y | exp y == x ]. +Definition ln x : R := [get y | exp y == x ]. Fact ln0 x : x <= 0 -> ln x = 0. Proof. @@ -632,12 +640,16 @@ Proof. by rewrite /power_pos; case: ifPn; rewrite ?eqxx// mul0r expR0. Qed. Lemma power_pos1 : power_pos 1 = fun=> 1. Proof. by apply/funext => x; rewrite /power_pos oner_eq0 ln1 mulr0 expR0. Qed. -Lemma power_pos_eq0 x p : x `^ p = 0 -> x = 0. +Lemma power_pos_eq0 x p : (x `^ p == 0) = (x == 0) && (p != 0). Proof. -rewrite /power_pos. have [->|_] := eqVneq x 0 => //. -by move: (expR_gt0 (p * ln x)) => /gt_eqF /eqP. +rewrite /power_pos; have [_|x_neq0] := eqVneq x 0 => //. + by case: (p == 0); rewrite (oner_eq0, eqxx). +by rewrite expR_eq0. Qed. +Lemma power_pos_eq0_eq0 x p : x `^ p = 0 -> x = 0. +Proof. by move=> /eqP; rewrite power_pos_eq0 => /andP[/eqP]. Qed. + Lemma ler_power_pos a : 1 <= a -> {homo power_pos a : x y / x <= y}. Proof. move=> a1 x y xy. @@ -658,86 +670,59 @@ Qed. Lemma power_posM x y r : 0 <= x -> 0 <= y -> (x * y) `^ r = x `^ r * y `^ r. Proof. -have [->|r0] := eqVneq r 0; first by rewrite !power_posr0 mulr1. -rewrite 2!le_eqVlt. -move=> /predU1P[<-|x0] /predU1P[<-|y0]; rewrite ?(mulr0, mul0r, power_pos0)//. -- rewrite /power_pos mulf_eq0; case: eqP => [->|x0']/=. - rewrite (@gt_eqF _ _ y)//. - by case: eqP => /=; rewrite ?mul0r ?mul1r// => ->; rewrite mul0r expR0. - by rewrite gt_eqF// lnM ?posrE // -expRD mulrDr. +rewrite /power_pos mulf_eq0. +case: (ltgtP x 0) => // x0 _; case: (ltgtP y 0) => //= y0 _; do ? + by case: eqVneq => [r0|]; rewrite ?r0 ?mul0r ?expR0 ?mulr0 ?mul1r. +by rewrite lnM// mulrDr expRD. Qed. Lemma power_posrM (x y z : R) : x `^ (y * z) = (x `^ y) `^ z. Proof. -rewrite /power_pos; have [->/=|y0] := eqVneq y 0. - by rewrite !mul0r expR0 eqxx/= if_same oner_eq0 ln1 mulr0 expR0. -have [->/=|z0] := eqVneq z 0. - by rewrite !mulr0 !mul0r expR0 eqxx 2!if_same. -case: ifPn => [_/=|x0]; first by rewrite eqxx mulf_eq0 (negbTE y0) (negbTE z0). -by rewrite gt_eqF ?expR_gt0// expRK mulrCA mulrA. +rewrite /power_pos mulf_eq0; have [_|xN0] := eqVneq x 0. + by case: (y == 0); rewrite ?eqxx//= oner_eq0 ln1 mulr0 expR0. +by rewrite expR_eq0 expRK mulrCA mulrA. Qed. Lemma power_posAC x y z : (x `^ y) `^ z = (x `^ z) `^ y. +Proof. by rewrite -!power_posrM mulrC. Qed. + +Lemma power_posD x r s : + (r + s == 0) ==> (x != 0) -> x `^ (r + s) = x `^ r * x `^ s. Proof. -rewrite /power_pos; have [->/=|z0] := eqVneq z 0; rewrite ?mul0r. -- have [->/=|y0] := eqVneq y 0; rewrite ?mul0r//=. - have [x0|x0] := eqVneq x 0; rewrite ?eqxx ?oner_eq0 ?ln1 ?mulr0 ?expR0//. - by rewrite oner_eq0 if_same ln1 mulr0 expR0. -- have [->/=|y0] := eqVneq y 0; rewrite ?mul0r/=. - have [x0|x0] := eqVneq x 0; rewrite ?eqxx ?oner_eq0 ?ln1 ?mulr0 ?expR0//. - by rewrite oner_eq0 if_same ln1 mulr0 expR0. - have [x0|x0] := eqVneq x 0; first by rewrite eqxx. - by rewrite gt_eqF ?expR_gt0// gt_eqF ?expR_gt0 ?expRK 1?mulrCA. +rewrite /power_pos; case: (eqVneq x 0) => //= [_|x_neq0 _]; + last by rewrite mulrDl expRD. +have [->|] := eqVneq r 0; first by rewrite mul1r add0r. +by rewrite implybF mul0r => _ /negPf ->. Qed. -Lemma power_posD a : 0 < a -> {morph power_pos a : x y / x + y >-> x * y}. -Proof. by move=> a0 x y; rewrite /power_pos gt_eqF// mulrDl expRD. Qed. - -Lemma power_posB x r s : r != s -> x `^ (r - s) = x `^ r * x `^ (- s). +Lemma power_posN x r : x `^ (- r) = (x `^ r)^-1. Proof. -move=> rs. -have [->|r0] := eqVneq r 0%R; first by rewrite power_posr0 sub0r mul1r. -have [->|s0] := eqVneq s 0%R; first by rewrite subr0 oppr0 power_posr0 mulr1. -have [x0|x0|<-] := ltgtP 0 x. -- by rewrite /power_pos gt_eqF// mulrDl expRD. -- by rewrite /power_pos lt_eqF// -expRD -mulrDl. -- by rewrite !power_pos0 ?mulr0// ?subr_eq0// oppr_eq0. +have [r0|r0] := eqVneq r 0%R; first by rewrite r0 oppr0 power_posr0 invr1. +have [->|xN0] := eqVneq x 0; first by rewrite !power_pos0 ?oppr_eq0// invr0. +rewrite -div1r; apply: (canRL (mulfK _)). + by rewrite power_pos_eq0 (negPf xN0). +by rewrite -power_posD ?addNr ?power_posr0// xN0 eqxx. Qed. +Lemma power_posB x r s : + (r == s) ==> (x != 0) -> x `^ (r - s) = x `^ r / x `^ s. +Proof. by move=> ?; rewrite power_posD ?subr_eq0// power_posN. Qed. + Lemma power_pos_mulrn a n : 0 <= a -> a `^ n%:R = a ^+ n. Proof. -move=> a0; elim: n => [|n ih]. - by rewrite mulr0n expr0 power_posr0//; apply: lt0r_neq0. -move: a0; rewrite le_eqVlt => /predU1P[<-|a0]. - by rewrite !power_pos0 ?mulrn_eq0//= expr0n. -by rewrite -natr1 power_posD// ih power_posr1// ?exprS 1?mulrC// ltW. +move=> a_ge0; elim: n => [|n IHn]; first by rewrite power_posr0 expr0. +by rewrite -natr1 power_posD ?natr1 ?pnatr_eq0// power_posr1// IHn exprSr. Qed. Lemma power_pos_inv1 a : 0 <= a -> a `^ (-1) = a ^-1. -Proof. -rewrite le_eqVlt => /predU1P[<-|a0]; first by rewrite power_pos0// invr0. -apply/(@mulrI _ a); first by rewrite unitfE gt_eqF. -rewrite -[X in X * _ = _](power_posr1 (ltW a0)) -power_posD// subrr. -by rewrite power_posr0 divff// gt_eqF. -Qed. +Proof. by move=> a_ge0; rewrite power_posN power_posr1. Qed. -Lemma power_pos_inv a n : 0 <= a -> a `^ (- n%:R) = a ^- n. -Proof. -move=> a0; elim: n => [|n ih]. - by rewrite -mulNrn mulr0n power_posr0 -exprVn expr0. -move: a0; rewrite le_eqVlt => /predU1P[<-|a0]. - by rewrite power_pos0 ?mulrn_eq0// exprnN exp0rz oppr_eq0. -rewrite -natr1 opprD power_posD// (power_pos_inv1 (ltW a0)) ih. -by rewrite -[in RHS]exprVn exprS [in RHS]mulrC exprVn. -Qed. +Lemma power_pos_invn a n : 0 <= a -> a `^ (- n%:R) = a ^- n. +Proof. by move=> a_ge0; rewrite power_posN power_pos_mulrn. Qed. Lemma power_pos_intmul a (z : int) : 0 <= a -> a `^ z%:~R = a ^ z. Proof. -move=> a0; have [z0|z0] := leP 0 z. - rewrite -[in RHS](gez0_abs z0) abszE -exprnP -power_pos_mulrn//. - by rewrite natr_absz -abszE gez0_abs. -rewrite -(opprK z) (_ : - z = `|z|%N); last by rewrite ltz0_abs. -by rewrite -exprnN -power_pos_inv// nmulrn. +by move=> a0; case: z => n; [exact: power_pos_mulrn | exact: power_pos_invn]. Qed. Lemma ln_power_pos a x : ln (a `^ x) = x * ln a. @@ -841,74 +826,88 @@ move=> r0; move: x => [x|//|]; rewrite ?leeNe_eq// lee_fin !lte_fin. exact: gt0_power_pos. Qed. -Lemma powere_pos_eq0 x r : -oo < x -> x `^ r = 0 -> x = 0. +Lemma powere_pos_eq0 x r : 0 <= x -> (x `^ r == 0) = ((x == 0) && (r != 0%R)). Proof. move: x => [x _|_/=|//]. -- by rewrite powere_pos_EFin => -[] /power_pos_eq0 ->. -- by case: ifPn => // _ /eqP; rewrite onee_eq0. + by rewrite powere_pos_EFin eqe power_pos_eq0. +by case: ifP => //; rewrite onee_eq0. Qed. +Lemma powere_pos_eq0_eq0 x r : 0 <= x -> x `^ r = 0 -> x = 0. +Proof. by move=> + /eqP => /powere_pos_eq0-> /andP[/eqP]. Qed. + Lemma powere_posM x y r : 0 <= x -> 0 <= y -> (x * y) `^ r = x `^ r * y `^ r. Proof. -move: x y => [x| |] [y| |]//=; first by move=> x0 y0; rewrite -EFinM power_posM. -- move=> x0 _; case: ifPn => /= [/eqP ->|r0]. - + by rewrite mule1 power_posr0 powere_pose0. - + move: x0; rewrite le_eqVlt => /predU1P[[]<-|/[1!(@lte_fin R)] x0]. - * by rewrite mul0e powere_pos0r// power_pos0// mul0e. - * by rewrite mulry [RHS]mulry !gtr0_sg ?power_pos_gt0// !mul1e powere_posyr. -- move=> _ y0; case: ifPn => /= [/eqP ->|r0]. - + by rewrite power_posr0 powere_pose0 mule1. - + move: y0; rewrite le_eqVlt => /predU1P[[]<-|/[1!(@lte_fin R)] u0]. - by rewrite mule0 powere_pos0r// power_pos0// mule0. - + by rewrite 2!mulyr !gtr0_sg ?power_pos_gt0// mul1e powere_posyr. -- move=> _ _; case: ifPn => /= [/eqP ->|r0]. - + by rewrite powere_pose0 mule1. - + by rewrite mulyy powere_posyr. +have [->|rN0] := eqVneq r 0%R; first by rewrite !powere_pose0 mule1. +have powyrM s : (0 <= s)%R -> (+oo * s%:E) `^ r = +oo `^ r * s%:E `^ r. + case: ltgtP => // [s_gt0 _|<- _]; last first. + by rewrite mule0 powere_posyr// !powere_pos0r// mule0. + by rewrite gt0_mulye// powere_posyr// gt0_mulye// powere_pos_gt0. +case: x y => [x| |] [y| |]// x0 y0; first by rewrite /= -EFinM power_posM. +- by rewrite muleC powyrM// muleC. +- by rewrite powyrM. +- by rewrite mulyy !powere_posyr// mulyy. Qed. Lemma powere_posrM x r s : x `^ (r * s) = (x `^ r) `^ s. Proof. -case: x => [x| |]/=; first by rewrite power_posrM. -- have [->|r0] := eqVneq r 0%R; first by rewrite mul0r eqxx powere_pos1r. - have [->|s0] := eqVneq s 0%R; first by rewrite mulr0 eqxx powere_pose0. - by rewrite mulf_eq0 (negbTE s0) orbF (negbTE r0) ?powere_posyr. -- have [->|r0] := eqVneq r 0%R; first by rewrite mul0r eqxx powere_pos1r. - have [->|s0] := eqVneq s 0%R; first by rewrite mulr0 eqxx powere_pose0. - by rewrite mulf_eq0 (negbTE s0) orbF (negbTE r0) powere_pos0r. +have [->|s0] := eqVneq s 0%R; first by rewrite mulr0 !powere_pose0. +have [->|r0] := eqVneq r 0%R; first by rewrite mul0r powere_pose0 powere_pos1r. +case: x => [x| |]//; first by rewrite /= power_posrM. + by rewrite !powere_posyr// mulf_neq0. +by rewrite !powere_posNyr ?powere_pos0r ?(negPf s0)// mulf_neq0. Qed. Lemma powere_posAC x r s : (x `^ r) `^ s = (x `^ s) `^ r. -Proof. -case: x => [x| |]/=; first by rewrite power_posAC. -- case: ifPn => [/eqP ->|r0] /=; first by rewrite powere_pose0 power_pos1. - by case: ifPn => //; rewrite ?powere_pos1r// powere_posyr. -case: ifPn => [/eqP ->|r0] /=; first by rewrite power_pos1 powere_pose0. -case: ifPn => [/eqP ->|s0]; first by rewrite power_posr0 powere_pos1r. -by rewrite power_pos0// powere_pos0r. -Qed. +Proof. by rewrite -!powere_posrM mulrC. Qed. + +Definition powere_posD_def x r s := ((r + s == 0)%R ==> + ((x != 0) && ((x \isn't a fin_num) ==> (r == 0%R) && (s == 0%R)))). +Notation "x `^?( r +? s )" := (powere_posD_def x r s) : ereal_scope. + +Lemma powere_posD_defE x r s : + x `^?(r +? s) = ((r + s == 0)%R ==> + ((x != 0) && ((x \isn't a fin_num) ==> (r == 0%R) && (s == 0%R)))). +Proof. by []. Qed. -Lemma powere_posD x r s : 0 < x -> (0 <= r)%R -> (0 <= s)%R -> - x `^ (r + s) = x `^ r * x `^ s. +Lemma powere_posB_defE x r s : + x `^?(r +? - s) = ((r == s)%R ==> + ((x != 0) && ((x \isn't a fin_num) ==> (r == 0%R) && (s == 0%R)))). +Proof. by rewrite powere_posD_defE subr_eq0 oppr_eq0. Qed. + +Lemma add_neq0_powere_posD_def x r s : (r + s != 0)%R -> x `^?(r +? s). +Proof. by rewrite powere_posD_defE => /negPf->. Qed. + +Lemma add_neq0_powere_posB_def x r s : (r != s)%R -> x `^?(r +? - s). +Proof. by rewrite powere_posB_defE => /negPf->. Qed. + +Lemma nneg_neq0_powere_posD_def x r s : x != 0 -> (r >= 0)%R -> (s >= 0)%R -> + x `^?(r +? s). Proof. -move=> x0 r_ge0 s_ge0; move: x0; case: x => [x|_/=|//]. - by rewrite lte_fin/= => x0; rewrite -EFinM power_posD. -have [->|r0] := eqVneq r 0%R; first by rewrite mul1e add0r. -have [->|s0] := eqVneq s 0%R; first by rewrite addr0 (negbTE r0) mule1. -by rewrite paddr_eq0// (negbTE r0) (negbTE s0) mulyy. +move=> xN0 rge0 sge0; rewrite /powere_posD_def xN0/=. +by case: ltgtP rge0 => // [r_gt0|<-]; case: ltgtP sge0 => // [s_gt0|<-]//=; + rewrite ?addr0 ?add0r ?implybT// gt_eqF//= ?addr_gt0. Qed. -Lemma powere_posB x r s : r != s -> x `^ (r - s) = x `^ r * x `^ (- s). +Lemma nneg_neq0_powere_posB_def x r s : x != 0 -> (r >= 0)%R -> (s <= 0)%R -> + x `^?(r +? - s). +Proof. by move=> *; rewrite nneg_neq0_powere_posD_def// oppr_ge0. Qed. + +Lemma powere_posD x r s : x `^?(r +? s) -> x `^ (r + s) = x `^ r * x `^ s. Proof. -move=> rs. -have [->|r0] := eqVneq r 0%R; first by rewrite powere_pose0 sub0r mul1e. -have [->|s0] := eqVneq s 0%R; first by rewrite subr0 oppr0 powere_pose0 mule1. -rewrite /powere_pos. -case: x => [x| |]/=. -- by rewrite -EFinM power_posB. -- by rewrite subr_eq0 (negbTE rs) (negbTE r0) oppr_eq0 (negbTE s0) mulyy. -- by rewrite subr_eq0 (negbTE rs) (negbTE r0) mul0e. +rewrite /powere_posD_def. +have [->|r0]/= := eqVneq r 0%R; first by rewrite add0r powere_pose0 mul1e. +have [->|s0]/= := eqVneq s 0%R; first by rewrite addr0 powere_pose0 mule1. +case: x => // [t|/=|/=]; rewrite ?(negPf r0, negPf s0, implybF); last 2 first. +- by move=> /negPf->; rewrite mulyy. +- by move=> /negPf->; rewrite mule0. +rewrite !powere_pos_EFin eqe => /implyP/(_ _)/andP cnd. +by rewrite power_posD//; apply/implyP => /cnd[]. Qed. +Lemma powere_posB x r s : x `^?(r +? - s) -> x `^ (r - s) = x `^ r * x `^ (- s). +Proof. by move=> rs; rewrite powere_posD. Qed. + Lemma powere12_sqrt x : 0 <= x -> x `^ 2^-1 = sqrte x. Proof. move: x => [x|_|//]; last by rewrite powere_posyr. diff --git a/theories/itv.v b/theories/itv.v index 2603bc6118..34ba6dc8d5 100644 --- a/theories/itv.v +++ b/theories/itv.v @@ -2,7 +2,7 @@ From Coq Require Import ssreflect ssrfun ssrbool. From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint. From mathcomp Require Import interval. -From mathcomp.classical Require Import boolp mathcomp_extra. +From mathcomp.classical Require Import mathcomp_extra boolp. Require Import signed. (******************************************************************************)