theory for type of bounded linear functions; differentiation under the integral sign
--- 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]
--- 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"
--- /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
--- 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"
--- 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
--- 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>
--- 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
--- 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)
--- 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)