English
If the dual is bounded on a set, a small scalar multiple lies in the polar.
Русский
Если линейный функционал ограничен на множество, то маленькое скалярное умножение принадлежит полю.
LaTeX
$$$(\\forall z, z \\in s \\Rightarrow \\|x'(z)\\| \\le \\|c\\|)$ implies $c^{-1} \\cdot x' \\in \\operatorname{polar} s$$$
Lean4
/-- If `x'` is a `StrongDual 𝕜 E` element such that the norms `‖x' z‖` are bounded for `z ∈ s`, then
a small scalar multiple of `x'` is in `polar 𝕜 s`. -/
theorem smul_mem_polar {s : Set E} {x' : StrongDual 𝕜 E} {c : 𝕜} (hc : ∀ z, z ∈ s → ‖x' z‖ ≤ ‖c‖) :
c⁻¹ • x' ∈ StrongDual.polar 𝕜 s := by
by_cases c_zero : c = 0
· simp only [c_zero, inv_zero, zero_smul]
exact (topDualPairing 𝕜 E).flip.zero_mem_polar _
have eq : ∀ z, ‖c⁻¹ • x' z‖ = ‖c⁻¹‖ * ‖x' z‖ := fun z => norm_smul c⁻¹ _
have le : ∀ z, z ∈ s → ‖c⁻¹ • x' z‖ ≤ ‖c⁻¹‖ * ‖c‖ := by
intro z hzs
rw [eq z]
apply mul_le_mul (le_of_eq rfl) (hc z hzs) (norm_nonneg _) (norm_nonneg _)
have cancel : ‖c⁻¹‖ * ‖c‖ = 1 := by simp only [c_zero, norm_eq_zero, Ne, not_false_iff, inv_mul_cancel₀, norm_inv]
rwa [cancel] at le
