header {* Bounded Linear Function *}

theory Bounded_Linear_Function
imports Integration "../ODE_Auxiliarities"
begin

lemma (in real_inner) parallelogram_law: "(norm (x + y))\<^sup>2 + (norm (x - y))\<^sup>2 = 2 * (norm x)\<^sup>2 + 2 * (norm y)\<^sup>2"
proof -
  have "(norm (x + y))\<^sup>2 + (norm (x - y))\<^sup>2 = inner (x + y) (x + y) + inner (x - y) (x - y)"
    by (simp add: norm_eq_sqrt_inner)
  also have "\<dots> = 2 * (norm x)\<^sup>2 + 2 * (norm y)\<^sup>2"
    by (simp add: algebra_simps norm_eq_sqrt_inner)
  finally show ?thesis .
qed

typedef 'a blinfun = "{f::'a::real_normed_vector\<Rightarrow>'a::real_normed_vector. bounded_linear f}"
  morphisms blinfun_apply Blinfun
  by (auto intro!: exI[where x="\<lambda>x. 0"])

no_notation vec_nth (infixl "$" 90)
notation blinfun_apply (infixl "$" 999)

declare [[coercion
    "blinfun_apply :: ('a::real_normed_vector) blinfun \<Rightarrow> 'a \<Rightarrow> 'a"]]

lemma bounded_linear_blinfun_apply[intro, simp]: "bounded_linear (op $ f)"
  by (metis blinfun_apply mem_Collect_eq)

setup_lifting type_definition_blinfun

instantiation blinfun :: (real_normed_vector) real_normed_vector
begin

lift_definition norm_blinfun :: "'a blinfun \<Rightarrow> real" is onorm .

lift_definition minus_blinfun :: "'a blinfun \<Rightarrow> 'a blinfun \<Rightarrow> 'a blinfun"
  is "\<lambda>f g x. f x - g x"
  by (rule bounded_linear_sub)

definition dist_blinfun :: "'a blinfun \<Rightarrow> 'a blinfun \<Rightarrow> real"
  where "dist_blinfun a b = norm (a - b)"

definition open_blinfun :: "'a blinfun set \<Rightarrow> bool"
  where "open_blinfun S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"

lift_definition uminus_blinfun :: "'a blinfun \<Rightarrow> 'a blinfun" is "\<lambda>f x. - f x"
  by (rule bounded_linear_minus)

lift_definition zero_blinfun :: "'a blinfun" is "\<lambda>x. 0"
  by (rule bounded_linear_zero)

lift_definition plus_blinfun :: "'a blinfun \<Rightarrow> 'a blinfun \<Rightarrow> 'a blinfun"
  is "\<lambda>f g x. f x + g x"
  by (metis bounded_linear_add)

lift_definition scaleR_blinfun::"real \<Rightarrow> 'a blinfun \<Rightarrow> 'a blinfun" is "\<lambda>r f x. r *\<^sub>R f x"
  by (metis bounded_linear_compose bounded_linear_scaleR_right)

definition sgn_blinfun :: "'a blinfun \<Rightarrow> 'a blinfun"
  where "sgn_blinfun x = x /\<^sub>R norm x"

instance
  apply default
  unfolding dist_blinfun_def open_blinfun_def sgn_blinfun_def
  apply (rule refl)+
  apply (transfer, force simp: onorm_triangle onorm_scaleR onorm_eq_0 algebra_simps)+
  done

end

lemma norm_blinfun_eqI:
  assumes "n \<le> norm (f $ x) / norm x"
  assumes "\<And>x. norm (f $ x) \<le> n * norm x"
  assumes "0 \<le> n"
  shows "norm f = n"
  by (auto simp: norm_blinfun_def intro!: antisym onorm_bound assms order_trans[OF _ le_onorm])

lemma norm_blinfun: "norm (f $ x) \<le> norm f * norm x"
  by transfer (rule onorm)

lemma norm_blinfun_bound: "0 \<le> b \<Longrightarrow> (\<And>x. norm (f $ x) \<le> b * norm x) \<Longrightarrow> norm f \<le> b"
  by transfer (rule onorm_bound)

