From 4a697268b509033094aadcb9818589389d175877 Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Thu, 26 Jun 2025 19:35:20 +0900 Subject: [PATCH 1/2] add lemmas --- CHANGELOG_UNRELEASED.md | 9 +++ theories/realfun.v | 126 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 135 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 399f8064a..d3faa277f 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -172,6 +172,15 @@ - in `constructive_ereal.v`: + lemmas `div1e`, `divee`, `inve_eq1`, `Nyconjugate` +- in `realfun.v` + + lemmas `derivable_oy_continuous_within_itvcy`, + `derivable_oy_continuous_within_itvNyc` + + lemmas `derivable_oo_continuous_bndW`, + `derivable_oy_continuous_bndW_oo`, + `derivable_oy_continuous_bndW`, + `derivable_Nyo_continuous_bndW_oo`, + `derivable_Nyo_continuous_bndW` + ### Changed - in `measure.v`: diff --git a/theories/realfun.v b/theories/realfun.v index 214fa3aad..acc47f486 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1188,8 +1188,134 @@ Definition derivable_Nyo_continuous_bnd (f : R -> V) (x : R) := Definition derivable_oy_continuous_bnd (f : R -> V) (x : R) := {in `]x, +oo[, forall x, derivable f x 1} /\ f @ x^'+ --> f x. +Lemma derivable_oy_continuous_within_itvcy (f : R -> V) (x : R) : + derivable_oy_continuous_bnd f x -> {within `[x, +oo[, continuous f}. +Proof. +move=> [df cfx]. +apply/subspace_continuousP => z /=. +rewrite in_itv/= => /andP[]; rewrite le_eqVlt => /predU1P[<-{z} _|]. + have := cvg_at_right_within cfx; apply: cvg_trans; apply: cvg_app. + by apply: within_subset => z/=; rewrite in_itv/= => /andP[]. +move=> xz _. +apply: cvg_within_filter. +apply/differentiable_continuous; rewrite -derivable1_diffP. +by apply: df; rewrite in_itv/= xz. +Qed. + +Lemma derivable_oy_continuous_within_itvNyc (f : R -> V) (x : R) : + derivable_Nyo_continuous_bnd f x -> {within `]-oo, x], continuous f}. +Proof. +move=> [df cfx]. +apply/subspace_continuousP => z /=. +rewrite in_itv/=; rewrite le_eqVlt => /predU1P[->{z}|]. + have := cvg_at_left_within cfx; apply: cvg_trans; apply: cvg_app. + by apply: within_subset => z/=; rewrite in_itv/=. +move=> cx. +apply: cvg_within_filter. +apply/differentiable_continuous; rewrite -derivable1_diffP. +by apply: df; rewrite in_itv/=. +Qed. + End derivable_oo_continuous_bnd. +Section derivable_oo_continuous_bndW. +Context {R : realFieldType} {V : normedModType R}. + +Lemma derivable_oo_continuous_bndW (a b c d : R) (f : R -> V) : + (c < d) -> + (a <= c) -> (d <= b) -> + derivable_oo_continuous_bnd f a b -> + derivable_oo_continuous_bnd f c d. +Proof. +move=> cd ac db [/[dup]df + fa fb]. +move/derivable_within_continuous; rewrite continuous_open_subspace// => cf. +split. +- apply: in1_subset_itv df. + exact: subset_itvW. +- move: ac; rewrite le_eqVlt => /predU1P[<- //|ac]. + apply: cvg_at_right_filter. + by apply: cf; rewrite inE/= in_itv/= ac/= (lt_le_trans cd db). +- move: db; rewrite le_eqVlt => /predU1P[-> //|db]. + apply: cvg_at_left_filter. + by apply cf; rewrite inE/= in_itv/= db andbT (le_lt_trans ac cd). +Qed. + +Lemma derivable_oy_continuous_bndW_oo (a c d : R) (f : R -> V) : + (c < d) -> + (a <= c) -> + derivable_oy_continuous_bnd f a -> + derivable_oo_continuous_bnd f c d. +Proof. +move=> cd ac[df fa]. +split => //. +- apply: in1_subset_itv df. + exact: subset_itv. +- move: ac; rewrite le_eqVlt => /predU1P[<-//|ac]. + apply: cvg_at_right_filter. + have := derivable_within_continuous df. + rewrite continuous_open_subspace//; apply. + by rewrite inE/= in_itv/= ac. +- apply: cvg_at_left_filter. + have := derivable_within_continuous df. + rewrite continuous_open_subspace//; apply. + by rewrite inE/= in_itv/= (le_lt_trans ac cd). +Qed. + +Lemma derivable_oy_continuous_bndW (a c : R) (f : R -> V) : + (a <= c) -> + derivable_oy_continuous_bnd f a -> + derivable_oy_continuous_bnd f c. +Proof. +move=> ac[df fa]. +split => //. +- apply: in1_subset_itv df. + exact: subset_itv. +- move: ac; rewrite le_eqVlt => /predU1P[<- //|ac]. + apply: cvg_at_right_filter. + have := derivable_within_continuous df. + rewrite continuous_open_subspace//; apply. + by rewrite inE/= in_itv/= ac. +Qed. + +Lemma derivable_Nyo_continuous_bndW_oo (b c d : R) (f : R -> V) : + (c < d) -> + (d <= b) -> + derivable_Nyo_continuous_bnd f b -> + derivable_oo_continuous_bnd f c d. +Proof. +move=> cd db [df fa]. +split => //. +- apply: in1_subset_itv df. + exact: subset_itv. +- apply: cvg_at_right_filter. + have := derivable_within_continuous df. + rewrite continuous_open_subspace//; apply. + by rewrite inE/= in_itv/= (lt_le_trans cd db). +- move: db; rewrite le_eqVlt => /predU1P[-> //|db]. + apply: cvg_at_left_filter. + have := derivable_within_continuous df. + rewrite continuous_open_subspace//; apply. + by rewrite inE/= in_itv/=. +Qed. + +Lemma derivable_Nyo_continuous_bndW (b d : R) (f : R -> V) : + (d <= b) -> + derivable_Nyo_continuous_bnd f b -> + derivable_Nyo_continuous_bnd f d. +Proof. +move=> db [df fa]. +split => //. +- apply: in1_subset_itv df. + exact: subset_itv. +- move: db; rewrite le_eqVlt => /predU1P[-> //|db]. + apply: cvg_at_left_filter. + have := derivable_within_continuous df. + rewrite continuous_open_subspace//; apply. + by rewrite inE/= in_itv/=. +Qed. + +End derivable_oo_continuous_bndW. + Section real_inverse_functions. Variable R : realType. Implicit Types (a b : R) (f g : R -> R). From 79facfc16bc6882dffd51acfe97a0f0f959fb210 Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Thu, 26 Jun 2025 23:37:05 +0900 Subject: [PATCH 2/2] minor fix --- CHANGELOG_UNRELEASED.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d3faa277f..1943e630e 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -172,9 +172,9 @@ - in `constructive_ereal.v`: + lemmas `div1e`, `divee`, `inve_eq1`, `Nyconjugate` -- in `realfun.v` +- in `realfun.v`: + lemmas `derivable_oy_continuous_within_itvcy`, - `derivable_oy_continuous_within_itvNyc` + `derivable_oy_continuous_within_itvNyc`, + lemmas `derivable_oo_continuous_bndW`, `derivable_oy_continuous_bndW_oo`, `derivable_oy_continuous_bndW`,