[Merged by Bors] - feat(Analysis/Normed/Module/WeakDual): register bornology and boundedness API

[mike1729]

Description

This PR registers Bornology instance and introduces a boundedness API as discussed on Zulip.

Main additions

• WeakDual.instBornology: Bornology instance on WeakDual 𝕜 E inherited from StrongDual 𝕜 E via inferInstanceAs. This makes IsBounded available directly on weak dual sets, where boundedness means operator-norm boundedness.

• isBounded_iff_isVonNBounded: For normed spaces over ℝ or ℂ, norm-boundedness and weak-* von Neumann boundedness coincide (via Banach–Steinhaus).

• isBounded_polar and isBounded_closedBall: Standalone lemmas replacing repeated inline isBounded_toStrongDual_preimage_iff_isBounded.mpr ... patterns.

• Simp lemmas: isBounded_toStrongDual_preimage_iff_isBounded and isBounded_toWeakDual_preimage_iff_isBounded for translating between weak and strong dual boundedness.

API simplification

The existing lemmas isClosed_image_coe_of_bounded_of_closed, isCompact_of_bounded_of_closed, and isSeqCompact_of_isBounded_of_isClosed now take IsBounded s directly instead of the more verbose IsBounded (StrongDual.toWeakDual ⁻¹' s), since the two are definitionally equal with the new bornology instance.

Minor changes

• Replaced grind tactic usage with explicit term
• Fixed deprecation dates from 2024-11-19 to 2025-11-19
• Renamed local variable F to E for consistency with the rest of the file
• Added comprehensive module and declaration docstrings

---

• depends on: —
• modifies an existing declaration: yes (simplified signatures of isClosed_image_coe_of_bounded_of_closed, isCompact_of_bounded_of_closed, isSeqCompact_of_isBounded_of_isClosed)
• adds new declarations: yes (instBornology, isBounded_toStrongDual_preimage_iff_isBounded, isBounded_toWeakDual_preimage_iff_isBounded, isVonNBounded_iff_pointwise_bounded, isBounded_iff_isVonNBounded, isBounded_iff_pointwise_bounded, isBounded_closedBall, isBounded_polar)

---

Open in Gitpod
-->

[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 6d1799a50b

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Normed.Module.WeakDual	2162	2168	+6 (+0.28%)
Mathlib.Analysis.Normed.Algebra.Basic	2265	2271	+6 (+0.26%)

Import changes for all files

Files	Import difference
19 files Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.CStarAlgebra.CStarMatrix Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order 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.Unitary.Connected Mathlib.Analysis.CStarAlgebra.Unitary.Span Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order	3
Mathlib.Analysis.Normed.Algebra.Basic Mathlib.Analysis.Normed.Module.WeakDual	6

---

Declarations diff

+ instBornology
+ isBounded_closedBall
+ isBounded_iff_isVonNBounded
+ isBounded_polar
+ isBounded_toStrongDual_preimage_iff_isBounded
+ isBounded_toWeakDual_preimage_iff_isBounded
+ 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
8700	4	backward.isDefEq

Current commit e52bb3dff4
Reference commit 6d1799a50b

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).

[j-loreaux]

looks reasonable, but see my comments. If I have time, I will take care of the simp issue I mentioned, but I will check to see if you have tackled it first. And if I do, I will post on this PR before I embark on it, so that we don't duplicate effort.

[j-loreaux]

also please update the PR description to match now that things have changed slightly.

[j-loreaux]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-Build Step
• ci (staging) / Build
• ci (staging) / Post-CI job
• ci (staging) / Lint style