# Theory Extra_Vector_Spaces

```section ‹‹Extra_Vector_Spaces› -- Additional facts about vector spaces›

theory Extra_Vector_Spaces
imports
"HOL-Analysis.Inner_Product"
"HOL-Analysis.Euclidean_Space"
"HOL-Library.Indicator_Function"
"HOL-Analysis.Topology_Euclidean_Space"
"HOL-Analysis.Line_Segment"
"HOL-Analysis.Bounded_Linear_Function"
Extra_General
begin

subsection ‹Euclidean spaces›

typedef 'a euclidean_space = "UNIV :: ('a ⇒ real) set" ..
setup_lifting type_definition_euclidean_space

instantiation euclidean_space :: (type) real_vector begin
lift_definition plus_euclidean_space ::
"'a euclidean_space ⇒ 'a euclidean_space ⇒ 'a euclidean_space"
is "λf g x. f x + g x" .
lift_definition zero_euclidean_space :: "'a euclidean_space" is "λ_. 0" .
lift_definition uminus_euclidean_space ::
"'a euclidean_space ⇒ 'a euclidean_space"
is "λf x. - f x" .
lift_definition minus_euclidean_space ::
"'a euclidean_space ⇒ 'a euclidean_space ⇒ 'a euclidean_space"
is "λf g x. f x - g x".
lift_definition scaleR_euclidean_space ::
"real ⇒ 'a euclidean_space ⇒ 'a euclidean_space"
is "λc f x. c * f x" .
instance
apply intro_classes
by (transfer; auto intro: distrib_left distrib_right)+
end

instantiation euclidean_space :: (finite) real_inner begin
lift_definition inner_euclidean_space :: "'a euclidean_space ⇒ 'a euclidean_space ⇒ real"
is "λf g. ∑x∈UNIV. f x * g x :: real" .
definition "norm_euclidean_space (x::'a euclidean_space) = sqrt (inner x x)"
definition "dist_euclidean_space (x::'a euclidean_space) y = norm (x-y)"
definition "sgn x = x /⇩R norm x" for x::"'a euclidean_space"
definition "uniformity = (INF e∈{0<..}. principal {(x::'a euclidean_space, y). dist x y < e})"
definition "open U = (∀x∈U. ∀⇩F (x'::'a euclidean_space, y) in uniformity. x' = x ⟶ y ∈ U)"
instance
proof intro_classes
fix x :: "'a euclidean_space"
and y :: "'a euclidean_space"
and z :: "'a euclidean_space"
show "dist (x::'a euclidean_space) y = norm (x - y)"
and "sgn (x::'a euclidean_space) = x /⇩R norm x"
and "uniformity = (INF e∈{0<..}. principal {(x, y). dist (x::'a euclidean_space) y < e})"
and "open U = (∀x∈U. ∀⇩F (x', y) in uniformity. (x'::'a euclidean_space) = x ⟶ y ∈ U)"
and "norm x = sqrt (inner x x)" for U
unfolding dist_euclidean_space_def norm_euclidean_space_def sgn_euclidean_space_def
uniformity_euclidean_space_def open_euclidean_space_def
by simp_all

show "inner x y = inner y x"
apply transfer
show "inner (x + y) z = inner x z + inner y z"
proof transfer
fix x y z::"'a ⇒ real"
have "(∑i∈UNIV. (x i + y i) * z i) = (∑i∈UNIV. x i * z i + y i * z i)"
thus "(∑i∈UNIV. (x i + y i) * z i) = (∑j∈UNIV. x j * z j) + (∑k∈UNIV. y k * z k)"
by (subst sum.distrib[symmetric])
qed

show "inner (r *⇩R x) y = r * (inner x y)" for r
proof transfer
fix r and x y::"'a⇒real"
have "(∑i∈UNIV. r * x i * y i) = (∑i∈UNIV. r * (x i * y i))"
thus "(∑i∈UNIV. r * x i * y i) = r * (∑j∈UNIV. x j * y j)"
by (subst sum_distrib_left)
qed
show "0 ≤ inner x x"
apply transfer
show "(inner x x = 0) = (x = 0)"
proof (transfer, rule)
fix f :: "'a ⇒ real"
assume "(∑i∈UNIV. f i * f i) = 0"
hence "f x * f x = 0" for x
apply (rule_tac sum_nonneg_eq_0_iff[THEN iffD1, rule_format, where A=UNIV and x=x])
by auto
thus "f = (λ_. 0)"
by auto
qed auto
qed
end

instantiation euclidean_space :: (finite) euclidean_space begin
lift_definition euclidean_space_basis_vector :: "'a ⇒ 'a euclidean_space" is
"λx. indicator {x}" .
definition "Basis_euclidean_space == (euclidean_space_basis_vector ` UNIV)"
instance
proof intro_classes
fix u :: "'a euclidean_space"
and v :: "'a euclidean_space"
show "(Basis::'a euclidean_space set) ≠ {}"
unfolding Basis_euclidean_space_def by simp
show "finite (Basis::'a euclidean_space set)"
unfolding Basis_euclidean_space_def by simp
show "inner u v = (if u = v then 1 else 0)"
if "u ∈ Basis" and "v ∈ Basis"
using that unfolding Basis_euclidean_space_def
apply transfer apply auto
by (auto simp: indicator_def)
show "(∀v∈Basis. inner u v = 0) = (u = 0)"
unfolding Basis_euclidean_space_def
apply transfer
by auto
qed
end (* euclidean_space :: (finite) euclidean_space *)

