Theory Inner_Completion
section ‹Completions of Normed Vector Spaces›
theory Inner_Completion
imports
Complex_Bounded_Operators.Complex_Inner_Product
Gromov_Hyperbolicity.Metric_Completion
begin
subsection ‹Helper lemmas›
lemma Cauchy_norm_bounded:
assumes "Cauchy X"
shows "∃B. ∀n. norm (X n) < B"
by (meson cauchy_imp_bounded assms bounded_normE_less rangeI)
lemma convergent_Cauchy_norm:
fixes u v::"nat ⇒ ('a::real_normed_vector)"
assumes "Cauchy u"
shows "convergent (λn. norm (u n))"
unfolding norm_conv_dist using convergent_Cauchy_dist assms convergent_Cauchy convergent_const
by blast
lemma Cauchy_norm_if_Cauchy:
assumes "Cauchy u"
shows "Cauchy (λn. norm (u n))"
unfolding norm_conv_dist
using assms convergent_Cauchy convergent_Cauchy_norm by auto
lemma lim_ge: "convergent f ⟹ (⋀n. f n ≥ x) ⟹ lim f ≥ x"
for x :: "'a::linorder_topology"
using LIMSEQ_le_const[of f "lim f" x] by (simp add: convergent_LIMSEQ_iff)
lemma
assumes "convergent u"
shows lim_Re: "lim (λn. Re (u n)) = Re (lim (λn. u n))"
and lim_Im: "lim (λn. Im (u n)) = Im (lim (λn. u n))"
by (intro limI tendsto_Re tendsto_Im, simp add: assms[unfolded convergent_LIMSEQ_iff])+
lemma Cauchy_sum:
fixes x1 x2 :: "nat⇒'a::real_normed_vector"
assumes "Cauchy x1" "Cauchy x2"
shows "Cauchy (x1+x2)"
proof (unfold Cauchy_def[of "x+y" for x y], intro allI impI)
fix e::real
assume "0 < e"
then
obtain M1 M3
where M: "∀m≥M1. ∀n≥M1. dist ((x1) m) ((x1) n) < e/2"
"∀m≥M3. ∀n≥M3. dist ((x2) m) ((x2) n) < e/2"
using zero_less_divide_iff zero_less_numeral
by (metis Cauchy_def assms)
let ?M = "if M1≥M3 then M1 else M3"
{ fix m n assume "m≥?M" "n≥?M"
hence mn: "m≥M1" "n≥M1" "m≥M3" "n≥M3" by presburger+
have "norm (x1 n - x1 m) + norm (x2 m - x2 n) < e"
using M mn unfolding dist_norm by fastforce
hence "norm ((x1 + x2) m - (x1 + x2) n) < e"
unfolding plus_fun_apply
by (metis add.commute add_diff_eq diff_diff_eq norm_minus_commute norm_triangle_lt)
hence "dist ((x1 + x2) m) ((x1 + x2) n) < e"
unfolding dist_norm by blast }
thus "∃M. ∀m≥M. ∀n≥M. dist ((x1 + x2) m) ((x1 + x2) n) < e"
by blast
qed
subsection ‹The Cauchy completion of a normed vector space is a Banach space.›
instantiation metric_completion :: (real_normed_vector) scaleR
begin
lift_definition scaleR_metric_completion :: "real ⇒ 'a metric_completion ⇒ 'a metric_completion"
is "λr x. λn. (scaleR r) (x n)"
using bounded_linear.Cauchy bounded_linear_scaleR_right tendsto_mult_right_zero
by (auto simp add: scaleR_diff_right[symmetric] dist_norm)
instance by standard
end
instantiation metric_completion :: (real_normed_vector) real_vector
begin
lift_definition uminus_metric_completion :: "'a metric_completion ⇒ 'a metric_completion"
is uminus
by (simp add: Cauchy_def dist_minus)
lift_definition zero_metric_completion :: "'a metric_completion"
is "λn. 0"
by (simp add: Cauchy_def)
lift_definition plus_metric_completion ::
"'a metric_completion ⇒ 'a metric_completion ⇒ 'a metric_completion"
is plus
proof (intro conjI; elim conjE)
fix x1 x2 x3 x4 :: "nat ⇒ 'a"
assume cauchy: "Cauchy x1" "Cauchy x2" "Cauchy x3" "Cauchy x4"
assume dist_conv: "(λn. dist (x1 n) (x2 n)) ⇢ 0" "(λn. dist (x3 n) (x4 n)) ⇢ 0"
show cauchy_sum: "Cauchy (x1 + x3)" "Cauchy (x2 + x4)"
using Cauchy_sum cauchy by auto
show "(λn. dist ((x1 + x3) n) ((x2 + x4) n)) ⇢ 0"
proof -
have dist_conv_add: "(λn. dist (x1 n) (x2 n) + dist (x3 n) (x4 n)) ⇢ 0"
using dist_conv tendsto_add by fastforce
show ?thesis
apply (rule tendsto_sandwich[of "λ_. 0" _ _ "λn. dist (x1 n) (x2 n) + dist (x3 n) (x4 n)"])
using dist_conv_add by (auto simp: dist_triangle_add)
qed
qed
definition minus_metric_completion ::
"'a metric_completion ⇒ 'a metric_completion ⇒ 'a metric_completion"
where "minus_metric_completion a b ≡ a + (-b)"
instance
apply intro_classes
subgoal by (transfer, simp add: Cauchy_sum Groups.add_ac)
subgoal by (transfer, simp add: Groups.add_ac Cauchy_sum)
subgoal apply transfer by (transfer, simp add: plus_fun_def)
subgoal by (transfer, simp add: Cauchy_def)
subgoal by (simp add: minus_metric_completion_def)
subgoal apply (transfer, auto)
subgoal using Cauchy_sum bounded_linear.Cauchy
bounded_linear_scaleR_right by fastforce
subgoal by (simp add: Cauchy_sum bounded_linear.Cauchy bounded_linear_scaleR_right)
subgoal by (simp add: scaleR_add_right)
done
subgoal apply (transfer, auto)
using bounded_linear.Cauchy bounded_linear_scaleR_right apply blast
using bounded_linear.Cauchy bounded_linear_scaleR_right apply (metis Cauchy_sum)
using dist_self scaleR_add_left by (metis (mono_tags, lifting) LIMSEQ_def)
subgoal by (transfer, simp add: bounded_linear.Cauchy bounded_linear_scaleR_right)
subgoal by (transfer, simp)
done
end
instantiation metric_completion :: (complex_normed_vector) scaleC
begin
lift_definition scaleC_metric_completion :: "complex ⇒ 'a metric_completion ⇒ 'a metric_completion"
is "λc x. λn. (scaleC c) (x n)"
using bounded_clinear.Cauchy bounded_clinear_scaleC_right tendsto_mult_right_zero
by (auto simp add: scaleC_diff_right[symmetric] dist_norm)
instance
apply intro_classes
unfolding scaleR_metric_completion_def scaleC_metric_completion_def
by (simp add: scaleR_scaleC)
end
instance metric_completion :: (complex_normed_vector) complex_vector
apply intro_classes
subgoal apply (transfer, auto)
subgoal using Inner_Completion.Cauchy_sum bounded_clinear.Cauchy
bounded_clinear_scaleC_right by fastforce
subgoal by (simp add: Cauchy_sum bounded_clinear.Cauchy bounded_clinear_scaleC_right)
subgoal by (simp add: scaleC_add_right)
done
subgoal apply (transfer, auto)
using bounded_clinear.Cauchy bounded_clinear_scaleC_right apply blast
using bounded_clinear.Cauchy bounded_clinear_scaleC_right apply (metis Cauchy_sum)
using dist_self scaleC_add_left by (metis (mono_tags, lifting) LIMSEQ_def)
subgoal by (transfer, simp add: bounded_clinear.Cauchy bounded_clinear_scaleC_right)
subgoal by (transfer, simp)
done
instantiation metric_completion :: (real_normed_vector) banach
begin
lift_definition norm_metric_completion :: "'a metric_completion ⇒ real"
is "λX. lim (λn. norm (X n))"
unfolding dist_norm
apply (rule convergent_add_null(2))
subgoal using convergent_Cauchy_dist zero_metric_completion.rsp by force
using Lim_null_comparison eventually_sequentially norm_triangle_ineq3
by (metis (mono_tags, lifting) real_norm_def)
definition sgn_metric_completion :: "'a metric_completion ⇒ 'a metric_completion"
where "sgn_metric_completion x = x /⇩R norm x"
lemma metric_completion_triangle_ineq:
fixes x y :: "'a metric_completion"
shows "norm (x + y) ≤ norm x + norm y"
proof -
have 1: "lim (λn. norm (x n + y n)) ≤ lim (λn. norm (x n)) + lim (λn. norm (y n))"
if cauchy: "Cauchy x" "Cauchy y"
for x y :: "nat ⇒ 'a"
proof -
have lim_norm_sum_distrib: "lim (λn. norm (x n) + norm (y n)) =
lim (λn. norm (x n)) + lim (λn. norm (y n))"
apply (intro limI)
apply (rule tendsto_add)
using cauchy convergent_Cauchy_dist convergent_LIMSEQ_iff zero_metric_completion.rsp
by fastforce+
have conv_norm_plus: "convergent (λn. norm (x n + y n))"
apply (simp only: norm_conv_dist)
apply (intro convergent_Cauchy_dist)
apply (metis (no_types, lifting) ext Cauchy_sum cauchy(1,2) plus_fun_apply)
by (simp add: zero_metric_completion.rsp)
have conv_plus_norm: "convergent (λn. norm (x n) + norm (y n))"
apply (rule convergent_add)
apply (simp_all only: norm_conv_dist)
apply (rule convergent_Cauchy_dist[OF cauchy(1) zero_metric_completion.rsp[THEN conjunct1]])
by (rule convergent_Cauchy_dist[OF cauchy(2) zero_metric_completion.rsp[THEN conjunct1]])
thus ?thesis
apply (simp flip: lim_norm_sum_distrib)
apply (rule lim_mono[of _ "(λn. norm (x n + y n))" "(λn. norm (x n) + norm (y n))"])
using conv_norm_plus conv_plus_norm
by (simp_all add: norm_triangle_ineq convergent_LIMSEQ_iff[symmetric])
qed
show ?thesis
apply transfer
using 1 by auto
qed
instance
apply intro_classes
unfolding minus_metric_completion_def sgn_metric_completion_def
subgoal by (transfer, simp add: dist_norm)
subgoal apply (transfer, auto)
using bounded_linear.Cauchy bounded_linear_scaleR_right by blast
subgoal apply (transfer, auto)
subgoal using zero_metric_completion.rsp by blast
subgoal using convergent_Cauchy_dist convergent_LIMSEQ_iff zero_metric_completion.rsp by force
subgoal by (simp add: tendsto_Lim)
done
subgoal using metric_completion_triangle_ineq .
subgoal
apply (transfer, auto)
apply (intro limI)
apply (rule tendsto_mult)
apply blast
apply (simp only: convergent_LIMSEQ_iff[symmetric] norm_conv_dist)
apply (rule convergent_Cauchy_dist)
using zero_metric_completion.rsp by simp_all
done
end
instance metric_completion :: (complex_normed_vector) cbanach
apply intro_classes
apply (transfer, auto)
apply (intro limI)
apply (rule tendsto_mult)
apply blast
apply (simp only: convergent_LIMSEQ_iff[symmetric] norm_conv_dist)
apply (rule convergent_Cauchy_dist)
using zero_metric_completion.rsp by simp_all
subsection ‹The Cauchy completion of an inner product space is a Hilbert space.›
instantiation metric_completion :: (complex_inner) chilbert_space
begin
lift_definition cinner_metric_completion ::
"'a metric_completion ⇒ 'a metric_completion ⇒ complex"
is "λx y. lim (λn. cinner (x n) (y n))"
proof (elim conjE)
fix x1 x2 x3 x4 :: "nat ⇒ 'a"
assume cauchy: "Cauchy x1" "Cauchy x2" "Cauchy x3" "Cauchy x4"
and dist_conv: "(λn. dist (x1 n) (x2 n)) ⇢ 0"
"(λn. dist (x3 n) (x4 n)) ⇢ 0"
have 1: "(λx. cmod ((x1 x - x2 x) ∙⇩C x3 x)) ⇢ 0"
if cauchy: "Cauchy x1" "Cauchy x2" "Cauchy x3"
and dist_conv: "(λn. dist (x1 n) (x2 n)) ⇢ 0"
for x1 x2 x3 :: "nat ⇒ 'a"
proof -
obtain B where B: "∀n. norm (x3 n) < B"
using Cauchy_norm_bounded[OF cauchy(3)] by blast
have *: "(λn. norm (x1 n - x2 n) * B) ⇢ 0"
apply (rule tendsto_mult[where a=0 and b=B, simplified])
by (metis (no_types, lifting) ext dist_conv dist_norm) simp
have norm_mult_tendsto_0: "(λn. norm (x1 n - x2 n) * norm (x3 n)) ⇢ 0"
apply (rule tendsto_sandwich[where f="λn. 0" and h="λn. norm (x1 n - x2 n) * B"])
using * B by (simp_all add: less_imp_le mult_left_mono)
show ?thesis
apply (rule tendsto_sandwich[where f="λn. 0" and h="λn. norm (x1 n - x2 n) * norm (x3 n)"])
by (simp_all add: Cauchy_Schwarz_ineq2 norm_mult_tendsto_0)
qed
have 2: "(λn. x1 n ∙⇩C x3 n - x2 n ∙⇩C x4 n) ⇢ 0"
proof -
have *: "x1 n ∙⇩C x3 n - x2 n ∙⇩C x4 n =
(x1 n - x2 n) ∙⇩C x3 n + x2 n ∙⇩C (x3 n - x4 n)" for n
by (simp add: cinner_simps(3,4))
show ?thesis
apply (simp only: *)
apply (rule tendsto_add[of _ 0 _ _ 0, simplified]; rule tendsto_norm_zero_cancel)
apply (rule 1[OF cauchy(1-3) dist_conv(1)])
apply (subst complex_mod_cnj[symmetric])
apply (subst cinner_commute[symmetric])
by (rule 1[OF cauchy(3,4,2) dist_conv(2)])
qed
show "lim (λn. x1 n ∙⇩C x3 n) = lim (λn. x2 n ∙⇩C x4 n)"
apply (intro convergent_add_null(2))
using 2 by (simp_all add: Cauchy_cinner_Cauchy cauchy(2,4) complex_Cauchy_convergent)
qed
instance
proof (intro_classes; transfer; elim conjE)
have conv_cinner_self: "convergent (λn. x n ∙⇩C x n)"
if "Cauchy x" for x :: "nat ⇒ 'a"
using Cauchy_cinner_Cauchy Cauchy_convergent_iff that by blast
fix x :: "nat ⇒ 'a"
assume x: "Cauchy x"
note conv_xx = conv_cinner_self[OF x]
have "0 ≤ Re (lim (λn. x n ∙⇩C x n))"
unfolding lim_Re[symmetric, OF conv_xx]
apply (rule lim_ge)
using cinner_ge_zero less_eq_complex_def
by (auto simp add: Cauchy_Re Cauchy_cinner_Cauchy real_Cauchy_convergent x)
moreover have "Im (lim (λn. x n ∙⇩C x n)) = 0"
by (simp add: lim_Im[symmetric, OF conv_xx])
ultimately show "0 ≤ lim (λn. x n ∙⇩C x n)"
by (simp add: less_eq_complex_def)
show "lim (λn. norm (x n)) = sqrt (cmod (lim (λn. x n ∙⇩C x n)))"
apply (intro limI)
apply (rule tendsto_real_sqrt[
where f="λn. cmod (x n ∙⇩C x n)" for x n,
folded norm_eq_sqrt_cinner])
using Cauchy_cinner_Cauchy convergent_eq_Cauchy limI tendsto_norm x by fastforce
show "(lim (λn. x n ∙⇩C x n) = 0) =
(Cauchy x ∧ Cauchy (λn. 0::'a) ∧ (λn. dist (x n) 0) ⇢ 0)"
proof -
have Cauchy_0: "Cauchy (λn. 0::'a)"
using zero_metric_completion.rsp by simp
{ assume lim_cinner_self: "lim (λn. x n ∙⇩C x n) = 0"
have tendsto_cinner_self: "(λn. cmod (x n ∙⇩C x n)) ⇢ 0"
using lim_cinner_self conv_xx unfolding convergent_LIMSEQ_iff
by (simp add: tendsto_norm_zero)
have "(λn. norm (x n)) ⇢ 0"
unfolding norm_eq_sqrt_cinner[of "x n" for n]
apply (rule tendsto_real_sqrt[of _ 0, simplified])
using tendsto_cinner_self . }
note t0_if_inner_t0 = this
{ assume "(λn. norm (x n)) ⇢ 0"
hence "lim (λn. x n ∙⇩C x n) = 0"
apply (intro limI)
using tendsto_cinner tendsto_norm_zero_cancel by fastforce }
note inner_t0_if_t0 = this
show ?thesis
using t0_if_inner_t0 inner_t0_if_t0 x Cauchy_0 by auto
qed
fix y :: "nat ⇒ 'a" assume y: "Cauchy y"
show "lim (λn. x n ∙⇩C y n) = cnj (lim (λn. y n ∙⇩C x n))"
apply (intro limI)
unfolding lim_cnj[of "λn. x n ∙⇩C y n" for x y, unfolded cinner_commute', of _ _ _ sequentially]
using Cauchy_cinner_Cauchy convergent_eq_Cauchy limI x y by blast
{ fix r :: complex
have "lim (λn. cnj r * (x n ∙⇩C y n)) = cnj r * lim (λn. x n ∙⇩C y n)"
apply (intro limI tendsto_mult)
using Cauchy_cinner_Cauchy convergent_eq_Cauchy limI x y by blast+
thus "lim (λn. r *⇩C x n ∙⇩C y n) = cnj r * lim (λn. x n ∙⇩C y n)" by simp }
fix z :: "nat ⇒ 'a" assume z: "Cauchy z"
show "lim (λn. ((x + y) n) ∙⇩C z n) = lim (λn. x n ∙⇩C z n) + lim (λn. y n ∙⇩C z n)"
apply (simp only: cinner_add_left plus_fun_def)
apply (intro limI tendsto_add)
using Cauchy_cinner_Cauchy convergent_eq_Cauchy limI x y z by blast+
qed
end
subsection ‹The embedding \<^term>‹to_metric_completion››
text ‹And now we get all sorts of metric lemmas for inner products,
e.g. an isometry (see @{thm to_metric_completion_isometry}) into
a dense subset (see @{thm to_metric_completion_dense'}) of a \<^class>‹chilbert_space›.
This isometry is (complex-)linear, and preserves norms and inner products.›
lemma to_metric_completion_linear: "linear to_metric_completion" (is ‹linear ?g›)
and to_metric_completion_clinear: "clinear to_metric_completion" (is ‹clinear ?f›)
proof -
note plus_abs_mc = plus_metric_completion.abs_eq
[symmetric, of "λn. b1" "λn. b2" for b1 b2, simplified, unfolded plus_fun_def]
have "⋀r b. ?g (r *⇩R b) = r *⇩R ?g b" "⋀r b. ?f (r *⇩C b) = r *⇩C ?f b"
unfolding to_metric_completion_def
by (simp_all add: Cauchy_def scaleR_metric_completion.abs_eq scaleC_metric_completion.abs_eq)
moreover have "⋀b1 b2. ?g (b1 + b2) = ?g b1 + ?g b2" "⋀b1 b2. ?f (b1 + b2) = ?f b1 + ?f b2"
unfolding to_metric_completion_def
by (rule plus_abs_mc; simp add: Cauchy_def)+
ultimately show "linear ?g" "clinear ?f"
by unfold_locales (auto)
qed
lemma to_metric_completion_norm:
shows "norm (to_metric_completion c) = norm c"
unfolding to_metric_completion_def
apply (rule norm_metric_completion.abs_eq[of "λn. c", simplified])
by (simp add: Cauchy_def)
lemma to_metric_completion_bounded_clinear:
shows "bounded_clinear to_metric_completion"
apply unfold_locales
apply (simp add: linear_add to_metric_completion_linear)
apply (simp add: complex_vector.linear_scale to_metric_completion_clinear)
by (metis mult.right_neutral norm_imp_pos_and_ge to_metric_completion_norm)
lemma to_metric_completion_cinner:
"(to_metric_completion c) ∙⇩C (to_metric_completion d) = c ∙⇩C d"
unfolding to_metric_completion_def
apply (rule cinner_metric_completion.abs_eq[of "λn. b1" "λn. b2" for b1 b2, simplified])
by (simp_all add: Cauchy_def)
end