lemma blinfun_minus_apply[simp]: "(f - g) $ x = f $ x - g $ x"
  by transfer simp

lemma blinfun_add_apply[simp]: "(f + g) $ x = f $ x + g $ x"
  by transfer simp

lemma blinfun_uminus_apply[simp]: "(- f) $ x = - f $ x"
  by transfer simp

lemma blinfun_scaleR_apply[simp]: "(r *\<^sub>R f) $ x = r *\<^sub>R f $x"
  by transfer simp

lemma blinfun_zero_apply[simp]: "0 $ x = 0"
  by transfer simp

lemma blinfun_apply_minus[simp]: " f $ (x - y) =  f $ x -  f $ y"
  by transfer (simp add:  linear_sub bounded_linear.linear)

lemma blinfun_apply_add[simp]: "f $ (x + y) = f $ x + f $ y"
  by transfer (simp add: bounded_linear.linear linear_add)

lemma blinfun_apply_uminus[simp]: "f $ (- x) = - f $ x"
  by transfer (simp add: bounded_linear.linear linear_neg)

lemma blinfun_apply_scaleR[simp]: "f $ (r *\<^sub>R x) = r *\<^sub>R f $ x"
  by transfer (simp add: bounded_linear.linear linear_cmul)

lemma blinfun_apply_zero[simp]: "x $ 0 = 0"
  by transfer (simp add: bounded_linear.linear linear_0)

lemma blinfun_eqI: "(\<And>i. x $ i = y $ i) \<Longrightarrow> x = y"
  by transfer auto

lemma blinfun_apply_setsum[simp]: "(\<Sum>i\<in>A. f i) $ x = (\<Sum>i\<in>A. (f i) $ x)"
  by (induct A rule: infinite_finite_induct) auto

lemma bounded_linear_apply_blinfun[intro, simp]: "bounded_linear (\<lambda>f. f $ i)"
  by (rule bounded_linearI[where K="norm i"]) (auto simp: norm_blinfun_def onorm)

lemma tendsto_blinfun_apply[tendsto_intros]:
  "(f ---> g) F \<Longrightarrow> ((\<lambda>x. (f x) $ i) ---> g $ i) F"
  using assms bounded_linear.Zfun[OF bounded_linear_apply_blinfun]
  by (auto simp: tendsto_Zfun_iff blinfun_minus_apply[symmetric] simp del: blinfun_minus_apply)

lemma continuous_blinfun_apply[continuous_intros]:
  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. (f x) $ i)"
  by (auto simp: continuous_def intro: tendsto_blinfun_apply)

lemma bounded_linear_Blinfun_apply: "bounded_linear f \<Longrightarrow> Blinfun f $ x = f x"
  by (auto simp: Blinfun_inverse)

