[Merged by Bors] - feat(Analysis/LocallyConvex/WeakDual): Weak Representation Theorem#35422
[Merged by Bors] - feat(Analysis/LocallyConvex/WeakDual): Weak Representation Theorem#35422PrParadoxy wants to merge 4 commits intoleanprover-community:masterfrom
Conversation
github-actions
bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary 56d691c029Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
✅ PR Title Formatted CorrectlyThe title of this PR has been updated to match our commit style conventions. |
PrParadoxy
changed the title
…35422) This PR uses the material in Topology/Algebra/Module/WeakBilin.lean from the unfinished PR #26345 by @mans0954. Given a bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜`, every continuous functional on `E` endowed with the `σ(E, F; B)`-topology is of the form `x ↦ B(x, y)` for some `y : F`. The result doesn't generally seem to be named, but Narici-Beckenstein's "Topological Vector Spaces" calls it the "weak representation theorem", a term we have used for the docstring. Co-authored-by: David Gross <[email protected]>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
…eanprover-community#35422) This PR uses the material in Topology/Algebra/Module/WeakBilin.lean from the unfinished PR leanprover-community#26345 by @mans0954. Given a bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜`, every continuous functional on `E` endowed with the `σ(E, F; B)`-topology is of the form `x ↦ B(x, y)` for some `y : F`. The result doesn't generally seem to be named, but Narici-Beckenstein's "Topological Vector Spaces" calls it the "weak representation theorem", a term we have used for the docstring. Co-authored-by: David Gross <[email protected]>
3 participants
This PR uses the material in Topology/Algebra/Module/WeakBilin.lean from the unfinished PR #26345 by @mans0954.
Given a bilinear form
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜, every continuous functional onEendowed with theσ(E, F; B)-topology is of the formx ↦ B(x, y)for somey : F.The result doesn't generally seem to be named, but Narici-Beckenstein's "Topological Vector Spaces" calls it the "weak representation theorem", a term we have used for the docstring.
Changes compared to #26345:
Analysis/LocallyConvex/WeakDual, as this is where the supporting resultmem_span_iff_continuousended up. (C.f. PR [Merged by Bors] - feat(Analysis/LocallyConvex/WeakDual): characterise the span of some functionals with continuity #27316)dualEmbedding_surjectiveis now much shorter and should no longer rely on defeqs.Co-authored-by: Christopher Hoskin