feat(topology/bounded_continuous_function): composition of limits when uniform convergence #2260
Conversation
…n uniform convergence
sgouezel
added
the
awaiting-review
|
This file lacks a good module docstring. It also contains stuff that have nothing to do with bounded functions, like the lemma added by this PR. Should it go somewhere else? I'm also a bit surprised to see all those uniform convergence lemmas stated and proved for metric spaces only. Don't they have version in general uniform spaces that could be applied to derive the metric statements? |
|
I proved the lemmas in the versions I needed, but you are right that it would be better to have a more general version on uniform spaces. Let me give it a shot. |
sgouezel
added
WIP
|
I have now properly defined uniform convergence of a sequence of functions taking values in a uniform space, together with the usual variations (locally uniform convergence, locally uniform convergence on a set, and so on), and proved the main theorems in this setting (most notably that continuity is preserved at the limit). |
sgouezel
added
awaiting-review
| uniformly by continuous functions. We give various versions, within a set or the whole space, at | ||
| a single point or at all points, with locally uniform approximation or uniform approximation. All | ||
| the statements are derived from a statement about locally uniform approximation within a set at | ||
| a point, called `continuous_within_at_of_locally_uniform_approx_of_continuous_within_at`. -/ |
There was a problem hiding this comment.
Should we have a definition for this L assumption?
There was a problem hiding this comment.
I am not sure. I don't think this will show up often (although I have stated the lemmas in this version because it seems to be the minimal version where it holds, and one never knows if this will be needed some day). I would say let's keep it like that, and if it turns out that people use this version then we can add a name.
PatrickMassot
added
ready-to-merge
…n uniform convergence (leanprover-community#2260) * feat(topology/bounded_continuous_function): composition of limits when uniform convergence * better statement * uniform space version * cleanup * fix linter * reviewer's comments Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
…n uniform convergence (leanprover-community#2260) * feat(topology/bounded_continuous_function): composition of limits when uniform convergence * better statement * uniform space version * cleanup * fix linter * reviewer's comments Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
…n uniform convergence (leanprover-community#2260) * feat(topology/bounded_continuous_function): composition of limits when uniform convergence * better statement * uniform space version * cleanup * fix linter * reviewer's comments Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Old version of the PR:
If
Fₙconverges uniformly to a functionfwhich is continuous atx, anduₙtends tox,then
Fₙ (uₙ)tends tof xNew version:
We formulate the notion of uniform convergence of a sequence of functions taking values in a uniform space, together with variations (locally uniform convergence on a set, and so on). We prove that continuity is preserved by such a limit, and also that if
Fₙconverges uniformly to a functionfwhich is continuous atx, anduₙtends tox, thenFₙ (uₙ)tends tof x. Partial implementations of these notions used to be inbounded_continuous_function.lean, only for metric spaces. I moved them to their own fileuniform_space/uniform_convergence.lean, and did a bit of cleanup of their uses.