From 1cc8c54a5132456bab0bcaf7ec6fb1d7e31a142a Mon Sep 17 00:00:00 2001 From: jmmarulang Date: Mon, 10 Nov 2025 11:02:52 +0000 Subject: [PATCH 1/5] poweR for extended reals --- theories/exp.v | 78 ++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 73 insertions(+), 5 deletions(-) diff --git a/theories/exp.v b/theories/exp.v index b5d37d171f..5430073103 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -1393,11 +1393,79 @@ Qed. Lemma poweRrM x r s : x `^ (r * s) = (x `^ r) `^ s. Proof. -have [->|s0] := eqVneq s 0%R; first by rewrite mulr0 !poweRe0. -have [->|r0] := eqVneq r 0%R; first by rewrite mul0r poweRe0 poweR1r. -case: x => [x| |]//; first by rewrite /= powRrM. - by rewrite !poweRyr// mulf_neq0. -by rewrite !poweRNyr ?poweR0r ?(negPf s0)// mulf_neq0. +rewrite poweRE; repeat case: ifPn=>//; move=>/orP[]/eqP ->; rewrite ?ltxx//. +by rewrite lte_fin ltr10. +Qed. + +Lemma lt0_gt0_poweR x y : x < 0%R -> 0%R < y -> x `^ y = 0. +move=> x0; rewrite poweRE x0; repeat case : ifPn=>//; case: (ltgtP y 0)=> //. +rewrite (_ : x == 1 = false)//=; apply/eqP. +by move: x0=>/[swap] ->; rewrite lte_fin ltr10. +Qed. + +Definition poweRrM_def x y z := + (z < 0) ==> (0 < x) ==> + (((x < +oo) || (0 <= y)) && + ((x <= 1) || (x == +oo) || (-oo < y)) && + ((1 <= x) || (y < +oo))). + +Lemma poweRrM (x y z : \bar R) : (0 <= x) -> poweRrM_def x y z -> + x `^ (y * z) = (x `^ y) `^ z. +Proof. +rewrite /poweRrM_def. +case: (ltgtP z 0); case: (ltgtP y 0); case: (ltgtP x 0)=> //=; last first. +1-6: by move=> + + -> //=; rewrite mule0 !poweRe0. +1-2,7-8: by move=> + -> //=; rewrite mul0e !poweRe0 poweR1. +1,3,5,7: move=> -> y0 z0; rewrite !poweR0e ?mule_neq0//. +1-16: by rewrite ?(gt_eqF y0) ?(gt_eqF z0) ?(lt_eqF y0) ?(lt_eqF z0)//. +all: case: (ltgtP x 1)=> [||->]; last by rewrite !poweR1. +all: case: x=> [r||]// + + y0 z0. +3: by rewrite (gt0_poweRye y0) (gt0_poweRye z0) gt0_poweRye ?(mule_gt0 y0 z0). +5: {rewrite (lt0_poweRye y0) poweR0e; last by rewrite (gt_eqF z0). + by rewrite lt0_poweRye ?(mule_lt0_gt0 y0 z0). } +7: {rewrite (gt0_poweRye y0) (lt0_poweRye z0) lt0_poweRye//. + by rewrite (mule_gt0_lt0 y0 z0). } +all: move: y z y0 z0=> [s||] [t||]//= s0 t0 r1 r0; rewrite ?ltxx ?andbF//. +all: try by rewrite -EFinM !poweR_EFin ?ltW ?powRrM ?powR_gt0. +- rewrite (gt0_muley s0) poweR_EFin ?poweRey_lt1 ?ltW ?lte_fin ?powR_gt0//. + rewrite (_ : 1 = 1 `^ s)%R; last by rewrite powR1. + by rewrite gt0_ltr_powR ?nnegrE ?ltW. +- by rewrite (gt0_mulye t0) poweRey_lt1 ?ltW ?poweR0e ?gt_eqF. +- by rewrite gt0_mulye ?poweRey_lt1 ?lexx ?ltW ?lte01. +- rewrite (gt0_muley s0) poweR_EFin ?ltW ?poweRey_gt1 ?lte_fin//. + rewrite (_ : 1 = 1 `^ s)%R; last by rewrite powR1. + by rewrite gt0_ltr_powR ?nnegrE ?ltW. +- by rewrite (gt0_mulye t0) ?poweRey_gt1 ?gt0_poweRye. +- by rewrite gt0_muley ?poweRey_gt1 ?ltey. +- rewrite (lt0_muley s0) poweR_EFin ?poweRey_gt1 ?ltW ?poweReNy_lt1 ?r0//. + rewrite (_ : 1 = 1 `^ s)%R; last by rewrite powR1. + by rewrite !lte_fin gt0_gtr_powR ?posrE ?ltW. +- by rewrite (gt0_mulNye t0) ?poweReNy_lt1 ?gt0_poweRye ?r0. +- by rewrite lt0_muley ?poweReNy_lt1 ?r0. +- rewrite (lt0_muley s0) ?poweReNy_gt1 ?poweRey_lt1 ?poweR_ge0//. + rewrite poweR_EFin ?ltW// (_ : 1 = 1 `^ s)%R; last by rewrite powR1. + by rewrite !lte_fin gt0_gtr_powR ?posrE ?ltW. +- by rewrite (gt0_mulNye t0) ?poweReNy_gt1 ?poweR0e ?gt_eqF. +- by rewrite lt0_muley ?poweReNy_gt1 ?poweR0e. +- rewrite (gt0_muleNy s0) poweR_EFin ?ltW ?poweReNy_lt1 ?r0 ?r1 //. + rewrite !lte_fin powR_gt0// (_ : 1 = 1 `^ s)%R; last by rewrite powR1. + by rewrite gt0_ltr_powR ?nnegrE ?ltW. +- rewrite (gt0_muleNy s0) poweR_EFin ?ltW ?poweReNy_gt1 //. + rewrite lte_fin (_ : 1 = 1 `^ s)%R; last by rewrite powR1. + by rewrite ?gt0_ltr_powR ?nnegrE ?ltW. +- by rewrite (lt0_mulye t0) ?poweReNy_gt1 ?poweRey_gt1 ?lt0_poweRye. +- by rewrite gt0_muleNy ?poweReNy_gt1 ?poweRey_gt1 ?ltey_eq. +- rewrite (lt0_muleNy s0) poweR_EFin ?ltW// poweReNy_gt1; last first. + rewrite lte_fin (_ : 1 = 1 `^ s)%R; last by rewrite powR1. + by rewrite ?gt0_gtr_powR ?posrE ?ltW. + by rewrite poweRey_lt1 ?ltW ?r0 ?r1. +- rewrite (lt0_mulNye t0) ?poweReNy_lt1 ?poweRey_lt1 ?ltW ?r0 ?r1 //. + by rewrite lt0_poweRye. +- rewrite lt0_mulNye ?poweRey_lt1 ?ltW ?r0 ?r1//. + by rewrite [X in _ = X `^ _]poweReNy_lt1 ?r0 ?r1. +- rewrite (lt0_muleNy s0) poweR_EFin ?ltW// ?poweRey_gt1 ?r0 ?r1 //. + rewrite ?poweReNy_lt1// !lte_fin (_ : 1 = 1 `^ s)%R; last by rewrite powR1. + by rewrite ?gt0_gtr_powR ?posrE ?ltW ?powR_gt0. Qed. Lemma poweRAC x r s : (x `^ r) `^ s = (x `^ s) `^ r. From d2064b7d137bfd8f41c9a344c6b307652607a3d3 Mon Sep 17 00:00:00 2001 From: jmmarulang Date: Mon, 10 Nov 2025 11:15:55 +0000 Subject: [PATCH 2/5] poweRrM again --- theories/exp.v | 380 ++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 299 insertions(+), 81 deletions(-) diff --git a/theories/exp.v b/theories/exp.v index 5430073103..5dfbf31ab4 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -1,9 +1,10 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix. -From mathcomp Require Import interval rat interval_inference. +From mathcomp Require Import interval rat. From mathcomp Require Import boolp classical_sets functions mathcomp_extra. -From mathcomp Require Import unstable reals topology ereal tvs normedtype. -From mathcomp Require Import landau sequences derive realfun convex. +From mathcomp Require Import unstable reals ereal interval_inference. +From mathcomp Require Import topology tvs normedtype landau sequences derive. +From mathcomp Require Import realfun interval_inference convex. (**md**************************************************************************) (* # Theory of exponential/logarithm functions *) @@ -784,13 +785,6 @@ have [x0|x0 x1] := leP x 0; first by rewrite ln0. by rewrite -ler_expR expR0 lnK. Qed. -Lemma ln_eq0 x : 0 < x -> (ln x == 0) = (x == 1). -Proof. -move=> x0; apply/idP/idP => [/eqP lnx0|/eqP ->]; last by rewrite ln1. -have [| |//] := ltgtP x 1; last by move/ln_gt0; rewrite lnx0 ltxx. -by move/(conj x0)/andP/ln_lt0; rewrite lnx0 ltxx. -Qed. - Lemma continuous_ln x : 0 < x -> {for x, continuous ln}. Proof. move=> x_gt0; rewrite -[x]lnK//. @@ -1148,6 +1142,38 @@ have [x0|x0|->]/= := ltgtP x 0; first by rewrite lt0_powR1// eqxx. - by rewrite powR0// eq_sym oner_eq0. Qed. +(*New!*) +Lemma gt0_gtr_powR r : r < 0 -> + {in Num.pos &, {homo powR ^~ r : x y / x < y >-> y < x}}. +Proof. +move=> r0 x y /[!posrE]=> x0 y0 xy; rewrite -(invrK (x`^r)). +rewrite invf_pgt ?posrE ?invr_gt0 ?powR_gt0 -?powR_inv1 ?powR_ge0 //. +by rewrite -?powRrM ?gt0_ltr_powR ?nnegrE ?ltW ?nmulr_rgt0. +Qed. + +Lemma powR1r r : 1 `^ r = 1. +Proof. by apply/eqP; rewrite powR_eq1 eq_refl. Qed. + +Lemma powR_gt1 r s : 0 <= s -> r `^ s < 1 -> r < 1. +Proof. + case: (ltgtP s 0)=> //[s0|->]; last by rewrite powRr0 ltxx. + case: (ltgtP r 0)=> [r0|r0|->]; last by rewrite powR0 ?gt_eqF. + by rewrite lt0_powR1 ?ltxx. + case: (ltgtP r 1)=>//[r1|->]; last by rewrite powR1 ltxx. + have : 1 `^ s < r `^ s; first by apply /gt0_ltr_powR; rewrite ?nnegrE ?ltW. + by rewrite powR1; case: (ltgtP (r `^ s) 1). +Qed. + +Lemma powR_lt1 r s : 0 <= s -> 1 < r `^ s -> 1 < r. +Proof. + case: (ltgtP s 0)=> //[s0|->]; last by rewrite powRr0 ltxx. + case: (ltgtP r 0)=> [r0|r0|->]; last by rewrite powR0 ?gt_eqF. + by rewrite lt0_powR1 ?ltxx. + case: (ltgtP r 1)=>//[r1|->]; last by rewrite powR1 ltxx. + have : r `^ s < 1 `^ s ; first by apply /gt0_ltr_powR; rewrite ?nnegrE ?ltW. + by rewrite powR1; case: (ltgtP (r `^ s) 1). +Qed. + End PowR. Notation "a `^ x" := (powR a x) : ring_scope. @@ -1252,9 +1278,12 @@ Proof. by rewrite 2!ltNge lne_ge0. Qed. Lemma lne_eq0 x : (lne x == 0) = (x == 1). Proof. -rewrite /lne; move: x => [r| |] //; case: ifPn => r0. - by apply/esym; rewrite lt_eqF// lte_fin (le_lt_trans r0). -by rewrite !eqe ln_eq0// ltNge. +apply/idP/idP => /eqP; last by move=> ->; rewrite lne1. +have [|x0] := leP x 0. + by case: x => [r| |]//; rewrite lee_fin => /= ->. +rewrite -lne1 => /lne_inj. +rewrite ?in_itv/= ?leey ?andbT// => /(_ _ _)/eqP. +by apply => //; exact: ltW. Qed. Lemma lne_gt0 x : (0 < lne x) = (1 < x). @@ -1268,130 +1297,312 @@ End Lne. Section poweR. Local Open Scope ereal_scope. Context {R : realType}. -Implicit Types (s r : R) (x y : \bar R). +Implicit Types (s r : R) (x y z : \bar R). -Definition poweR x r := +Definition poweR x y := if x == 0 then (y == 0)%:R%:E else expeR (y * lne x). + +(*Definition poweR x r := match x with | x'%:E => (x' `^ r)%:E | +oo => if r == 0%R then 1%E else +oo | -oo => if r == 0%R then 1%E else 0%E end. +*) -Local Notation "x `^ r" := (poweR x r). +Local Notation "x `^ y" := (poweR x y). -Lemma poweR_EFin s r : s%:E `^ r = (s `^ r)%:E. -Proof. by []. Qed. +Lemma poweR_EFin r s : (0 <= r)%R -> r%:E `^ s%:E = (r `^ s)%:E. +Proof. +move => le0r; rewrite /poweR /powR; symmetry. +(repeat case: ifPn) => //[/[swap] /eqP -> /eqP //=|/eqP| _ r0]; first by rewrite -eqe => -> /eqP. +by move : le0r; rewrite le0r (negbTE r0) /=; case : (ltgtP r 0%R). +Qed. -Lemma poweRyr r : r != 0%R -> +oo `^ r = +oo. -Proof. by move/negbTE => /= ->. Qed. +(*Lemma poweR_EFin s r : s%:E `^ r = (s `^ r)%:E.*) -Lemma poweRe0 x : x `^ 0 = 1. -Proof. by move: x => [x'| |]/=; rewrite ?powRr0// eqxx. Qed. +Lemma gt0_poweRye y : 0 < y -> +oo `^ y = +oo. +Proof. by move=> ?; rewrite /poweR gt_eqF// gt0_muley. Qed. -Lemma poweRe1 x : 0 <= x -> x `^ 1 = x. -Proof. -by move: x => [x'| |]//= x0; rewrite ?powRr1// (negbTE (oner_neq0 _)). -Qed. +Lemma lt0_poweRye y : y < 0 -> +oo `^ y = 0. +Proof. move=> ?; rewrite /poweR gt_eqF// lt0_muley //. Qed. -Lemma poweRN x r : x \is a fin_num -> x `^ (- r) = (fine x `^ r)^-1%:E. -Proof. by case: x => // x xf; rewrite poweR_EFin powRN. Qed. +(*Lemma poweRye y : y != 0%R -> +oo `^ y = +oo.*) -Lemma poweRNyr r : r != 0%R -> -oo `^ r = 0. -Proof. by move=> r0 /=; rewrite (negbTE r0). Qed. +Lemma poweRe0 x : x `^ 0 = 1. +Proof. by rewrite /poweR; case: ifPn => _; rewrite ?eqxx// mul0e expeR0. Qed. +Lemma poweRe1 x : 0 <= x -> x `^ 1 = x. +Proof. +move=> ?; rewrite /poweR; case : ifPn; first by move /eqP; rewrite onee_eq0. +by rewrite mul1e lneK// in_itv/= leey /= andbT. Qed. + +Lemma poweRN x y : + 0 <= x -> x \is a fin_num -> y \is a fin_num -> + x `^ (- y) = (fine x `^ fine y)^-1%:E. +Proof. +case: x => // r x0; case : y => //s _/=; case : (ltgtP r 0%R) => r0; +try by rewrite ?r0 poweR_EFin// ?ltW// powRN//. +Qed. + +(*Lemma poweRN x r : x \is a fin_num -> x `^ (- r) = (fine x `^ r)^-1%:E.*) + +Lemma lt0_poweRNye y : y < 0 -> -oo `^ y = +oo. +Proof. by move=> ?; rewrite /poweR lt_eqF//= lt0_muleNy. Qed. + +Lemma gt0_poweRNye y : 0 < y -> -oo `^ y = 0. +Proof. by move=> ?; rewrite /poweR lt_eqF//= gt0_muleNy. Qed. + +(*Lemma poweRNyr r : r != 0%R -> -oo `^ r = 0.*) + +Lemma poweRE x y : + poweR x y = if (x == 1) || (y == 0) then 1 + else if x < 0 then + if y < 0 then +oo else 0 + else if x == 0 then 0 + else if x < 1 then + if y == -oo then +oo + else if y == +oo then 0 else (fine x `^ fine y)%:E + else if x == +oo then + if y < 0 then 0 else +oo + else if y == +oo then +oo else + if y == -oo then 0 else (fine x `^ fine y)%:E. +Proof. + repeat case: ifPn. + rewrite /poweR; case : ifPn. + by move=> /eqP -> ; rewrite lt_eqF //= => ->. + by move=> _ /orP [] /eqP ->; rewrite ?lne1 ?mul0e ?mule0 expeR0. + move=> + +; rewrite /poweR; case : ifPn; first by move=> /eqP ->; rewrite ltxx. + by move=> _ ? ?; rewrite le0_lneNy ?ltW ?lt0_muleNy. + move=> + ? H; rewrite /poweR lt_eqF // ; case : (ltgtP y 0) => // y0. + by rewrite le0_lneNy ?ltW // gt0_muleNy. + by move: y0 H => ->; rewrite (_ : 0 == 0) ?orbT. + by move=> /eqP ->; rewrite /poweR (_ : 0 == 0) //; case : (ltgtP y 0) => //=; rewrite orbT. + move=> /eqP ->; rewrite /poweR; case : (ltgtP x 0) => // ? ?. + by rewrite lt0_mulNye ?/expeR ?lne_lt0. + move=> /eqP -> _ ?; rewrite /poweR; case : (ltgtP x 0) => // ?. + by rewrite lt0_mulye ?/expeR ?lne_lt0. + by case : y => // s; case : (ltgtP x 0); case : x=> //= r ? ?; rewrite poweR_EFin ?ltW. + by move=> /[swap] /eqP -> //= ?; rewrite lt0_poweRye. + by case : (ltgtP y 0) => //= + _ /eqP -> //= => ?; rewrite gt0_poweRye. + move=> /eqP ->; rewrite /poweR; case : ifPn=> //=. + by case : (ltgtP x 1) => //= ?; rewrite gt0_mulye ?/expeR ?lne_gt0. + move=> /eqP -> //= _; rewrite /poweR; case : ifPn=> //=; case : (ltgtP x 1)=> //= ?. + by rewrite gt0_mulNye ?/expeR ?lne_gt0. + case : (ltgtP x 1)=> //; case : x; case y => //= s r r1. + by rewrite poweR_EFin// ltW//; apply /lt_trans /r1. +Qed. + + +(* Lemma poweRE x r : poweR x r = if r == 0%R then (if x \is a fin_num then fine x `^ r else 1)%:E else if x == +oo then +oo else if x == -oo then 0 else (fine x `^ r)%:E. +*) + +Lemma poweR_eqy x y : x `^ y = +oo -> if x < 1 then y < 0 else (x == +oo) || (y == +oo). Proof. -case: ifPn => [/eqP r0|r0]. - case: ifPn => finx; last by rewrite r0 poweRe0. - by rewrite -poweR_EFin; case: x finx. -case: ifPn => [/eqP ->|xy]; first by rewrite poweRyr. -case: ifPn => [/eqP ->|xNy]; first by rewrite poweRNyr. -by rewrite -poweR_EFin// fineK// fin_numE xNy. + rewrite poweRE; repeat case : ifPn => //. + case : (ltgtP x 1); case : (ltgtP y 0)=> //= _ x1 _ _ x0; exfalso. + rewrite -falseE -(@ltr10 R); apply : (lt_trans x1 x0). + by move=> /eqP ->. Qed. -Lemma poweR_eqy x r : x `^ r = +oo -> x = +oo. -Proof. by case: x => [x| |] //=; case: ifP. Qed. +(*Lemma poweR_eqy x r : x `^ r = +oo -> x = +oo.*) + +(*Redundant*) +(* +Lemma eqy_poweR x y : 0 < y -> x = +oo -> x `^ y = +oo. +Proof. move=> + ->; apply gt0_poweRye. Qed. +*) -Lemma eqy_poweR x r : (0 < r)%R -> x = +oo -> x `^ r = +oo. -Proof. by move: x => [| |]//= r0 _; rewrite gt_eqF. Qed. +Lemma poweR_lty x y : (if x < 1 then 0 <= y else (x < +oo) && (y < +oo)) -> x `^ y < +oo. +Proof. + rewrite poweRE; repeat case : ifPn => //=; try by rewrite ltry. + by case : (ltgtP y 0). + by move=> /eqP ->. + case : (ltgtP x 1) => //= x1 _ x0; exfalso; + rewrite -falseE -(@ltr10 R); apply : (lt_trans x1 x0). + by case : (ltgtP x +oo). + by case : (ltgtP y +oo); rewrite ?andbF. +Qed. -Lemma poweR_lty x r : x < +oo -> x `^ r < +oo. +(*Lemma poweR_lty x y : x < +oo -> x `^ y < +oo.*) + +Lemma lty_poweRy x y : 0 < y -> x `^ y < +oo -> x < +oo. Proof. -by move: x => [x| |]//=; rewrite ?ltry//; case: ifPn => // _; rewrite ltry. + move : x => [r | |]// y0; first by rewrite ltry. + by rewrite /poweR gt0_muley. Qed. -Lemma lty_poweRy x r : r != 0%R -> x `^ r < +oo -> x < +oo. +(*Lemma lty_poweRy x r : r != 0%R -> x `^ r < +oo -> x < +oo.*) + +Lemma poweR0e y : y != 0 -> 0 `^ y = 0. +Proof. by rewrite /poweR (_ : 0 == 0) //; case : (ltgtP y 0). Qed. + +(*Lemma poweR0r r : r != 0%R -> 0 `^ r = 0.*) + +Lemma poweR1 : poweR 1 = (fun => 1). +Proof. +by apply /funext=> y; rewrite /poweR gt_eqF// lne1 mule0 expeR0. +Qed. + +(*Redundant*) +Lemma poweR1e y : 1 `^ y = 1. +Proof. by rewrite /poweR gt_eqF// lne1 mule0 expeR0. Qed. + +(*Lemma poweR1r r : 1 `^ r = 1*) + +Lemma fine_poweR x y : 0 < x -> y \is a fin_num -> + fine (x `^ y) = ((fine x) `^ (fine y))%R. Proof. -by move=> r0; move: x => [x| | _]//=; rewrite ?ltry// (negbTE r0). +case : y=> //=s + _; case : x=> //= [? ?|]; first by rewrite poweR_EFin ?ltW. +case : (ltgtP s 0%R) => [s0|s0|->]; last by rewrite poweRe0 powRr0. +- by rewrite powR0 ?lt0_poweRye//; move: s0; case : (ltgtP s 0%R). +- by rewrite powR0 ?gt0_poweRye//; move: s0; case : (ltgtP s 0%R). Qed. -Lemma poweR0r r : r != 0%R -> 0 `^ r = 0. -Proof. by move=> r0; rewrite poweR_EFin powR0. Qed. +(*fine_poweR x r : fine (x `^ r) = ((fine x) `^ r)%R.*) + +Lemma poweR_ge0 x y : 0 <= x `^ y. +Proof. by rewrite poweRE; repeat case: ifPn=>//; rewrite lee_fin powR_ge0. Qed. + +(*Lemma poweR_ge0 x r : 0 <= x `^ r.*) + +(* +Lemma poweR_gt0 x y : (if x < 0 then y < 0 else + if x == 0 then y == 0 else + if x < 1 then y <= 0 else + if 1 < x then 0 <= y else true) + -> 0 < x `^ y. *) -Lemma poweR1r r : 1 `^ r = 1. Proof. by rewrite poweR_EFin powR1. Qed. +Lemma poweR_gt0 x y : (if x < 0 then y < 0 else + if x == 0 then y == 0 else + if x < 1 then y <= 0 else + (1 < x) ==> (0 <= y)) + -> 0 < x `^ y. +Proof. +repeat case: ifPn. +- by rewrite poweRE; repeat case: ifPn. +- by move=> /eqP -> + /eqP ->; rewrite poweRe0. +- rewrite poweRE; repeat case: ifPn; case: (ltgtP x 0)=> //. + by move=> + /eqP ->. + by case: x; case: y=>//= ? ? ?; rewrite !lte_fin powR_gt0. +- rewrite poweRE; repeat case: ifPn; case: (ltgtP x 0); case: (ltgtP x 1)=>//=. + + by case: (ltgtP y 0). + + by move=> + + /eqP ->. + + by move=> + x0 + + xy; rewrite lte_fin powR_gt0; move : xy x0; case: x. +Qed. + +(*Lemma poweR_gt0 x r : 0 < x -> 0 < x `^ r.*) -Lemma fine_poweR x r : fine (x `^ r) = ((fine x) `^ r)%R. +Lemma gt0_poweR x y : 0 < y -> 0 <= x -> 0 < x `^ y -> 0 < x. Proof. -by move: x => [x| |]//=; case: ifPn => [/eqP ->|?]; rewrite ?powRr0 ?powR0. +case: x =>// r; rewrite lee_fin. +by case: (ltgtP r 0%R)=> //; move=> -> y0; rewrite poweR0e ?gt_eqF. Qed. -Lemma poweR_ge0 x r : 0 <= x `^ r. -Proof. by move: x => [x| |]/=; rewrite ?lee_fin ?powR_ge0//; case: ifPn. Qed. +(*Lemma gt0_poweR x r : (0 < r)%R -> 0 <= x -> 0 < x `^ r -> 0 < x.*) -Lemma poweR_gt0 x r : 0 < x -> 0 < x `^ r. +Lemma poweRey_gt1 x : 1 < x -> x `^ +oo = +oo. Proof. -by move: x => [x|_|]//=; [rewrite lte_fin; exact: powR_gt0|case: ifPn]. +rewrite /poweR => x1; rewrite gt_eqF// ?(lt_trans lte01)//. +by apply/eqP; rewrite expeR_eqy gt0_mulye// lne_gt0. Qed. -Lemma gt0_poweR x r : (0 < r)%R -> 0 <= x -> 0 < x `^ r -> 0 < x. +Lemma poweReNy_gt1 x : 1 < x -> x `^ -oo = 0. Proof. -move=> r0; move: x => [x|//|]; rewrite ?leeNe_eq// lee_fin !lte_fin. -exact: gt0_powR. +rewrite /poweR => x1; rewrite gt_eqF// ?(lt_trans lte01)//. +by apply/eqP; rewrite expeR_eq0 gt0_mulNye// lne_gt0. Qed. -Lemma poweR_eq0 x r : 0 <= x -> (x `^ r == 0) = ((x == 0) && (r != 0%R)). +Lemma poweRey_lt1 x : 0 <= x < 1 -> x `^ +oo = 0. Proof. -move: x => [x _|_/=|//]; first by rewrite poweR_EFin eqe powR_eq0. -by case: ifP => //; rewrite onee_eq0. +rewrite /poweR le_eqVlt => /andP[/orP[/eqP <- _|x0 x1]]; first by rewrite eqxx. +by rewrite gt_eqF//; apply/eqP; rewrite expeR_eq0 lt0_mulye// lne_lt0// x0 x1. Qed. -Lemma poweR_eq0_eq0 x r : 0 <= x -> x `^ r = 0 -> x = 0. -Proof. by move=> + /eqP => /poweR_eq0-> /andP[/eqP]. Qed. +Lemma poweReNy_lt1 x : 0 < x < 1 -> x `^ -oo = +oo. +Proof. +rewrite /poweR => /andP[x0 x1];rewrite gt_eqF//; apply/eqP. +by rewrite expeR_eqy lt0_mulNye// lne_lt0// x0 x1. +Qed. -Lemma gt0_ler_poweR r : (0 <= r)%R -> - {in `[0, +oo] &, {homo poweR ^~ r : x y / x <= y >-> x <= y}}. +Lemma poweR_eq0y x y : + 0 <= x -> + (x `^ y == 0) = ((x == 0) && (y != 0)) || + ((1 < x) && (y == -oo)) || + ((0 < x < 1) && (y == +oo)) || + ((x == +oo) && (y < 0)). Proof. -move=> r0 + y; case=> //= [x /[1!in_itv]/= /andP[xint _]| _ _]. -- case: y => //= [y /[1!in_itv]/= /andP[yint _] xy| _ _]. - + by rewrite !lee_fin ge0_ler_powR. - + by case: eqP => [->|]; rewrite ?powRr0 ?leey. -- by rewrite leye_eq => /eqP ->. +case: x => [r||]; case: y => [s||]//=. +all: rewrite ?(@gt_eqF _ _ s%:E -oo) ?(@lt_eqF _ _ s%:E +oo) ?ltNye ?ltey//=. +- by move=> ?; rewrite poweR_EFin// !eqe powR_eq0 !andbF !orbF. +1,2: case: (ltgtP r%:E 0)=>//[r0|->]; last by rewrite poweR0e ?eq_refl. +1,2: case: (ltgtP r%:E 1)=> r1; last by rewrite r1 poweR1 gt_eqF. + + by rewrite poweRey_lt1 ?r1 ?eq_refl ?ltW. + + by rewrite poweRey_gt1 ?r1. + + by rewrite poweReNy_lt1 ?r0 ?r1. + + by rewrite poweReNy_gt1 ?r1 ?eq_refl. +- case: (ltgtP s%:E 0)=> s0; last by rewrite s0 poweRe0 ?gt_eqF. + by rewrite lt0_poweRye ?s0 ?eq_refl. + by rewrite gt0_poweRye ?s0 ?gt_eqF. +- by rewrite lt0_poweRye ?eq_refl. Qed. + +(*Lemma poweR_eq0 x r : 0 <= x -> (x `^ r == 0) = ((x == 0) && (r != 0%R)).*) -Lemma fin_num_poweR x r : x \is a fin_num -> x `^ r \is a fin_num. +(*No longer true*) +(*Lemma poweR_eq0_eq0 x y : 0 <= x -> x `^ y = 0 -> x = 0.*) + +Lemma gt0_ler_poweR z : 0 <= z -> + {in `[0, +oo] &, {homo poweR ^~ z : x y / x <= y >-> x <= y}}. Proof. -by move=> xfin; rewrite ge0_fin_numE ?poweR_lty ?ltey_eq ?xfin// poweR_ge0. +move=> z0 + y; case=> //= [r /[!in_itv]/= /andP[r0 _] /andP[]|]; last first. + by move=> _ _; rewrite leye_eq=> /eqP -> /[!@lexx]. +move: z0; case : z=> //[t t0| _]; case: y=> //[s s0 _ rs | _ _]; last first. +- by rewrite !gt0_poweRye // !leey. +- case : (ltgtP 1 r%:E)=> r1. + by rewrite !poweRey_gt1//; apply /(lt_le_trans r1). + by rewrite poweRey_lt1 ?poweR_ge0 ?r1 ?r0. +- move: rs; rewrite -r1 poweR1e; case : (ltgtP 1 s%:E)=> // s1 _. + by rewrite poweRey_gt1 ?leey. + by rewrite -s1 poweR1e. +- move: t0; case:(ltgtP 0 t%:E)=>//[t0|<-]; last by rewrite !poweRe0. + by rewrite gt0_poweRye ?leey. +- by rewrite !poweR_EFin// lee_fin ?ge0_ler_powR. Qed. -Lemma poweRM x y r : 0 <= x -> 0 <= y -> (x * y) `^ r = x `^ r * y `^ r. +Lemma fin_num_poweR x y : 0 <= x -> x \is a fin_num -> y \is a fin_num -> + x `^ y \is a fin_num. +Proof. by case: x; case: y=>// ? ? ?; rewrite poweR_EFin//. Qed. + +(*Lemma fin_num_poweR x r : x \is a fin_num -> x `^ r \is a fin_num.*) + +Lemma poweRM x y r : (r != 0)%R -> 0 <= x -> 0 <= y -> + (x * y) `^ r%:E = x `^ r%:E * y `^ r%:E. Proof. have [->|rN0] := eqVneq r 0%R; first by rewrite !poweRe0 mule1. -have powyrM s : (0 <= s)%R -> (+oo * s%:E) `^ r = +oo `^ r * s%:E `^ r. +have powyrM s : (0 <= s)%R -> (+oo * s%:E) `^ r%:E = +oo `^ r%:E * s%:E `^ r%:E. case: ltgtP => // [s_gt0 _|<- _]; last first. - by rewrite mule0 poweRyr// !poweR0r// mule0. - by rewrite gt0_mulye// poweRyr// gt0_mulye// poweR_gt0. -case: x y => [x| |] [y| |]// x0 y0; first by rewrite /= -EFinM powRM. -- by rewrite muleC powyrM// muleC. + by rewrite poweR0e // !mule0 poweR0e. + rewrite gt0_mulye //;move: rN0;case: (ltgtP r 0%R) => // p0 _. + by rewrite lt0_poweRye ?mul0e. + by rewrite gt0_poweRye ?gt0_mulye ?poweR_EFin ?ltW ?lte_fin ?powR_gt0. +case: x y => [x||] [y||]// _ x0 y0. +- by rewrite ?poweR_EFin ?mulr_ge0 // -EFinM; f_equal; rewrite powRM. +- by rewrite muleC [X in _ = X]muleC powyrM. - by rewrite powyrM. -- by rewrite mulyy !poweRyr// mulyy. +- rewrite mulyy; move: rN0; case: (ltgtP r 0%R) => // rN0 _. + by rewrite lt0_poweRye ?mule0. + by rewrite gt0_poweRye ?mulyy. Qed. -Lemma poweRrM x r s : x `^ (r * s) = (x `^ r) `^ s. +(*Lemma poweRM x y r : 0 <= x -> 0 <= y -> (x * y) `^ r = x `^ r * y `^ r.*) + +Lemma lt0_lt0_poweR x y : x < 0%R -> y < 0%R -> x `^ y = +oo. Proof. rewrite poweRE; repeat case: ifPn=>//; move=>/orP[]/eqP ->; rewrite ?ltxx//. by rewrite lte_fin ltr10. @@ -1468,8 +1679,15 @@ all: try by rewrite -EFinM !poweR_EFin ?ltW ?powRrM ?powR_gt0. by rewrite ?gt0_gtr_powR ?posrE ?ltW ?powR_gt0. Qed. -Lemma poweRAC x r s : (x `^ r) `^ s = (x `^ s) `^ r. -Proof. by rewrite -!poweRrM mulrC. Qed. + +(*Lemma poweRrM x r s : x `^ (r * s) = (x `^ r) `^ s.*) + +Lemma poweRAC x y z : (0 <= x) -> poweRrM_def x y z -> poweRrM_def x z y -> (x `^ y) `^ z = (x `^ z) `^ y. +Proof. +move=> x0 ACdefr ACdefl; rewrite -!poweRrM//; first by rewrite muleC. +Qed. + +(*Lemma poweRAC x r s : (x `^ r) `^ s = (x `^ s) `^ r.*) Definition poweRD_def x r s := ((r + s == 0)%R ==> ((x != 0) && ((x \isn't a fin_num) ==> (r == 0%R) && (s == 0%R)))). @@ -1549,4 +1767,4 @@ move/(series_le_cvg harmonic_ge0 (fun i => ltW (riemannR_gt0 i a0))). by move/contra_not; apply; exact: dvg_harmonic. Qed. -End riemannR_series. +End riemannR_series. \ No newline at end of file From 8c4491b4c212e957556bd543a606e224504a7ac9 Mon Sep 17 00:00:00 2001 From: jmmarulang <78051861+jmmarulang@users.noreply.github.com> Date: Sat, 20 Dec 2025 13:56:07 +0000 Subject: [PATCH 3/5] finished poweR --- theories/exp.v | 775 ++++++++++++++++++++++++++++++------------------- 1 file changed, 480 insertions(+), 295 deletions(-) diff --git a/theories/exp.v b/theories/exp.v index 5dfbf31ab4..e941608621 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -831,8 +831,12 @@ Proof. by rewrite /powR gt_eqF ?expR_gt0// expRK mulrC. Qed. Lemma powR_ge0 a x : 0 <= a `^ x. Proof. by rewrite /powR; case: ifPn => // _; exact: expR_ge0. Qed. -Lemma powR_gt0 a x : 0 < a -> 0 < a `^ x. -Proof. by move=> a0; rewrite /powR gt_eqF// expR_gt0. Qed. +(*Generalized*) + Lemma powR_gt0 a x : 0 != a -> 0 < a `^ x. +Proof. +rewrite /powR; case: ifPn; first by move=> /eqP -> /[!@eq_refl]. +by rewrite expR_gt0. +Qed. Lemma gt0_powR a x : 0 < x -> 0 <= a -> 0 < a `^ x -> 0 < a. Proof. @@ -915,7 +919,7 @@ Proof. rewrite le_eqVlt => /predU1P[<- x y _ _ _|]; first by rewrite !powRr0. move=> a0 x y; rewrite 2!nnegrE !le_eqVlt => /predU1P[<-|x0]. move=> /predU1P[<- _|y0 _]; first by rewrite eqxx. - by rewrite !powR0 ?(gt_eqF a0)// powR_gt0 ?orbT. + by rewrite !powR0 ?(gt_eqF a0) ?powR_gt0 ?orbT ?(lt_eqF y0). move=> /predU1P[<-|y0]; first by rewrite gt_eqF//= ltNge (ltW x0). move=> /predU1P[->//|xy]; first by rewrite eqxx. by apply/orP; right; rewrite /powR !gt_eqF// ltr_expR ltr_pM2l// ltr_ln. @@ -1016,7 +1020,7 @@ have /eqP : (a `^ (2^-1)) ^+ 2 = (Num.sqrt a) ^+ 2. rewrite sqr_sqrtr; last exact: ltW. by rewrite /powR gt_eqF// -expRM_natl mulrA divff ?mul1r// lnK. rewrite eqf_sqr => /predU1P[//|/eqP h]. -have : 0 < a `^ 2^-1 by exact: powR_gt0. +have : 0 < a `^ 2^-1 by apply /powR_gt0; rewrite lt_eqF. by rewrite h oppr_gt0 ltNge sqrtr_ge0. Qed. @@ -1043,8 +1047,8 @@ rewrite le_eqVlt => /predU1P[<- b0 p0 q0 _|a0]. rewrite le_eqVlt => /predU1P[<-|b0] p0 q0 pq. by rewrite mulr0 powR0 ?gt_eqF// mul0r addr0 divr_ge0 ?powR_ge0 ?ltW. have iq1 : q^-1 <= 1 by rewrite -pq ler_wpDl// invr_ge0 ltW. -have ap0 : (0 < a `^ p)%R by rewrite powR_gt0. -have bq0 : (0 < b `^ q)%R by rewrite powR_gt0. +have ap0 : (0 < a `^ p)%R by rewrite powR_gt0 ?lt_eqF. +have bq0 : (0 < b `^ q)%R by rewrite powR_gt0 ?lt_eqF. have := @concave_ln _ (Itv01 (eqbRL (invr_ge0 _) (ltW q0)) iq1) _ _ bq0 ap0. rewrite 2!(convC (Itv01 _ _)). have pq' : (p^-1 = 1 - q^-1)%R by rewrite -pq addrK. @@ -1072,9 +1076,9 @@ rewrite {}/r; case: i x => [|[l u]] x /=; [by apply/and3P; rewrite ?num_real|]. case: x => [x /=/and3P[xr lx xu]]; apply/and3P; split; [exact: num_real| |by[]]. case: l lx => [[] [[|l] |//] |//]; rewrite !bnd_simp => lx. - by rewrite powR_ge0. -- by apply: powR_gt0; apply: lt_le_trans lx. -- by apply: powR_gt0; apply: le_lt_trans lx. -- by apply: powR_gt0; apply: le_lt_trans lx. +- by apply: powR_gt0; rewrite lt_eqF//; apply: lt_le_trans lx. +- by apply: powR_gt0; rewrite lt_eqF//; apply: le_lt_trans lx. +- by apply: powR_gt0; rewrite lt_eqF//; apply: le_lt_trans lx. Qed. Canonical powR_inum (i : Itv.t) (x : Itv.def (@Itv.num_sem R) i) p := @@ -1149,6 +1153,7 @@ Proof. move=> r0 x y /[!posrE]=> x0 y0 xy; rewrite -(invrK (x`^r)). rewrite invf_pgt ?posrE ?invr_gt0 ?powR_gt0 -?powR_inv1 ?powR_ge0 //. by rewrite -?powRrM ?gt0_ltr_powR ?nnegrE ?ltW ?nmulr_rgt0. +all: by rewrite lt_eqF. Qed. Lemma powR1r r : 1 `^ r = 1. @@ -1299,7 +1304,7 @@ Local Open Scope ereal_scope. Context {R : realType}. Implicit Types (s r : R) (x y z : \bar R). -Definition poweR x y := if x == 0 then (y == 0)%:R%:E else expeR (y * lne x). +(*Definition poweR x y := if x == 0 then (y == 0)%:R%:E else expeR (y * lne x).*) (*Definition poweR x r := match x with @@ -1309,32 +1314,87 @@ Definition poweR x y := if x == 0 then (y == 0)%:R%:E else expeR (y * lne x). end. *) -Local Notation "x `^ y" := (poweR x y). +Definition poweR x y := + match (x, y) with + | (r%:E, s%:E) => (r `^ s)%:E + | (r%:E, +oo) => + if (r > 1)%R then +oo + else if (r == 1)%R then 1 else if (r >= 0)%R then 0 else 1 + | (r%:E, -oo) => + if (r > 1)%R then 0 + else if (r == 1)%R then 1 else if (r > 0)%R then +oo else + if (r == 0)%R then 0 else 1 + | (+oo, y) => if y > 0 then +oo else if y < 0 then 0 else 1 + | (-oo, y) => 1 + end. -Lemma poweR_EFin r s : (0 <= r)%R -> r%:E `^ s%:E = (r `^ s)%:E. -Proof. -move => le0r; rewrite /poweR /powR; symmetry. -(repeat case: ifPn) => //[/[swap] /eqP -> /eqP //=|/eqP| _ r0]; first by rewrite -eqe => -> /eqP. -by move : le0r; rewrite le0r (negbTE r0) /=; case : (ltgtP r 0%R). -Qed. +Definition poweR' x y := if x == 0 then (y == 0)%:R%:E else + if x > 0 then expeR (y * lne x) else 1. + +Lemma poweR_is_poweR' x y : poweR x y = poweR' x y. +Proof. +case x, y=> //=. +- rewrite /poweR /poweR'; repeat case: ifPn. + + by move=> /[!eqe] /eqP ->; rewrite /powR eq_refl. + + by rewrite lte_fin /powR; case: (ltgtP 0%R s)=>//?; rewrite lne_EFin. + + rewrite lte_fin; case: (ltgtP 0%R s)=>//[?|<-]; last by rewrite eq_refl. + by rewrite lt0_powR1. +- rewrite /poweR /poweR' eqe; repeat case : ifPn; case : (ltgtP 0%R s)=>//. + + by move=> <-; rewrite ltr10. + 1,2: by move=> s0 _ _ s1; rewrite gt0_mulye; rewrite ?lne_gt0 /expeR. + + by rewrite lte_fin=> ->. + + move=> s0 _ _ s1; exfalso; rewrite -falseE -(@ltxx _ R 0%R). + exact /(lt_trans ltr01) /(lt_trans s1 s0). + + by move=> <-_ /eqP; move: (@ltr01)=>/[swap] <-; rewrite ltxx. + 1,2: by move=> _ _ _ /eqP ->; rewrite lne1 mule0 expeR0. + + case: (ltgtP 1%R s)=>//s1 s0; rewrite lt0_mulye; last by rewrite lne_lt0. + by rewrite /expeR. + 1,2: by rewrite lte_fin; case: (ltgtP 0%R s). +- rewrite /poweR /poweR' eqe; repeat case : ifPn; case : (ltgtP 0%R s)=>//. + 1,2: by move=> _ _ _ s1; rewrite gt0_mulNye; rewrite ?lne_gt0 /expeR. + + by rewrite lte_fin; case: (ltgtP 0%R s). + + move=> s0 _ _ s1; exfalso; rewrite -falseE -(@ltxx _ R 0%R). + exact /(lt_trans ltr01) /(lt_trans s1 s0). + + by move=> <-_ /eqP; move: (@ltr01)=> /[swap] <-; rewrite ltxx. + 1,2: by move=> _ _ _ /eqP ->; rewrite lne1 mule0 expeR0. + + case: (ltgtP 1%R s)=>//s1 s0; rewrite lt0_mulNye; last by rewrite lne_lt0. + by rewrite /expeR. + 1,2: by rewrite lte_fin; case: (ltgtP 0%R s). +- rewrite /poweR /poweR' eqe; repeat case : ifPn; case : (ltgtP 0%R s)=>//. + + by move=> ?; rewrite /lne gt0_muley. + + by rewrite lte_fin; case: (ltgtP s 0%R). + + by move=> <-; rewrite ltxx. + 1-3: by case: (ltgtP +oo 0). + + by rewrite lte_fin; case: (ltgtP s 0%R). + + by move=> s0; rewrite /lne lt0_muley. + + by move=> <-; rewrite ltxx. + + by rewrite lte_fin; case: (ltgtP s 0%R). + 1,2: by rewrite lt0y. + 1-3: by case: (ltgtP s%:E 0)=> // ->; rewrite mul0e expeR0. +Qed. + +Local Notation "x `^ y" := (poweR x y). -(*Lemma poweR_EFin s r : s%:E `^ r = (s `^ r)%:E.*) +Lemma poweR_EFin r s : r%:E `^ s%:E = (r `^ s)%:E. +Proof. by []. Qed. Lemma gt0_poweRye y : 0 < y -> +oo `^ y = +oo. -Proof. by move=> ?; rewrite /poweR gt_eqF// gt0_muley. Qed. +Proof. by move=> y0; rewrite /poweR y0. Qed. Lemma lt0_poweRye y : y < 0 -> +oo `^ y = 0. -Proof. move=> ?; rewrite /poweR gt_eqF// lt0_muley //. Qed. - -(*Lemma poweRye y : y != 0%R -> +oo `^ y = +oo.*) +Proof. +rewrite /poweR; repeat case: (ifPn); case: (ltgtP y 0)=> //. +Qed. Lemma poweRe0 x : x `^ 0 = 1. -Proof. by rewrite /poweR; case: ifPn => _; rewrite ?eqxx// mul0e expeR0. Qed. +Proof. +by case: x=> [r||]; rewrite /poweR ?ltxx //= powRr0. +Qed. Lemma poweRe1 x : 0 <= x -> x `^ 1 = x. Proof. -move=> ?; rewrite /poweR; case : ifPn; first by move /eqP; rewrite onee_eq0. -by rewrite mul1e lneK// in_itv/= leey /= andbT. Qed. +by case: x=> [r||] x0; rewrite /poweR ?powRr1 // lte01. +Qed. Lemma poweRN x y : 0 <= x -> x \is a fin_num -> y \is a fin_num -> @@ -1344,156 +1404,123 @@ case: x => // r x0; case : y => //s _/=; case : (ltgtP r 0%R) => r0; try by rewrite ?r0 poweR_EFin// ?ltW// powRN//. Qed. -(*Lemma poweRN x r : x \is a fin_num -> x `^ (- r) = (fine x `^ r)^-1%:E.*) - -Lemma lt0_poweRNye y : y < 0 -> -oo `^ y = +oo. -Proof. by move=> ?; rewrite /poweR lt_eqF//= lt0_muleNy. Qed. - -Lemma gt0_poweRNye y : 0 < y -> -oo `^ y = 0. -Proof. by move=> ?; rewrite /poweR lt_eqF//= gt0_muleNy. Qed. - -(*Lemma poweRNyr r : r != 0%R -> -oo `^ r = 0.*) - -Lemma poweRE x y : - poweR x y = if (x == 1) || (y == 0) then 1 - else if x < 0 then - if y < 0 then +oo else 0 - else if x == 0 then 0 - else if x < 1 then - if y == -oo then +oo - else if y == +oo then 0 else (fine x `^ fine y)%:E - else if x == +oo then - if y < 0 then 0 else +oo - else if y == +oo then +oo else - if y == -oo then 0 else (fine x `^ fine y)%:E. -Proof. - repeat case: ifPn. - rewrite /poweR; case : ifPn. - by move=> /eqP -> ; rewrite lt_eqF //= => ->. - by move=> _ /orP [] /eqP ->; rewrite ?lne1 ?mul0e ?mule0 expeR0. - move=> + +; rewrite /poweR; case : ifPn; first by move=> /eqP ->; rewrite ltxx. - by move=> _ ? ?; rewrite le0_lneNy ?ltW ?lt0_muleNy. - move=> + ? H; rewrite /poweR lt_eqF // ; case : (ltgtP y 0) => // y0. - by rewrite le0_lneNy ?ltW // gt0_muleNy. - by move: y0 H => ->; rewrite (_ : 0 == 0) ?orbT. - by move=> /eqP ->; rewrite /poweR (_ : 0 == 0) //; case : (ltgtP y 0) => //=; rewrite orbT. - move=> /eqP ->; rewrite /poweR; case : (ltgtP x 0) => // ? ?. - by rewrite lt0_mulNye ?/expeR ?lne_lt0. - move=> /eqP -> _ ?; rewrite /poweR; case : (ltgtP x 0) => // ?. - by rewrite lt0_mulye ?/expeR ?lne_lt0. - by case : y => // s; case : (ltgtP x 0); case : x=> //= r ? ?; rewrite poweR_EFin ?ltW. - by move=> /[swap] /eqP -> //= ?; rewrite lt0_poweRye. - by case : (ltgtP y 0) => //= + _ /eqP -> //= => ?; rewrite gt0_poweRye. - move=> /eqP ->; rewrite /poweR; case : ifPn=> //=. - by case : (ltgtP x 1) => //= ?; rewrite gt0_mulye ?/expeR ?lne_gt0. - move=> /eqP -> //= _; rewrite /poweR; case : ifPn=> //=; case : (ltgtP x 1)=> //= ?. - by rewrite gt0_mulNye ?/expeR ?lne_gt0. - case : (ltgtP x 1)=> //; case : x; case y => //= s r r1. - by rewrite poweR_EFin// ltW//; apply /lt_trans /r1. -Qed. - - -(* -Lemma poweRE x r : - poweR x r = if r == 0%R then - (if x \is a fin_num then fine x `^ r else 1)%:E - else if x == +oo then +oo - else if x == -oo then 0 - else (fine x `^ r)%:E. -*) - -Lemma poweR_eqy x y : x `^ y = +oo -> if x < 1 then y < 0 else (x == +oo) || (y == +oo). +Lemma lt0_poweR1 x y : x < 0 -> x `^ y = 1. Proof. - rewrite poweRE; repeat case : ifPn => //. - case : (ltgtP x 1); case : (ltgtP y 0)=> //= _ x1 _ _ x0; exfalso. - rewrite -falseE -(@ltr10 R); apply : (lt_trans x1 x0). - by move=> /eqP ->. +rewrite poweR_is_poweR' /poweR'; repeat case: ifPn. +- by move=> /eqP ->; rewrite ltxx. +1,2: by case: (ltgtP x 0). Qed. -(*Lemma poweR_eqy x r : x `^ r = +oo -> x = +oo.*) - -(*Redundant*) -(* -Lemma eqy_poweR x y : 0 < y -> x = +oo -> x `^ y = +oo. -Proof. move=> + ->; apply gt0_poweRye. Qed. -*) +Lemma poweR_eqy x y : x `^ y = +oo -> + if x < 1 then y < 0 else (x == +oo) || (y == +oo). +Proof. +case: x=>// r; case: y=>//; rewrite /poweR; repeat case: ifPn=>//. +1,2: by rewrite lte_fin; case: (ltgtP r 1%R). +Qed. Lemma poweR_lty x y : (if x < 1 then 0 <= y else (x < +oo) && (y < +oo)) -> x `^ y < +oo. Proof. - rewrite poweRE; repeat case : ifPn => //=; try by rewrite ltry. - by case : (ltgtP y 0). - by move=> /eqP ->. - case : (ltgtP x 1) => //= x1 _ x0; exfalso; - rewrite -falseE -(@ltr10 R); apply : (lt_trans x1 x0). - by case : (ltgtP x +oo). - by case : (ltgtP y +oo); rewrite ?andbF. +case: x=>// [r|]; case: y=>//[s||]; rewrite /poweR; repeat case: ifPn=> //. +all: try by rewrite !ltry. +- by rewrite lte_fin; case: (ltgtP r 1%R). +- by rewrite lte_fin; case: (ltgtP r 1%R). Qed. -(*Lemma poweR_lty x y : x < +oo -> x `^ y < +oo.*) - Lemma lty_poweRy x y : 0 < y -> x `^ y < +oo -> x < +oo. Proof. - move : x => [r | |]// y0; first by rewrite ltry. - by rewrite /poweR gt0_muley. +move : x => [r | |]//; first by rewrite ltry. +by rewrite /poweR; repeat case: ifPn. Qed. -(*Lemma lty_poweRy x r : r != 0%R -> x `^ r < +oo -> x < +oo.*) - Lemma poweR0e y : y != 0 -> 0 `^ y = 0. -Proof. by rewrite /poweR (_ : 0 == 0) //; case : (ltgtP y 0). Qed. - -(*Lemma poweR0r r : r != 0%R -> 0 `^ r = 0.*) +Proof. +case: y=> [r||]; rewrite /poweR/=; repeat case: ifPn=> //. +- by move=> ?; rewrite powR0. +- by rewrite ltr10. +- by move=> /eqP <-. +- by rewrite lexx. +- by move=> /eqP <-. +- by rewrite ltxx. +- by rewrite eq_refl. +Qed. Lemma poweR1 : poweR 1 = (fun => 1). -Proof. -by apply /funext=> y; rewrite /poweR gt_eqF// lne1 mule0 expeR0. +Proof. +by apply /funext=> y; case: y=> [r||]; rewrite /poweR ?powR1 ?ltxx ?eq_refl. Qed. -(*Redundant*) -Lemma poweR1e y : 1 `^ y = 1. -Proof. by rewrite /poweR gt_eqF// lne1 mule0 expeR0. Qed. - -(*Lemma poweR1r r : 1 `^ r = 1*) - Lemma fine_poweR x y : 0 < x -> y \is a fin_num -> fine (x `^ y) = ((fine x) `^ (fine y))%R. Proof. -case : y=> //=s + _; case : x=> //= [? ?|]; first by rewrite poweR_EFin ?ltW. -case : (ltgtP s 0%R) => [s0|s0|->]; last by rewrite poweRe0 powRr0. -- by rewrite powR0 ?lt0_poweRye//; move: s0; case : (ltgtP s 0%R). -- by rewrite powR0 ?gt0_poweRye//; move: s0; case : (ltgtP s 0%R). +case: x=>// [r|]; case: y=>//= s _ _; rewrite /poweR; repeat case: ifPn=>//=. +- by move=> s0; rewrite ?powR0 ?gt_eqF. +- by move=> s0; rewrite ?powR0 ?lt_eqF. +- by case: (ltgtP s%:E 0)=> // /eqP /[!eqe] /eqP -> /[!powRr0]. Qed. -(*fine_poweR x r : fine (x `^ r) = ((fine x) `^ r)%R.*) - Lemma poweR_ge0 x y : 0 <= x `^ y. -Proof. by rewrite poweRE; repeat case: ifPn=>//; rewrite lee_fin powR_ge0. Qed. - -(*Lemma poweR_ge0 x r : 0 <= x `^ r.*) - -(* -Lemma poweR_gt0 x y : (if x < 0 then y < 0 else - if x == 0 then y == 0 else - if x < 1 then y <= 0 else - if 1 < x then 0 <= y else true) - -> 0 < x `^ y. *) - -Lemma poweR_gt0 x y : (if x < 0 then y < 0 else - if x == 0 then y == 0 else - if x < 1 then y <= 0 else - (1 < x) ==> (0 <= y)) - -> 0 < x `^ y. -Proof. +Proof. +case: x=> [r||]; case: y=> [s||]; rewrite /poweR; repeat case: ifPn=>//. +- by rewrite lee_fin powR_ge0. +all: by rewrite lee01. +Qed. + +(*TODO: move*) +Lemma leyr s : (+oo <= s%:E = false). +Proof. by case: (ltgtP +oo s%:E). Qed. + +Lemma ltyr s : (+oo < s%:E = false). +Proof. by case: (ltgtP +oo s%:E). Qed. + +Lemma ltrNy s : (s%:E < -oo = false). +Proof. by case: (ltgtP -oo s%:E). Qed. + + Lemma lerNy s : (s%:E <= -oo = false). +Proof. by case: (ltgtP -oo s%:E). Qed. + +(* + match (x, y) with + | (r%:E, s%:E) => (r `^ s)%:E + | (r%:E, +oo) => + if (r > 1)%R then +oo + else if (r == 1)%R then 1 else if (r >= 0)%R then 0 else 1 + | (r%:E, -oo) => + if (r > 1)%R then 0 + else if (r == 1)%R then 1 else if (r > 0)%R then +oo else + if (r == 0)%R then 0 else 1 + | (+oo, y) => if y > 0 then +oo else if y < 0 then 0 else 1 + | (-oo, y) => 1 + end. +*) + +Lemma poweR_gt0 x y : (if x == 0 then y == 0 else + if +oo <= x then 0 <= y else + if y <= -oo then x <= 1 else + (+oo <= y) ==> (1 <= x) || (x <= 0)) = (0 < x `^ y). +Proof. repeat case: ifPn. -- by rewrite poweRE; repeat case: ifPn. -- by move=> /eqP -> + /eqP ->; rewrite poweRe0. -- rewrite poweRE; repeat case: ifPn; case: (ltgtP x 0)=> //. - by move=> + /eqP ->. - by case: x; case: y=>//= ? ? ?; rewrite !lte_fin powR_gt0. -- rewrite poweRE; repeat case: ifPn; case: (ltgtP x 0); case: (ltgtP x 1)=>//=. +- move=> /eqP ->; case: (ltgtP y 0)=> [y0|y0|->]. + 1,2: by rewrite poweR0e ?ltxx ?(lt_eqF y0) ?(gt_eqF y0). + by rewrite /poweR //= /powR eq_refl //= lte01. +- case: x=>// _ _; rewrite /poweR; repeat case: ifPn. + + by move=> y0; rewrite ltW ?ltry. + by case: (ltgtP y 0). - + by move=> + + /eqP ->. - + by move=> + x0 + + xy; rewrite lte_fin powR_gt0; move : xy x0; case: x. + + by rewrite lte01; case: (ltgtP y 0). +- case: y; case: (ltgtP x +oo); case: x=>// [r|]; last first. + by rewrite !leNye /poweR lte01. + rewrite /poweR; repeat case: ifPn. + + by rewrite !lee_fin ltxx; case: (ltgtP r 1%R). + + by move=> /eqP ->; rewrite !lexx lte01. + + by rewrite !ltry lee_fin; case: (ltgtP r 1%R). + + by move=> /eqP -> /[!eq_refl]. + + by rewrite lte01 lee_fin; case: (ltgtP r 1%R). +- case: (ltgtP x +oo); case: (ltgtP y -oo); case: x; case: y=>//. + + by move=> r s _ _ _ _ s0; rewrite leyr /= /poweR lte_fin powR_gt0 // eq_sym. + + move=> r; rewrite lexx /poweR !lee_fin. + case: (ltgtP r 0%R); case: (ltgtP r 1%R); rewrite ?lte01 ?ltry //=. + - by move=> _ -> /[!@eq_refl]. + - by move=> r; rewrite leyr /poweR lte01. + - by rewrite lexx leNye /poweR lte01. Qed. (*Lemma poweR_gt0 x r : 0 < x -> 0 < x `^ r.*) @@ -1508,51 +1535,52 @@ Qed. Lemma poweRey_gt1 x : 1 < x -> x `^ +oo = +oo. Proof. -rewrite /poweR => x1; rewrite gt_eqF// ?(lt_trans lte01)//. -by apply/eqP; rewrite expeR_eqy gt0_mulye// lne_gt0. +by case: x=>// [r|]; rewrite /poweR ?lte_fin ?ltry//; move=> ->. Qed. Lemma poweReNy_gt1 x : 1 < x -> x `^ -oo = 0. Proof. -rewrite /poweR => x1; rewrite gt_eqF// ?(lt_trans lte01)//. -by apply/eqP; rewrite expeR_eq0 gt0_mulNye// lne_gt0. +by case: x=>// [r|]; rewrite /poweR ?lte_fin ?ltrNy ?ltNyr//; move=> ->. Qed. Lemma poweRey_lt1 x : 0 <= x < 1 -> x `^ +oo = 0. Proof. -rewrite /poweR le_eqVlt => /andP[/orP[/eqP <- _|x0 x1]]; first by rewrite eqxx. -by rewrite gt_eqF//; apply/eqP; rewrite expeR_eq0 lt0_mulye// lne_lt0// x0 x1. +case: x=>// [r|]; rewrite /poweR ?lte_fin ?lee_fin. + by case: (ltgtP r 0%R); case: (ltgtP r 1%R). +by rewrite ?leey ?ltyr ?ltry. Qed. Lemma poweReNy_lt1 x : 0 < x < 1 -> x `^ -oo = +oo. Proof. -rewrite /poweR => /andP[x0 x1];rewrite gt_eqF//; apply/eqP. -by rewrite expeR_eqy lt0_mulNye// lne_lt0// x0 x1. -Qed. - -Lemma poweR_eq0y x y : - 0 <= x -> - (x `^ y == 0) = ((x == 0) && (y != 0)) || - ((1 < x) && (y == -oo)) || - ((0 < x < 1) && (y == +oo)) || - ((x == +oo) && (y < 0)). -Proof. -case: x => [r||]; case: y => [s||]//=. -all: rewrite ?(@gt_eqF _ _ s%:E -oo) ?(@lt_eqF _ _ s%:E +oo) ?ltNye ?ltey//=. -- by move=> ?; rewrite poweR_EFin// !eqe powR_eq0 !andbF !orbF. -1,2: case: (ltgtP r%:E 0)=>//[r0|->]; last by rewrite poweR0e ?eq_refl. -1,2: case: (ltgtP r%:E 1)=> r1; last by rewrite r1 poweR1 gt_eqF. - + by rewrite poweRey_lt1 ?r1 ?eq_refl ?ltW. - + by rewrite poweRey_gt1 ?r1. - + by rewrite poweReNy_lt1 ?r0 ?r1. - + by rewrite poweReNy_gt1 ?r1 ?eq_refl. -- case: (ltgtP s%:E 0)=> s0; last by rewrite s0 poweRe0 ?gt_eqF. - by rewrite lt0_poweRye ?s0 ?eq_refl. - by rewrite gt0_poweRye ?s0 ?gt_eqF. -- by rewrite lt0_poweRye ?eq_refl. -Qed. - -(*Lemma poweR_eq0 x r : 0 <= x -> (x `^ r == 0) = ((x == 0) && (r != 0%R)).*) +case: x=>// [r|]; rewrite /poweR ?lte_fin ?lee_fin ?ltyr ?andbF //. + by case: (ltgtP r 0%R); case: (ltgtP r 1%R). +Qed. + +Lemma poweR_eq0 x y : + (if x == 0 then y != 0 else + if x == +oo then y < 0 else + if y == +oo then (0 < x < 1) else + if (y == -oo) then (1 < x) else false) = (x `^ y == 0). +Proof. +repeat case: ifPn. +- move=> /eqP ->; case: (ltgtP y 0)=> [y0|y0|->]. + + by rewrite poweR0e ?(lt_eqF y0) ?eq_refl. + + by rewrite poweR0e ?(gt_eqF y0) ?eq_refl. + + by rewrite /poweR /= /powR ?eq_refl /= gt_eqF. +- move=> /eqP ->; rewrite /poweR; repeat case: ifPn; case: (ltgtP y 0)=>//. + by rewrite eq_refl. + by rewrite !gt_eqF. +- move=> /eqP ->; case: x=>//[r|]; last by rewrite ltrNy /= /poweR gt_eqF. + rewrite /poweR !lte_fin ?eqe. + by case: (ltgtP 0%R r); case: (ltgtP 1%R r)=>//=; rewrite ?eq_refl ?gt_eqF. +- move=>/eqP ->; case: x=>//[r|]; rewrite /poweR ?lte_fin; last first. + by rewrite ltrNy [X in _ = X]gt_eqF. + rewrite eqe; repeat case: ifPn=> //=; first by rewrite eq_refl. + 1,2: by rewrite [X in _ = X]gt_eqF. +- case: y=>// s; case: x=> //[r|]; rewrite /poweR; last first. + by rewrite [X in _ = X]gt_eqF. + by move=> /[!@eqe] /[!@powR_eq0]; case: (ltgtP r 0%R). +Qed. (*No longer true*) (*Lemma poweR_eq0_eq0 x y : 0 <= x -> x `^ y = 0 -> x = 0.*) @@ -1565,22 +1593,22 @@ move=> z0 + y; case=> //= [r /[!in_itv]/= /andP[r0 _] /andP[]|]; last first. move: z0; case : z=> //[t t0| _]; case: y=> //[s s0 _ rs | _ _]; last first. - by rewrite !gt0_poweRye // !leey. - case : (ltgtP 1 r%:E)=> r1. - by rewrite !poweRey_gt1//; apply /(lt_le_trans r1). - by rewrite poweRey_lt1 ?poweR_ge0 ?r1 ?r0. -- move: rs; rewrite -r1 poweR1e; case : (ltgtP 1 s%:E)=> // s1 _. - by rewrite poweRey_gt1 ?leey. - by rewrite -s1 poweR1e. + + by rewrite !poweRey_gt1//; apply /(lt_le_trans r1). + + by rewrite poweRey_lt1 ?r0 ?r1 ?poweR_ge0. + + move: r1 rs=> <-; rewrite poweR1; case: (ltgtP 1 s%:E)=>[||<-/[!@poweR1]]//. + by move=> s1; rewrite poweRey_gt1 ?leey. - move: t0; case:(ltgtP 0 t%:E)=>//[t0|<-]; last by rewrite !poweRe0. by rewrite gt0_poweRye ?leey. - by rewrite !poweR_EFin// lee_fin ?ge0_ler_powR. Qed. -Lemma fin_num_poweR x y : 0 <= x -> x \is a fin_num -> y \is a fin_num -> +Lemma fin_num_poweR x y : x \is a fin_num -> y \is a fin_num -> x `^ y \is a fin_num. Proof. by case: x; case: y=>// ? ? ?; rewrite poweR_EFin//. Qed. (*Lemma fin_num_poweR x r : x \is a fin_num -> x `^ r \is a fin_num.*) +(*TODO:check if this can be generalized*) Lemma poweRM x y r : (r != 0)%R -> 0 <= x -> 0 <= y -> (x * y) `^ r%:E = x `^ r%:E * y `^ r%:E. Proof. @@ -1590,7 +1618,7 @@ have powyrM s : (0 <= s)%R -> (+oo * s%:E) `^ r%:E = +oo `^ r%:E * s%:E `^ r%:E. by rewrite poweR0e // !mule0 poweR0e. rewrite gt0_mulye //;move: rN0;case: (ltgtP r 0%R) => // p0 _. by rewrite lt0_poweRye ?mul0e. - by rewrite gt0_poweRye ?gt0_mulye ?poweR_EFin ?ltW ?lte_fin ?powR_gt0. + by rewrite gt0_poweRye ?gt0_mulye ?poweR_EFin ?ltW ?lte_fin ?powR_gt0 ?lt_eqF. case: x y => [x||] [y||]// _ x0 y0. - by rewrite ?poweR_EFin ?mulr_ge0 // -EFinM; f_equal; rewrite powRM. - by rewrite muleC [X in _ = X]muleC powyrM. @@ -1602,6 +1630,7 @@ Qed. (*Lemma poweRM x y r : 0 <= x -> 0 <= y -> (x * y) `^ r = x `^ r * y `^ r.*) +(* Lemma lt0_lt0_poweR x y : x < 0%R -> y < 0%R -> x `^ y = +oo. Proof. rewrite poweRE; repeat case: ifPn=>//; move=>/orP[]/eqP ->; rewrite ?ltxx//. @@ -1613,96 +1642,261 @@ move=> x0; rewrite poweRE x0; repeat case : ifPn=>//; case: (ltgtP y 0)=> //. rewrite (_ : x == 1 = false)//=; apply/eqP. by move: x0=>/[swap] ->; rewrite lte_fin ltr10. Qed. +*) Definition poweRrM_def x y z := - (z < 0) ==> (0 < x) ==> - (((x < +oo) || (0 <= y)) && - ((x <= 1) || (x == +oo) || (-oo < y)) && - ((1 <= x) || (y < +oo))). - -Lemma poweRrM (x y z : \bar R) : (0 <= x) -> poweRrM_def x y z -> - x `^ (y * z) = (x `^ y) `^ z. -Proof. -rewrite /poweRrM_def. -case: (ltgtP z 0); case: (ltgtP y 0); case: (ltgtP x 0)=> //=; last first. -1-6: by move=> + + -> //=; rewrite mule0 !poweRe0. -1-2,7-8: by move=> + -> //=; rewrite mul0e !poweRe0 poweR1. -1,3,5,7: move=> -> y0 z0; rewrite !poweR0e ?mule_neq0//. -1-16: by rewrite ?(gt_eqF y0) ?(gt_eqF z0) ?(lt_eqF y0) ?(lt_eqF z0)//. -all: case: (ltgtP x 1)=> [||->]; last by rewrite !poweR1. -all: case: x=> [r||]// + + y0 z0. -3: by rewrite (gt0_poweRye y0) (gt0_poweRye z0) gt0_poweRye ?(mule_gt0 y0 z0). -5: {rewrite (lt0_poweRye y0) poweR0e; last by rewrite (gt_eqF z0). - by rewrite lt0_poweRye ?(mule_lt0_gt0 y0 z0). } -7: {rewrite (gt0_poweRye y0) (lt0_poweRye z0) lt0_poweRye//. - by rewrite (mule_gt0_lt0 y0 z0). } -all: move: y z y0 z0=> [s||] [t||]//= s0 t0 r1 r0; rewrite ?ltxx ?andbF//. -all: try by rewrite -EFinM !poweR_EFin ?ltW ?powRrM ?powR_gt0. -- rewrite (gt0_muley s0) poweR_EFin ?poweRey_lt1 ?ltW ?lte_fin ?powR_gt0//. - rewrite (_ : 1 = 1 `^ s)%R; last by rewrite powR1. - by rewrite gt0_ltr_powR ?nnegrE ?ltW. -- by rewrite (gt0_mulye t0) poweRey_lt1 ?ltW ?poweR0e ?gt_eqF. -- by rewrite gt0_mulye ?poweRey_lt1 ?lexx ?ltW ?lte01. -- rewrite (gt0_muley s0) poweR_EFin ?ltW ?poweRey_gt1 ?lte_fin//. - rewrite (_ : 1 = 1 `^ s)%R; last by rewrite powR1. - by rewrite gt0_ltr_powR ?nnegrE ?ltW. -- by rewrite (gt0_mulye t0) ?poweRey_gt1 ?gt0_poweRye. -- by rewrite gt0_muley ?poweRey_gt1 ?ltey. -- rewrite (lt0_muley s0) poweR_EFin ?poweRey_gt1 ?ltW ?poweReNy_lt1 ?r0//. - rewrite (_ : 1 = 1 `^ s)%R; last by rewrite powR1. - by rewrite !lte_fin gt0_gtr_powR ?posrE ?ltW. -- by rewrite (gt0_mulNye t0) ?poweReNy_lt1 ?gt0_poweRye ?r0. -- by rewrite lt0_muley ?poweReNy_lt1 ?r0. -- rewrite (lt0_muley s0) ?poweReNy_gt1 ?poweRey_lt1 ?poweR_ge0//. - rewrite poweR_EFin ?ltW// (_ : 1 = 1 `^ s)%R; last by rewrite powR1. - by rewrite !lte_fin gt0_gtr_powR ?posrE ?ltW. -- by rewrite (gt0_mulNye t0) ?poweReNy_gt1 ?poweR0e ?gt_eqF. -- by rewrite lt0_muley ?poweReNy_gt1 ?poweR0e. -- rewrite (gt0_muleNy s0) poweR_EFin ?ltW ?poweReNy_lt1 ?r0 ?r1 //. - rewrite !lte_fin powR_gt0// (_ : 1 = 1 `^ s)%R; last by rewrite powR1. - by rewrite gt0_ltr_powR ?nnegrE ?ltW. -- rewrite (gt0_muleNy s0) poweR_EFin ?ltW ?poweReNy_gt1 //. - rewrite lte_fin (_ : 1 = 1 `^ s)%R; last by rewrite powR1. - by rewrite ?gt0_ltr_powR ?nnegrE ?ltW. -- by rewrite (lt0_mulye t0) ?poweReNy_gt1 ?poweRey_gt1 ?lt0_poweRye. -- by rewrite gt0_muleNy ?poweReNy_gt1 ?poweRey_gt1 ?ltey_eq. -- rewrite (lt0_muleNy s0) poweR_EFin ?ltW// poweReNy_gt1; last first. - rewrite lte_fin (_ : 1 = 1 `^ s)%R; last by rewrite powR1. - by rewrite ?gt0_gtr_powR ?posrE ?ltW. - by rewrite poweRey_lt1 ?ltW ?r0 ?r1. -- rewrite (lt0_mulNye t0) ?poweReNy_lt1 ?poweRey_lt1 ?ltW ?r0 ?r1 //. - by rewrite lt0_poweRye. -- rewrite lt0_mulNye ?poweRey_lt1 ?ltW ?r0 ?r1//. - by rewrite [X in _ = X `^ _]poweReNy_lt1 ?r0 ?r1. -- rewrite (lt0_muleNy s0) poweR_EFin ?ltW// ?poweRey_gt1 ?r0 ?r1 //. - rewrite ?poweReNy_lt1// !lte_fin (_ : 1 = 1 `^ s)%R; last by rewrite powR1. - by rewrite ?gt0_gtr_powR ?posrE ?ltW ?powR_gt0. -Qed. - - -(*Lemma poweRrM x r s : x `^ (r * s) = (x `^ r) `^ s.*) - -Lemma poweRAC x y z : (0 <= x) -> poweRrM_def x y z -> poweRrM_def x z y -> (x `^ y) `^ z = (x `^ z) `^ y. -Proof. -move=> x0 ACdefr ACdefl; rewrite -!poweRrM//; first by rewrite muleC. -Qed. - -(*Lemma poweRAC x r s : (x `^ r) `^ s = (x `^ s) `^ r.*) - -Definition poweRD_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 )" := (poweRD_def x r s) : ereal_scope. - -Lemma poweRD_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. + match (x, y, z) with + | (+oo , y , z) => (0 <= z) || (0 <= y) + | (r%:E, +oo, -oo) => (1 <= r%:E) || (r%:E <= 0) + | (r%:E, -oo, -oo) => (r%:E <= 1) + | (r%:E, -oo, t%:E) => (t%:E < 0) ==> (r%:E <= 1) + | (r%:E, +oo, t%:E) => (t%:E < 0) ==> ((1 <= r%:E) || (r%:E <= 0)) + | _ => true + end. -Lemma poweRB_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 poweRD_defE subr_eq0 oppr_eq0. Qed. +Notation "x '`^?' ( y *? z )" := (poweRrM_def x y z) : ereal_scope. + +Lemma poweRrM (x y z : \bar R) : x `^? ( y *? z ) = + (x `^ (y * z) == (x `^ y) `^ z). +Proof. +have neq_01 : ((0%R : R) == (1%R : R) = false) by apply /lt_eqF. +have NyNy : ((-oo : \bar R) * -oo = +oo) by rewrite lt0_mulNye. +have yNy : ((+oo : \bar R) * -oo = -oo) by rewrite lt0_mulye. +have Nyy : ((-oo : \bar R) * +oo = -oo) by rewrite gt0_mulNye. +have yy : ((+oo : \bar R) * +oo = +oo) by rewrite gt0_mulye. +case: (ltgtP x 0)=> x0; rewrite ?x0. +- have x1 : (x < 1) by apply /(lt_trans x0). + rewrite ?(lt0_poweR1 _ x0) ?poweR1 ?eq_refl//. + move: x y z x0 x1=> [r||] [s||] [t||]; rewrite /poweRrM_def//. + 1,2: by case: (ltgtP r%:E 0)=>//; rewrite ?orbT ?implybT. + 1,2: by case: (ltgtP r%:E 1)=>//; rewrite ?orbT ?implybT. +- move: x y z x0=> [r||] [s||] [t||]; rewrite /poweRrM_def; last first. + 1-27: rewrite ?/poweR ?lerNy ?orbF ?NyNy ?yNy ?Nyy ?yy ?ltry ?ltNyr //=. + 1-18: rewrite ?neq_01 ?ltxx ?ltr10 ?lexx ?eq_refl ?leey ?orbT//=. + 14: by rewrite powRrM eq_refl. + 1,2: case: (ltgtP t%:E 0)=> [t0|t0|/eqP /[!eqe] /eqP ->]. + - by rewrite lt0_mulNye ?ltry. + - by rewrite gt0_mulNye ?ltrNy ?ltNyr ?powR0 ?eq_refl ?gt_eqF. + 1,4: by rewrite mule0 ltxx ?powRr0 ?eq_refl. + - by rewrite lt0_mulye ?ltrNy ?ltNyr ?eq_refl. + - by rewrite gt0_mulye ?ltry. + 1,2: case: (ltgtP s%:E 0)=> [s0|s0|/eqP /[!eqe] /eqP ->]. + - by rewrite lt0_muleNy ?ltry/= ?ltr10 ?neq_01 ?ltxx ?eq_refl. + - by rewrite gt0_muleNy ?ltrNy ?ltNyr ?eq_refl. + 1,4: by rewrite mul0e ?ltxx ?eq_refl. + - by rewrite lt0_muley ?ltrNy ?ltNyr/= ?ltr10 ?neq_01 ?lexx ?eq_refl. + - by rewrite gt0_muley ?ltry. + + case: (ltgtP s%:E 0); case: (ltgtP t%:E 0)=>//= t0 s0. + - by have := mule_lt0_lt0 s0 t0; case: (ltgtP (s%:E * t%:E) 0). + - have := mule_lt0_gt0 s0 t0; case: (ltgtP (s%:E * t%:E) 0)=>//. + by rewrite powR0 ?eq_refl// gt_eqF. + - by move: t0=> /eqP /[!eqe] /eqP ->; rewrite mule0 ltxx powRr0 eq_refl. + - have := mule_gt0_lt0 s0 t0; case: (ltgtP (s%:E * t%:E) 0)=>//. + by rewrite eq_refl. + - by have := mule_gt0 s0 t0; case: (ltgtP (s%:E * t%:E) 0). + - by move: t0=> /eqP /[!eqe] /eqP ->; rewrite mule0 ltxx eq_refl. + 1-3: by move: s0=> /eqP /[!eqe] /eqP ->; rewrite mul0e ltxx powR1 eq_refl. + + rewrite lte_fin lee_fin; case: (ltgtP r 1)%R; case: (ltgtP r 0)%R=>//=. + - by rewrite eq_refl. + - by rewrite ltr10 neq_01 ltxx eq_refl. + - by rewrite ltxx !eq_refl. + + rewrite lte_fin; case: (ltgtP r 1)%R; case: (ltgtP r 0)%R=>//=. + by rewrite ltr10 neq_01 lexx eq_refl. + by rewrite ltxx !eq_refl. + + rewrite !lte_fin !lee_fin; case: (ltgtP t 0)%R=>//=t0. + 1-3: case: (ltgtP r 1)%R; case: (ltgtP r 0)%R=>//=. + 1-3: by rewrite lt0_mulNye ?powR1 ?eq_refl. + 1-3: by rewrite gt0_mulNye ?powR0 ?powR1 ?eq_refl ?gt_eqF. + 1-3: by rewrite t0 mule0/= !powRr0 eq_refl. + + rewrite lte_fin !lee_fin; case: (ltgtP r 1)%R; case: (ltgtP r 0)%R=>//=. + 1-3: by rewrite ?ltxx ?eq_refl ?ltr10 ?neq_01. + + rewrite lte_fin ; case: (ltgtP r 1)%R; case: (ltgtP r 0)%R=>//=. + by rewrite ltr10 neq_01 lexx eq_refl. + by rewrite ltxx !eq_refl. + + rewrite !lte_fin !lee_fin; case: (ltgtP t 0)%R=>//=t0. + 1-3: case: (ltgtP r 1)%R; case: (ltgtP r 0)%R=>//=. + 1-3: by rewrite lt0_mulye ?powR1 ?eq_refl. + 1-2: by rewrite gt0_mulye ?powR0 ?eq_refl// gt_eqF. + - by move=> /[swap] ->; rewrite gt0_mulye ?powR1 ?eq_refl. + 1-3: by rewrite t0 mule0/= !powRr0 eq_refl. + + rewrite !lte_fin; case: (ltgtP s 0)%R=>//s0; last first. + - by rewrite s0 mul0e/= powRr0 ltxx !eq_refl. + 1-2: case: (ltgtP r 1)%R; case: (ltgtP r 0)%R=>//= r0 r1. + - have : (r `^ s < 1 `^ s)%R by apply /gt0_ltr_powR; rewrite ?nnegrE ?ltW. + rewrite powR1 gt0_muleNy//. + by case: (ltgtP (r `^ s) 1)%R; rewrite ?powR_gt0// lt_eqF. + - have : (1 `^ s < r `^ s)%R by apply /gt0_ltr_powR; rewrite ?nnegrE ?ltW. + rewrite powR1 gt0_muleNy//. + by case: (ltgtP (r `^ s) 1)%R; rewrite ?powR_gt0 ?eq_refl// lt_eqF. + - by rewrite r1 gt0_muleNy// powR1 ltxx !eq_refl. + - have : (1 `^ s < r `^ s)%R by apply /gt0_gtr_powR; rewrite ?posrE. + rewrite powR1 lt0_muleNy//. + by case: (ltgtP (r `^ s) 1)%R; rewrite ?eq_refl. + - have : (r `^ s < 1 `^ s)%R by apply /gt0_gtr_powR; rewrite ?posrE ?ltW. + rewrite powR1 lt0_muleNy//. + by case: (ltgtP (r `^ s) 1)%R; rewrite ?powR_gt0 ?eq_refl// lt_eqF. + - by rewrite r1 lt0_muleNy// powR1 ltxx !eq_refl. + + rewrite !lte_fin; case: (ltgtP s 0)%R=>//s0; last first. + - by rewrite s0 mul0e/= powRr0 ltxx !eq_refl. + 1-2: case: (ltgtP r 1)%R; case: (ltgtP r 0)%R=>//= r0 r1. + - have : (r `^ s < 1 `^ s)%R by apply /gt0_ltr_powR; rewrite ?nnegrE ?ltW. + rewrite powR1 gt0_muley//. + by case: (ltgtP (r `^ s) 1)%R; rewrite ?powR_ge0 ?eq_refl. + - have : (1 `^ s < r `^ s)%R by apply /gt0_ltr_powR; rewrite ?nnegrE ?ltW. + by rewrite powR1 gt0_muley; case: (ltgtP (r `^ s) 1)%R. + - by rewrite r1 gt0_muley// powR1 ltxx !eq_refl. + - have : (1 `^ s < r `^ s)%R by apply /gt0_gtr_powR; rewrite ?posrE. + by rewrite powR1 lt0_muley; case: (ltgtP (r `^ s) 1)%R. + - have : (r `^ s < 1 `^ s)%R by apply /gt0_gtr_powR; rewrite ?posrE ?ltW. + rewrite powR1 lt0_muley//. + by case: (ltgtP (r `^ s) 1)%R; rewrite ?powR_ge0 ?eq_refl. + - by rewrite r1 lt0_muley ?powR1 ?ltxx ?eq_refl. +- case: (eqVneq y 0)=> y0; case: (eqVneq z 0)=> z0. + all: rewrite ?y0 ?z0 ?mule0 ?mul0e ?poweRe0 ?poweR1 ?eq_refl//. + by move: y y0=> [s||]; rewrite /poweRrM_def//= ?ltxx. + rewrite !poweR0e ?eq_refl ?mule_neq0//=. + move: y z y0 z0 => [s||] [t||]; rewrite /poweRrM_def //=. + all: by rewrite ?lexx ?lee01 ?orbT ?implybT. +Qed. + +Lemma poweRAC x y z : poweRrM_def x y z -> poweRrM_def x z y -> + (x `^ y) `^ z = (x `^ z) `^ y. +Proof. by rewrite !poweRrM muleC=> /eqP <- /eqP. Qed. + +Definition poweRD_def x y z := + match x, y, z with + | x%:E , y%:E , z%:E => (y + z == 0%R) ==> + ((x != 0%R) || ((y == 0%R) && (z == 0%R))) + | x%:E , -oo , +oo => (x <= 0)%R || (1 <= x)%R + | x%:E , +oo , -oo => (x <= 0)%R || (1 <= x)%R + | +oo , y%:E , z%:E => + if (y + z < 0)%R then ((z <= 0) || (y <= 0))%R else + if (y + z > 0)%R then ((y >= 0)%R && (z >= 0))%R else + ((y == 0) && (z == 0))%R + | +oo , +oo , z%:E => (0 <= z)%R + | +oo , y%:E , +oo => (0 <= y)%R + | _ , _ , _ => true + end. + +Notation "x '`^?' ( y +? z )" := (poweRD_def x y z) : ereal_scope. + +Lemma poweRD x y z : x `^? ( y +? z ) = (x `^ (y + z) == x `^ y * x `^ z). +Proof. +case: x=> [r||]; case: y=> [s||]; case: z=> [t||]=>//=; last first. +all: rewrite -?EFinD ?poweR_EFin -?EFinM ?eqe ?mul1r ?eq_refl//=. +all: rewrite ?addeNy ?addNye//=. +- by rewrite /poweR/= ltNyr mule0 eq_refl. +- by rewrite /poweR/= ltNyr ltry mul0e eq_refl. +- by rewrite /poweR/= ltNyr mul0e eq_refl. +- by rewrite /poweR/= ltNyr ltry mule0 eq_refl. +- by rewrite /poweR/= ltry mulyy. +- rewrite /poweR !lte_fin; case: (ltgtP 0 t)%R=> t0//=. + + by rewrite ltry mulyy. + + by rewrite ltry mule0. + + by rewrite ltry mule1. +- by rewrite /poweR/= ltNyr; repeat case: ifPn; rewrite mule0 eq_refl. +- rewrite /poweR addey// ltry !lte_fin. + by repeat case: ifPn; case: (ltgtP s 0)%R=>//; rewrite ?mul0e ?mul1e. +- have:= (@addr_ss_eq0 _ s t). +case:(ltgtP (s + t) 0)%R; case:(ltgtP s 0)%R; case:(ltgtP t 0)%R; last first. + 1-27: move=> //= t0 s0 st0. + 1-27: rewrite ?t0 ?s0 ?st0 ?addr0 ?add0r ?poweRe0 ?mul1e ?eq_refl//. + 1-27: try by move=> C; exfalso; rewrite -falseE -C. + + rewrite /poweR !lte_fin; move: t0 s0 st0. + by case: (ltgtP s 0)%R; case: (ltgtP t 0)%R=>//; rewrite mule0 gt_eqF. + + rewrite /poweR !lte_fin; move: t0 s0 st0. + by case: (ltgtP s 0)%R; case: (ltgtP t 0)%R=>//; rewrite mul0e gt_eqF. + + by move: s0 t0 st0=> ->; rewrite add0r; case: (ltgtP t 0)%R. + + by rewrite /poweR !lte_fin s0 mule1. + + by rewrite /poweR !lte_fin st0 s0 t0 mulyy. + + rewrite /poweR !lte_fin st0 s0 t0; move: t0 st0; case: (ltgtP t 0)%R=>//. + by rewrite mule0. + + by move: t0 s0 st0 ->; rewrite addr0; case: (ltgtP s 0)%R. + + rewrite /poweR !lte_fin st0 t0 s0; move: s0 st0; case: (ltgtP s 0)%R=>//. + by rewrite mul0e. + + rewrite /poweR !lte_fin st0 t0 s0. + by move: s0 t0 st0; case: (ltgtP s 0)%R; case: (ltgtP t 0)%R. + + by move: t0 s0 st0=> ->; rewrite addr0; case: (ltgtP s 0)%R. + + rewrite /poweR !lte_fin st0 t0 s0. + by move: st0; case:(ltgtP (s + t) 0)%R. + + rewrite /poweR !lte_fin st0 t0 s0. + move: s0 t0 st0; case:(ltgtP (s + t) 0)%R; case: (ltgtP t 0)%R=>//. + by rewrite mule0 eq_refl. + + move: t0 s0 st0=> ->; rewrite addr0; case: (ltgtP s 0)%R=>//. + by rewrite mule1 eq_refl. + + rewrite /poweR !lte_fin t0 s0 st0. + move: s0 t0 st0; case:(ltgtP (s + t) 0)%R; case: (ltgtP s 0)%R=>//. + by rewrite mul0e eq_refl. + + rewrite /poweR !lte_fin t0 s0 st0. + move: s0 t0 st0; case:(ltgtP (s + t) 0)%R; case: (ltgtP s 0)%R=>//. + by rewrite mul0e eq_refl. +- case: (ltgtP 0 r)%R=> r0; last first. + + by rewrite -r0 poweR0e ?mule0 ?eq_refl. + + by rewrite lt0_poweR1 ?mul1e ?eq_refl. + + rewrite /poweR r0; repeat case: ifPn. + - by rewrite mule0 eq_refl. + - by rewrite mule1 eq_refl. + - by rewrite mulyy. +- case: (ltgtP 0 r)%R=>//= r0; last first. + + by rewrite -r0 poweR0e// mul0e eq_refl. + + by rewrite !lt0_poweR1// mule1 eq_refl. + + case: (ltgtP 1 r)%R=>//= r1; last first. + - by rewrite -r1 poweR1 mule1 eq_refl. + - rewrite /poweR r0; move: r1 r0. + case: (ltgtP r 0)%R; case: (ltgtP r 1)%R=>//. + by rewrite mule0. + - by rewrite /poweR r1 mul0e eq_refl. +- rewrite /poweR; repeat case: ifPn. + + by rewrite mul0e eq_refl. + + by move=> /eqP ->; rewrite powR1 mul1e eq_refl. + + by move=> r0; rewrite gt0_mulye ?lte_fin ?powR_gt0// lt_eqF. + + by rewrite mul0e eq_refl. +- by case: (ltgtP r 0)%R=>// r0; rewrite lt0_powR1 ?mul1e ?eq_refl. +- case: (ltgtP 0 r)%R=>//= r0; last first. + + by rewrite -r0 poweR0e// mule0 eq_refl. + + by rewrite !lt0_poweR1// mule1 eq_refl. + + case: (ltgtP 1 r)%R=>//= r1; last first. + - by rewrite -r1 poweR1 mule1 eq_refl. + - rewrite /poweR r0; move: r1 r0. + case: (ltgtP r 0)%R; case: (ltgtP r 1)%R=>//. + by rewrite mul0e. + - by rewrite /poweR r0 r1 mule0 eq_refl. +- rewrite addey// /poweR; repeat case: ifPn. + + by rewrite mulyy. + + by move=> /eqP ->; rewrite mul1e eq_refl. + + by rewrite mul0e eq_refl. + + by rewrite mul1e eq_refl. +- rewrite addye// /poweR; repeat case: ifPn. + + move=> r1; rewrite gt0_mulye ?lte_fin ?powR_gt0// lt_eqF//. + exact /(lt_trans ltr01). + + by move=> /eqP ->; rewrite powR1 mule1 eq_refl. + + by rewrite mul0e eq_refl. + + case: (ltgtP 0 r)%R=>// r0. + by rewrite lt0_powR1 ?mule1 ?eq_refl. +- rewrite /poweR; repeat case: ifPn. + + by rewrite mule0 eq_refl. + + by move=> /eqP ->; rewrite powR1 mule1 eq_refl. + + by move=> r0; rewrite gt0_muley// lte_fin powR_gt0// lt_eqF. + + by move=> /eqP ->; rewrite mule0 eq_refl. + + by case: (ltgtP r 0)%R=>// r0; rewrite lt0_powR1// mule1 eq_refl. +- rewrite addey// /poweR; repeat case: ifPn. + + move=> r1; rewrite gt0_muley// lte_fin powR_gt0// lt_eqF//. + exact /(lt_trans ltr01). + + by move=> /eqP ->; rewrite powR1 mule1 eq_refl. + + by rewrite mule0 eq_refl. + + by case: (ltgtP r 0)%R=>// r0; rewrite lt0_powR1// mule1 eq_refl. +- case: (eqVneq (s + t) 0)%R; case: (eqVneq r 0)%R=>//= r0 st0. + + rewrite r0 st0; case: (eqVneq s 0)%R; case: (eqVneq t 0)%R=>/= t0 s0. + - by rewrite t0 s0 powRr0 mul1r eq_refl. + - by rewrite s0 powRr0 powR0// mulr0 gt_eqF. + - by rewrite t0 powRr0 powR0// mul0r gt_eqF. + - by rewrite powRr0 powR0// mul0r gt_eqF. + + by rewrite powRD ?st0 ?eq_refl. + 1,2: rewrite powRD ?eq_refl//. + 1,2: by move: st0; case: (eqVneq (s + t) 0)%R. +Qed. +(* Lemma add_neq0_poweRD_def x r s : (r + s != 0)%R -> x `^?(r +? s). Proof. by rewrite poweRD_defE => /negPf->. Qed. @@ -1720,26 +1914,16 @@ Qed. Lemma nneg_neq0_poweRB_def x r s : x != 0 -> (r >= 0)%R -> (s <= 0)%R -> x `^?(r +? - s). Proof. by move=> *; rewrite nneg_neq0_poweRD_def// oppr_ge0. Qed. +*) -Lemma poweRD x r s : x `^?(r +? s) -> x `^ (r + s) = x `^ r * x `^ s. -Proof. -rewrite /poweRD_def. -have [->|r0]/= := eqVneq r 0%R; first by rewrite add0r poweRe0 mul1e. -have [->|s0]/= := eqVneq s 0%R; first by rewrite addr0 poweRe0 mule1. -case: x => // [t|/=|/=]; rewrite ?(negPf r0, negPf s0, implybF); last 2 first. -- by move=> /negPf->; rewrite mulyy. -- by move=> /negPf->; rewrite mule0. -rewrite !poweR_EFin eqe => /implyP/(_ _)/andP cnd. -by rewrite powRD//; apply/implyP => /cnd[]. -Qed. - -Lemma poweRB x r s : x `^?(r +? - s) -> x `^ (r - s) = x `^ r * x `^ (- s). -Proof. by move=> rs; rewrite poweRD. Qed. +Lemma poweRB x y z : x `^?(y +? - z) -> x `^ (y - z) = x `^ y * x `^ (- z). +Proof. by rewrite poweRD=> /eqP. Qed. -Lemma poweR12_sqrt x : 0 <= x -> x `^ 2^-1 = sqrte x. +(*Have not bee able to work with 2^-1 instead of (2^-1)%:E*) +Lemma poweR12_sqrt x : 0 <= x -> x `^ (2^-1)%:E = sqrte x. Proof. -move: x => [x|_|//]; last by rewrite poweRyr. -by rewrite lee_fin => x0 /=; rewrite powR12_sqrt. +move: x => [x|_|//]; last by rewrite /poweR //= lte_fin (_ : 0 < 2^-1)%R. +by rewrite lee_fin => x0 /=; rewrite poweR_EFin powR12_sqrt. Qed. End poweR. @@ -1754,14 +1938,15 @@ Definition riemannR a : R ^nat := fun n => (n.+1%:R `^ a)^-1. Arguments riemannR a n /. Lemma riemannR_gt0 a i : 0 <= a -> 0 < riemannR a i. -Proof. by move=> ?; rewrite /riemannR invr_gt0 powR_gt0. Qed. +Proof. +by move=> ?; rewrite /riemannR invr_gt0 powR_gt0 ?lt_eqF//. Qed. Lemma dvg_riemannR a : 0 <= a <= 1 -> ~ cvgn (series (riemannR a)). Proof. move=> /andP[a0 a1]. have : forall n, harmonic n <= riemannR a n. move=> [/=|n]; first by rewrite powR1 invr1. - rewrite -[leRHS]div1r ler_pdivlMr ?powR_gt0// mulrC ler_pdivrMr//. + rewrite -[leRHS]div1r ler_pdivlMr ?powR_gt0 ?lt_eqF// mulrC ler_pdivrMr//. by rewrite mul1r -[leRHS]powRr1// ler_powR// ler1n. move/(series_le_cvg harmonic_ge0 (fun i => ltW (riemannR_gt0 i a0))). by move/contra_not; apply; exact: dvg_harmonic. From 5c9abce7be7fc67e693b17044199cbfc684ee6cf Mon Sep 17 00:00:00 2001 From: jmmarulang <78051861+jmmarulang@users.noreply.github.com> Date: Sun, 21 Dec 2025 22:07:43 +0000 Subject: [PATCH 4/5] test --- theories/exp.v | 1 + 1 file changed, 1 insertion(+) diff --git a/theories/exp.v b/theories/exp.v index e941608621..39cbdc5d8f 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -1952,4 +1952,5 @@ move/(series_le_cvg harmonic_ge0 (fun i => ltW (riemannR_gt0 i a0))). by move/contra_not; apply; exact: dvg_harmonic. Qed. + End riemannR_series. \ No newline at end of file From cc4a1121f3e33ec2d1afe2328144a763f783c7ae Mon Sep 17 00:00:00 2001 From: jmmarulang <78051861+jmmarulang@users.noreply.github.com> Date: Sat, 3 Jan 2026 01:52:39 +0000 Subject: [PATCH 5/5] corrected hoelder --- reals/constructive_ereal.v | 8 + theories/exp.v | 308 +++++++++--------- theories/hoelder.v | 158 +++++---- .../measurable_fun_approximation.v | 30 +- 4 files changed, 269 insertions(+), 235 deletions(-) diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index d9cd247e12..755e1e65b8 100644 --- a/reals/constructive_ereal.v +++ b/reals/constructive_ereal.v @@ -414,6 +414,14 @@ Lemma le0y : (0 : \bar R) <= +oo. Proof. exact: real0. Qed. Lemma leNy0 : -oo <= (0 : \bar R). Proof. exact: real0. Qed. +Lemma leyr r : +oo <= r%:E = false. Proof. by []. Qed. + +Lemma ltyr r : +oo < r%:E = false. Proof. by []. Qed. + +Lemma ltrNy r : r%:E < -oo = false. Proof. by []. Qed. + +Lemma lerNy r : r%:E <= -oo = false. Proof. by []. Qed. + Lemma cmp0y : ((0 : \bar R) >=< +oo%E)%O. Proof. by rewrite /Order.comparable le0y. Qed. diff --git a/theories/exp.v b/theories/exp.v index 031477edf1..74d9a623dd 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -464,13 +464,13 @@ Qed. Lemma expRB x y : expR (x - y) = expR x / expR y. Proof. by rewrite expRD expRN. Qed. -Lemma ltr_expR : {mono (@expR R) : x y / x < y}. +Lemma ltr_expR : {mono ( @expR R) : x y / x < y}. Proof. move=> x y. by rewrite -[in LHS](subrK x y) expRD ltr_pMl ?expR_gt0 // expR_gt1 subr_gt0. Qed. -Lemma ler_expR : {mono (@expR R) : x y / x <= y}. +Lemma ler_expR : {mono ( @expR R) : x y / x <= y}. Proof. move=> x y. case: (ltrgtP x y) => [xLy|yLx|<-]; last by rewrite lexx. @@ -1042,8 +1042,8 @@ rewrite le_eqVlt => /predU1P[<- b0 p0 q0 _|a0]. rewrite le_eqVlt => /predU1P[<-|b0] p0 q0 pq. by rewrite mulr0 powR0 ?gt_eqF// mul0r addr0 divr_ge0 ?powR_ge0 ?ltW. have iq1 : q^-1 <= 1 by rewrite -pq ler_wpDl// invr_ge0 ltW. -have ap0 : (0 < a `^ p)%R by rewrite powR_gt0. -have bq0 : (0 < b `^ q)%R by rewrite powR_gt0. +have ap0 : (0 < a `^ p)%R by rewrite powR_gt0 ?lt_eqF. +have bq0 : (0 < b `^ q)%R by rewrite powR_gt0 ?lt_eqF. have pq' : (p^-1 = 1 - q^-1)%R by rewrite -pq addrK. have qp' : (q^-1 = 1 - p^-1)%R by rewrite -pq -addrA subrKC. have := @concave_ln _ (Itv01 (eqbRL (invr_ge0 _) (ltW q0)) iq1) _ _ bq0 ap0. @@ -1295,16 +1295,6 @@ Local Open Scope ereal_scope. Context {R : realType}. Implicit Types (s r : R) (x y z : \bar R). -(*Definition poweR x y := if x == 0 then (y == 0)%:R%:E else expeR (y * lne x).*) - -(*Definition poweR x r := - match x with - | x'%:E => (x' `^ r)%:E - | +oo => if r == 0%R then 1%E else +oo - | -oo => if r == 0%R then 1%E else 0%E - end. -*) - Definition poweR x y := match (x, y) with | (r%:E, s%:E) => (r `^ s)%:E @@ -1315,7 +1305,9 @@ Definition poweR x y := if (r > 1)%R then 0 else if (r == 1)%R then 1 else if (r > 0)%R then +oo else if (r == 0)%R then 0 else 1 - | (+oo, y) => if y > 0 then +oo else if y < 0 then 0 else 1 + | (+oo, s%:E) => if (s > 0)%R then +oo else if (s < 0)%R then 0 else 1 + | (+oo, +oo) => +oo + | (+oo, -oo) => 0 | (-oo, y) => 1 end. @@ -1353,15 +1345,12 @@ case x, y=> //=. 1,2: by rewrite lte_fin; case: (ltgtP 0%R s). - rewrite /poweR /poweR' eqe; repeat case : ifPn; case : (ltgtP 0%R s)=>//. + by move=> ?; rewrite /lne gt0_muley. - + by rewrite lte_fin; case: (ltgtP s 0%R). - + by move=> <-; rewrite ltxx. - 1-3: by case: (ltgtP +oo 0). - + by rewrite lte_fin; case: (ltgtP s 0%R). + + by rewrite ltry. + by move=> s0; rewrite /lne lt0_muley. - + by move=> <-; rewrite ltxx. - + by rewrite lte_fin; case: (ltgtP s 0%R). - 1,2: by rewrite lt0y. - 1-3: by case: (ltgtP s%:E 0)=> // ->; rewrite mul0e expeR0. + + by rewrite ltry. + + by move=> <-; rewrite mul0e expeR0. + + by rewrite /poweR /poweR' ltry. + + by rewrite /poweR /poweR'/= ltry. Qed. Local Notation "x `^ y" := (poweR x y). @@ -1370,21 +1359,24 @@ Lemma poweR_EFin r s : r%:E `^ s%:E = (r `^ s)%:E. Proof. by []. Qed. Lemma gt0_poweRye y : 0 < y -> +oo `^ y = +oo. -Proof. by move=> y0; rewrite /poweR y0. Qed. +Proof. +by case: y => //s; move=> /[!@lte_fin] s0; rewrite /poweR s0. +Qed. Lemma lt0_poweRye y : y < 0 -> +oo `^ y = 0. Proof. -rewrite /poweR; repeat case: (ifPn); case: (ltgtP y 0)=> //. +case: y=> // s/[!@lte_fin]. +rewrite /poweR; repeat case: (ifPn); case: (ltgtP s 0%R)=> //. Qed. Lemma poweRe0 x : x `^ 0 = 1. Proof. -by case: x=> [r||]; rewrite /poweR ?ltxx //= powRr0. +by case: x=> //[r|]; rewrite /poweR/= ?ltxx ?powRr0. Qed. Lemma poweRe1 x : 0 <= x -> x `^ 1 = x. Proof. -by case: x=> [r||] x0; rewrite /poweR ?powRr1 // lte01. +by case: x=> [r||] x0; rewrite /poweR ?powRr1// ltr01. Qed. Lemma poweRN x y : @@ -1395,6 +1387,44 @@ case: x => // r x0; case : y => //s _/=; case : (ltgtP r 0%R) => r0; try by rewrite ?r0 poweR_EFin// ?ltW// powRN//. Qed. +Lemma poweRNye y : -oo `^ y = 1. +Proof. by []. Qed. + +(*TODO: move*) +(* + Lemma leyr s : (+oo <= s%:E = false). +Proof. by case: (ltgtP +oo s%:E). Qed. + +Lemma ltyr s : (+oo < s%:E = false). +Proof. by case: (ltgtP +oo s%:E). Qed. + +Lemma ltrNy s : (s%:E < -oo = false). +Proof. by case: (ltgtP -oo s%:E). Qed. + + Lemma lerNy s : (s%:E <= -oo = false). +Proof. by case: (ltgtP -oo s%:E). Qed. +*) + +Lemma poweRE x y : + poweR x y = + if (y == 0) || (x < 0) || (x == 1) then 1 else + if x == +oo then (if y > 0 then +oo else 0) else + if y == -oo then (if x > 1 then 0 else if x > 0 then +oo else 0) else + if y == +oo then (if x > 1 then +oo else 0) else (fine x `^ fine y)%:E. +Proof. +move: x y=> [r||] [s||] //=; last first. +1,2: by rewrite ltNyr. +- by rewrite /poweR ltNyr orbT. +- by rewrite /poweR ltry. +- by rewrite /poweR eqe lte_fin; case: (ltgtP s 0)%R. +1-2:rewrite /poweR eqe !lte_fin; case: (ltgtP r 0)%R; case: (ltgtP r 1)%R=>//=. +1-2:by move=> r1 r0; exfalso; rewrite -falseE -(@ltr10 R); apply /(lt_trans r1). +- rewrite /poweR !eqe !lte_fin; case: ifPn=>// /orP [/orP [/eqP ->|r0]|/eqP ->]. + + by rewrite powRr0. + + by rewrite lt0_powR1. + + by rewrite powR1. +Qed. + Lemma lt0_poweR1 x y : x < 0 -> x `^ y = 1. Proof. rewrite poweR_is_poweR' /poweR'; repeat case: ifPn. @@ -1409,7 +1439,13 @@ case: x=>// r; case: y=>//; rewrite /poweR; repeat case: ifPn=>//. 1,2: by rewrite lte_fin; case: (ltgtP r 1%R). Qed. -Lemma poweR_lty x y : (if x < 1 then 0 <= y else (x < +oo) && (y < +oo)) -> x `^ y < +oo. +Lemma eqy_poweR x y : 0 < y -> x = +oo -> x `^ y = +oo. +Proof. +by move: x y=> []//= [s||]//= s0 _;rewrite /poweR -lte_fin s0. +Qed. + +Lemma poweR_lty x y : (if x < 1 then 0 <= y else (x < +oo) && (y < +oo)) -> + x `^ y < +oo. Proof. case: x=>// [r|]; case: y=>//[s||]; rewrite /poweR; repeat case: ifPn=> //. all: try by rewrite !ltry. @@ -1417,10 +1453,13 @@ all: try by rewrite !ltry. - by rewrite lte_fin; case: (ltgtP r 1%R). Qed. +Lemma poweR_ltr x s : x < +oo -> x `^ s%:E < +oo. +Proof. by case: x=>//=[r|]; rewrite /poweR ?ltry. Qed. + Lemma lty_poweRy x y : 0 < y -> x `^ y < +oo -> x < +oo. Proof. -move : x => [r | |]//; first by rewrite ltry. -by rewrite /poweR; repeat case: ifPn. +move: x y=> [r||] [s||]//=; rewrite ?ltry//. +by rewrite /poweR lte_fin=> ->. Qed. Lemma poweR0e y : y != 0 -> 0 `^ y = 0. @@ -1440,50 +1479,22 @@ Proof. by apply /funext=> y; case: y=> [r||]; rewrite /poweR ?powR1 ?ltxx ?eq_refl. Qed. -Lemma fine_poweR x y : 0 < x -> y \is a fin_num -> +Lemma fine_poweR x y : 0 <= x -> y \is a fin_num -> fine (x `^ y) = ((fine x) `^ (fine y))%R. Proof. case: x=>// [r|]; case: y=>//= s _ _; rewrite /poweR; repeat case: ifPn=>//=. - by move=> s0; rewrite ?powR0 ?gt_eqF. - by move=> s0; rewrite ?powR0 ?lt_eqF. -- by case: (ltgtP s%:E 0)=> // /eqP /[!eqe] /eqP -> /[!powRr0]. +- by case: (ltgtP s 0)%R=> // -> /[!powRr0]. Qed. Lemma poweR_ge0 x y : 0 <= x `^ y. Proof. case: x=> [r||]; case: y=> [s||]; rewrite /poweR; repeat case: ifPn=>//. - by rewrite lee_fin powR_ge0. -all: by rewrite lee01. +all: by rewrite ?lee01. Qed. -(*TODO: move*) -Lemma leyr s : (+oo <= s%:E = false). -Proof. by case: (ltgtP +oo s%:E). Qed. - -Lemma ltyr s : (+oo < s%:E = false). -Proof. by case: (ltgtP +oo s%:E). Qed. - -Lemma ltrNy s : (s%:E < -oo = false). -Proof. by case: (ltgtP -oo s%:E). Qed. - - Lemma lerNy s : (s%:E <= -oo = false). -Proof. by case: (ltgtP -oo s%:E). Qed. - -(* - match (x, y) with - | (r%:E, s%:E) => (r `^ s)%:E - | (r%:E, +oo) => - if (r > 1)%R then +oo - else if (r == 1)%R then 1 else if (r >= 0)%R then 0 else 1 - | (r%:E, -oo) => - if (r > 1)%R then 0 - else if (r == 1)%R then 1 else if (r > 0)%R then +oo else - if (r == 0)%R then 0 else 1 - | (+oo, y) => if y > 0 then +oo else if y < 0 then 0 else 1 - | (-oo, y) => 1 - end. -*) - Lemma poweR_gt0 x y : (if x == 0 then y == 0 else if +oo <= x then 0 <= y else if y <= -oo then x <= 1 else @@ -1493,10 +1504,10 @@ repeat case: ifPn. - move=> /eqP ->; case: (ltgtP y 0)=> [y0|y0|->]. 1,2: by rewrite poweR0e ?ltxx ?(lt_eqF y0) ?(gt_eqF y0). by rewrite /poweR //= /powR eq_refl //= lte01. -- case: x=>// _ _; rewrite /poweR; repeat case: ifPn. +- case: x=>// _ _; rewrite /poweR; case: y=> [s||]//=; repeat case: ifPn. + by move=> y0; rewrite ltW ?ltry. - + by case: (ltgtP y 0). - + by rewrite lte01; case: (ltgtP y 0). + + by rewrite lee_fin; case: (ltgtP s 0)%R. + + by rewrite lte01 lee_fin; case: (ltgtP s 0)%R. - case: y; case: (ltgtP x +oo); case: x=>// [r|]; last first. by rewrite !leNye /poweR lte01. rewrite /poweR; repeat case: ifPn. @@ -1514,24 +1525,20 @@ repeat case: ifPn. - by rewrite lexx leNye /poweR lte01. Qed. -(*Lemma poweR_gt0 x r : 0 < x -> 0 < x `^ r.*) - Lemma gt0_poweR x y : 0 < y -> 0 <= x -> 0 < x `^ y -> 0 < x. Proof. case: x =>// r; rewrite lee_fin. by case: (ltgtP r 0%R)=> //; move=> -> y0; rewrite poweR0e ?gt_eqF. Qed. -(*Lemma gt0_poweR x r : (0 < r)%R -> 0 <= x -> 0 < x `^ r -> 0 < x.*) - Lemma poweRey_gt1 x : 1 < x -> x `^ +oo = +oo. Proof. -by case: x=>// [r|]; rewrite /poweR ?lte_fin ?ltry//; move=> ->. +by case: x=>// [r]; rewrite /poweR ?lte_fin ?ltry//; move=> ->. Qed. Lemma poweReNy_gt1 x : 1 < x -> x `^ -oo = 0. Proof. -by case: x=>// [r|]; rewrite /poweR ?lte_fin ?ltrNy ?ltNyr//; move=> ->. +by case: x=>// [r]; rewrite /poweR ?lte_fin ?ltrNy ?ltNyr//; move=> ->. Qed. Lemma poweRey_lt1 x : 0 <= x < 1 -> x `^ +oo = 0. @@ -1558,8 +1565,8 @@ repeat case: ifPn. + by rewrite poweR0e ?(lt_eqF y0) ?eq_refl. + by rewrite poweR0e ?(gt_eqF y0) ?eq_refl. + by rewrite /poweR /= /powR ?eq_refl /= gt_eqF. -- move=> /eqP ->; rewrite /poweR; repeat case: ifPn; case: (ltgtP y 0)=>//. - by rewrite eq_refl. +- move=> /eqP ->; rewrite /poweR; case: y=> [s||]//=; rewrite ?eq_refl ?ltNyr//. + rewrite lte_fin; repeat case: ifPn; case: (ltgtP s 0)%R; rewrite ?eq_refl//=. by rewrite !gt_eqF. - move=> /eqP ->; case: x=>//[r|]; last by rewrite ltrNy /= /poweR gt_eqF. rewrite /poweR !lte_fin ?eqe. @@ -1573,10 +1580,7 @@ repeat case: ifPn. by move=> /[!@eqe] /[!@powR_eq0]; case: (ltgtP r 0%R). Qed. -(*No longer true*) -(*Lemma poweR_eq0_eq0 x y : 0 <= x -> x `^ y = 0 -> x = 0.*) - -Lemma gt0_ler_poweR z : 0 <= z -> +Lemma gt0_lee_poweR z : 0 <= z -> {in `[0, +oo] &, {homo poweR ^~ z : x y / x <= y >-> x <= y}}. Proof. move=> z0 + y; case=> //= [r /[!in_itv]/= /andP[r0 _] /andP[]|]; last first. @@ -1593,12 +1597,21 @@ move: z0; case : z=> //[t t0| _]; case: y=> //[s s0 _ rs | _ _]; last first. - by rewrite !poweR_EFin// lee_fin ?ge0_ler_powR. Qed. +Lemma gt0_lte_poweR t : (0 < t)%R -> + {in `[0, +oo] &, {homo poweR ^~ t%:E : x y / x < y >-> x < y}}. +Proof. +move=> t0 x y x0 y0 xy. +rewrite lt_def; apply /andP; split; last by apply gt0_lee_poweR; rewrite ?ltW. +move: x y x0 y0 xy => [r||] [s||]//= x0 y0 xy; last by rewrite !/poweR//= t0. +rewrite !poweR_EFin eqe gt_eqF ?gt0_ltr_powR ?nnegrE//=. + by move: x0=> /andP []. +by move: y0=> /andP []. +Qed. + Lemma fin_num_poweR x y : x \is a fin_num -> y \is a fin_num -> x `^ y \is a fin_num. Proof. by case: x; case: y=>// ? ? ?; rewrite poweR_EFin//. Qed. -(*Lemma fin_num_poweR x r : x \is a fin_num -> x `^ r \is a fin_num.*) - (*TODO:check if this can be generalized*) Lemma poweRM x y r : (r != 0)%R -> 0 <= x -> 0 <= y -> (x * y) `^ r%:E = x `^ r%:E * y `^ r%:E. @@ -1619,22 +1632,6 @@ case: x y => [x||] [y||]// _ x0 y0. by rewrite gt0_poweRye ?mulyy. Qed. -(*Lemma poweRM x y r : 0 <= x -> 0 <= y -> (x * y) `^ r = x `^ r * y `^ r.*) - -(* -Lemma lt0_lt0_poweR x y : x < 0%R -> y < 0%R -> x `^ y = +oo. -Proof. -rewrite poweRE; repeat case: ifPn=>//; move=>/orP[]/eqP ->; rewrite ?ltxx//. -by rewrite lte_fin ltr10. -Qed. - -Lemma lt0_gt0_poweR x y : x < 0%R -> 0%R < y -> x `^ y = 0. -move=> x0; rewrite poweRE x0; repeat case : ifPn=>//; case: (ltgtP y 0)=> //. -rewrite (_ : x == 1 = false)//=; apply/eqP. -by move: x0=>/[swap] ->; rewrite lte_fin ltr10. -Qed. -*) - Definition poweRrM_def x y z := match (x, y, z) with | (+oo , y , z) => (0 <= z) || (0 <= y) @@ -1647,7 +1644,7 @@ Definition poweRrM_def x y z := Notation "x '`^?' ( y *? z )" := (poweRrM_def x y z) : ereal_scope. -Lemma poweRrM (x y z : \bar R) : x `^? ( y *? z ) = +Lemma poweRrM_eq (x y z : \bar R) : x `^? ( y *? z ) = (x `^ (y * z) == (x `^ y) `^ z). Proof. have neq_01 : ((0%R : R) == (1%R : R) = false) by apply /lt_eqF. @@ -1665,28 +1662,28 @@ case: (ltgtP x 0)=> x0; rewrite ?x0. 1-27: rewrite ?/poweR ?lerNy ?orbF ?NyNy ?yNy ?Nyy ?yy ?ltry ?ltNyr //=. 1-18: rewrite ?neq_01 ?ltxx ?ltr10 ?lexx ?eq_refl ?leey ?orbT//=. 14: by rewrite powRrM eq_refl. - 1,2: case: (ltgtP t%:E 0)=> [t0|t0|/eqP /[!eqe] /eqP ->]. + 1,2: rewrite ?lee_fin; case: (ltgtP t 0)%R=> [t0|t0|->]. - by rewrite lt0_mulNye ?ltry. - by rewrite gt0_mulNye ?ltrNy ?ltNyr ?powR0 ?eq_refl ?gt_eqF. - 1,4: by rewrite mule0 ltxx ?powRr0 ?eq_refl. - - by rewrite lt0_mulye ?ltrNy ?ltNyr ?eq_refl. + 1,4: by rewrite mule0/= ltxx ?powRr0 ?eq_refl. + - by rewrite lt0_mulye//= ?ltrNy ?ltNyr ?eq_refl. - by rewrite gt0_mulye ?ltry. - 1,2: case: (ltgtP s%:E 0)=> [s0|s0|/eqP /[!eqe] /eqP ->]. + 1,2: rewrite ?lee_fin; case: (ltgtP s 0)%R=> [s0|s0|->]. - by rewrite lt0_muleNy ?ltry/= ?ltr10 ?neq_01 ?ltxx ?eq_refl. - by rewrite gt0_muleNy ?ltrNy ?ltNyr ?eq_refl. - 1,4: by rewrite mul0e ?ltxx ?eq_refl. + 1,4: by rewrite mul0e/= ?ltxx ?eq_refl. - by rewrite lt0_muley ?ltrNy ?ltNyr/= ?ltr10 ?neq_01 ?lexx ?eq_refl. - by rewrite gt0_muley ?ltry. - + case: (ltgtP s%:E 0); case: (ltgtP t%:E 0)=>//= t0 s0. - - by have := mule_lt0_lt0 s0 t0; case: (ltgtP (s%:E * t%:E) 0). - - have := mule_lt0_gt0 s0 t0; case: (ltgtP (s%:E * t%:E) 0)=>//. + + rewrite !lee_fin; case: (ltgtP s 0)%R; case: (ltgtP t 0)%R=>//=/[dup]+t0 s0. + - by rewrite -(@nmulr_rgt0 _ s t s0); case: (ltgtP (s * t) 0)%R. + - rewrite -(@nmulr_rlt0 _ s t s0); case: (ltgtP (s * t) 0)%R=>//. by rewrite powR0 ?eq_refl// gt_eqF. - - by move: t0=> /eqP /[!eqe] /eqP ->; rewrite mule0 ltxx powRr0 eq_refl. - - have := mule_gt0_lt0 s0 t0; case: (ltgtP (s%:E * t%:E) 0)=>//. + - by move=> ->; rewrite mulr0 ltxx powRr0 eq_refl. + - rewrite -(@pmulr_rlt0 _ s t s0); case: (ltgtP (s * t) 0)%R=>//. by rewrite eq_refl. - - by have := mule_gt0 s0 t0; case: (ltgtP (s%:E * t%:E) 0). - - by move: t0=> /eqP /[!eqe] /eqP ->; rewrite mule0 ltxx eq_refl. - 1-3: by move: s0=> /eqP /[!eqe] /eqP ->; rewrite mul0e ltxx powR1 eq_refl. + - by rewrite -(@pmulr_rgt0 _ s t s0); case: (ltgtP (s * t) 0)%R. + - by move=> ->; rewrite mulr0 ltxx eq_refl. + 1-3: by rewrite s0 mul0r ltxx powR1 eq_refl. + rewrite lte_fin lee_fin; case: (ltgtP r 1)%R; case: (ltgtP r 0)%R=>//=. - by rewrite eq_refl. - by rewrite ltr10 neq_01 ltxx eq_refl. @@ -1750,9 +1747,13 @@ case: (ltgtP x 0)=> x0; rewrite ?x0. all: by rewrite ?lexx ?lee01 ?orbT ?implybT. Qed. +Lemma poweRrM (x y z : \bar R) : x `^? ( y *? z ) -> + (x `^ (y * z) = (x `^ y) `^ z). +Proof. by rewrite poweRrM_eq=> /eqP. Qed. + Lemma poweRAC x y z : poweRrM_def x y z -> poweRrM_def x z y -> (x `^ y) `^ z = (x `^ z) `^ y. -Proof. by rewrite !poweRrM muleC=> /eqP <- /eqP. Qed. +Proof. by rewrite !poweRrM_eq muleC=> /eqP <- /eqP. Qed. Definition poweRD_def x y z := match x, y, z with @@ -1771,54 +1772,65 @@ Definition poweRD_def x y z := Notation "x '`^?' ( y +? z )" := (poweRD_def x y z) : ereal_scope. -Lemma poweRD x y z : x `^? ( y +? z ) = (x `^ (y + z) == x `^ y * x `^ z). +(*x \is a fin_num*) +Lemma poweRD_defE x y z : + poweRD_def x y z = + if ((x \is a fin_num) && (y \is a fin_num) && (z \is a fin_num)) then + (y + z == 0) ==> ((x != 0) || ((y == 0) && (z == 0))) else + if ((x \is a fin_num) && (y == -oo) && (z == +oo)) || + ((x \is a fin_num) && (y == +oo) && (z == -oo)) then + (x <= 0) || (1 <= x) else + if ((x == +oo) && (y \is a fin_num) && (z \is a fin_num)) then + (if (y + z < 0) then ((z <= 0) || (y <= 0)) else + if (y + z > 0) then ((y >= 0) && (z >= 0)) else + ((y == 0) && (z == 0))) else + if ((x == +oo) && (y == +oo) && (z \is a fin_num)) then + (0 <= z) else + ((x == +oo) && (y \is a fin_num) && (z == +oo)) ==> (0 <= y). +Proof. by move: x y z=> [r||] [s||] [t||]. Qed. + +Lemma poweRD_eq x y z : x `^? ( y +? z ) = (x `^ (y + z) == x `^ y * x `^ z). Proof. case: x=> [r||]; case: y=> [s||]; case: z=> [t||]=>//=; last first. all: rewrite -?EFinD ?poweR_EFin -?EFinM ?eqe ?mul1r ?eq_refl//=. -all: rewrite ?addeNy ?addNye//=. -- by rewrite /poweR/= ltNyr mule0 eq_refl. -- by rewrite /poweR/= ltNyr ltry mul0e eq_refl. -- by rewrite /poweR/= ltNyr mul0e eq_refl. -- by rewrite /poweR/= ltNyr ltry mule0 eq_refl. -- by rewrite /poweR/= ltry mulyy. -- rewrite /poweR !lte_fin; case: (ltgtP 0 t)%R=> t0//=. - + by rewrite ltry mulyy. - + by rewrite ltry mule0. - + by rewrite ltry mule1. -- by rewrite /poweR/= ltNyr; repeat case: ifPn; rewrite mule0 eq_refl. -- rewrite /poweR addey// ltry !lte_fin. - by repeat case: ifPn; case: (ltgtP s 0)%R=>//; rewrite ?mul0e ?mul1e. -- have:= (@addr_ss_eq0 _ s t). +all: rewrite ?addeNy ?addNye ?mulr0 ?eq_refl//=. +1-3: by rewrite /poweR/= ?mul0e ?mule0 eq_refl. +- rewrite addye /poweR; case: (ltgtP 0 t)%R=> t0//=. + by rewrite mule0. + by rewrite mule1. +- by rewrite /poweR; case: (ltgtP s 0)%R=>//; rewrite ?mule0 ?eq_refl. +- by rewrite addey// /poweR; case: (ltgtP s 0)%R=>//; rewrite ?mul0e ?mul1e. +- have:= ( @addr_ss_eq0 _ s t). case:(ltgtP (s + t) 0)%R; case:(ltgtP s 0)%R; case:(ltgtP t 0)%R; last first. 1-27: move=> //= t0 s0 st0. 1-27: rewrite ?t0 ?s0 ?st0 ?addr0 ?add0r ?poweRe0 ?mul1e ?eq_refl//. 1-27: try by move=> C; exfalso; rewrite -falseE -C. - + rewrite /poweR !lte_fin; move: t0 s0 st0. + + rewrite /poweR; move: t0 s0 st0. by case: (ltgtP s 0)%R; case: (ltgtP t 0)%R=>//; rewrite mule0 gt_eqF. - + rewrite /poweR !lte_fin; move: t0 s0 st0. + + rewrite /poweR; move: t0 s0 st0. by case: (ltgtP s 0)%R; case: (ltgtP t 0)%R=>//; rewrite mul0e gt_eqF. + by move: s0 t0 st0=> ->; rewrite add0r; case: (ltgtP t 0)%R. - + by rewrite /poweR !lte_fin s0 mule1. - + by rewrite /poweR !lte_fin st0 s0 t0 mulyy. - + rewrite /poweR !lte_fin st0 s0 t0; move: t0 st0; case: (ltgtP t 0)%R=>//. + + by rewrite /poweR s0 mule1. + + by rewrite /poweR st0 s0 t0 mulyy. + + rewrite /poweR st0 s0 t0; move: t0 st0; case: (ltgtP t 0)%R=>//. by rewrite mule0. + by move: t0 s0 st0 ->; rewrite addr0; case: (ltgtP s 0)%R. - + rewrite /poweR !lte_fin st0 t0 s0; move: s0 st0; case: (ltgtP s 0)%R=>//. + + rewrite /poweR st0 t0 s0; move: s0 st0; case: (ltgtP s 0)%R=>//. by rewrite mul0e. - + rewrite /poweR !lte_fin st0 t0 s0. + + rewrite /poweR st0 t0 s0. by move: s0 t0 st0; case: (ltgtP s 0)%R; case: (ltgtP t 0)%R. + by move: t0 s0 st0=> ->; rewrite addr0; case: (ltgtP s 0)%R. - + rewrite /poweR !lte_fin st0 t0 s0. + + rewrite /poweR st0 t0 s0. by move: st0; case:(ltgtP (s + t) 0)%R. - + rewrite /poweR !lte_fin st0 t0 s0. + + rewrite /poweR st0 t0 s0. move: s0 t0 st0; case:(ltgtP (s + t) 0)%R; case: (ltgtP t 0)%R=>//. by rewrite mule0 eq_refl. + move: t0 s0 st0=> ->; rewrite addr0; case: (ltgtP s 0)%R=>//. by rewrite mule1 eq_refl. - + rewrite /poweR !lte_fin t0 s0 st0. + + rewrite /poweR t0 s0 st0. move: s0 t0 st0; case:(ltgtP (s + t) 0)%R; case: (ltgtP s 0)%R=>//. by rewrite mul0e eq_refl. - + rewrite /poweR !lte_fin t0 s0 st0. + + rewrite /poweR t0 s0 st0. move: s0 t0 st0; case:(ltgtP (s + t) 0)%R; case: (ltgtP s 0)%R=>//. by rewrite mul0e eq_refl. - case: (ltgtP 0 r)%R=> r0; last first. @@ -1887,33 +1899,16 @@ case:(ltgtP (s + t) 0)%R; case:(ltgtP s 0)%R; case:(ltgtP t 0)%R; last first. 1,2: by move: st0; case: (eqVneq (s + t) 0)%R. Qed. -(* -Lemma add_neq0_poweRD_def x r s : (r + s != 0)%R -> x `^?(r +? s). -Proof. by rewrite poweRD_defE => /negPf->. Qed. - -Lemma add_neq0_poweRB_def x r s : (r != s)%R -> x `^?(r +? - s). -Proof. by rewrite poweRB_defE => /negPf->. Qed. - -Lemma nneg_neq0_poweRD_def x r s : x != 0 -> (r >= 0)%R -> (s >= 0)%R -> - x `^?(r +? s). -Proof. -move=> xN0 rge0 sge0; rewrite /poweRD_def xN0/=. -by case: ltgtP rge0 => // [r_gt0|<-]; case: ltgtP sge0 => // [s_gt0|<-]//=; - rewrite ?addr0 ?add0r ?implybT// gt_eqF//= ?addr_gt0. -Qed. - -Lemma nneg_neq0_poweRB_def x r s : x != 0 -> (r >= 0)%R -> (s <= 0)%R -> - x `^?(r +? - s). -Proof. by move=> *; rewrite nneg_neq0_poweRD_def// oppr_ge0. Qed. -*) +Lemma poweRD x y z : x `^? ( y +? z ) -> (x `^ (y + z) = x `^ y * x `^ z). +Proof. by rewrite poweRD_eq=>/eqP. Qed. Lemma poweRB x y z : x `^?(y +? - z) -> x `^ (y - z) = x `^ y * x `^ (- z). -Proof. by rewrite poweRD=> /eqP. Qed. +Proof. by rewrite poweRD_eq=> /eqP. Qed. (*Have not bee able to work with 2^-1 instead of (2^-1)%:E*) Lemma poweR12_sqrt x : 0 <= x -> x `^ (2^-1)%:E = sqrte x. Proof. -move: x => [x|_|//]; last by rewrite /poweR //= lte_fin (_ : 0 < 2^-1)%R. +move: x => [x|_|//]; last by rewrite /poweR //= (_ : 0 < 2^-1)%R. by rewrite lee_fin => x0 /=; rewrite poweR_EFin powR12_sqrt. Qed. @@ -1943,5 +1938,4 @@ move/(series_le_cvg harmonic_ge0 (fun i => ltW (riemannR_gt0 i a0))). by move/contra_not; apply; exact: dvg_harmonic. Qed. - End riemannR_series. \ No newline at end of file diff --git a/theories/hoelder.v b/theories/hoelder.v index 1b24000c39..5a2fc3a7b7 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -62,7 +62,7 @@ Local Open Scope ereal_scope. HB.lock Definition Lnorm {d} {T : measurableType d} {R : realType} (mu : {measure set T -> \bar R}) (p : \bar R) (f : T -> \bar R) := match p with - | p%:E => (\int[mu]_x `|f x| `^ p) `^ p^-1 + | p%:E => (\int[mu]_x `|f x| `^ p%:E) `^ (p^-1)%:E (* (mu (f @^-1` (setT `\ 0%R))) when p = 0? *) | +oo%E => if mu [set: T] > 0 then ess_sup mu (abse \o f) else 0 | -oo%E => if mu [set: T] > 0 then ess_inf mu (abse \o f) else 0 @@ -86,8 +86,8 @@ Lemma Lnorm0 p : p != 0 -> 'N_p[cst 0] = 0. Proof. rewrite unlock /Lnorm; case: p => [r|_|_]. - rewrite eqe => r0. - under eq_integral => x _ do rewrite /= normr0 powR0//. - by rewrite integral0 poweR0r// invr_neq0. + under eq_integral => x _ do rewrite /= normr0 poweR0e//. + by rewrite integral0 poweR0e// invr_neq0. - case: ifPn => // mu0; apply: ess_sup_ae_cst => //. by apply/nearW => x/=; rewrite normr0. - case: ifPn => // mu0; apply: ess_inf_ae_cst => //. @@ -103,10 +103,12 @@ Qed. Lemma eq_Lnorm p f g : f =1 g -> 'N_p[f] = 'N_p[g]. Proof. by move=> fg; congr Lnorm; apply/eq_fun => ?; rewrite /= fg. Qed. -Lemma poweR_Lnorm f r : r != 0%R -> - 'N_r%:E[f] `^ r = \int[mu]_x (`| f x | `^ r). +Lemma poweR_Lnorm f r : (0 < r)%R -> + 'N_r%:E[f] `^ r%:E = \int[mu]_x (`| f x | `^ r%:E). Proof. -move=> r0; rewrite unlock -poweRrM mulVf// poweRe1//. +move=> r0; rewrite unlock -poweRrM; last first. + by case: (\int[mu]_x `|f x| `^ r%:E)=>//; rewrite /poweRrM_def lee_fin ltW. +rewrite -EFinM mulVf ?gt_eqF// poweRe1//. by apply: integral_ge0 => x _; exact: poweR_ge0. Qed. @@ -117,9 +119,9 @@ rewrite unlock /Lnorm NfE; case: p => /= [r|//|//]. by under eq_integral => x _ do rewrite abseN. Qed. -Lemma Lnorm_cst1 r : 'N_r%:E[cst 1] = mu [set: T] `^ (r^-1). +Lemma Lnorm_cst1 r : 'N_r%:E[cst 1] = mu [set: T] `^ (r^-1)%:E. Proof. -rewrite unlock /Lnorm; under eq_integral do rewrite /= normr1 powR1. +rewrite unlock /Lnorm; under eq_integral do rewrite/= normr1 poweR1. by rewrite integral_cst// mul1e. Qed. @@ -134,18 +136,23 @@ Lemma Lnorm_eq0_eq0 f p : measurable_fun [set: T] f -> 0 < p -> 'N_p[f] = 0 -> f = \0 %[ae mu]. Proof. rewrite unlock /Lnorm => mf; case: p => [r||//]. -- rewrite lte_fin => r0 /poweR_eq0_eq0 => /(_ (integral_ge0 _ _)) h. - have : \int[mu]_x `| `|f x| `^ r | = 0%R. +- rewrite lte_fin => r0 /eqP; rewrite -poweR_eq0/=. + repeat case: ifPn=>//; last first. + by rewrite lte_fin invr_lt0; move: r0; case: (ltgtP r 0)%R. + move=> /eqP h /[!@eqe] /[!@invr_eq0] rneq0. + have : \int[mu]_x `| `|f x| `^ r%:E | = 0%R. under eq_integral. move=> x _; rewrite gee0_abs; last by rewrite poweR_ge0. over. - by apply: h => x _; rewrite poweR_ge0. - have mp : measurable_fun [set: T] (fun x => `|f x| `^ r). - apply: (@measurableT_comp _ _ _ _ _ _ (fun x => x `^ r)) => //=. + by apply h. + have mp : measurable_fun [set: T] (fun x => `|f x| `^ r%:E). + apply: ( @measurableT_comp _ _ _ _ _ _ (fun x => x `^ r%:E)) => //=. exact: (measurableT_comp (measurable_poweR _)). exact: measurableT_comp. move/(ae_eq_integral_abs mu measurableT mp). apply: filterS => x/= /[apply]. - by move=> /poweR_eq0_eq0 /eqP => /(_ (abse_ge0 _)); rewrite abse_eq0 => /eqP. + move=> /eqP; rewrite -poweR_eq0 //=; repeat case: ifPn=>//; last first. + by move: r0; rewrite lte_fin; case: (ltgtP 0 r)%R. + by rewrite abse_eq0=> /eqP. - case: ifPn => [mu0 _|]. move=> /abs_sup_eq0_ae_eq/=. by apply: filterS => x/= /(_ I) /eqP + _ => /eqP. @@ -154,7 +161,8 @@ rewrite unlock /Lnorm => mf; case: p => [r||//]. by apply/eqP; rewrite eq_le mu0/=. Qed. -Lemma powR_Lnorm f r : r != 0%R -> 'N_r%:E[f] `^ r = \int[mu]_x `| f x | `^ r. +Lemma powR_Lnorm f r : (0 < r)%R -> + 'N_r%:E[f] `^ r%:E = \int[mu]_x `| f x | `^ r%:E. Proof. by move=> r0; rewrite poweR_Lnorm. Qed. Lemma Lnorm_abse f p : 'N_p[abse \o f] = 'N_p[f]. @@ -175,7 +183,7 @@ Local Open Scope ereal_scope. Local Notation "'N_ p [ f ]" := (Lnorm counting p f). Lemma Lnorm_counting p (f : (\bar R)^nat) : (0 < p)%R -> - 'N_p%:E [f] = (\sum_(k p0; rewrite unlock ge0_integral_count// => k; rewrite poweR_ge0. Qed. @@ -372,7 +380,7 @@ move=> p0 mf foo; apply/integrableP; split. apply: measurableT_comp => //; apply: measurableT_comp_powR. exact: measurableT_comp. rewrite ltey; apply: contra foo. -move=> /eqP/(@eqy_poweR _ _ p^-1); rewrite invr_gt0 => /(_ p0) <-. +move=> /eqP/(@eqy_poweR _ _ (p^-1)%:E); rewrite lte_fin invr_gt0 => /(_ p0) <-. rewrite unlock; apply/eqP; congr (_ `^ _). by apply/eq_integral => t _; rewrite [RHS]gee0_abs// lee_fin powR_ge0. Qed. @@ -404,16 +412,20 @@ Let integral_normalized f p : (0 < p)%R -> 0 < 'N_p%:E[f] -> \int[mu]_x (normalized p f x `^ p)%:E = 1. Proof. move=> p0 fpos ifp. -transitivity (\int[mu]_x (`|f x| `^ p / fine ('N_p%:E[f] `^ p))%:E). +transitivity (\int[mu]_x (`|f x| `^ p / fine ('N_p%:E[f] `^ p%:E))%:E). apply: eq_integral => t _. rewrite powRM//; last by rewrite invr_ge0 fine_ge0// Lnorm_ge0. rewrite -[in LHS]powR_inv1; last by rewrite fine_ge0 // Lnorm_ge0. - by rewrite fine_poweR powRAC -powR_inv1 // powR_ge0. + by rewrite fine_poweR ?Lnorm_ge0//powRAC -powR_inv1// powR_ge0. have fp0 : 0 < \int[mu]_x (`|f x| `^ p)%:E. rewrite unlock in fpos. - apply: gt0_poweR fpos; rewrite ?invr_gt0//. + apply: gt0_poweR fpos; rewrite ?lte_fin ?invr_gt0//. by apply integral_ge0 => x _; rewrite lee_fin; exact: powR_ge0. -rewrite unlock -poweRrM mulVf ?(gt_eqF p0)// (poweRe1 (ltW fp0))//. +rewrite unlock -poweRrM; last first. + rewrite /poweRrM_def; case: (\int[mu]_x `|(EFin \o f) x| `^ p%:E)=>//. + by rewrite lee_fin ltW. +rewrite -EFinM mulVf; last by rewrite gt_eqF. +rewrite ?(gt_eqF p0)// (poweRe1 (ltW fp0))//. under eq_integral do rewrite EFinM muleC. have foo : \int[mu]_x (`|f x| `^ p)%:E < +oo. move/integrableP: ifp => -[_]. @@ -507,16 +519,16 @@ have := hoelder counting (mf a1 a2) (mf b1 b2) p0 q0 pq. rewrite !Lnorm_counting//. rewrite (nneseries_split 0 2); last by move=> k; rewrite lee_fin powR_ge0. rewrite add0n ereal_series_cond eseries0 ?adde0; last first. - by move=> [//|] [//|n _]; rewrite /f /= mulr0 normr0 powR0. + by move=> [//|] [//|n _]; rewrite /f/= mulr0 normr0 poweR0e. rewrite big_mkord 2!big_ord_recr/= big_ord0 add0e. -rewrite powRr1 ?normr_ge0 ?powRr1 ?normr_ge0//. +rewrite !poweRe1 ?lee_fin ?normr_ge0//. rewrite (nneseries_split 0 2); last by move=> k; rewrite lee_fin powR_ge0. rewrite ereal_series_cond eseries0 ?adde0; last first. - by move=> [//|] [//|n _]; rewrite /f /= normr0 powR0// gt_eqF. + by move=> [//|] [//|n _]; rewrite /f/= poweR_EFin normr0 powR0// gt_eqF. rewrite big_mkord 2!big_ord_recr /= big_ord0 add0e -EFinD poweR_EFin. rewrite (nneseries_split 0 2); last by move=> k; rewrite lee_fin powR_ge0. rewrite ereal_series_cond eseries0 ?adde0; last first. - by move=> [//|] [//|n _]; rewrite /f /= normr0 powR0// gt_eqF. + by move=> [//|] [//|n _]; rewrite /f/= poweR_EFin normr0 powR0// gt_eqF. rewrite big_mkord 2!big_ord_recr /= big_ord0 add0e -EFinD poweR_EFin. rewrite -EFinM invr1 powRr1; last by rewrite addr_ge0. do 2 (rewrite ger0_norm; last by rewrite mulr_ge0). @@ -614,16 +626,19 @@ Let minkowski_lty f g p : Proof. move=> mf mg p1 Nfoo Ngoo. have p0 : p != 0%R by rewrite gt_eqF// (lt_le_trans _ p1). +have gtp0 : (0 < p)%R by exact /(lt_le_trans _ p1). have h x : (`| f x + g x | `^ p <= 2 `^ (p - 1) * (`| f x | `^ p + `| g x | `^ p))%R. have := convex_powR_abs_half (fun x => 2 * f x)%R (fun x => 2 * g x)%R x p1. rewrite !normrM (@ger0_norm _ 2)// !mulrA mulVf// !mul1r => /le_trans; apply. rewrite !powRM// !mulrA -powR_inv1// -powRD ?pnatr_eq0 ?implybT//. by rewrite (addrC _ p) -mulrDr. -rewrite unlock poweR_lty//. +rewrite unlock poweR_ltr//. pose x := \int[mu]_x (2 `^ (p - 1) * (`|f x| `^ p + `|g x| `^ p))%:E. +set y := \int[mu]_x0 `|(f x0 + g x0)%E|%:E `^ p%:E. apply: (@le_lt_trans _ _ x). rewrite ge0_le_integral//=. + - by move=> ? _; rewrite lee_fin. - apply/measurable_EFinP/measurableT_comp_powR/measurableT_comp => //. exact: measurable_funD. - by apply/measurable_EFinP/measurable_funM/measurable_funD => //; @@ -638,9 +653,9 @@ under eq_integral do rewrite EFinD. rewrite ge0_integralD//; last 2 first. - exact/measurable_EFinP/measurableT_comp_powR/measurableT_comp. - exact/measurable_EFinP/measurableT_comp_powR/measurableT_comp. -by rewrite lte_add_pinfty//; - under eq_integral do rewrite -poweR_EFin -abse_EFin; - rewrite -powR_Lnorm// poweR_lty. +rewrite lte_add_pinfty//; under eq_integral do rewrite -poweR_EFin -abse_EFin. + by rewrite -powR_Lnorm// poweR_ltr//=; case: ifPn; rewrite ?ltW// Nfoo ltry. +by rewrite -powR_Lnorm// poweR_ltr//=; case: ifPn; rewrite ?ltW// Ngoo ltry. Qed. Lemma minkowski_EFin f g p : @@ -654,21 +669,23 @@ have [->|Ngoo] := eqVneq 'N_p%:E[g] +oo. by rewrite addey ?leey// -ltNye (lt_le_trans _ (Lnorm_ge0 _ _ _)). have Nfgoo : 'N_p%:E[(f \+ g)%R] < +oo. by rewrite minkowski_lty// ?ltW// ltey; [exact: Nfoo|exact: Ngoo]. -suff : 'N_p%:E[(f \+ g)%R] `^ p <= ('N_p%:E[f] + 'N_p%:E[g]) * - 'N_p%:E[(f \+ g)%R] `^ p * (fine 'N_p%:E[(f \+ g)%R])^-1%:E. +have p0 : (0 < p)%R by exact: (lt_trans _ p1). +suff : 'N_p%:E[(f \+ g)%R] `^ p%:E <= ('N_p%:E[f] + 'N_p%:E[g]) * + 'N_p%:E[(f \+ g)%R] `^ p%:E * (fine 'N_p%:E[(f \+ g)%R])^-1%:E. have [-> _|Nfg0] := eqVneq 'N_p%:E[(f \+ g)%R] 0. by rewrite adde_ge0 ?Lnorm_ge0. rewrite lee_pdivlMr ?fine_gt0// ?lt0e ?Nfg0 ?Lnorm_ge0//. - rewrite -{1}(@fineK _ ('N_p%:E[(f \+ g)%R] `^ p)); last first. + rewrite -{1}(@fineK _ ('N_p%:E[(f \+ g)%R] `^ p%:E)); last first. by rewrite fin_num_poweR// ge0_fin_numE// Lnorm_ge0. rewrite -(invrK (fine _)) lee_pdivrMl; last first. - rewrite invr_gt0 fine_gt0// (poweR_lty _ Nfgoo) andbT poweR_gt0//. - by rewrite lt0e Nfg0 Lnorm_ge0. + rewrite invr_gt0 fine_gt0// poweR_ltr//=. + rewrite andbT -poweR_gt0//=; move: (Nfg0); repeat case: ifPn=>//. + by rewrite lee_fin=> _ _ _ /[!@ltW]//; apply /(lt_trans _ p1). rewrite fineK ?ge0_fin_numE ?Lnorm_ge0// => /le_trans; apply. rewrite lee_pdivrMl; last first. - by rewrite fine_gt0// poweR_lty// andbT poweR_gt0// lt0e Nfg0 Lnorm_ge0. + rewrite fine_gt0// poweR_ltr// andbT -poweR_gt0//=; move: (Nfg0). + by repeat case: ifPn=>//=; move=> _ _ _; rewrite lee_fin ltW. by rewrite fineK// 1?muleC// fin_num_poweR// ge0_fin_numE ?Lnorm_ge0. -have p0 : (0 < p)%R by exact: (lt_trans _ p1). rewrite powR_Lnorm ?gt_eqF//. under eq_integral. move=> x _. @@ -693,7 +710,7 @@ rewrite ge0_integralD//; last 2 first. exact: measurableT_comp. exact/measurableT_comp_powR/measurableT_comp/measurable_funD. rewrite [leRHS](_ : _ = ('N_p%:E[f] + 'N_p%:E[g]) * - (\int[mu]_x (`|f x + g x| `^ p)%:E) `^ `1-(p^-1)). + (\int[mu]_x (`|f x + g x| `^ p)%:E) `^ (`1-(p^-1))%:E). rewrite muleDl; last 2 first. - rewrite fin_num_poweR//. under eq_integral do rewrite -poweR_EFin -abse_EFin. @@ -730,12 +747,23 @@ rewrite [leRHS](_ : _ = ('N_p%:E[f] + 'N_p%:E[g]) * + by rewrite invrK subrKC. rewrite -muleA; congr (_ * _). under [X in X * _]eq_integral=> x _ do rewrite mulr_powRB1 ?subr_gt0//. -rewrite poweRD; last by rewrite poweRD_defE gt_eqF ?implyFb// subr_gt0 invf_lt1. -rewrite poweRe1; last by apply: integral_ge0 => x _; rewrite lee_fin powR_ge0. -congr (_ * _); rewrite poweRN. -- by rewrite unlock fine_poweR. +rewrite EFinD poweRD; last first. + under eq_integral do rewrite -poweR_EFin -abse_EFin. + rewrite -powR_Lnorm//. + move: (Nfgoo). + set Nfg := 'N_p%:E [(f \+ g)%R]. + have: 0 <= Nfg by rewrite Lnorm_ge0. + case: Nfg=>//= r r0 _. + by rewrite subr_eq0 eq_sym invr_eq1 gt_eqF. +rewrite poweRe1; last by rewrite integral_ge0. +congr (_ * _). +rewrite (_ : (- p^-1)%:E = - (p^-1)%:E)// poweRN//=; last first. - under eq_integral do rewrite -poweR_EFin -abse_EFin. - by rewrite -powR_Lnorm ?gt_eqF// fin_num_poweR// ge0_fin_numE ?Lnorm_ge0. + by rewrite -powR_Lnorm// fin_num_poweR// ge0_fin_numE ?Lnorm_ge0//. +- exact: integral_ge0 => x _; rewrite lee_fin powR_ge0. +under eq_integral do rewrite -poweR_EFin -abse_EFin. + rewrite -powR_Lnorm// fine_poweR ?Lnorm_ge0//=. + by rewrite -powRrM divff ?gt_eqF// powRr1//= fine_ge0// Lnorm_ge0//. Qed. Lemma lerB_DLnorm f g p : @@ -976,20 +1004,23 @@ Lemma LnormZ (f : LfunType mu p1) a : Proof. rewrite unlock /Lnorm. case: p p1 f => //[r r1 f|? f]. -- under eq_integral do rewrite /= -mulr_algl scaler1 normrM powRM ?EFinM//. +- under eq_integral=> x _. + rewrite /= -mulr_algl scaler1 normrM poweR_EFin powRM// EFinM. + over. rewrite integralZl//; last first. apply/integrableP; split. apply: measurableT_comp => //. apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ r)) => //. exact: measurableT_comp. - apply: (@lty_poweRy _ _ r^-1). - by rewrite gt_eqF// invr_gt0 ?(lt_le_trans ltr01). + apply: (@lty_poweRy _ _ (r^-1)%:E). + by rewrite lte_fin invr_gt0 ?(lt_le_trans ltr01). rewrite [ltLHS](_ : _ = 'N[mu]_r%:E[EFin \o f]%E). exact: Lfunction_finite. rewrite unlock /Lnorm. by under eq_integral do rewrite gee0_abs ?lee_fin ?powR_ge0//. rewrite poweRM ?integral_ge0//. by rewrite poweR_EFin -powRrM mulfV ?gt_eqF ?(lt_le_trans ltr01)// powRr1. + by rewrite gt_eqF// invr_gt0; apply /(lt_le_trans ltr01). - case: ifPn => mu0; last by rewrite mule0. rewrite -ess_supZl//; apply/eq_ess_sup/nearW => t /=. by rewrite normrZ EFinM. @@ -1097,7 +1128,7 @@ apply/integrableP; split => //. apply: measurableT_comp => //. apply: (measurableT_comp (measurable_powR _)) => //. exact: measurableT_comp. -move: lpf => /(poweR_lty r). +move: lpf => /(poweR_ltr r). rewrite powR_Lnorm// ?gt_eqF// ?(lt_le_trans ltr01)//. apply: le_lt_trans. by under eq_integral => x _ do rewrite gee0_abs ?lee_fin ?powR_ge0//. @@ -1125,14 +1156,17 @@ rewrite inE => /andP[mf]; rewrite inE/= => l2f. move: mf; rewrite inE/= => mf. apply/integrableP; split. by apply/measurable_EFinP; exact: measurable_funX. -rewrite (@lty_poweRy _ _ 2^-1)//. +rewrite (@lty_poweRy _ _ 2^-1) ?inve_gt0//. rewrite (le_lt_trans _ l2f)//. rewrite unlock. -rewrite gt0_ler_poweR//. -- by rewrite in_itv/= leey integral_ge0. +rewrite inver//= (_ : 2%R == 0%R = false); last by rewrite gt_eqF. +rewrite gt0_lee_poweR//. - by rewrite in_itv/= leey integral_ge0. +- rewrite in_itv/= leey integral_ge0//. + by move=> x _ ; rewrite poweR_ge0. - rewrite ge0_le_integral//. + apply: measurableT_comp => //; apply/measurable_EFinP. + repeat apply: measurableT_comp=>//. exact: measurable_funX. + apply/measurable_EFinP. apply/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x `^ 2)%R) => //. @@ -1163,8 +1197,8 @@ rewrite inE; apply/andP; split. move: lf; rewrite inE => /andP[/[!inE]/= lf _]. exact: measurable_funM. rewrite !inE/= /finite_norm unlock /Lnorm. -rewrite poweR_lty//=. -under eq_integral => x _ do rewrite normrM powRM// EFinM. +rewrite poweR_ltr//=. +under eq_integral => x _ do rewrite normrM poweR_EFin powRM// EFinM. rewrite integralZr// ?Lfun_integrable//. rewrite muleC lte_mul_pinfty// ?lee_fin ?powR_ge0//. move: lpf => /(Lfun_integrable r1) /integrableP[_]. @@ -1182,8 +1216,9 @@ Variable mu : {finite_measure set T -> \bar R}. Lemma Lfun_cst c r : cst c \in Lfun mu r%:E. Proof. rewrite inE/=; apply/andP; split; rewrite inE//=. -rewrite /finite_norm unlock poweR_lty//. -under eq_integral => x _/= do rewrite (_ : `|c| `^ r = cst (`|c| `^ r) x)//. +rewrite /finite_norm unlock poweR_ltr//. +under eq_integral => x _/= do + rewrite poweR_EFin (_ : `|c| `^ r = cst (`|c| `^ r) x)//. apply/integrable_lty => //. exact: finite_measure_integrable_cst. Qed. @@ -1205,9 +1240,9 @@ rewrite le_eqVlt => /predU1P[mu0 p1 q1 muTfin pq f +|mu_pos]. rewrite inE; apply/andP; split; rewrite inE//=. rewrite /finite_norm unlock /Lnorm. move: p p1 {pq} => [r r1| |//]; last by rewrite -mu0 ltxx ltry. - under eq_integral do rewrite /= -[(_ `^ _)%R]ger0_norm ?powR_ge0//=. + under eq_integral do rewrite /= poweR_EFin -[(_ `^ _)%R]ger0_norm ?powR_ge0//=. rewrite (@integral_abs_eq0 _ _ _ _ _ (fun x => (`|f x| `^ r)%:E))//. - by rewrite poweR0r// invr_neq0// gt_eqF// -lte_fin (lt_le_trans _ r1). + by rewrite poweR_EFin ltry. apply/measurable_EFinP/(@measurableT_comp _ _ _ _ _ _ (@powR R ^~ r)) => //. exact: measurableT_comp. move: p q => [p| |//] [q| |]// p1 q1. @@ -1235,23 +1270,26 @@ move: p q => [p| |//] [q| |]// p1 q1. rewrite /r ltr_pdivlMr// mul1r. have rr'1 : (r^-1 + r'^-1 = 1)%R by rewrite /r' /r invf_div invrK subrKC. move=> /(_ mfp m1 r0 r'0 rr'1). - under [in leLHS] eq_integral do rewrite /= powRr1// norm_powR// normrE. + under [in leLHS] eq_integral do rewrite /= poweR_EFin powRr1// norm_powR// normrE. under [in leRHS] eq_integral do - rewrite /= norm_powR// normr_id -powRrM mulrCA divff// mulr1. + rewrite /= poweR_EFin norm_powR// normr_id -powRrM mulrCA divff// mulr1. rewrite [X in X <= _]poweRe1; last by apply: integral_ge0 => x _; rewrite lee_fin powR_ge0. move=> h1 /lty_poweRy h2. - apply/poweR_lty/(le_lt_trans h1). + apply/poweR_ltr/(le_lt_trans h1). rewrite muleC lte_mul_pinfty ?fin_numElt?poweR_ge0//. by rewrite (lt_le_trans _ (poweR_ge0 _ _))//= ltey_eq fin_num_poweR. - rewrite poweR_lty// (lty_poweRy qinv0)//. + rewrite poweR_ltr//. + apply /lty_poweRy. + apply /(_ : 0 < (q^-1)%:E). + by rewrite lte_fin invr_gt0. by have:= ffin; rewrite /finite_norm unlock /Lnorm. - have p0 : (0 < p)%R by rewrite ?(lt_le_trans ltr01). move=> muoo _ f. rewrite !inE => /andP[/[1!inE]/= mf]. rewrite !inE/= /finite_norm unlock /Lnorm mu_pos => supf_lty. apply/andP; split; rewrite inE//= /finite_norm unlock /Lnorm. - rewrite poweR_lty//; move: supf_lty => /ess_supr_bounded[M fM]. + rewrite poweR_ltr//; move: supf_lty => /ess_supr_bounded[M fM]. rewrite (@le_lt_trans _ _ (\int[mu]_x (M `^ p)%:E)); [by []| |]; last first. by rewrite integral_cst// ltey_eq fin_numM. apply: ae_ge0_le_integral => //. diff --git a/theories/lebesgue_integral_theory/measurable_fun_approximation.v b/theories/lebesgue_integral_theory/measurable_fun_approximation.v index 88af112a6a..63272b04ff 100644 --- a/theories/lebesgue_integral_theory/measurable_fun_approximation.v +++ b/theories/lebesgue_integral_theory/measurable_fun_approximation.v @@ -671,24 +671,18 @@ Qed. End emeasurable_fun_comparison. -Lemma measurable_poweR (R : realType) r : - measurable_fun [set: \bar R] (poweR ^~ r). -Proof. -under eq_fun do rewrite poweRE. -rewrite -/(measurable_fun _ _). -apply: measurable_fun_ifT => //=. - apply/measurable_EFinP => //=. - apply: measurable_fun_ifT => //=. - apply: (measurable_fun_bool true). - rewrite setTI (_ : _ @^-1` _ = EFin @` setT). - by apply: measurable_image_EFin; exact: measurableT. - apply/seteqP; split => [x finx|x [s sx <-//]]/=. - by exists (fine x) => //; rewrite fineK. - exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ r)). -apply: measurable_fun_ifT => //=; first exact: measurable_fun_eqe. -apply: measurable_fun_ifT => //=; first exact: measurable_fun_eqe. -apply/measurable_EFinP => //=. -exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ r)). +Lemma measurable_poweR (R : realType) y : + measurable_fun [set: \bar R] (poweR ^~ y). +under eq_fun do rewrite poweRE. +case: y=> [s||]//=; rewrite -/(measurable_fun _ _). +- repeat apply: measurable_fun_ifT=>//=. + 1-3: by apply: measurable_fun_lte + apply: measurable_fun_eqe. + apply/measurable_EFinP=>//=. + exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ s)). +- repeat apply: measurable_fun_ifT=>//=. + 1-4: by apply: measurable_fun_lte + apply: measurable_fun_eqe. +- repeat apply: measurable_fun_ifT=>//=. + 1-5: by apply: measurable_fun_lte + apply: measurable_fun_eqe. Qed. Section measurable_comparison.