From a706b7fc19d9c0c5e953160040a49e10996799cc Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Fri, 11 Apr 2025 17:17:52 +0900 Subject: [PATCH 1/8] add is_derive1_powR --- CHANGELOG_UNRELEASED.md | 4 +++ theories/exp.v | 54 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 58 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c3166b5229..35866468ec 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -26,6 +26,10 @@ - in `lebesgue_integral_approximation.v`: + lemma `measurable_prod` +- in `exp.v`: + + lemmas `lnNy`, `powR_cvg0`, `derivable_powR`, `powR_derive1` + + Instance `is_derive1_powR` + ### Changed - in `pi_irrational`: diff --git a/theories/exp.v b/theories/exp.v index 230b3c1abf..b6058292bc 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -790,6 +790,12 @@ by rewrite !lnK// -(@ler_ln) ?posrE ?expR_gt0 ?conv_gt0// expRK. Qed. Local Close Scope convex_scope. +Lemma lnNy : ln x @[x --> 0^'+] --> -oo. +Proof. +apply/cvgrNyPle => y; near=> x; rewrite -ler_expR lnK; last by rewrite posrE. +by near: x; apply: nbhs_right_le; exact: expR_gt0. +Unshelve. end_near. Qed. + End Ln. Section PowR. @@ -1053,6 +1059,54 @@ Qed. Canonical powR_inum (i : Itv.t) (x : Itv.def (@Itv.num_sem R) i) p := Itv.mk (num_spec_powR x p). +Lemma powR_cvg0 (x : R) : 0 < x -> + a `^ x @[a --> 0^'+] --> 0. +Proof. +move=> x0; apply: (@cvg_trans _ ((expR (ln a * x)) @[a --> 0^'+])). + by apply: near_eq_cvg; near=> a; rewrite /powR gt_eqF 1?mulrC. +apply: (@cvg_comp _ _ _ _ _ _ (@ninfty_nbhs R)). + by apply: gt0_cvgMlNy; rewrite ?x0//; exact: lnNy. +exact/cvgNy_compNP/cvgr_expR. +Unshelve. end_near. Qed. + +Lemma derivable_powR v x : v != 0 -> + {in `]0, +oo[, forall a, + derivable (powR ^~ x) a v}. +Proof. +move=> v0 a; rewrite in_itv/= andbT => a0. +apply: (@near_eq_derivable _ _ _ (fun a' => expR (x * ln a'))) => //. + by near=> b; rewrite /powR gt_eqF//; near: b; exact: lt_nbhsr. +apply: diff_derivable; apply: differentiable_comp; last exact/derivable1_diffP. +apply: differentiableM => //; apply/derivable1_diffP. +by apply: ex_derive; exact: is_derive1_ln. +Unshelve. end_near. Qed. + +Lemma powR_derive1 a : {in `]0, +oo[%R, + (powR ^~ a) ^`()%classic =1 (fun x => a * x `^ (a - 1))}. +Proof. +move=> x; rewrite in_itv/= andbT => x0. +rewrite derive1E. +rewrite (@near_eq_derive _ _ _ _ (fun x => expR (a * ln x)))//; last first. + by near=> z; rewrite /powR gt_eqF//; near: z; exact: lt_nbhsr. +rewrite -derive1E. +rewrite derive1_comp//=; last first. + by apply: derivableM => //; apply: ex_derive; exact: is_derive1_ln. +rewrite 2!derive1E. +rewrite deriveM//; last by apply: ex_derive; exact: is_derive1_ln. +rewrite !derive_val scaler0 addr0. +have [_ ->] := (is_derive1_ln x0). +rewrite mulrC powRB; last by rewrite (@gt_eqF _ _ x)//; apply: implybT. +by rewrite powRr1 ?ltW// mulrA [in RHS]mulrAC /powR gt_eqF. +Unshelve. end_near. Qed. + +Global Instance is_derive1_powR (a x : R) : 0 < x -> + is_derive x 1 (powR ^~ a) (a * x `^ (a - 1))%R. +Proof. +move=> x_gt0; split. + by apply: derivable_powR; rewrite ?in_itv/= ?andbT. +by rewrite -derive1E powR_derive1// in_itv andbT. +Qed. + End PowR. Notation "a `^ x" := (powR a x) : ring_scope. From 74c604a01ead11b2ad4e78c3ccf8bb3741491d45 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Wed, 30 Apr 2025 13:11:31 +0900 Subject: [PATCH 2/8] Update CHANGELOG_UNRELEASED.md --- CHANGELOG_UNRELEASED.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 35866468ec..c89d899c72 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -42,6 +42,19 @@ ### Generalized +- in `constructive_ereal.v`: + + lemma `EFin_natmul` + +- in `lebesgue_integral.v` + + lemmas `measurable_funP`, `ge0_integral_pushforward`, + `integrable_pushforward`, `integral_pushforward` + +- in `real_interval.v`: + + lemmas `bigcup_itvT`, `itv_bndy_bigcup_BRight`, `itv_bndy_bigcup_BLeft_shift` + +- in `normedtype.v`: + + lemmas `gt0_cvgMlNy`, `gt0_cvgMly` + ### Deprecated ### Removed From dcbd6207e6dde2080eb9c5dba3f76e9cf3722750 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Wed, 30 Apr 2025 13:12:11 +0900 Subject: [PATCH 3/8] Update theories/exp.v --- theories/exp.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/theories/exp.v b/theories/exp.v index b6058292bc..22dba6857e 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -1070,8 +1070,7 @@ exact/cvgNy_compNP/cvgr_expR. Unshelve. end_near. Qed. Lemma derivable_powR v x : v != 0 -> - {in `]0, +oo[, forall a, - derivable (powR ^~ x) a v}. + {in `]0, +oo[, forall a, derivable (powR ^~ x) a v}. Proof. move=> v0 a; rewrite in_itv/= andbT => a0. apply: (@near_eq_derivable _ _ _ (fun a' => expR (x * ln a'))) => //. From a7dcced10c5585fbf7d2d5221b90cb9bd96f962b Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Wed, 30 Apr 2025 13:12:36 +0900 Subject: [PATCH 4/8] Update theories/exp.v --- theories/exp.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/theories/exp.v b/theories/exp.v index 22dba6857e..ac49403b13 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -1059,8 +1059,7 @@ Qed. Canonical powR_inum (i : Itv.t) (x : Itv.def (@Itv.num_sem R) i) p := Itv.mk (num_spec_powR x p). -Lemma powR_cvg0 (x : R) : 0 < x -> - a `^ x @[a --> 0^'+] --> 0. +Lemma powR_cvg0 (x : R) : 0 < x -> a `^ x @[a --> 0^'+] --> 0. Proof. move=> x0; apply: (@cvg_trans _ ((expR (ln a * x)) @[a --> 0^'+])). by apply: near_eq_cvg; near=> a; rewrite /powR gt_eqF 1?mulrC. From 68b1af5e3abb78ee37bb7d51616a387ff47a0880 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 30 Apr 2025 14:27:00 +0900 Subject: [PATCH 5/8] fix --- theories/normedtype_theory/num_normedtype.v | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/theories/normedtype_theory/num_normedtype.v b/theories/normedtype_theory/num_normedtype.v index 08b8eec1d6..1527b46943 100644 --- a/theories/normedtype_theory/num_normedtype.v +++ b/theories/normedtype_theory/num_normedtype.v @@ -505,19 +505,20 @@ rewrite pmulrn ceil_le_int// [ceil _]intEsign. by rewrite le_gtF ?expr0 ?mul1r ?lez_nat ?ceil_ge0//; near: n; apply: Foo. Unshelve. all: by end_near. Qed. -Lemma gt0_cvgMlNy {R : realFieldType} (M : R) (f : R -> R) : (0 < M)%R -> - (f r) @[r --> -oo] --> -oo -> (f r * M)%R @[r --> -oo] --> -oo. +Lemma gt0_cvgMlNy {R : realFieldType} {F : set_system R} {FF : Filter F} (M : R) + (f : R -> R) : + (0 < M)%R -> (f r) @[r --> F] --> -oo -> (f r * M)%R @[r --> F] --> -oo. Proof. move=> M0 /cvgrNyPle fy; apply/cvgrNyPle => A. by apply: filterS (fy (A / M)) => x; rewrite ler_pdivlMr. Qed. -Lemma gt0_cvgMly {R : realFieldType} (M : R) (f : R -> R) : (0 < M)%R -> - f r @[r --> +oo] --> +oo -> (f r * M)%R @[r --> +oo] --> +oo. +Lemma gt0_cvgMly {R : realFieldType} {F : set_system R} {FF : Filter F} (M : R) + (f : R -> R) : + (0 < M)%R -> f r @[r --> F] --> +oo -> (f r * M)%R @[r --> F] --> +oo. Proof. move=> M0 /cvgryPge fy; apply/cvgryPge => A. -apply: filterS (fy (A / M)) => x. -by rewrite ler_pdivrMr. +by apply: filterS (fy (A / M)) => x; rewrite ler_pdivrMr. Qed. Lemma cvgNy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T) From d4b701e29e4c20e5e993c763e0daba3efeb77e5d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 30 Apr 2025 14:28:30 +0900 Subject: [PATCH 6/8] fix --- CHANGELOG_UNRELEASED.md | 10 ---------- experimental_reals/discrete.v | 2 +- reals/reals.v | 2 +- 3 files changed, 2 insertions(+), 12 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c89d899c72..fdde6ee25f 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -42,16 +42,6 @@ ### Generalized -- in `constructive_ereal.v`: - + lemma `EFin_natmul` - -- in `lebesgue_integral.v` - + lemmas `measurable_funP`, `ge0_integral_pushforward`, - `integrable_pushforward`, `integral_pushforward` - -- in `real_interval.v`: - + lemmas `bigcup_itvT`, `itv_bndy_bigcup_BRight`, `itv_bndy_bigcup_BLeft_shift` - - in `normedtype.v`: + lemmas `gt0_cvgMlNy`, `gt0_cvgMly` diff --git a/experimental_reals/discrete.v b/experimental_reals/discrete.v index 63ca0e73b8..412877a07b 100644 --- a/experimental_reals/discrete.v +++ b/experimental_reals/discrete.v @@ -4,7 +4,7 @@ (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) -From Corelib Require Setoid. +From Coq Require Setoid. From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra. From mathcomp.classical Require Import boolp. diff --git a/reals/reals.v b/reals/reals.v index 601ad4fe7c..90bb30d878 100644 --- a/reals/reals.v +++ b/reals/reals.v @@ -38,7 +38,7 @@ (* *) (******************************************************************************) -From Corelib Require Import Setoid. +From Coq Require Import Setoid. From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra archimedean. From mathcomp Require Import boolp classical_sets set_interval. From 5454cb4d55fbcdee6c020ca8555e5e504360d1fc Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Wed, 30 Apr 2025 14:54:24 +0900 Subject: [PATCH 7/8] Update reals/reals.v --- reals/reals.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/reals/reals.v b/reals/reals.v index 90bb30d878..601ad4fe7c 100644 --- a/reals/reals.v +++ b/reals/reals.v @@ -38,7 +38,7 @@ (* *) (******************************************************************************) -From Coq Require Import Setoid. +From Corelib Require Import Setoid. From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra archimedean. From mathcomp Require Import boolp classical_sets set_interval. From a1519ac79e4cccfe26209f5e2628b0b852db4063 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Wed, 30 Apr 2025 14:54:52 +0900 Subject: [PATCH 8/8] Update experimental_reals/discrete.v --- experimental_reals/discrete.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/experimental_reals/discrete.v b/experimental_reals/discrete.v index 412877a07b..63ca0e73b8 100644 --- a/experimental_reals/discrete.v +++ b/experimental_reals/discrete.v @@ -4,7 +4,7 @@ (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) -From Coq Require Setoid. +From Corelib Require Setoid. From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra. From mathcomp.classical Require Import boolp.