-
Notifications
You must be signed in to change notification settings - Fork 259
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.
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
[Merged by Bors] - feat(Analysis/LocallyConvex/WithSeminorms): characterize continuous seminorms #5501
Conversation
bors r+ |
…eminorms (#5501) This shows that, if the topology of `E` is defined by some family of seminorms `p`, then a seminorm `q` is continuous iff `∃ s : Finset ι, ∃ C : ℝ≥0, C ≠ 0 ∧ q ≤ C • s.sup p`. Via [Seminorm.continuous_iff_continuous_comp](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/LocallyConvex/WithSeminorms.html#Seminorm.continuous_iff_continuous_comp) this gives the converse of [Seminorm.continuous_from_bounded](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/LocallyConvex/WithSeminorms.html#Seminorm.continuous_from_bounded) and hence a characterization of continuous linear maps between such spaces. To do that, we restate all of the "bound of shell" lemmas in terms of seminorms, which needs changing some imports, but I've checked the current state of the port and this should not cause too much trouble since most of the touched files are already ported so we can changes the imports in mathlib4 too. The `WithSeminorms` file needs a naming/dot notation refactor at some point, because the naming scheme is neither predictable nor convenient to use, but this PR is already large enough.
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
…eminorms (#5501) This shows that, if the topology of `E` is defined by some family of seminorms `p`, then a seminorm `q` is continuous iff `∃ s : Finset ι, ∃ C : ℝ≥0, C ≠ 0 ∧ q ≤ C • s.sup p`. Via [Seminorm.continuous_iff_continuous_comp](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/LocallyConvex/WithSeminorms.html#Seminorm.continuous_iff_continuous_comp) this gives the converse of [Seminorm.continuous_from_bounded](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/LocallyConvex/WithSeminorms.html#Seminorm.continuous_from_bounded) and hence a characterization of continuous linear maps between such spaces. To do that, we restate all of the "bound of shell" lemmas in terms of seminorms, which needs changing some imports, but I've checked the current state of the port and this should not cause too much trouble since most of the touched files are already ported so we can changes the imports in mathlib4 too. The `WithSeminorms` file needs a naming/dot notation refactor at some point, because the naming scheme is neither predictable nor convenient to use, but this PR is already large enough.
…eminorms (#5501) This shows that, if the topology of `E` is defined by some family of seminorms `p`, then a seminorm `q` is continuous iff `∃ s : Finset ι, ∃ C : ℝ≥0, C ≠ 0 ∧ q ≤ C • s.sup p`. Via [Seminorm.continuous_iff_continuous_comp](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/LocallyConvex/WithSeminorms.html#Seminorm.continuous_iff_continuous_comp) this gives the converse of [Seminorm.continuous_from_bounded](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/LocallyConvex/WithSeminorms.html#Seminorm.continuous_from_bounded) and hence a characterization of continuous linear maps between such spaces. To do that, we restate all of the "bound of shell" lemmas in terms of seminorms, which needs changing some imports, but I've checked the current state of the port and this should not cause too much trouble since most of the touched files are already ported so we can changes the imports in mathlib4 too. The `WithSeminorms` file needs a naming/dot notation refactor at some point, because the naming scheme is neither predictable nor convenient to use, but this PR is already large enough.
This shows that, if the topology of
E
is defined by some family of seminormsp
, then a seminormq
is continuous iff∃ s : Finset ι, ∃ C : ℝ≥0, C ≠ 0 ∧ q ≤ C • s.sup p
. Via Seminorm.continuous_iff_continuous_comp this gives the converse of Seminorm.continuous_from_bounded and hence a characterization of continuous linear maps between such spaces.To do that, we restate all of the "bound of shell" lemmas in terms of seminorms, which needs changing some imports, but I've checked the current state of the port and this should not cause too much trouble since most of the touched files are already ported so we can changes the imports in mathlib4 too.
The
WithSeminorms
file needs a naming/dot notation refactor at some point, because the naming scheme is neither predictable nor convenient to use, but this PR is already large enough.This is a manual port of leanprover-community/mathlib#17298 which was already
maintainer merge
-d andbors delegate
-d, but I thought it would be easier to just make a new Mathlib4 PR.There's one thing I'm not sure about: I moved some lemmas to other files (and I moved the
#align
s with them), will that be a problem for mathport? If so we should also merge the Mathlib3 PR, otherwise I can just close it.