subsection ‹Misc›

lemma closure_bounded_linear_image_subset_eq:
assumes f: "bounded_linear f"
shows "closure (f ` closure S) = closure (f ` S)"
by (meson closed_closure closure_bounded_linear_image_subset closure_minimal closure_mono closure_subset f image_mono subset_antisym)

lemma not_singleton_real_normed_is_perfect_space[simp]: ‹class.perfect_space (open :: 'a::{not_singleton,real_normed_vector} set ⇒ bool)›
apply standard
by (metis UNIV_not_singleton clopen closed_singleton empty_not_insert)

lemma infsum_bounded_linear:
assumes ‹bounded_linear h›
assumes ‹f summable_on A›
shows ‹infsum (λx. h (f x)) A = h (infsum f A)›
by (auto intro!: infsum_bounded_linear_strong assms summable_on_bounded_linear[where h=h])

lemma abs_summable_on_bounded_linear:
fixes h f A
assumes ‹bounded_linear h›
assumes ‹f abs_summable_on A›
shows ‹(h o f) abs_summable_on A›
proof -
have bound: ‹norm (h (f x)) ≤ onorm h * norm (f x)› for x
apply (rule onorm)

from assms(2) have ‹(λx. onorm h *⇩R f x) abs_summable_on A›
by (auto intro!: summable_on_cmult_right)
then have ‹(λx. h (f x)) abs_summable_on A›
apply (rule abs_summable_on_comparison_test)
using bound by (auto simp: assms(1) onorm_pos_le)
then show ?thesis
by auto
qed

lemma norm_plus_leq_norm_prod: ‹norm (a + b) ≤ sqrt 2 * norm (a, b)›
proof -
have ‹(norm (a + b))⇧2 ≤ (norm a + norm b)⇧2›
using norm_triangle_ineq by auto
also have ‹… ≤ 2 * ((norm a)⇧2 + (norm b)⇧2)›
by (smt (verit, best) power2_sum sum_squares_bound)
also have ‹… ≤ (sqrt 2 * norm (a, b))⇧2›
by (auto simp: power_mult_distrib norm_prod_def simp del: power_mono_iff)
finally show ?thesis
by auto
qed

lemma ex_norm1:
assumes ‹(UNIV::'a::real_normed_vector set) ≠ {0}›
shows ‹∃x::'a. norm x = 1›
proof-
have ‹∃x::'a. x ≠ 0›
using assms by fastforce
then obtain x::'a where ‹x ≠ 0›
by blast
hence ‹norm x ≠ 0›
by simp
hence ‹(norm x) / (norm x) = 1›
by simp
moreover have ‹(norm x) / (norm x) = norm (x /⇩R (norm x))›
by simp
ultimately have ‹norm (x /⇩R (norm x)) = 1›
by simp
thus ?thesis
by blast
qed

lemma bdd_above_norm_f:
assumes "bounded_linear f"
shows ‹bdd_above {norm (f x) |x. norm x = 1}›
proof-
have ‹∃M. ∀x. norm x = 1 ⟶ norm (f x) ≤ M›
using assms
by (metis bounded_linear.axioms(2) bounded_linear_axioms_def)
thus ?thesis by auto
qed

lemma any_norm_exists:
assumes ‹n ≥ 0›
shows ‹∃ψ::'a::{real_normed_vector,not_singleton}. norm ψ = n›
proof -
obtain ψ :: 'a where ‹ψ ≠ 0›
using not_singleton_card
by force
then have ‹norm (n *⇩R sgn ψ) = n›
using assms by (auto simp: sgn_div_norm abs_mult)
then show ?thesis
by blast
qed

lemma abs_summable_on_scaleR_left [intro]:
fixes c :: ‹'a :: real_normed_vector›
assumes "c ≠ 0 ⟹ f abs_summable_on A"
shows   "(λx. f x *⇩R c) abs_summable_on A"
apply (cases ‹c = 0›)
apply simp
by (auto intro!: summable_on_cmult_left assms simp flip: real_norm_def)

lemma abs_summable_on_scaleR_right [intro]:
fixes f :: ‹'a ⇒ 'b :: real_normed_vector›
assumes "c ≠ 0 ⟹ f abs_summable_on A"
shows   "(λx. c *⇩R f x) abs_summable_on A"
apply (cases ‹c = 0›)
apply simp
by (auto intro!: summable_on_cmult_right assms)

end
```