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
    by (simp add: mult.commute)
  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)"
      by (simp add: distrib_left mult.commute)
    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))"
      by (simp add: mult.assoc)
    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
    by (simp add: sum_nonneg)
  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)
    by (simp add: assms(1))

  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