# HG changeset patch
# User immler
# Date 1450817907 -3600
# Node ID e9812a95d108826d9498c6ef8805eb702682da8d
# Parent  16bfe0a6702dbecde8884affa0597b2102988c4e
theory for type of bounded linear functions; differentiation under the integral sign

diff -r 16bfe0a6702d -r e9812a95d108 src/HOL/Library/Inner_Product.thy
--- a/src/HOL/Library/Inner_Product.thy	Tue Dec 22 15:39:01 2015 +0100
+++ b/src/HOL/Library/Inner_Product.thy	Tue Dec 22 21:58:27 2015 +0100
@@ -213,6 +213,10 @@
 lemmas bounded_linear_inner_right =
   bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
 
+lemmas bounded_linear_inner_left_comp = bounded_linear_inner_left[THEN bounded_linear_compose]
+
+lemmas bounded_linear_inner_right_comp = bounded_linear_inner_right[THEN bounded_linear_compose]
+
 lemmas has_derivative_inner_right [derivative_intros] =
   bounded_linear.has_derivative [OF bounded_linear_inner_right]
 
diff -r 16bfe0a6702d -r e9812a95d108 src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Tue Dec 22 15:39:01 2015 +0100
+++ b/src/HOL/Library/Product_Vector.thy	Tue Dec 22 21:58:27 2015 +0100
@@ -449,6 +449,10 @@
   using snd_add snd_scaleR
   by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
 
+lemmas bounded_linear_fst_comp = bounded_linear_fst[THEN bounded_linear_compose]
+
+lemmas bounded_linear_snd_comp = bounded_linear_snd[THEN bounded_linear_compose]
+
 lemma bounded_linear_Pair:
   assumes f: "bounded_linear f"
   assumes g: "bounded_linear g"