instance blinfun :: (banach) banach
proof
  fix X::"nat \<Rightarrow> 'a blinfun"
  assume "Cauchy X"
  {
    fix x::'a
    {
      fix x::'a
      assume "norm x \<le> 1"
      have "Cauchy (\<lambda>n. X n $ x)"
      proof (rule CauchyI)
        fix e::real
        assume "0 < e"
        from CauchyD[OF `Cauchy X` `0 < e`] obtain M
          where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> norm (X m - X n) < e"
          by auto
        show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m $ x - X n $ x) < e"
        proof (safe intro!: exI[where x=M])
          fix m n
          assume le: "M \<le> m" "M \<le> n"
          have "norm (X m $ x - X n $ x) = norm ((X m - X n) $ x)"
            by simp
          also have "\<dots> \<le> norm (X m - X n) * norm x"
             by (rule norm_blinfun)
          also have "\<dots> \<le> norm (X m - X n) * 1"
            using `norm x \<le> 1` norm_ge_zero by (rule mult_left_mono)
          also have "\<dots> = norm (X m - X n)" by simp
          also have "\<dots> < e" using le by fact
          finally show "norm (X m $ x - X n $ x) < e" .
        qed
      qed
      hence "convergent (\<lambda>n. X n $ x)"
        by (metis Cauchy_convergent_iff)
    } note convergent_norm1 = this
    def y \<equiv> "x /\<^sub>R norm x"
    have y: "norm y \<le> 1" and xy: "x = norm x *\<^sub>R y"
      by (simp_all add: y_def inverse_eq_divide)
    have "convergent (\<lambda>n. norm x *\<^sub>R X n $ y)"
      by (intro bounded_bilinear.convergent[OF bounded_bilinear_scaleR] convergent_const
        convergent_norm1 y)
    also have "(\<lambda>n. norm x *\<^sub>R X n $ y) = (\<lambda>n. X n $ x)"
      by (subst xy) simp
    finally have "convergent (\<lambda>n. X n $ x)" .
  }
  then obtain v where v: "\<And>x. (\<lambda>n. X n $ x) ----> v x"
    unfolding convergent_def
    by metis

  have "Cauchy (\<lambda>n. norm (X n))"
  proof (rule CauchyI)
    fix e::real
    assume "e > 0"
    from CauchyD[OF `Cauchy X` `0 < e`] obtain M
      where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> norm (X m - X n) < e"
      by auto
    show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (norm (X m) - norm (X n)) < e"
    proof (safe intro!: exI[where x=M])
      fix m n assume mn: "m \<ge> M" "n \<ge> M"
      have "norm (norm (X m) - norm (X n)) \<le> norm (X m - X n)"
        by (metis norm_triangle_ineq3 real_norm_def)
      also have "\<dots> < e" using mn by fact
      finally show "norm (norm (X m) - norm (X n)) < e" .
    qed
  qed
  then obtain K where K: "(\<lambda>n. norm (X n)) ----> K"
    unfolding Cauchy_convergent_iff convergent_def
    by metis

  have "bounded_linear v"
  proof
    fix x y and r::real
    from tendsto_add[OF v[of x] v [of y]] v[of "x + y", simplified]
      tendsto_scaleR[OF tendsto_const[of r] v[of x]] v[of "r *\<^sub>R x", simplified]
    show "v (x + y) = v x + v y" "v (r *\<^sub>R x) = r *\<^sub>R v x"
      by (metis (poly_guards_query) LIMSEQ_unique)+
    show "\<exists>K. \<forall>x. norm (v x) \<le> norm x * K"
    proof (safe intro!: exI[where x=K])
      fix x
      have "norm (v x) \<le> K * norm x"
        by (rule tendsto_le[OF _ tendsto_mult[OF K tendsto_const] tendsto_norm[OF v]])
          (auto simp: norm_blinfun)
      thus "norm (v x) \<le> norm x * K"
        by (simp add: ac_simps)
    qed
  qed
  hence Bv: "\<And>x. (\<lambda>n. X n $ x) ----> Blinfun v $ x"
    by (auto simp: bounded_linear_Blinfun_apply v)

  have "X ----> Blinfun v"
  proof (rule LIMSEQ_I)
    fix r::real assume "r > 0"
    def r' \<equiv> "r / 2"
    have "0 < r'" "r' < r" using `r > 0` by (simp_all add: r'_def)
    from CauchyD[OF `Cauchy X` `r' > 0`]
    obtain M where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> norm (X m - X n) < r'"
      by metis
    show "\<exists>no. \<forall>n\<ge>no. norm (X n - Blinfun v) < r"
    proof (safe intro!: exI[where x=M])
      fix n assume n: "M \<le> n"
      have "norm (X n - Blinfun v) \<le> r'"
      proof (rule norm_blinfun_bound)
        fix x
        have "eventually (\<lambda>m. m \<ge> M) sequentially"
          by (metis eventually_ge_at_top)
        hence ev_le: "eventually (\<lambda>m. norm (X n $ x - X m $ x) \<le> r' * norm x) sequentially"
        proof eventually_elim
          case elim
          have "norm (X n $ x - X m $ x) = norm ((X n - X m) $ x)"
            by simp
          also have "\<dots> \<le> norm ((X n - X m)) * norm x"
            by (rule norm_blinfun)
          also have "\<dots> \<le> r' * norm x"
            using M[OF n elim] by (simp add: mult_right_mono)
          finally show ?case .
        qed
        have tendsto_v: "(\<lambda>m. norm (X n $ x - X m $ x)) ----> norm (X n $ x - Blinfun v $ x)"
          by (auto intro!: tendsto_intros Bv)
        show "norm ((X n - Blinfun v) $ x) \<le> r' * norm x"
          by (auto intro!: tendsto_ge_const tendsto_v ev_le)
      qed (simp add: `0 < r'` less_imp_le)
      thus "norm (X n - Blinfun v) < r"
        by (metis `r' < r` le_less_trans)
    qed
  qed
  thus "convergent X"
    by (rule convergentI)
qed

instantiation blinfun::("{real_normed_vector, perfect_space}") real_normed_algebra_1
begin

lift_definition one_blinfun::"'a blinfun" is "\<lambda>x. x" by (rule bounded_linear_ident)

lift_definition times_blinfun :: "'a blinfun \<Rightarrow> 'a blinfun \<Rightarrow> 'a blinfun"
  is "op o" unfolding o_def by (rule bounded_linear_compose)


lemma blinfun_apply_times_blinfun[simp]:
  "(f * g) $ x = f $ (g $ x)"
  by transfer simp

instance
proof
  from not_open_singleton[of "0::'a"] have "{0::'a} \<noteq> UNIV" by auto
  then obtain x :: 'a where "x \<noteq> 0" by auto
  show "0 \<noteq> (1::'a blinfun)"
    by transfer (auto dest!: fun_cong[where x=x] simp: `x \<noteq> 0`)
qed (transfer, simp add: o_def linear_simps onorm_compose onorm_id onorm_compose[simplified o_def])+

end

subsection {* On Euclidean Space *}

lemma blinfun_euclidean_eqI:
  fixes f g::"('a::euclidean_space) blinfun"
  shows "(\<And>i. i \<in> Basis \<Longrightarrow> f $ i = g $ i) \<Longrightarrow> f = g"
  by (auto simp: fun_eq_iff Derivative.linear_componentwise bounded_linear.linear
    intro!: euclidean_eqI[where 'a='a] blinfun_eqI)

instantiation prod :: (zero_neq_one, zero_neq_one) zero_neq_one
begin

definition "1 = (1, 1)"

instance by default (simp add: zero_prod_def one_prod_def)
end

locale no_real_inner
begin

lift_definition fstzero::"(real*real) blinfun" is "\<lambda>(x, y). (x, 0)"
  by (auto intro!: bounded_linearI')

lemma [simp]: "fstzero $ (a, b) = (a, 0)"
  by transfer simp

lift_definition zerosnd::"(real*real) blinfun" is "\<lambda>(x, y). (0, y)"
  by (auto intro!: bounded_linearI')

lemma [simp]: "zerosnd $ (a, b) = (0, b)"
  by transfer simp

lemma fstzero_add_zerosnd: "fstzero + zerosnd = 1"
  by transfer auto

lemma norm_fstzero_zerosnd: "norm fstzero = 1" "norm zerosnd = 1" "norm (fstzero - zerosnd) = 1"
  by (rule norm_blinfun_eqI[where x="(1, 0)"]) (auto simp: norm_Pair
    intro: norm_blinfun_eqI[where x="(0, 1)"] norm_blinfun_eqI[where x="(1, 0)"])

text {* compare with @{thm parallelogram_law} *}

lemma "(norm (fstzero + zerosnd))\<^sup>2 + (norm (fstzero - zerosnd))\<^sup>2 \<noteq>
    2 * (norm fstzero)\<^sup>2 + 2 * (norm zerosnd)\<^sup>2"
  by (simp add: fstzero_add_zerosnd norm_fstzero_zerosnd)

end

lift_definition
  blinfun_of_matrix::"('a::euclidean_space \<Rightarrow> 'a::euclidean_space \<Rightarrow> real) \<Rightarrow> 'a blinfun"
  is "\<lambda>a x. \<Sum>i\<in>Basis. \<Sum>j\<in>Basis. ((x \<bullet> j) * a i j) *\<^sub>R i"
  by (intro bounded_linear_setsum bounded_linear_scaleR_const bounded_linear_mult_const
    bounded_linear_inner_left)

lemma blinfun_of_matrix_works:
  fixes f::"'a::euclidean_space blinfun" shows "blinfun_of_matrix (\<lambda>i j. (f $ j) \<bullet> i) = f"
proof (transfer, rule,  rule euclidean_eqI)
  fix f::"'a \<Rightarrow> 'a" and x b::'a assume "bounded_linear f" and b: "b \<in> Basis"
  then interpret bounded_linear f by simp
  have "(\<Sum>j\<in>Basis. \<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j)) *\<^sub>R j) \<bullet> b
    = (\<Sum>j\<in>Basis. if j = b then (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j))) else 0)"
    using b
    by (auto simp add: algebra_simps inner_setsum_left inner_Basis split: split_if intro!: setsum.cong)
  also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> b)))"
    using b by (simp add: setsum.delta)
  also have "\<dots> = f x \<bullet> b"
    by (subst Derivative.linear_componentwise[symmetric]) (unfold_locales, rule)
  finally show "(\<Sum>j\<in>Basis. \<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j)) *\<^sub>R j) \<bullet> b = f x \<bullet> b" .
