Commit 2026-03-23 18:23 5197eece

feat(Analysis/Normed/Module/WeakDual): register bornology and boundedness API (#36332)

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