diff -r 16bfe0a6702d -r e9812a95d108 src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Tue Dec 22 21:58:27 2015 +0100
@@ -0,0 +1,726 @@
+(*  Title:      HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
+    Author:     Fabian Immler, TU München
+*)
+
+section {* Bounded Linear Function *}
+
+theory Bounded_Linear_Function
+imports
+  Topology_Euclidean_Space
+  Operator_Norm
+begin
+
+subsection {* Intro rules for @{term bounded_linear} *}
+
+named_theorems bounded_linear_intros
+
+lemma onorm_inner_left:
+  assumes "bounded_linear r"
+  shows "onorm (\<lambda>x. r x \<bullet> f) \<le> onorm r * norm f"
+proof (rule onorm_bound)
+  fix x
+  have "norm (r x \<bullet> f) \<le> norm (r x) * norm f"
+    by (simp add: Cauchy_Schwarz_ineq2)
+  also have "\<dots> \<le> onorm r * norm x * norm f"
+    by (intro mult_right_mono onorm assms norm_ge_zero)
+  finally show "norm (r x \<bullet> f) \<le> onorm r * norm f * norm x"
+    by (simp add: ac_simps)
+qed (intro mult_nonneg_nonneg norm_ge_zero onorm_pos_le assms)
+
+lemma onorm_inner_right:
+  assumes "bounded_linear r"
+  shows "onorm (\<lambda>x. f \<bullet> r x) \<le> norm f * onorm r"
+  apply (subst inner_commute)
+  apply (rule onorm_inner_left[OF assms, THEN order_trans])
+  apply simp
+  done
+
+lemmas [bounded_linear_intros] =
+  bounded_linear_zero
+  bounded_linear_add
+  bounded_linear_const_mult
+  bounded_linear_mult_const
+  bounded_linear_scaleR_const
+  bounded_linear_const_scaleR
+  bounded_linear_ident
+  bounded_linear_setsum
+  bounded_linear_Pair
+  bounded_linear_sub
+  bounded_linear_fst_comp
+  bounded_linear_snd_comp
+  bounded_linear_inner_left_comp
+  bounded_linear_inner_right_comp
+
+
+subsection \<open>declaration of derivative/continuous/tendsto introduction rules for bounded linear functions\<close>
+
+attribute_setup bounded_linear =
+  \<open>Scan.succeed (Thm.declaration_attribute (fn thm =>
+    fold (fn (r, s) => Named_Theorems.add_thm s (thm RS r))
+      [
+        (@{thm bounded_linear.has_derivative}, "Deriv.derivative_intros"),
+        (@{thm bounded_linear.tendsto}, "Topological_Spaces.tendsto_intros"),
+        (@{thm bounded_linear.continuous}, "Topological_Spaces.continuous_intros"),
+        (@{thm bounded_linear.continuous_on}, "Topological_Spaces.continuous_intros"),
+        (@{thm bounded_linear.uniformly_continuous_on}, "Topological_Spaces.continuous_intros"),
+        (@{thm bounded_linear_compose}, "Bounded_Linear_Function.bounded_linear_intros")
+      ]))\<close>
+
+attribute_setup bounded_bilinear =
+  \<open>Scan.succeed (Thm.declaration_attribute (fn thm =>
+    fold (fn (r, s) => Named_Theorems.add_thm s (thm RS r))
+      [
+        (@{thm bounded_bilinear.FDERIV}, "Deriv.derivative_intros"),
+        (@{thm bounded_bilinear.tendsto}, "Topological_Spaces.tendsto_intros"),
+        (@{thm bounded_bilinear.continuous}, "Topological_Spaces.continuous_intros"),
+        (@{thm bounded_bilinear.continuous_on}, "Topological_Spaces.continuous_intros"),
+        (@{thm bounded_linear_compose[OF bounded_bilinear.bounded_linear_left]},
+          "Bounded_Linear_Function.bounded_linear_intros"),
+        (@{thm bounded_linear_compose[OF bounded_bilinear.bounded_linear_right]},
+          "Bounded_Linear_Function.bounded_linear_intros"),
+        (@{thm bounded_linear.uniformly_continuous_on[OF bounded_bilinear.bounded_linear_left]},
+          "Topological_Spaces.continuous_intros"),
+        (@{thm bounded_linear.uniformly_continuous_on[OF bounded_bilinear.bounded_linear_right]},
+          "Topological_Spaces.continuous_intros")
+      ]))\<close>
+
+
+subsection \<open>type of bounded linear functions\<close>
+
+typedef (overloaded) ('a, 'b) blinfun ("(_ \<Rightarrow>\<^sub>L /_)" [22, 21] 21) =
+  "{f::'a::real_normed_vector\<Rightarrow>'b::real_normed_vector. bounded_linear f}"
+  morphisms blinfun_apply Blinfun
+  by (blast intro: bounded_linear_intros)
+
+declare [[coercion
+    "blinfun_apply :: ('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'b"]]
+
+lemma bounded_linear_blinfun_apply[bounded_linear_intros]:
+  "bounded_linear g \<Longrightarrow> bounded_linear (\<lambda>x. blinfun_apply f (g x))"
+  by (metis blinfun_apply mem_Collect_eq bounded_linear_compose)
+
+setup_lifting type_definition_blinfun
+
+lemma blinfun_eqI: "(\<And>i. blinfun_apply x i = blinfun_apply y i) \<Longrightarrow> x = y"
+  by transfer auto
+
+lemma bounded_linear_Blinfun_apply: "bounded_linear f \<Longrightarrow> blinfun_apply (Blinfun f) = f"
+  by (auto simp: Blinfun_inverse)
+
+
+subsection \<open>type class instantiations\<close>
+
+instantiation blinfun :: (real_normed_vector, real_normed_vector) real_normed_vector
+begin
+
+lift_definition norm_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> real" is onorm .
+
+lift_definition minus_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
+  is "\<lambda>f g x. f x - g x"
+  by (rule bounded_linear_sub)
+
+definition dist_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> real"
+  where "dist_blinfun a b = norm (a - b)"
+
+definition open_blinfun :: "('a \<Rightarrow>\<^sub>L 'b) 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 \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b" is "\<lambda>f x. - f x"
+  by (rule bounded_linear_minus)
+
+lift_definition zero_blinfun :: "'a \<Rightarrow>\<^sub>L 'b" is "\<lambda>x. 0"
+  by (rule bounded_linear_zero)
+
+lift_definition plus_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
+  is "\<lambda>f g x. f x + g x"
+  by (metis bounded_linear_add)
+
+lift_definition scaleR_blinfun::"real \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b" is "\<lambda>r f x. r *\<^sub>R f x"
+  by (metis bounded_linear_compose bounded_linear_scaleR_right)
+
+definition sgn_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
+  where "sgn_blinfun x = scaleR (inverse (norm x)) x"
+
+instance
+  apply standard
+  unfolding dist_blinfun_def open_blinfun_def sgn_blinfun_def
+  apply (transfer, force simp: onorm_triangle onorm_scaleR onorm_eq_0 algebra_simps)+
+  done
+
+end
+
+lemma norm_blinfun_eqI:
+  assumes "n \<le> norm (blinfun_apply f x) / norm x"
+  assumes "\<And>x. norm (blinfun_apply 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]
+    bounded_linear_intros)
+
+lemma norm_blinfun: "norm (blinfun_apply f x) \<le> norm f * norm x"
+  by transfer (rule onorm)
+
+lemma norm_blinfun_bound: "0 \<le> b \<Longrightarrow> (\<And>x. norm (blinfun_apply f x) \<le> b * norm x) \<Longrightarrow> norm f \<le> b"
+  by transfer (rule onorm_bound)
+
+lemma bounded_bilinear_blinfun_apply[bounded_bilinear]: "bounded_bilinear blinfun_apply"
+proof
+  fix f g::"'a \<Rightarrow>\<^sub>L 'b" and a b::'a and r::real
+  show "(f + g) a = f a + g a" "(r *\<^sub>R f) a = r *\<^sub>R f a"
+    by (transfer, simp)+
+  interpret bounded_linear f for f::"'a \<Rightarrow>\<^sub>L 'b"
+    by (auto intro!: bounded_linear_intros)
+  show "f (a + b) = f a + f b" "f (r *\<^sub>R a) = r *\<^sub>R f a"
+    by (simp_all add: add scaleR)
+  show "\<exists>K. \<forall>a b. norm (blinfun_apply a b) \<le> norm a * norm b * K"
+    by (auto intro!: exI[where x=1] norm_blinfun)
+qed
+
+interpretation blinfun: bounded_bilinear blinfun_apply
+  by (rule bounded_bilinear_blinfun_apply)
+
+lemmas bounded_linear_apply_blinfun[intro, simp] = blinfun.bounded_linear_left
+
+
+context bounded_bilinear
+begin
+
+named_theorems bilinear_simps
+
+lemmas [bilinear_simps] =
+  add_left
+  add_right
+  diff_left
+  diff_right
+  minus_left
+  minus_right
+  scaleR_left
+  scaleR_right
+  zero_left
+  zero_right
+  setsum_left
+  setsum_right
+
+end
+
+
+instance blinfun :: (banach, banach) banach
+proof
+  fix X::"nat \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
+  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 add: blinfun.bilinear_simps)
+          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 add: blinfun.bilinear_simps)
+    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", unfolded blinfun.bilinear_simps]
+      tendsto_scaleR[OF tendsto_const[of r] v[of x]] v[of "r *\<^sub>R x", unfolded blinfun.bilinear_simps]
+    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 m)
+          have "norm (X n x - X m x) = norm ((X n - X m) x)"
+            by (simp add: blinfun.bilinear_simps)
+          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 simp: blinfun.bilinear_simps)
+      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
+
+subsection {* On Euclidean Space *}
+
+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 norm_blinfun_euclidean_le:
+  fixes a::"'a::euclidean_space \<Rightarrow>\<^sub>L 'b::real_normed_vector"
+  shows "norm a \<le> setsum (\<lambda>x. norm (a x)) Basis"
+  apply (rule norm_blinfun_bound)
+   apply (simp add: setsum_nonneg)
+  apply (subst euclidean_representation[symmetric, where 'a='a])
+  apply (simp only: blinfun.bilinear_simps setsum_left_distrib)
+  apply (rule order.trans[OF norm_setsum setsum_mono])
+  apply (simp add: abs_mult mult_right_mono ac_simps Basis_le_norm)
+  done
+
+lemma tendsto_componentwise1:
+  fixes a::"'a::euclidean_space \<Rightarrow>\<^sub>L 'b::real_normed_vector"
+    and b::"'c \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
+  assumes "(\<And>j. j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n j) ---> a j) F)"
+  shows "(b ---> a) F"
+proof -
+  have "\<And>j. j \<in> Basis \<Longrightarrow> Zfun (\<lambda>x. norm (b x j - a j)) F"
+    using assms unfolding tendsto_Zfun_iff Zfun_norm_iff .
+  hence "Zfun (\<lambda>x. \<Sum>j\<in>Basis. norm (b x j - a j)) F"
+    by (auto intro!: Zfun_setsum)
+  thus ?thesis
+    unfolding tendsto_Zfun_iff
+    by (rule Zfun_le)
+      (auto intro!: order_trans[OF norm_blinfun_euclidean_le] simp: blinfun.bilinear_simps)
+qed
+
+lift_definition
+  blinfun_of_matrix::"('b::euclidean_space \<Rightarrow> 'a::euclidean_space \<Rightarrow> real) \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
+  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_intros)
+
+lemma blinfun_of_matrix_works:
+  fixes f::"'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space"
+  shows "blinfun_of_matrix (\<lambda>i j. (f j) \<bullet> i) = f"
+proof (transfer, rule,  rule euclidean_eqI)
+  fix f::"'a \<Rightarrow> 'b" and x::'a and b::'b 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 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 add: setsum_nonneg)
+  apply (simp only: blinfun_of_matrix_apply setsum_left_distrib)
+  apply (rule order_trans[OF norm_setsum setsum_mono])
+  apply (rule order_trans[OF norm_setsum setsum_mono])
+  apply (simp add: abs_mult mult_right_mono ac_simps Basis_le_norm)
+  done
+
+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:
+  fixes a::"'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space"
+    and b::"'c \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
+  shows "(\<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 \<Rightarrow>\<^sub>L 'c::euclidean_space"
+  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)
+
+lemma
+  continuous_blinfun_componentwiseI1:
+  fixes f:: "'b::t2_space \<Rightarrow> 'a::euclidean_space \<Rightarrow>\<^sub>L 'c::real_normed_vector"
+  assumes "\<And>i. i \<in> Basis \<Longrightarrow> continuous F (\<lambda>x. f x i)"
+  shows "continuous F f"
+  using assms by (auto simp: continuous_def intro!: tendsto_componentwise1)
+
+lemma bounded_linear_blinfun_matrix: "bounded_linear (\<lambda>x. (x::_\<Rightarrow>\<^sub>L _) j \<bullet> i)"
+  by (auto intro!: bounded_linearI' bounded_linear_intros)
+
+lemma continuous_blinfun_matrix:
+  fixes f:: "'b::t2_space \<Rightarrow> 'a::real_normed_vector \<Rightarrow>\<^sub>L 'c::real_inner"
+  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::real_normed_vector \<Rightarrow>\<^sub>L 'c::real_inner"
+  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 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 this and @{thm compact_lemma}?! *}
+lemma compact_blinfun_lemma:
+  fixes f :: "nat \<Rightarrow> 'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space"
+  assumes "bounded (range f)"
+  shows "\<forall>d\<subseteq>Basis. \<exists>l::'a \<Rightarrow>\<^sub>L 'b. \<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 \<Rightarrow>\<^sub>L 'b. \<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. blinfun_apply x k) ` range f)"
+      using `bounded (range f)`
+      by (auto intro!: bounded_linear_image bounded_linear_intros)
+    obtain l1::"'a \<Rightarrow>\<^sub>L 'b" 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. blinfun_apply 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 \<Rightarrow>\<^sub>L 'b"
+    {
+      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='b])
+      {
+        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='b])
+      } 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
+
+lemma blinfun_euclidean_eqI: "(\<And>i. i \<in> Basis \<Longrightarrow> blinfun_apply x i = blinfun_apply y i) \<Longrightarrow> x = y"
+  apply (auto intro!: blinfun_eqI)
+  apply (subst (2) euclidean_representation[symmetric, where 'a='a])
+  apply (subst (1) euclidean_representation[symmetric, where 'a='a])
+  apply (simp add: blinfun.bilinear_simps)
+  done
+
+text {* TODO: generalize (via @{thm compact_cball})? *}
+instance blinfun :: (euclidean_space, euclidean_space) heine_borel
+proof
+  fix f :: "nat \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
+  assume f: "bounded (range f)"
+  then obtain l::"'a \<Rightarrow>\<^sub>L 'b" 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('b)"
+    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::'b set). e / real_of_nat DIM('b))"
+      proof (rule setsum_strict_mono)
+        fix i::'b 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 blinfun.bilinear_simps)
+          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('b)"
+          by simp
+        finally show "(\<Sum>j\<in>Basis. \<bar>(f (r n) - l) j \<bullet> i\<bar>) < e / real_of_nat DIM('b)"
+          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"
+      using eventually_elim2 by force
+  }
+  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
+
+
+subsection \<open>concrete bounded linear functions\<close>
+
+lemma bounded_linear_bounded_bilinear_blinfun_applyI: --"TODO: transfer rule!"
+  assumes n: "bounded_bilinear (\<lambda>i x. (blinfun_apply (f x) i))"
+  shows "bounded_linear f"
+proof (unfold_locales, safe intro!: blinfun_eqI)
+  fix i
+  interpret bounded_bilinear "\<lambda>i x. f x i" by fact
+  show "f (x + y) i = (f x + f y) i" "f (r *\<^sub>R x) i = (r *\<^sub>R f x) i" for r x y
+    by (auto intro!: blinfun_eqI simp: blinfun.bilinear_simps)
+  from _ nonneg_bounded show "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
+    by (rule ex_reg) (auto intro!: onorm_bound simp: norm_blinfun.rep_eq assms ac_simps)
+qed
+
+context bounded_bilinear
+begin
+
+lift_definition prod_left::"'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'c" is "(\<lambda>b a. prod a b)"
+  by (rule bounded_linear_left)
+declare prod_left.rep_eq[simp]
+
+lemma bounded_linear_prod_left[bounded_linear]: "bounded_linear prod_left"
+  by (rule bounded_linear_bounded_bilinear_blinfun_applyI) (auto simp: bounded_bilinear_axioms)
+
+lift_definition prod_right::"'a \<Rightarrow> 'b \<Rightarrow>\<^sub>L 'c" is "(\<lambda>a b. prod a b)"
+  by (rule bounded_linear_right)
+declare prod_right.rep_eq[simp]
+
+lemma bounded_linear_prod_right[bounded_linear]: "bounded_linear prod_right"
+  by (rule bounded_linear_bounded_bilinear_blinfun_applyI) (auto simp: flip)
+
+end
+
+lift_definition id_blinfun::"'a::real_normed_vector \<Rightarrow>\<^sub>L 'a" is "\<lambda>x. x"
+  by (rule bounded_linear_ident)
+
+lemmas blinfun_apply_id_blinfun[simp] = id_blinfun.rep_eq
+
+lemma norm_blinfun_id[simp]:
+  "norm (id_blinfun::'a::{real_normed_vector, perfect_space} \<Rightarrow>\<^sub>L 'a) = 1"
+  by transfer (auto simp: onorm_id)
+
+lemma norm_blinfun_id_le:
+  "norm (id_blinfun::'a::real_normed_vector \<Rightarrow>\<^sub>L 'a) \<le> 1"
+  by transfer (auto simp: onorm_id_le)
+
+
+lift_definition fst_blinfun::"('a::real_normed_vector \<times> 'b::real_normed_vector) \<Rightarrow>\<^sub>L 'a" is fst
+  by (rule bounded_linear_fst)
+
+lemma blinfun_apply_fst_blinfun[simp]: "blinfun_apply fst_blinfun = fst"
+  by transfer (rule refl)
+
+
+lift_definition snd_blinfun::"('a::real_normed_vector \<times> 'b::real_normed_vector) \<Rightarrow>\<^sub>L 'b" is snd
+  by (rule bounded_linear_snd)
+
+lemma blinfun_apply_snd_blinfun[simp]: "blinfun_apply snd_blinfun = snd"
+  by transfer (rule refl)
+
+
+lift_definition blinfun_compose::
+  "'a::real_normed_vector \<Rightarrow>\<^sub>L 'b::real_normed_vector \<Rightarrow>
+    'c::real_normed_vector \<Rightarrow>\<^sub>L 'a \<Rightarrow>
+    'c \<Rightarrow>\<^sub>L 'b" (infixl "o\<^sub>L" 55) is "op o"
+  parametric comp_transfer
+  unfolding o_def
+  by (rule bounded_linear_compose)
+
+lemma blinfun_apply_blinfun_compose[simp]: "(a o\<^sub>L b) c = a (b c)"
+  by (simp add: blinfun_compose.rep_eq)
+
+lemma norm_blinfun_compose:
+  "norm (f o\<^sub>L g) \<le> norm f * norm g"
+  by transfer (rule onorm_compose)
+
+lemma bounded_bilinear_blinfun_compose[bounded_bilinear]: "bounded_bilinear op o\<^sub>L"
+  by unfold_locales
+    (auto intro!: blinfun_eqI exI[where x=1] simp: blinfun.bilinear_simps norm_blinfun_compose)
+
+
+lift_definition blinfun_inner_right::"'a::real_inner \<Rightarrow> 'a \<Rightarrow>\<^sub>L real" is "op \<bullet>"
+  by (rule bounded_linear_inner_right)
+declare blinfun_inner_right.rep_eq[simp]
+
+lemma bounded_linear_blinfun_inner_right[bounded_linear]: "bounded_linear blinfun_inner_right"
+  by (rule bounded_linear_bounded_bilinear_blinfun_applyI)
+    (auto simp: bounded_bilinear.flip[OF bounded_bilinear_inner])
+
+
+lift_definition blinfun_inner_left::"'a::real_inner \<Rightarrow> 'a \<Rightarrow>\<^sub>L real" is "\<lambda>x y. y \<bullet> x"
+  by (rule bounded_linear_inner_left)
+declare blinfun_inner_left.rep_eq[simp]
+
+lemma bounded_linear_blinfun_inner_left[bounded_linear]: "bounded_linear blinfun_inner_left"
+  by (rule bounded_linear_bounded_bilinear_blinfun_applyI) (auto simp: bounded_bilinear_inner)
+
+
+lift_definition blinfun_scaleR_right::"real \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_vector" is "op *\<^sub>R"
+  by (rule bounded_linear_scaleR_right)
+declare blinfun_scaleR_right.rep_eq[simp]
+
+lemma bounded_linear_blinfun_scaleR_right[bounded_linear]: "bounded_linear blinfun_scaleR_right"
+  by (rule bounded_linear_bounded_bilinear_blinfun_applyI)
+    (auto simp: bounded_bilinear.flip[OF bounded_bilinear_scaleR])
+
+
+lift_definition blinfun_scaleR_left::"'a::real_normed_vector \<Rightarrow> real \<Rightarrow>\<^sub>L 'a" is "\<lambda>x y. y *\<^sub>R x"
+  by (rule bounded_linear_scaleR_left)
+lemmas [simp] = blinfun_scaleR_left.rep_eq
+
+lemma bounded_linear_blinfun_scaleR_left[bounded_linear]: "bounded_linear blinfun_scaleR_left"
+  by (rule bounded_linear_bounded_bilinear_blinfun_applyI) (auto simp: bounded_bilinear_scaleR)
+
+
+lift_definition blinfun_mult_right::"'a \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_algebra" is "op *"
+  by (rule bounded_linear_mult_right)
+declare blinfun_mult_right.rep_eq[simp]
+
+lemma bounded_linear_blinfun_mult_right[bounded_linear]: "bounded_linear blinfun_mult_right"
+  by (rule bounded_linear_bounded_bilinear_blinfun_applyI)
+    (auto simp: bounded_bilinear.flip[OF bounded_bilinear_mult])
+
+
+lift_definition blinfun_mult_left::"'a::real_normed_algebra \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a" is "\<lambda>x y. y * x"
+  by (rule bounded_linear_mult_left)
+lemmas [simp] = blinfun_mult_left.rep_eq
+
+lemma bounded_linear_blinfun_mult_left[bounded_linear]: "bounded_linear blinfun_mult_left"
+  by (rule bounded_linear_bounded_bilinear_blinfun_applyI) (auto simp: bounded_bilinear_mult)
+
+end
diff -r 16bfe0a6702d -r e9812a95d108 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Dec 22 15:39:01 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Dec 22 21:58:27 2015 +0100
@@ -9,6 +9,27 @@
 imports Brouwer_Fixpoint Operator_Norm Uniform_Limit
 begin
 