qed

lemma blinfun_of_matrix_apply:
  "blinfun_of_matrix a $ x = (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. ((x \<bullet> j) * a i j) *\<^sub>R i)"
  by transfer simp

lemma blinfun_of_matrix_minus: "blinfun_of_matrix x - blinfun_of_matrix y = blinfun_of_matrix (x - y)"
  by transfer (auto simp: algebra_simps setsum_subtractf)

lemma norm_blinfun_of_matrix: "norm (blinfun_of_matrix a) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. abs (a i j))"
  apply (rule norm_blinfun_bound)
  apply (simp_all add: setsum_nonneg blinfun_of_matrix_apply setsum_left_distrib)
  apply (auto simp: abs_mult ac_simps intro!: mult_right_mono Basis_le_norm setsum_mono order_trans[OF norm_setsum])
  done

lemma Zfun_setsum:
  assumes "finite s"
  assumes f: "\<And>i. i \<in> s \<Longrightarrow> Zfun (f i) F"
  shows "Zfun (\<lambda>x. setsum (\<lambda>i. f i x) s) F"
  using assms by induct (auto intro!: Zfun_zero Zfun_add)

lemma tendsto_blinfun_of_matrix:
  assumes "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n i j) ---> a i j) F"
  shows "((\<lambda>n. blinfun_of_matrix (b n)) ---> blinfun_of_matrix a) F"
