English
If f: p →L[𝕜] F has finite-dimensional range, there exists a g: E →L[𝕜] F with f = g ∘ p.subtypeL (extension of f to E).
Русский
Если f: p →L[𝕜] F имеет конечномерный диапазон, существует непрерывно линейное отображение g: E →L[𝕜] F такое, что f = g ∘ p.subtypeL (расширение f на E).
LaTeX
$$$\\exists g: E \\toL[𝕜] F,\\ f = g \\circ p.subtypeL$$$
Lean4
/-- **Hahn-Banach theorem** for continuous linear functions over `𝕜`
satisfying `IsRCLikeNormedField 𝕜`. -/
theorem exists_extension_norm_eq (p : Subspace 𝕜 E) (f : StrongDual 𝕜 p) :
∃ g : StrongDual 𝕜 E, (∀ x : p, g x = f x) ∧ ‖g‖ = ‖f‖ :=
by
letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
letI : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
letI : IsScalarTower ℝ 𝕜 E := RestrictScalars.isScalarTower _ _ _
letI : NormedSpace ℝ E :=
NormedSpace.restrictScalars _ 𝕜
_
-- Let `fr: StrongDual ℝ p` be the real part of `f`.
let fr :=
reCLM.comp
(f.restrictScalars ℝ)
-- Use the real version to get a norm-preserving extension of `fr`, which
-- we'll call `g : StrongDual ℝ E`.
rcases Real.exists_extension_norm_eq (p.restrictScalars ℝ) fr with
⟨g, ⟨hextends, hnormeq⟩⟩
-- Now `g` can be extended to the `StrongDual 𝕜 E` we need.
refine
⟨g.extendTo𝕜, ?_⟩
-- It is an extension of `f`.
have h : ∀ x : p, g.extendTo𝕜 x = f x := by
intro x
rw [ContinuousLinearMap.extendTo𝕜_apply, ← Submodule.coe_smul]
-- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
-- The goal has a coercion from `RestrictScalars ℝ 𝕜 StrongDual ℝ E`, but
-- `hextends` involves a coercion from `StrongDual ℝ E`.
erw [hextends]
erw [hextends]
have : (fr x : 𝕜) - I * ↑(fr ((I : 𝕜) • x)) = (re (f x) : 𝕜) - (I : 𝕜) * re (f ((I : 𝕜) • x)) := by
rfl
-- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
erw [this]
apply ext
·
simp only [add_zero, Algebra.id.smul_eq_mul, I_re, ofReal_im, AddMonoidHom.map_add, zero_sub, I_im', zero_mul,
ofReal_re, sub_zero, mul_neg, ofReal_neg, mul_re, mul_zero, sub_neg_eq_add, ContinuousLinearMap.map_smul]
·
simp only [Algebra.id.smul_eq_mul, I_re, ofReal_im, AddMonoidHom.map_add, zero_sub, I_im', zero_mul, ofReal_re,
mul_neg, mul_im, zero_add, ofReal_neg, mul_re, sub_neg_eq_add, ContinuousLinearMap.map_smul]
-- And we derive the equality of the norms by bounding on both sides.
refine ⟨h, le_antisymm ?_ ?_⟩
·
calc
‖g.extendTo𝕜‖ = ‖g‖ := g.norm_extendTo𝕜
_ = ‖fr‖ := hnormeq
_ ≤ ‖reCLM‖ * ‖f‖ := (ContinuousLinearMap.opNorm_comp_le _ _)
_ = ‖f‖ := by rw [reCLM_norm, one_mul]
· exact f.opNorm_le_bound g.extendTo𝕜.opNorm_nonneg fun x => h x ▸ g.extendTo𝕜.le_opNorm x