+lemma onorm_inner_left:
+  assumes "bounded_linear r"
+  shows "onorm (\<lambda>x. r x \<bullet> f) \<le> onorm r * norm f"
+proof (rule onorm_bound)
+  fix x
+  have "norm (r x \<bullet> f) \<le> norm (r x) * norm f"
+    by (simp add: Cauchy_Schwarz_ineq2)
+  also have "\<dots> \<le> onorm r * norm x * norm f"
+    by (intro mult_right_mono onorm assms norm_ge_zero)
+  finally show "norm (r x \<bullet> f) \<le> onorm r * norm f * norm x"
+    by (simp add: ac_simps)
+qed (intro mult_nonneg_nonneg norm_ge_zero onorm_pos_le assms)
+
+lemma onorm_inner_right:
+  assumes "bounded_linear r"
+  shows "onorm (\<lambda>x. f \<bullet> r x) \<le> norm f * onorm r"
+  apply (subst inner_commute)
+  apply (rule onorm_inner_left[OF assms, THEN order_trans])
+  apply simp
+  done
+
 declare has_derivative_bounded_linear[dest]
 
 subsection \<open>Derivatives\<close>
@@ -506,18 +527,6 @@
 
 subsection \<open>The traditional Rolle theorem in one dimension\<close>
 