proof -
  have "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> Zfun (\<lambda>x. norm (b x i j - a i j)) F"
    using assms unfolding tendsto_Zfun_iff Zfun_norm_iff .
  hence "Zfun (\<lambda>x. (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. abs (b x i j - a i j))) F"
    by (auto intro!: Zfun_setsum)
  thus ?thesis
    unfolding tendsto_Zfun_iff blinfun_of_matrix_minus
    by (rule Zfun_le) (auto intro!: order_trans[OF norm_blinfun_of_matrix])
qed

lemma tendsto_componentwise:
  "(\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n $ j \<bullet> i) ---> a $ j \<bullet> i) F) \<Longrightarrow> (b ---> a) F"
  apply (subst blinfun_of_matrix_works[of a, symmetric])
  apply (subst blinfun_of_matrix_works[of "b x" for x, symmetric, abs_def])
  by (rule tendsto_blinfun_of_matrix)

lemma
  continuous_blinfun_componentwiseI:
  fixes f:: "'b::t2_space \<Rightarrow> ('a::euclidean_space) blinfun"
  assumes "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> continuous F (\<lambda>x. (f x) $ j \<bullet> i)"
  shows "continuous F f"
  using assms by (auto simp: continuous_def intro!: tendsto_componentwise)

lemmas bounded_linear_inner_const = bounded_linear_inner_left[THEN bounded_linear_compose]

