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

## Description

This PR registers `Bornology` instance and introduces a boundedness API as discussed [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/instBornology.20for.20WeakSpace.20and.20WeakDual/with/577457935).

### 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

Author: mike1729

Mathlib/Analysis/Normed/Algebra/Basic.lean

@@ -62,7 +62,7 @@ instance [ProperSpace 𝕜] : CompactSpace (characterSpace 𝕜 A) := by
     intro φ hφ
     rw [Set.mem_preimage, mem_closedBall_zero_iff]
     exact (norm_le_norm_one ⟨φ, ⟨hφ.1, hφ.2⟩⟩ :)
-  exact (isCompact_closedBall 𝕜 0 _).of_isClosed_subset CharacterSpace.isClosed h
+  exact (isCompact_closedBall 0 _).of_isClosed_subset CharacterSpace.isClosed h
 
 end CharacterSpace