-lemma linear_componentwise:
-  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
-  assumes lf: "linear f"
-  shows "(f x) \<bullet> j = (\<Sum>i\<in>Basis. (x\<bullet>i) * (f i\<bullet>j))" (is "?lhs = ?rhs")
-proof -
-  have "?rhs = (\<Sum>i\<in>Basis. (x\<bullet>i) *\<^sub>R (f i))\<bullet>j"
-    by (simp add: inner_setsum_left)
-  then show ?thesis
-    unfolding linear_setsum_mul[OF lf, symmetric]
-    unfolding euclidean_representation ..
-qed
-
 text \<open>Derivatives of local minima and maxima are zero.\<close>
 
 lemma has_derivative_local_min:
@@ -1714,10 +1723,6 @@
 also continuous. So if we know for some other reason that the inverse
 function exists, it's OK.\<close>
 
-lemma bounded_linear_sub: "bounded_linear f \<Longrightarrow> bounded_linear g \<Longrightarrow> bounded_linear (\<lambda>x. f x - g x)"
-  using bounded_linear_add[of f "\<lambda>x. - g x"] bounded_linear_minus[of g]
-  by (auto simp add: algebra_simps)
-
 lemma has_derivative_locally_injective:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   assumes "a \<in> s"
diff -r 16bfe0a6702d -r e9812a95d108 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Dec 22 15:39:01 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Dec 22 21:58:27 2015 +0100
@@ -9,6 +9,7 @@
   Derivative
   Uniform_Limit
   "~~/src/HOL/Library/Indicator_Function"
