feat(Analysis/Normed/Module): add bornology and T2 instances for WeakSpace

[mike1729]

Register the norm bornology on WeakSpace 𝕜 E and prove that it coincides with the von Neumann bornology of the weak topology.

New declarations

• WeakSpace.instBornology: norm bornology inherited from E.
• WeakSpace.instT2Space: Hausdorff via Hahn–Banach separation.
• WeakSpace.norm_topology_le_weakSpace_topology: the weak topology is coarser than the norm topology.
• WeakSpace.isBounded_iff_isVonNBounded: norm-boundedness equals weak von Neumann boundedness (no [CompleteSpace E] needed).

---

[github-actions]

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. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

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 awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

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.

[github-actions]

PR summary 58f63c64f7

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.LocallyConvex.WeakSpace	2003	2009	+6 (+0.30%)

Import changes for all files

Files	Import difference
Mathlib.Analysis.LocallyConvex.WeakDual	-1805
74 files Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.CStarAlgebra.CStarMatrix Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.CStarAlgebra.PositiveLinearMap Mathlib.Analysis.CStarAlgebra.Projection Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Analysis.CStarAlgebra.Unitary.Connected Mathlib.Analysis.CStarAlgebra.Unitary.Span Mathlib.Analysis.Distribution.FourierMultiplier Mathlib.Analysis.Distribution.TemperedDistribution Mathlib.Analysis.Fourier.LpSpace Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.Analysis.InnerProductSpace.Positive Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.Analysis.InnerProductSpace.Reproducing Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.Analysis.InnerProductSpace.Trace Mathlib.Analysis.LocallyConvex.PointwiseConvergence Mathlib.Analysis.Matrix.HermitianFunctionalCalculus Mathlib.Analysis.Matrix.LDL Mathlib.Analysis.Matrix.Order Mathlib.Analysis.Matrix.PosDef Mathlib.Analysis.Matrix.Spectrum Mathlib.Analysis.Normed.Algebra.Basic Mathlib.Analysis.Normed.Algebra.GelfandFormula Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Analysis.Normed.Module.WeakDual Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.MeasureTheory.Function.ConvergenceInDistribution Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Measure.FiniteMeasurePi Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.MeasureTheory.Measure.LevyConvergence Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.MeasureTheory.Measure.Prokhorov Mathlib.MeasureTheory.Measure.TightNormed Mathlib.MeasureTheory.Measure.Tight Mathlib.Probability.Distributions.Gaussian.CharFun Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence Mathlib.Probability.Distributions.Gaussian.Multivariate Mathlib.Probability.Moments.CovarianceBilin Mathlib.Topology.Algebra.Module.CharacterSpace Mathlib.Topology.Algebra.Module.PointwiseConvergence Mathlib.Topology.Algebra.Module.WeakDual Mathlib.Topology.ContinuousMap.Ideals	1
Mathlib.Analysis.LocallyConvex.WeakSpace	6
Mathlib.Topology.Algebra.Module.WeakSpace (new file)	1209
Mathlib.Analysis.LocallyConvex.WeakBilin	1805
Mathlib.Analysis.Normed.Module.WeakSpace (new file)	2173

---

Declarations diff

+ instBornology
+ instT2Space
+ isBounded_iff_isVonNBounded
+ isBounded_toE_preimage
+ isBounded_toWeakSpace_preimage
+ norm_topology_le_weakSpace_topology
+ seminormFamily
+ seminormFamily_apply
+ withSeminorms

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (4.00, 0.00)

Current number	Change	Type
9509	4	backward.isDefEq

Current commit f35bacec01
Reference commit 58f63c64f7

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

---

note: file Mathlib/Analysis/LocallyConvex/WeakDual.lean` was renamed to `Mathlib/Analysis/LocallyConvex/WeakBilin.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

[mathlib-dependent-issues]

This PR/issue depends on:

• refactor(LocallyConvex,Topology): split WeakDual/WeakSpace and rename WeakBilin #37027
  By Dependent Issues (🤖). Happy coding!