normed type neighborhood lemmas

[nmolinamounier]

Motivation for this change

Split from #2023. Depends on #2024 and #2027.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md
• Merge Utility lemmas in filter.v #2024
• Merge New topology lemmas #2027

• 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

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

(not yet reviewed but rebased)

[affeldt-aist]

The statement of near_shiftE and nbhsDl are the same but on different structures that maybe ought to share an interface. This is an observation that has already been done for other lemmas, so maybe this is time to reconsider the hierarchy of mathematical structures to factorize code.

See
https://github.com/math-comp/analysis/blob/master/theories/normedtype_theory/tvs.v#L122-L128

NB(2026-10-01): The comment pointed at has been addressed by PR #2112

[affeldt-aist]

The duplication of code is calling for a more in-depth review (which might end up in adding structures) so we postpone to the next release (fyi: @mkerjean )

[affeldt-aist]

Just a thought:
We long had PseudoMetricNormedZmod defined with a numDomainType parameter.
Recently, we have added PseudoMetricNormedZmod0 and made PseudoMetricNormedZmod derive from Metric.
In fact, as a consequence, many lemmas can be changed from PseudoMetricNormedZmod down to PseudoMetricNormedZmod0 without impacting the code.
Which makes me wonder whether we shouldn't make PseudoMetricNormedZmod have a numFieldType as a parameter instead of sticking to numDomainType: this actually comes in the way when trying to refactor the code as hinted at in this conversation.

I retract this comment because the setting is a bit different now that we are heading for getting rid of UniformLmodule (see PR #2112 ).

[mkerjean]

I'm happy to do a review but I'm lacking a bit of context. Why are these lemmas duplicated ? What's the goal of this PR ?

[affeldt-aist]

I can't find uses ofnearZE and near_shiftE in this PR and or in other PRs that come after, is that ok?

[affeldt-aist]

That looks ok. Lemmas seem reasonable but they lack context to be sure. For example, how are near_shiftE and nearZE used (I couldn't find in subsequent PRs)? Should the statement of near_shiftE rather be written like nbhsDl (<- vs. =)? Shouldn't them be renamed to have matching names (I think so: can you propose a preferred name?)? fyi: @mkerjean (this PR is loosely related to PR #2112 )

[affeldt-aist]

That looks ok. Lemmas seem reasonable but they lack context to be sure. For example, how are near_shiftE and nearZE used (I couldn't find in subsequent PRs)? Should the statement of near_shiftE rather be written like nbhsDl (<- vs. =)? Shouldn't them be renamed to have matching names (I think so: can you propose a preferred name?)? fyi: @mkerjean (this PR is loosely related to PR #2112 )

ping @nmolinamounier ?

[nmolinamounier]

I was kind of surprised to realize some of these weren't used in my other PRs; chances are, they were used in some dead code that I later removed. As for usage, I don't really know how to describe it better than turning a goal of the form \forall y \near (x + a), P y into \forall y \near x, P (y + a) and \forall y \near c * x, P y into \forall y, P (c * y). I agree that <- (or even better, <->) would be better for the statements.

I think in my work it came up when working with derivatives : all of the relevant limits are stated around 0, but a derivative may be taken around any point. Thinking of it, it would perhaps be a good idea to have analogous results for cvg_to, in the same way as existing lemmas for -%R.

[affeldt-aist]

Would you consider removing (at least temporarily) the unused lemma from your PR?

[affeldt-aist]

All the lemmas look useful. Moreover, this PR has helped further motivate PR #2112.