+  Bounded_Linear_Function
 begin
 
 lemma cSup_abs_le: (* TODO: move to Conditionally_Complete_Lattices.thy? *)
@@ -2797,6 +2798,16 @@
 lemma integral_singleton [simp]: "integral {a} f = 0"
   by auto
 
+lemma integral_blinfun_apply:
+  assumes "f integrable_on s"
+  shows "integral s (\<lambda>x. blinfun_apply h (f x)) = blinfun_apply h (integral s f)"
+  by (subst integral_linear[symmetric, OF assms blinfun.bounded_linear_right]) (simp add: o_def)
+
+lemma blinfun_apply_integral:
+  assumes "f integrable_on s"
+  shows "blinfun_apply (integral s f) x = integral s (\<lambda>y. blinfun_apply (f y) x)"
+  by (metis (no_types, lifting) assms blinfun.prod_left.rep_eq integral_blinfun_apply integral_cong)
+
 
 subsection \<open>Cauchy-type criterion for integrability.\<close>
 
@@ -11280,19 +11291,6 @@
   using assms(1,2)
   by induct auto
 
-lemma bounded_linear_setsum:
-  fixes f :: "'i \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
-  assumes f: "\<And>i. i \<in> I \<Longrightarrow> bounded_linear (f i)"
-  shows "bounded_linear (\<lambda>x. \<Sum>i\<in>I. f i x)"
-proof (cases "finite I")
-  case True
-  from this f show ?thesis
-    by (induct I) (auto intro!: bounded_linear_add bounded_linear_zero)
-next
-  case False
-  then show ?thesis by simp
-qed
-
 lemma absolutely_integrable_vector_abs:
   fixes f :: "'a::euclidean_space => 'b::euclidean_space"
     and T :: "'c::euclidean_space \<Rightarrow> 'b"
@@ -11598,6 +11596,241 @@
 qed auto
 
 
