Skip to content

normed module identity convergence lemmas #2029

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
amolinamounier wants to merge 3 commits into
base: master
Choose a base branch
from
+71 −0
Open

normed module identity convergence lemmas #2029

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
75a0948
normed module identity convergence lemmas
amolinamounier Jul 15, 2026
7607dd5
Update changelog
amolinamounier Jul 15, 2026
b28ac89
Merge branch 'master' into identity_cvg_lemmas
amolinamounier Jul 22, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -243,6 +243,7 @@
`within_continuousMl`, and `within_continuousMr`
- in `pseudometric_normed_Zmodule.v`
+ new lemma `within_continuousN`

- in `lebesgue_stieltjes_measure.v`:
+ module `MeasurableRocitv`
+ definition `open_type`
Expand All @@ -260,6 +261,13 @@
- in `real_interval.v`:
+ lemma `set1_bigcap_oo`

- in `normed_module.v`,
+ new lemmas `cvg1MC`, `cvg1M`, `cvgCM1`, `cvgM1`, `cvg0MC`, `cvg0M`,
`cvgCM0`, and `cvgM0`.
- in `pseudometric_normed_Zmodule.v`,
+ new lemmas `cvgDl`, `cvgDr`, `cvgBl`, `cvgBr`, `cvg0D`, `cvg0DC`,
`cvgD0`, `cvgCD0`, `cvg0B`, `cvg0BC`, `cvgB0`, `cvgCB0`, and `cvgN0`.

### Changed

- in `realsum.v`:
Expand Down
24 changes: 24 additions & 0 deletions theories/normedtype_theory/normed_module.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -648,6 +648,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.

Expand Down
39 changes: 39 additions & 0 deletions theories/normedtype_theory/pseudometric_normed_Zmodule.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

@affeldt-aist affeldt-aist Jul 21, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What about cvgcstD to suggest that the constant is on the left (and cvgDcst instead of cvgDr)?
Because cvgDl does not really say what is on the left.

But in fact I am not sure that cvgDl, cvgDr, cvgBl, cvgBr are very useful,
because it is just cvg{D,B} with cvg_cst.
The application of cvg_cst should maybe be automatic instead
(and maybe it was thought as such because there is actually a Hint in topology_structure.v but it is not working here). Fixing the latter Hint could be better.

@amolinamounier amolinamounier Jul 21, 2026

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, I think that would be a better idea; I did find it a bit odd that cvg_cst didn't trigger automatically.

@affeldt-aist affeldt-aist Jul 22, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Trying to fix that: #2046

@affeldt-aist affeldt-aist Jul 28, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So now cvg_cst and is_cvg_cst are true hints, this PR can maybe be simplified.

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.
Expand Down
Loading