lemma bounded_linear_blinfun_matrix: "bounded_linear (\<lambda>x. x $ j \<bullet> i)"
  by (auto intro!: bounded_linearI' bounded_linear_inner_const)

lemma continuous_blinfun_matrix:
  assumes "continuous F f"
  shows "continuous F (\<lambda>x. (f x) $ j \<bullet>  i)"
  by (rule bounded_linear.continuous[OF bounded_linear_blinfun_matrix assms])

lemma continuous_on_blinfun_matrix:
  fixes f::"'a::t2_space \<Rightarrow> ('b::{heine_borel, banach, perfect_space, real_inner}) blinfun"
  assumes "continuous_on S f"
  shows "continuous_on S (\<lambda>x. (f x) j \<bullet> i)"
  using assms
  by (auto simp: continuous_on_eq_continuous_within continuous_blinfun_matrix)

lemma
  continuous_on_blinfun_apply_compose:
  fixes f::"'a::t2_space \<Rightarrow> ('b::euclidean_space) blinfun"
  assumes "continuous_on X f"
  assumes "continuous_on S h"
  assumes "continuous_on S g"
  assumes "g ` S \<subseteq> X"
  shows "continuous_on S (\<lambda>x. blinfun_apply (f (g x)) (h x))"
proof -
  have "(\<lambda>x. blinfun_apply (f (g x)) (h x)) =
    (\<lambda>x. (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. (f (g x)) j \<bullet> i * (h x \<bullet> j)) *\<^sub>R i))"
    by (subst blinfun_of_matrix_works[symmetric])
      (auto simp: algebra_simps scaleR_setsum_left blinfun_of_matrix_apply)
  moreover have "continuous_on S \<dots>"
    by (force intro: continuous_intros assms
      continuous_on_compose2[OF continuous_on_subset[OF continuous_on_blinfun_matrix `g \` S \<subseteq> X`]])
  ultimately show ?thesis by (simp only: )
qed

lemma mult_if_delta:
  "(if P then (1::'a::comm_semiring_1) else 0) * q = (if P then q else 0)"
  by auto

text {* TODO: generalize @{thm compact_lemma}?! *}
lemma compact_blinfun_lemma:
  fixes f :: "nat \<Rightarrow> 'a::euclidean_space blinfun"
  assumes "bounded (range f)"
  shows "\<forall>d\<subseteq>Basis. \<exists>l::'a blinfun. \<exists> r.
    subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) i) (l i) < e) sequentially)"
proof safe
  fix d :: "'a set"
  assume d: "d \<subseteq> Basis"
  with finite_Basis have "finite d"
    by (blast intro: finite_subset)
  from this d show "\<exists>l::'a blinfun. \<exists>r. subseq r \<and>
    (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) i) (l i) < e) sequentially)"
  proof (induct d)
    case empty
    then show ?case
      unfolding subseq_def by auto
  next
    case (insert k d)
    have k[intro]: "k \<in> Basis"
      using insert by auto
    have s': "bounded ((\<lambda>x. x $ k) ` range f)"
      using `bounded (range f)`
      by (auto intro!: bounded_linear_image bounded_linear_inner_left)
    obtain l1::"'a blinfun" and r1 where r1: "subseq r1"
      and lr1: "\<forall>e > 0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) i) (l1 i) < e) sequentially"
      using insert(3) using insert(4) by auto
    have f': "\<forall>n. f (r1 n) $ k \<in> (\<lambda>x. x $ k) ` range f"
      by simp
    have "bounded (range (\<lambda>i. f (r1 i) $ k))"
      by (metis (lifting) bounded_subset f' image_subsetI s')
    then obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) $ k) ---> l2) sequentially"
      using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) $ k"]
      by (auto simp: o_def)
    def r \<equiv> "r1 \<circ> r2"
    have r:"subseq r"
      using r1 and r2 unfolding r_def o_def subseq_def by auto
    moreover
    def l \<equiv> "blinfun_of_matrix (\<lambda>i j. if j = k then l2 \<bullet> i else l1 $ j \<bullet> i)::'a blinfun"
    {
      fix e::real
      assume "e > 0"
      from lr1 `e > 0` have N1: "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n)  i) (l1  i) < e) sequentially"
        by blast
      from lr2 `e > 0` have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n))  k) l2 < e) sequentially"
        by (rule tendstoD)
      from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n))  i) (l1  i) < e) sequentially"
        by (rule eventually_subseq)
      have l2: "l $ k = l2"
        using insert.prems
        by (auto simp: blinfun_of_matrix.rep_eq inner_Basis l_def mult_if_delta
          scaleR_setsum_left[symmetric] setsum.delta' intro!: euclidean_eqI[where 'a='a])
      {
        fix i assume "i \<in> d"
        with insert have "i \<in> Basis" "i \<noteq> k" by auto
        hence l1: "l $ i = (l1 $ i)"
          by (auto simp: blinfun_of_matrix.rep_eq inner_Basis l_def mult_if_delta
            scaleR_setsum_left[symmetric] setsum.delta' intro!: euclidean_eqI[where 'a='a])
      } note l1 = this
      have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n)  i) (l  i) < e) sequentially"
        using N1' N2
        by eventually_elim (insert insert.prems, auto simp: r_def o_def l1 l2)
    }
    ultimately show ?case by auto
  qed