+subsection \<open>differentiation under the integral sign\<close>
+
+lemma tube_lemma:
+  assumes "compact K"
+  assumes "open W"
+  assumes "{x0} \<times> K \<subseteq> W"
+  shows "\<exists>X0. x0 \<in> X0 \<and> open X0 \<and> X0 \<times> K \<subseteq> W"
+proof -
+  {
+    fix y assume "y \<in> K"
+    then have "(x0, y) \<in> W" using assms by auto
+    with \<open>open W\<close>
+    have "\<exists>X0 Y. open X0 \<and> open Y \<and> x0 \<in> X0 \<and> y \<in> Y \<and> X0 \<times> Y \<subseteq> W"
+      by (rule open_prod_elim) blast
+  } then obtain X0 Y where
+    "\<forall>y \<in> K. open (X0 y) \<and> open (Y y) \<and> x0 \<in> X0 y \<and> y \<in> Y y \<and> X0 y \<times> Y y \<subseteq> W"
+    by metis
+  moreover
+  then have "\<forall>t\<in>Y ` K. open t" "K \<subseteq> \<Union>(Y ` K)" by auto
+  with \<open>compact K\<close> obtain CC where "CC \<subseteq> Y ` K" "finite CC" "K \<subseteq> \<Union>CC"
+    by (rule compactE)
+  moreover
+  then obtain c where c:
+    "\<And>C. C \<in> CC \<Longrightarrow> c C \<in> K \<and> C = Y (c C)"
+    by (force intro!: choice)
+  ultimately show ?thesis
+    by (force intro!: exI[where x="\<Inter>C\<in>CC. X0 (c C)"])
+qed
+
+lemma eventually_closed_segment:
+  fixes x0::"'a::real_normed_vector"
+  assumes "open X0" "x0 \<in> X0"
+  shows "\<forall>\<^sub>F x in at x0 within U. closed_segment x0 x \<subseteq> X0"
+proof -
+  from openE[OF assms]
+  obtain e where e: "0 < e" "ball x0 e \<subseteq> X0" .
+  then have "\<forall>\<^sub>F x in at x0 within U. x \<in> ball x0 e"
+    by (auto simp: dist_commute eventually_at)
+  then show ?thesis
+  proof eventually_elim
+    case (elim x)
+    have "x0 \<in> ball x0 e" using \<open>e > 0\<close> by simp
+    from convex_ball[unfolded convex_contains_segment, rule_format, OF this elim]
+    have "closed_segment x0 x \<subseteq> ball x0 e" .
+    also note \<open>\<dots> \<subseteq> X0\<close>
+    finally show ?case .
+  qed
+qed
+
+lemma leibniz_rule:
+  fixes f::"'a::banach \<times> 'b::euclidean_space \<Rightarrow> 'c::banach"
+  assumes fx: "\<And>x t. x \<in> U \<Longrightarrow> t \<in> (cbox a b) \<Longrightarrow>
+    ((\<lambda>x. f (x, t)) has_derivative blinfun_apply (fx (x, t))) (at x within U)"
+  assumes integrable_f2: "\<And>x. x \<in> U \<Longrightarrow> (\<lambda>t. f (x, t)) integrable_on cbox a b"
+  assumes cont_fx: "continuous_on (U \<times> (cbox a b)) fx"
+  assumes [intro]: "x0 \<in> U"
+  assumes "convex U"
+  notes [continuous_intros] = continuous_on_compose2[OF cont_fx]
+  shows
+    "((\<lambda>x. integral (cbox a b) (\<lambda>t. f (x, t))) has_derivative integral (cbox a b) (\<lambda>t. fx (x0, t)))
+      (at x0 within U)"
+    (is "(?F has_derivative ?dF) _")
+proof cases
+  assume "content (cbox a b) \<noteq> 0"
+  then have ne: "cbox a b \<noteq> {}" by auto
+  show ?thesis
+  proof (intro has_derivativeI bounded_linear_scaleR_left tendstoI, fold norm_conv_dist)
+    have cont_f1: "\<And>t. t \<in> cbox a b \<Longrightarrow> continuous_on U (\<lambda>x. f (x, t))"
+      by (auto simp: continuous_on_eq_continuous_within intro!: has_derivative_continuous fx)
+    note [continuous_intros] = continuous_on_compose2[OF cont_f1]
+    fix e'::real
+    assume "e' > 0"
+    def e \<equiv> "e' / (content (cbox a b) + 1)"
+    have "e > 0" using \<open>e' > 0\<close> by (auto simp: e_def intro!: divide_pos_pos add_nonneg_pos)
+    def psi \<equiv> "\<lambda>(x, t). fx (x, t) - fx (x0, t)"
+    def W0 \<equiv> "{(x, t) \<in> U \<times> (cbox a b). norm (psi (x, t)) < e}"
+    have W0_eq: "W0 = (\<lambda>(x, t). norm (psi (x, t))) -` {..<e} \<inter> U \<times> (cbox a b)"
+      by (auto simp: vimage_def W0_def)
+    have "open {..<e}" by simp
+    have "continuous_on (U \<times> (cbox a b)) (\<lambda>(x, t). norm (psi (x, t)))"
+      by (auto intro!: continuous_intros simp: psi_def split_beta')
+    from this[unfolded continuous_on_open_invariant, rule_format, OF \<open>open {..<e}\<close>]
+    obtain W where W: "open W" "W \<inter> U \<times> (cbox a b) = W0 \<inter> U \<times> (cbox a b)"
+      unfolding W0_eq by blast
+    have "{x0} \<times> (cbox a b) \<subseteq> W \<inter> U \<times> (cbox a b)"
+      unfolding W
+      by (auto simp: W0_def psi_def \<open>0 < e\<close>)
+    then have "{x0} \<times> cbox a b \<subseteq> W" by blast
+    from tube_lemma[OF compact_cbox[of a b] \<open>open W\<close> this]
+    obtain X0 where X0: "x0 \<in> X0" "open X0" "X0 \<times> cbox a b \<subseteq> W"
+      by blast
+
+    note eventually_closed_segment[OF \<open>open X0\<close> \<open>x0 \<in> X0\<close>, of U]
+    moreover
+    have "\<forall>\<^sub>F x in at x0 within U. x \<in> X0"
+      using \<open>open X0\<close> \<open>x0 \<in> X0\<close> eventually_at_topological by blast
+    moreover have "\<forall>\<^sub>F x in at x0 within U. x \<noteq> x0"
+      by (auto simp: eventually_at_filter)
+    moreover have "\<forall>\<^sub>F x in at x0 within U. x \<in> U"
+      by (auto simp: eventually_at_filter)
+    ultimately
+    show "\<forall>\<^sub>F x in at x0 within U. norm ((?F x - ?F x0 - ?dF (x - x0)) /\<^sub>R norm (x - x0)) < e'"
+    proof eventually_elim
+      case (elim x)
+      from elim have "0 < norm (x - x0)" by simp
+      have "closed_segment x0 x \<subseteq> U"
+        by (rule \<open>convex U\<close>[unfolded convex_contains_segment, rule_format, OF \<open>x0 \<in> U\<close> \<open>x \<in> U\<close>])
+      from elim have [intro]: "x \<in> U" by auto
+
+      have "?F x - ?F x0 - ?dF (x - x0) =
+        integral (cbox a b) (\<lambda>xa. f (x, xa) - f (x0, xa) - fx (x0, xa) (x - x0))"
+        (is "_ = ?id")
+        using \<open>x \<noteq> x0\<close>
+        by (subst blinfun_apply_integral integral_diff,
+            auto intro!: integrable_diff integrable_f2 continuous_intros
+              intro: integrable_continuous)+
+      also
+      {
+        fix t assume t: "t \<in> (cbox a b)"
+        have seg: "\<And>t. t \<in> {0..1} \<Longrightarrow> x0 + t *\<^sub>R (x - x0) \<in> closed_segment x0 x \<inter> U"
+          using \<open>closed_segment x0 x \<subseteq> U\<close>
+          by (force simp: closed_segment_def algebra_simps)
+        from t have deriv:
+          "((\<lambda>x. f (x, t)) has_derivative (fx (y, t))) (at y within closed_segment x0 x \<inter> U)"
+          if "y \<in> closed_segment x0 x \<inter> U" for y
+          unfolding has_vector_derivative_def[symmetric]
+          using that \<open>x \<in> X0\<close>
+          by (intro has_derivative_within_subset[OF fx]) auto
+        have "\<forall>x\<in>closed_segment x0 x \<inter> U. norm (fx (x, t) - fx (x0, t)) \<le> e"
+        proof
+          fix y assume y: "y \<in> closed_segment x0 x \<inter> U"
+          have "norm (fx (y, t) - fx (x0, t)) = norm (psi (y, t))"
+            by (auto simp: psi_def)
+          also
+          {
+            have "(y, t) \<in> X0 \<times> (cbox a b)"
+              using t \<open>closed_segment x0 x \<subseteq> X0\<close> y
+              by auto
+            also note \<open>\<dots> \<subseteq> W\<close>
+            finally have "(y, t) \<in> W" .
+            with t y have "(y, t) \<in> W \<inter> U \<times> (cbox a b)"
+              by blast
+            also note \<open>W \<inter> U \<times> (cbox a b) = W0 \<inter> U \<times> (cbox a b)\<close>
+            finally  have "norm (psi (y, t)) < e"
+              by (auto simp: W0_def)
+          }
+          finally show "norm (fx (y, t) - fx (x0, t)) \<le> e" by simp
+        qed
+        then have onorm:
+          "\<forall>x\<in>closed_segment x0 x \<inter> U.
+            onorm (blinfun_apply (fx (x, t)) - blinfun_apply (fx (x0, t))) \<le> e"
+          by (auto simp: norm_blinfun.rep_eq blinfun.diff_left[abs_def] fun_diff_def)
+
+        from differentiable_bound_linearization[OF seg deriv onorm]
+        have "norm (f (x, t) - f (x0, t) - fx (x0, t) (x - x0)) \<le> e * norm (x - x0)"
+          by (auto simp add: ac_simps)
+      }
+      then have "norm ?id \<le> integral (cbox a b) (\<lambda>_. e * norm (x - x0))"
+        by (intro integral_norm_bound_integral)
+          (auto intro!: continuous_intros integrable_diff integrable_f2
+            intro: integrable_continuous)
+      also have "\<dots> = content (cbox a b) * e * norm (x - x0)"
+        by simp
+      also have "\<dots> < e' * norm (x - x0)"
+        using \<open>e' > 0\<close> content_pos_le[of a b]
+        by (intro mult_strict_right_mono[OF _ \<open>0 < norm (x - x0)\<close>])
+          (auto simp: divide_simps e_def)
+      finally have "norm (?F x - ?F x0 - ?dF (x - x0)) < e' * norm (x - x0)" .
+      then show ?case
+        by (auto simp: divide_simps)
+    qed
+  qed (rule blinfun.bounded_linear_right)
+qed (auto intro!: derivative_eq_intros simp: blinfun.bilinear_simps)
+
+lemma
+  has_vector_derivative_eq_has_derivative_blinfun:
+  "(f has_vector_derivative f') (at x within U) \<longleftrightarrow>
+    (f has_derivative blinfun_scaleR_left f') (at x within U)"
+  by (simp add: has_vector_derivative_def)
+
+lemma leibniz_rule_vector_derivative:
+  fixes f::"real \<times> 'b::euclidean_space \<Rightarrow> 'c::banach"
+  assumes fx: "\<And>x t. x \<in> U \<Longrightarrow> t \<in> (cbox a b) \<Longrightarrow>
+      ((\<lambda>x. f (x, t)) has_vector_derivative (fx (x, t))) (at x within U)"
+  assumes integrable_f2: "\<And>x. x \<in> U \<Longrightarrow> (\<lambda>t. f (x, t)) integrable_on cbox a b"
+  assumes cont_fx: "continuous_on (U \<times> (cbox a b)) fx"
+  assumes U: "x0 \<in> U" "convex U"
+  notes [continuous_intros] = continuous_on_compose2[OF cont_fx]
+  shows
+    "((\<lambda>x. integral (cbox a b) (\<lambda>t. f (x, t))) has_vector_derivative
+      integral (cbox a b) (\<lambda>t. fx (x0, t))) (at x0 within U)"
+proof -
+  have *: "blinfun_scaleR_left (integral (cbox a b) (\<lambda>t. fx (x0, t))) =
+    integral (cbox a b) (\<lambda>t. blinfun_scaleR_left (fx (x0, t)))"
+    by (subst integral_linear[symmetric])
+       (auto simp: has_vector_derivative_def o_def
+         intro!: integrable_continuous U continuous_intros bounded_linear_intros)
+  show ?thesis
+    unfolding has_vector_derivative_eq_has_derivative_blinfun
+    apply (rule has_derivative_eq_rhs)
+    apply (rule leibniz_rule[OF _ integrable_f2 _ U, where fx="\<lambda>x. blinfun_scaleR_left (fx x)"])
+    using assms(1)
+    apply (auto simp: has_vector_derivative_def * intro!: continuous_intros)
+    done
+qed
+
+lemma
+  has_field_derivative_eq_has_derivative_blinfun:
+  "(f has_field_derivative f') (at x within U) \<longleftrightarrow> (f has_derivative blinfun_mult_right f') (at x within U)"
+  by (simp add: has_field_derivative_def)
+
+lemma leibniz_rule_field_derivative:
+  fixes f::"'a::{real_normed_field, banach} \<times> 'b::euclidean_space \<Rightarrow> 'a"
+  assumes fx: "\<And>x t. x \<in> U \<Longrightarrow> t \<in> (cbox a b) \<Longrightarrow> ((\<lambda>x. f (x, t)) has_field_derivative (fx (x, t))) (at x within U)"
+  assumes integrable_f2: "\<And>x. x \<in> U \<Longrightarrow> (\<lambda>t. f (x, t)) integrable_on cbox a b"
+  assumes cont_fx: "continuous_on (U \<times> (cbox a b)) fx"
+  assumes U: "x0 \<in> U" "convex U"
+  notes [continuous_intros] = continuous_on_compose2[OF cont_fx]
+  shows "((\<lambda>x. integral (cbox a b) (\<lambda>t. f (x, t))) has_field_derivative integral (cbox a b) (\<lambda>t. fx (x0, t))) (at x0 within U)"
+proof -
+  have *: "blinfun_mult_right (integral (cbox a b) (\<lambda>t. fx (x0, t))) =
+    integral (cbox a b) (\<lambda>t. blinfun_mult_right (fx (x0, t)))"
+    by (subst integral_linear[symmetric])
+      (auto simp: has_vector_derivative_def o_def
+        intro!: integrable_continuous U continuous_intros bounded_linear_intros)
+  show ?thesis
+    unfolding has_field_derivative_eq_has_derivative_blinfun
+    apply (rule has_derivative_eq_rhs)
+    apply (rule leibniz_rule[OF _ integrable_f2 _ U, where fx="\<lambda>x. blinfun_mult_right (fx x)"])
+    using assms(1)
+    apply (auto simp: has_field_derivative_def * intro!: continuous_intros)
+    done
+qed
+
+
 subsection \<open>Exchange uniform limit and integral\<close>
 
 lemma
diff -r 16bfe0a6702d -r e9812a95d108 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Dec 22 15:39:01 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Dec 22 21:58:27 2015 +0100
@@ -314,6 +314,18 @@
   shows "f (a *\<^sub>R x + b *\<^sub>R y) = a *\<^sub>R f x +  b *\<^sub>R f y"
   using linear_add[of f] linear_cmul[of f] assms by simp
 
+lemma linear_componentwise:
+  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
+  assumes lf: "linear f"
+  shows "(f x) \<bullet> j = (\<Sum>i\<in>Basis. (x\<bullet>i) * (f i\<bullet>j))" (is "?lhs = ?rhs")
+proof -
+  have "?rhs = (\<Sum>i\<in>Basis. (x\<bullet>i) *\<^sub>R (f i))\<bullet>j"
+    by (simp add: inner_setsum_left)
+  then show ?thesis
+    unfolding linear_setsum_mul[OF lf, symmetric]
+    unfolding euclidean_representation ..
+qed
+
 
 subsection \<open>Bilinear functions.\<close>
 
diff -r 16bfe0a6702d -r e9812a95d108 src/HOL/Multivariate_Analysis/Operator_Norm.thy
--- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Tue Dec 22 15:39:01 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Tue Dec 22 21:58:27 2015 +0100
@@ -96,6 +96,20 @@
   shows "0 < onorm f \<longleftrightarrow> \<not> (\<forall>x. f x = 0)"
   by (simp add: less_le onorm_pos_le [OF f] onorm_eq_0 [OF f])
 
+lemma onorm_id_le: "onorm (\<lambda>x. x) \<le> 1"
+  by (rule onorm_bound) simp_all
+
+lemma onorm_id: "onorm (\<lambda>x. x::'a::{real_normed_vector, perfect_space}) = 1"
+proof (rule antisym[OF onorm_id_le])
+  have "{0::'a} \<noteq> UNIV" by (metis not_open_singleton open_UNIV)
+  then obtain x :: 'a where "x \<noteq> 0" by fast
+  hence "1 \<le> norm x / norm x"
+    by simp
+  also have "\<dots> \<le> onorm (\<lambda>x::'a. x)"
+    by (rule le_onorm) (rule bounded_linear_ident)
+  finally show "1 \<le> onorm (\<lambda>x::'a. x)" .
+qed
+
 lemma onorm_compose:
   assumes f: "bounded_linear f"
   assumes g: "bounded_linear g"
@@ -146,6 +160,46 @@
   qed
 qed (simp add: onorm_zero)
 
+lemma onorm_scaleR_left_lemma:
+  assumes r: "bounded_linear r"
+  shows "onorm (\<lambda>x. r x *\<^sub>R f) \<le> onorm r * norm f"
+proof (rule onorm_bound)
+  fix x
+  have "norm (r x *\<^sub>R f) = norm (r x) * norm f"
+    by simp
+  also have "\<dots> \<le> onorm r * norm x * norm f"
+    by (intro mult_right_mono onorm r norm_ge_zero)
+  finally show "norm (r x *\<^sub>R f) \<le> onorm r * norm f * norm x"
+    by (simp add: ac_simps)
+qed (intro mult_nonneg_nonneg norm_ge_zero onorm_pos_le r)
+
+lemma onorm_scaleR_left:
+  assumes f: "bounded_linear r"
+  shows "onorm (\<lambda>x. r x *\<^sub>R f) = onorm r * norm f"
+proof (cases "f = 0")
+  assume "f \<noteq> 0"
+  show ?thesis
+  proof (rule order_antisym)
+    show "onorm (\<lambda>x. r x *\<^sub>R f) \<le> onorm r * norm f"
+      using f by (rule onorm_scaleR_left_lemma)
+  next
+    have bl1: "bounded_linear (\<lambda>x. r x *\<^sub>R f)"
+      by (metis bounded_linear_scaleR_const f)
+    have "bounded_linear (\<lambda>x. r x * norm f)"
+      by (metis bounded_linear_mult_const f)
+    from onorm_scaleR_left_lemma[OF this, of "inverse (norm f)"]
+    have "onorm r \<le> onorm (\<lambda>x. r x * norm f) * inverse (norm f)"
+      using `f \<noteq> 0`
+      by (simp add: inverse_eq_divide)
+    also have "onorm (\<lambda>x. r x * norm f) \<le> onorm (\<lambda>x. r x *\<^sub>R f)"
+      by (rule onorm_bound)
+        (auto simp: abs_mult bl1 onorm_pos_le intro!: order_trans[OF _ onorm])
+    finally show "onorm r * norm f \<le> onorm (\<lambda>x. r x *\<^sub>R f)"
+      using `f \<noteq> 0`
+      by (simp add: inverse_eq_divide pos_le_divide_eq mult.commute)
+  qed
+qed (simp add: onorm_zero)
+
 lemma onorm_neg:
   shows "onorm (\<lambda>x. - f x) = onorm f"
   unfolding onorm_def by simp
diff -r 16bfe0a6702d -r e9812a95d108 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Dec 22 15:39:01 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Dec 22 21:58:27 2015 +0100
@@ -5388,6 +5388,24 @@
     unfolding uniformly_continuous_on_def by blast
 qed
 
+lemma continuous_on_tendsto_compose:
+  assumes f_cont: "continuous_on s f"
+  assumes g: "(g ---> l) F"
+  assumes l: "l \<in> s"
+  assumes ev: "\<forall>\<^sub>F x in F. g x \<in> s"
+  shows "((\<lambda>x. f (g x)) ---> f l) F"
+proof -
+  from f_cont have f: "(f ---> f l) (at l within s)"
+    by (auto simp: l continuous_on)
+  have i: "((\<lambda>x. if g x = l then f l else f (g x)) ---> f l) F"
+    by (rule filterlim_If)
+      (auto intro!: filterlim_compose[OF f] eventually_conj tendsto_mono[OF _ g]
+        simp: filterlim_at eventually_inf_principal eventually_mono[OF ev])
+  show ?thesis
+    by (rule filterlim_cong[THEN iffD1[OF _ i]]) auto
+qed
+
+
 text\<open>The usual transformation theorems.\<close>
 
 lemma continuous_transform_within:
@@ -8451,18 +8469,8 @@
 
 lemma cball_eq_ball_iff:
   fixes x :: "'a :: euclidean_space"
-  shows "cball x d = ball y e \<longleftrightarrow> d < 0 \<and> e \<le> 0" (is "?lhs = ?rhs")
-proof
-  assume ?lhs
-  then show ?rhs
-    apply (auto simp add: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff algebra_simps)
-    apply (metis add_increasing2 add_le_cancel_right add_less_same_cancel1 dist_not_less_zero less_le_trans zero_le_dist)
-    apply (metis add_less_same_cancel1 dist_not_less_zero less_le_trans not_le)
-    using \<open>?lhs\<close> ball_eq_empty cball_eq_empty apply blast+
-    done
-next
-  assume ?rhs then show ?lhs  using ball_eq_cball_iff by blast
-qed
+  shows "cball x d = ball y e \<longleftrightarrow> d < 0 \<and> e \<le> 0"
+  using ball_eq_cball_iff by blast
 
 no_notation
   eucl_less (infix "<e" 50)
diff -r 16bfe0a6702d -r e9812a95d108 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Tue Dec 22 15:39:01 2015 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Tue Dec 22 21:58:27 2015 +0100
@@ -1404,6 +1404,15 @@
   "prod a (b - b') = prod a b - prod a b'"
 by (rule additive.diff [OF additive_right])
 
+lemma setsum_left:
+  "prod (setsum g S) x = setsum ((\<lambda>i. prod (g i) x)) S"
+by (rule additive.setsum [OF additive_left])
+
+lemma setsum_right:
+  "prod x (setsum g S) = setsum ((\<lambda>i. (prod x (g i)))) S"
+by (rule additive.setsum [OF additive_right])
+
+
 lemma bounded_linear_left:
   "bounded_linear (\<lambda>a. a ** b)"
 apply (cut_tac bounded, safe)
@@ -1463,6 +1472,21 @@
     done
 qed
 
+lemma bounded_linear_sub: "bounded_linear f \<Longrightarrow> bounded_linear g \<Longrightarrow> bounded_linear (\<lambda>x. f x - g x)"
+  using bounded_linear_add[of f "\<lambda>x. - g x"] bounded_linear_minus[of g]
+  by (auto simp add: algebra_simps)
+
+lemma bounded_linear_setsum:
+  fixes f :: "'i \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+  assumes "\<And>i. i \<in> I \<Longrightarrow> bounded_linear (f i)"
+  shows "bounded_linear (\<lambda>x. \<Sum>i\<in>I. f i x)"
+proof cases
+  assume "finite I"
+  from this show ?thesis
+    using assms
+    by (induct I) (auto intro!: bounded_linear_add)
+qed simp
+
 lemma bounded_linear_compose:
   assumes "bounded_linear f"
   assumes "bounded_linear g"
@@ -1543,6 +1567,12 @@
   using bounded_bilinear_scaleR
   by (rule bounded_bilinear.bounded_linear_right)
 
+lemmas bounded_linear_scaleR_const =
+  bounded_linear_scaleR_left[THEN bounded_linear_compose]
+
+lemmas bounded_linear_const_scaleR =
+  bounded_linear_scaleR_right[THEN bounded_linear_compose]
+
 lemma bounded_linear_of_real: "bounded_linear (\<lambda>r. of_real r)"
   unfolding of_real_def by (rule bounded_linear_scaleR_left)