Skip to content

Conversation

Tragicus
Copy link
Collaborator

@Tragicus Tragicus commented Aug 23, 2025

Motivation for this change

A general continuity lemma for bigops.

Checklist
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

  • PRs with several commits that make sense individually and that
    all compile are preferentially merged into master.
  • PRs with disorganized commits are very likely to be squash-rebased.
Reminder to reviewers

@Tragicus Tragicus force-pushed the continuous_big branch 3 times, most recently from 4c6067c to 7edc06e Compare August 23, 2025 09:39
@affeldt-aist
Copy link
Member

I am a bit surprised to see a mix of { ... } and [ ... ] in the arguments. We very rarely use [ ... ]. What is the rationale?


Lemma cvg_big (T : Type) (U : topologicalType) [F : set_system T] [I : Type]
(r : seq I) (P : pred I) (Ff : I -> T -> U) (Fa : I -> U)
(op : U -> U -> U) (x0 : U):
Copy link
Member

Choose a reason for hiding this comment

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

Suggested change
(op : U -> U -> U) (x0 : U):
(op : U -> U -> U) (x0 : U) :

under eq_cvg do rewrite big_nil.
exact: cvg_cst.
rewrite big_cons (eq_cvg _ _ (fun x => big_cons _ _ _ _ _ _)).
case/boolP: (P x) => // Px.
Copy link
Member

@affeldt-aist affeldt-aist Aug 23, 2025

Choose a reason for hiding this comment

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

Suggested change
case/boolP: (P x) => // Px.
case: ifPn => // Px.

exact: cvg_cst.
rewrite big_cons (eq_cvg _ _ (fun x => big_cons _ _ _ _ _ _)).
case/boolP: (P x) => // Px.
apply: (@cvg_comp _ _ _ (fun x1 => (Ff x x1, \big[op/x0]_(j <- r | P j) Ff j x1)) _ _ (nbhs (Fa x, \big[op/x0]_(j <- r | P j) Fa j)) _ _ (continuous_curry_cvg opC0)).
Copy link
Member

Choose a reason for hiding this comment

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

Suggested change
apply: (@cvg_comp _ _ _ (fun x1 => (Ff x x1, \big[op/x0]_(j <- r | P j) Ff j x1)) _ _ (nbhs (Fa x, \big[op/x0]_(j <- r | P j) Fa j)) _ _ (continuous_curry_cvg opC0)).
apply: (@cvg_comp _ _ _
(fun x1 => (Ff x x1, \big[op/x0]_(j <- r | P j) Ff j x1)) _ _
(nbhs (Fa x, \big[op/x0]_(j <- r | P j) Fa j)) _ _
(continuous_curry_cvg opC0)).

Copy link
Member

Choose a reason for hiding this comment

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

Just because I couldn't read it easily ^_^

@affeldt-aist
Copy link
Member

I am a bit surprised to see a mix of { ... } and [ ... ] in the arguments. We very rarely use [ ... ]. What is the rationale?

Also, since this is a section, we can maybe exploit some sharing with Context or Variable since, for example, both lemmas use an op binary operator over a topological space, etc.

@Tragicus
Copy link
Collaborator Author

I am a bit surprised to see a mix of { ... } and [ ... ] in the arguments. We very rarely use [ ... ]. What is the rationale?

That is an excellent question. I guess I saw other lemmas doing it and I assumed this was the way to go.

@Tragicus
Copy link
Collaborator Author

I am a bit surprised to see a mix of { ... } and [ ... ] in the arguments. We very rarely use [ ... ]. What is the rationale?

Also, since this is a section, we can maybe exploit some sharing with Context or Variable since, for example, both lemmas use an op binary operator over a topological space, etc.

Would that not mess with the order of the arguments?

@affeldt-aist
Copy link
Member

I am a bit surprised to see a mix of { ... } and [ ... ] in the arguments. We very rarely use [ ... ]. What is the rationale?

Also, since this is a section, we can maybe exploit some sharing with Context or Variable since, for example, both lemmas use an op binary operator over a topological space, etc.

Would that not mess with the order of the arguments?

It will have an impact on it.
I have prepared such a commit for the sake of concreteness:
affeldt-aist@f613919
(I created a continuous_big branch on my fork because I couldn't push on yours.)
The idea is to use sharing of arguments and hypotheses to lighten the statements
and highlight the differences.
(There is also an artificial suff step to compensate for the unfortunate loss of notations)

What do you think?

Co-authored-by: Reynald Affeldt <[email protected]>
@Tragicus
Copy link
Collaborator Author

I took your commit, I am surprised you can not push on my branch. I am more convinced by uniformity of statements than sharing of arguments, but this is fine, I guess. The suff is not really needed.

@affeldt-aist affeldt-aist added this to the 1.14.0 milestone Sep 11, 2025
@affeldt-aist affeldt-aist added the enhancement ✨ This issue/PR is about adding new features enhancing the library label Sep 11, 2025
@affeldt-aist affeldt-aist self-requested a review September 11, 2025 13:25
@affeldt-aist affeldt-aist merged commit 923370c into math-comp:master Sep 11, 2025
66 of 67 checks passed
hoheinzollern pushed a commit to hoheinzollern/analysis that referenced this pull request Sep 22, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement ✨ This issue/PR is about adding new features enhancing the library

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants