From 75a094838ef79bf40182e28f9915d37c82a637fa Mon Sep 17 00:00:00 2001 From: Arthur Molina-Mounier Date: Wed, 15 Jul 2026 15:43:21 +0200 Subject: [PATCH 1/2] normed module identity convergence lemmas --- theories/normedtype_theory/normed_module.v | 24 ++++++++++++ .../pseudometric_normed_Zmodule.v | 39 +++++++++++++++++++ 2 files changed, 63 insertions(+) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 1252178b3f..94a72d0f8e 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -642,6 +642,30 @@ Proof. exact: cvgZr_tmp. Qed. Lemma cvgMl_tmp g a b : g @ F --> b -> a * g x @[x --> F] --> a * b. Proof. exact: cvgZl_tmp. Qed. +Lemma cvg1MC f a : f @ F --> (1 :> K) -> f x * a @[x --> F] --> a. +Proof. by move/(cvgMr_tmp (b := a)); rewrite mul1r. Qed. + +Lemma cvg1M f g a : f @ F --> (1 :> K) -> g @ F --> a -> f \* g @ F --> a. +Proof. by move=> /cvgM /[apply]; rewrite mul1r. Qed. + +Lemma cvgCM1 f a : f @ F --> (1 :> K) -> a * f x @[x --> F] --> a. +Proof. by move/(cvgMl_tmp (a := a)); rewrite mulr1. Qed. + +Lemma cvgM1 f g a : f @ F --> a -> g @ F --> (1 :> K) -> f \* g @ F --> a. +Proof. by move=> /cvgM /[apply]; rewrite mulr1. Qed. + +Lemma cvg0MC f a : f @ F --> 0 -> f x * a @[x --> F] --> 0. +Proof. by move/(cvgMr_tmp (b := a)); rewrite mul0r. Qed. + +Lemma cvg0M f g a : f @ F --> 0 -> g @ F --> a -> f \* g @ F --> 0. +Proof. by move=> /cvgM /[apply]; rewrite mul0r. Qed. + +Lemma cvgCM0 f a : f @ F --> 0 -> a * f x @[x --> F] --> 0. +Proof. by move/(cvgMl_tmp (a := a)); rewrite mulr0. Qed. + +Lemma cvgM0 f g a : f @ F --> a -> g @ F --> 0 -> f \* g @ F --> 0. +Proof. by move=> /cvgM /[apply]; rewrite mulr0. Qed. + Lemma is_cvgM f g : cvg (f @ F) -> cvg (g @ F) -> cvg (f \* g @ F). Proof. exact: is_cvgZ. Qed. diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index 9f945624de..82c259cf1f 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -1098,6 +1098,45 @@ Qed. Lemma is_cvgDrE f g : cvg (f @ F) -> cvg ((f + g) @ F) = cvg (g @ F). Proof. by rewrite addrC; apply: is_cvgDlE. Qed. +Lemma cvgDl f a b : f @ F --> b -> a + f x @[x --> F] --> a + b. +Proof. apply: cvgD; exact: cvg_cst. Qed. + +Lemma cvgDr f a b : f @ F --> a -> f x + b @[x --> F] --> a + b. +Proof. move/cvgD; apply; exact: cvg_cst. Qed. + +Lemma cvgBl f a b : f @ F --> b -> a - f x @[x --> F] --> a - b. +Proof. by move/cvgN; apply: cvgDl. Qed. + +Lemma cvgBr f a b : f @ F --> a -> f x - b @[x --> F] --> a - b. +Proof. exact: cvgDr. Qed. + +Lemma cvg0D f g a : f @ F --> 0 -> g @ F --> a -> f x + g x @[x --> F] --> a. +Proof. by move=> /cvgD /[apply]; rewrite add0r. Qed. + +Lemma cvg0DC f a : f @ F --> 0 -> f x + a @[x --> F] --> a. +Proof. by move=> /(cvgDr (b := a)); rewrite add0r. Qed. + +Lemma cvgD0 f g a : f @ F --> a -> g @ F --> 0 -> f x + g x @[x --> F] --> a. +Proof. by move=> /cvgD /[apply]; rewrite addr0. Qed. + +Lemma cvgCD0 f a : f @ F --> 0 -> a + f x @[x --> F] --> a. +Proof. by move/(@cvgDl _ a); rewrite addr0. Qed. + +Lemma cvg0B f g a : f @ F --> 0 -> g @ F --> a -> f x - g x @[x --> F] --> -a. +Proof. by move=> /cvgB /[apply]; rewrite add0r. Qed. + +Lemma cvg0BC f a : f @ F --> 0 -> f x - a @[x --> F] --> -a. +Proof. by move=> /(cvgBr (b := a)); rewrite add0r. Qed. + +Lemma cvgB0 f g a : f @ F --> a -> g @ F --> 0 -> f x - g x @[x --> F] --> a. +Proof. by move=> /cvgB /[apply]; rewrite subr0. Qed. + +Lemma cvgCB0 f a : f @ F --> 0 -> a - f x @[x --> F] --> a. +Proof. by move/(@cvgBl _ a); rewrite subr0. Qed. + +Lemma cvgN0 f : f @ F --> 0 -> - f @ F --> 0. +Proof. by rewrite -{2}oppr0; exact: cvgN. Qed. + Lemma cvg_sub0 f g a : (f - g) @ F --> (0 : V) -> g @ F --> a -> f @ F --> a. Proof. by move=> Cfg Cg; have := cvgD Cfg Cg; rewrite subrK add0r; apply. From 7607dd53424ebb74098d5e3299408d8f5e0a33c0 Mon Sep 17 00:00:00 2001 From: Arthur Molina-Mounier Date: Wed, 15 Jul 2026 15:44:31 +0200 Subject: [PATCH 2/2] Update changelog --- CHANGELOG_UNRELEASED.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2d85fdc0a5..ee32fdf6d9 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -234,6 +234,13 @@ - in `measurable_structure.v`: + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable` +- in file `normed_module.v`, + + new lemmas `cvg1MC`, `cvg1M`, `cvgCM1`, `cvgM1`, `cvg0MC`, `cvg0M`, + `cvgCM0`, and `cvgM0`. +- in file `pseudometric_normed_Zmodule.v`, + + new lemmas `cvgDl`, `cvgDr`, `cvgBl`, `cvgBr`, `cvg0D`, `cvg0DC`, + `cvgD0`, `cvgCD0`, `cvg0B`, `cvg0BC`, `cvgB0`, `cvgCB0`, and `cvgN0`. + ### Changed - in `realsum.v`: