[Merged by Bors] - feat: define the weak operator topology

[dupuisf]

This PR defines the weak operator topology on maps between normed spaces and proves some of its basic properties. It creates a type copy of E →L[𝕜] F endowed with the WOT rather than the norm topology.

Along the way, we define several lemmas that are useful for proving properties of a topology that is induced by a bundled hom.

Note: I've defined the global notation E →WOT[𝕜] F for the type copy; I don't think this is likely to collide with anything else, but I can make it scoped if this is deemed preferable.

Co-authored-by: Jireh Loreaux [email protected]

---

[github-actions]

PR summary a156413ac6

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.NormedSpace.WeakOperatorTopology	1512
Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology	1558

---

Declarations diff

+ ContinuousInv.induced
+ ContinuousLinearMap.continuous_toWOT
+ ContinuousLinearMap.toWOTCLM
+ ContinuousLinearMapWOT
+ ContinuousMul.induced
+ ContinuousSMul.induced
+ _root_.ContinuousLinearMap.toWOT
+ _root_.ContinuousLinearMap.toWOT_apply
+ add_apply
+ basisSets_mem_nhds
+ continuous_dual_apply
+ continuous_inducingFn
+ continuous_of_dual_apply_continuous
+ embedding_inducingFn
+ ext
+ ext_dual
+ ext_dual_iff
+ ext_iff
+ ext_inner
+ ext_inner_iff
+ hasBasis_seminorms
+ inducingFn
+ instAddCommGroup
+ instContinuousAdd
+ instContinuousLinearMapClass
+ instContinuousNeg
+ instContinuousSMul
+ instFunLike
+ instLocallyConvexSpace
+ instModule
+ instT3Space
+ instTopologicalAddGroup
+ instTopologicalSpace
+ instUniformAddGroup
+ instUniformSpace
+ le_nhds_iff_forall_dual_apply_le_nhds
+ le_nhds_iff_forall_inner_apply_le_nhds
+ neg_apply
+ seminorm
+ seminormFamily
+ smul_apply
+ sub_apply
+ tendsto_iff_forall_dual_apply_tendsto
+ tendsto_iff_forall_inner_apply_tendsto
+ withSeminorms
+ zero_apply

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[j-loreaux]

This is a first pass. I may have more thoughts about simplifying the proof of the hasBasis theorem later. This mostly looks really nice though, thanks!

[dupuisf]

Thanks @j-loreaux ! Regarding the HasBasis proof, note that I mostly cribbed it from LinearMap.hasBasis_weakBilin; if you have ideas to simplify it, they probably apply there as well!

[j-loreaux]

Does ext behave well where there are competing ext lemmas? If we have both this and ext_dual_iff.mpr tagged as ext, they would both apply in the Hilbert space case.

I think this was a problem at one point, but I don't think it is any longer. I believe we have resurrected the Lean 3 behavior where the one declared later has priority, so in this case, the inner product version. You could test it though.

[j-loreaux]

If you want, you can save completeness for a future PR.

bors d+

[mathlib-bors]

✌️ dupuisf can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[dupuisf]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style