English
If two dual functionals fr and fr1 are equal, then their extensions extendTo𝕜'(fr) and extendTo𝕜'(fr1) are equal.
Русский
Если два двойственных функционала fr и fr1 равны, то их расширения extendTo𝕜'(fr) и extendTo𝕜'(fr1) равны.
LaTeX
$$$fr = fr_1 \\Rightarrow \\text{extendTo}_{\\mathbb{C}}'(fr) = \\text{extendTo}_{\\mathbb{C}}'(fr_1)$$$
Lean4
/-- Extend `fr : Dual ℝ F` to `Dual 𝕜 F` in a way that will also be continuous and have its norm
(as a continuous linear map) equal to `‖fr‖` when `fr` is itself continuous on a normed space. -/
noncomputable def extendTo𝕜' (fr : Dual ℝ F) : Dual 𝕜 F :=
letI fc : F → 𝕜 := fun x => (fr x : 𝕜) - (I : 𝕜) * fr ((I : 𝕜) • x)
have add (x y) : fc (x + y) = fc x + fc y :=
by
simp only [fc, smul_add, map_add, mul_add]
abel
have A (c : ℝ) (x : F) : (fr ((c : 𝕜) • x) : 𝕜) = (c : 𝕜) * (fr x : 𝕜) := by simp
have smul_ℝ (c : ℝ) (x : F) : fc ((c : 𝕜) • x) = (c : 𝕜) * fc x := by
simp only [fc, A, smul_comm I, mul_comm I, mul_sub, mul_assoc]
have smul_I (x : F) : fc ((I : 𝕜) • x) = (I : 𝕜) * fc x :=
by
obtain (h | h) := @I_mul_I_ax 𝕜 _
· simp [fc, h]
· simp [fc, mul_sub, ← mul_assoc, smul_smul, h, add_comm]
have smul_𝕜 (c : 𝕜) (x : F) : fc (c • x) = c • fc x :=
by
rw [← re_add_im c]
simp only [add_smul, ← smul_smul, add, smul_ℝ, smul_I, ← mul_assoc, smul_eq_mul, add_mul]
{ toFun := fc
map_add' := add
map_smul' := smul_𝕜 }