qed

text {* TODO: can generalize? *}
instance blinfun :: (euclidean_space) heine_borel
proof
  fix f :: "nat \<Rightarrow> 'a blinfun"
  assume f: "bounded (range f)"
  then obtain l::"'a blinfun" and r where r: "subseq r"
    and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) $ i) (l $ i) < e) sequentially"
    using compact_blinfun_lemma [OF f] by blast
  {
    fix e::real
    let ?d = "real_of_nat DIM('a) * real_of_nat DIM('a)"
    assume "e > 0"
    hence "e / ?d > 0" by (simp add: DIM_positive)
    with l have "eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) i) (l i) < e / ?d) sequentially"
      by simp
    moreover
    {
      fix n
      assume n: "\<forall>i\<in>Basis. dist (f (r n) i) (l i) < e / ?d"
      have "norm (f (r n) - l) = norm (blinfun_of_matrix (\<lambda>i j. (f (r n) - l) $ j \<bullet> i))"
        unfolding blinfun_of_matrix_works ..
      also note norm_blinfun_of_matrix
      also have "(\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. \<bar>(f (r n) - l) $ j \<bullet> i\<bar>) < (\<Sum>i\<in>(Basis::'a set). e / real_of_nat DIM('a))"
      proof (rule setsum_strict_mono)
        fix i::'a assume i: "i \<in> Basis"
        have "(\<Sum>j::'a\<in>Basis. \<bar>(f (r n) - l) $ j \<bullet> i\<bar>) < (\<Sum>j::'a\<in>Basis. e / ?d)"
        proof (rule setsum_strict_mono)
          fix j::'a assume j: "j \<in> Basis"
          have "\<bar>(f (r n) - l) $ j \<bullet> i\<bar> \<le> norm ((f (r n) - l) $ j)"
            by (simp add: Basis_le_norm i)
          also have "\<dots> < e / ?d"
            using n i j by (auto simp: dist_norm)
          finally show "\<bar>(f (r n) - l) $ j \<bullet> i\<bar> < e / ?d" by simp
        qed simp_all
        also have "\<dots> \<le> e / real_of_nat DIM('a)"
          by simp
        finally show "(\<Sum>j\<in>Basis. \<bar>(f (r n) - l) $ j \<bullet> i\<bar>) < e / real_of_nat DIM('a)"
          by simp
      qed simp_all
      also have "\<dots> \<le> e" by simp
      finally have "dist (f (r n)) l < e"
        by (auto simp: dist_norm)
    }
    ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
      by (rule eventually_elim1)
  }
  then have *: "((f \<circ> r) ---> l) sequentially"
    unfolding o_def tendsto_iff by simp
  with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
    by auto
qed

no_notation
  blinfun_apply (infixl "$" 999)
notation vec_nth (infixl "$" 90)

end
