--- a/src/HOL/Analysis/Inner_Product.thy Fri Apr 11 22:17:06 2025 +0100
+++ b/src/HOL/Analysis/Inner_Product.thy Sat Apr 12 22:42:32 2025 +0100
@@ -87,6 +87,9 @@
lemma power2_norm_eq_inner: "(norm x)\<^sup>2 = inner x x"
by (simp add: norm_eq_sqrt_inner)
+lemma dot_square_norm: "inner x x = (norm x)\<^sup>2"
+ by (metis power2_norm_eq_inner)
+
text \<open>Identities involving real multiplication and division.\<close>
lemma inner_mult_left: "inner (of_real m * a) b = m * (inner a b)"
@@ -143,15 +146,15 @@
show "norm x = 0 \<longleftrightarrow> x = 0"
unfolding norm_eq_sqrt_inner by simp
show "norm (x + y) \<le> norm x + norm y"
- proof (rule power2_le_imp_le)
- have "inner x y \<le> norm x * norm y"
- by (rule norm_cauchy_schwarz)
- thus "(norm (x + y))\<^sup>2 \<le> (norm x + norm y)\<^sup>2"
- unfolding power2_sum power2_norm_eq_inner
- by (simp add: inner_add inner_commute)
- show "0 \<le> norm x + norm y"
- unfolding norm_eq_sqrt_inner by simp
- qed
+ proof (rule power2_le_imp_le)
+ have "inner x y \<le> norm x * norm y"
+ by (rule norm_cauchy_schwarz)
+ thus "(norm (x + y))\<^sup>2 \<le> (norm x + norm y)\<^sup>2"
+ unfolding power2_sum power2_norm_eq_inner
+ by (simp add: inner_add inner_commute)
+ show "0 \<le> norm x + norm y"
+ unfolding norm_eq_sqrt_inner by simp
+ qed
have "sqrt (a\<^sup>2 * inner x x) = \<bar>a\<bar> * sqrt (inner x x)"
by (simp add: real_sqrt_mult)
then show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x"
@@ -184,9 +187,7 @@
by (simp add: norm_eq_sqrt_inner)
lemma norm_eq: "norm x = norm y \<longleftrightarrow> inner x x = inner y y"
- apply (subst order_eq_iff)
- apply (auto simp: norm_le)
- done
+ by (simp add: norm_eq_sqrt_inner)
lemma norm_eq_1: "norm x = 1 \<longleftrightarrow> inner x x = 1"
by (simp add: norm_eq_sqrt_inner)
@@ -231,10 +232,7 @@
show "inner x (scaleR r y) = scaleR r (inner x y)"
unfolding real_scaleR_def by (rule inner_scaleR_right)
show "\<exists>K. \<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * K"
- proof
- show "\<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * 1"
- by (simp add: Cauchy_Schwarz_ineq2)
- qed
+ by (metis Cauchy_Schwarz_ineq2 mult.commute mult_1 real_norm_def)
qed
lemmas tendsto_inner [tendsto_intros] =
@@ -337,7 +335,6 @@
lemma complex_inner_i_right [simp]: "inner x \<i> = Im x"
unfolding inner_complex_def by simp
-
lemma dot_square_norm: "inner x x = (norm x)\<^sup>2"
by (simp only: power2_norm_eq_inner) (* TODO: move? *)
@@ -345,16 +342,10 @@
by (auto simp add: norm_eq_sqrt_inner)
lemma norm_le_square: "norm x \<le> a \<longleftrightarrow> 0 \<le> a \<and> inner x x \<le> a\<^sup>2"
- apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
- using norm_ge_zero[of x]
- apply arith
- done
+ by (metis norm_eq_sqrt_inner norm_ge_zero order_trans real_le_lsqrt sqrt_le_D)
lemma norm_ge_square: "norm x \<ge> a \<longleftrightarrow> a \<le> 0 \<or> inner x x \<ge> a\<^sup>2"
- apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
- using norm_ge_zero[of x]
- apply arith
- done
+ by (metis nle_le norm_eq_square norm_le_square)
lemma norm_lt_square: "norm x < a \<longleftrightarrow> 0 < a \<and> inner x x < a\<^sup>2"
by (metis not_le norm_ge_square)
@@ -368,11 +359,10 @@
inner_scaleR_left inner_scaleR_right
lemma dot_norm: "inner x y = ((norm (x + y))\<^sup>2 - (norm x)\<^sup>2 - (norm y)\<^sup>2) / 2"
- by (simp only: power2_norm_eq_inner inner_simps inner_commute) auto
+ by (auto simp: power2_norm_eq_inner inner_simps inner_commute)
lemma dot_norm_neg: "inner x y = (((norm x)\<^sup>2 + (norm y)\<^sup>2) - (norm (x - y))\<^sup>2) / 2"
- by (simp only: power2_norm_eq_inner inner_simps inner_commute)
- (auto simp add: algebra_simps)
+ by (auto simp: power2_norm_eq_inner inner_simps inner_commute)
lemma of_real_inner_1 [simp]:
"inner (of_real x) (1 :: 'a :: {real_inner, real_normed_algebra_1}) = x"
@@ -403,9 +393,7 @@
"\<lbrakk>GDERIV f x :> df; DERIV g (f x) :> dg\<rbrakk>
\<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df"
unfolding gderiv_def has_field_derivative_def
- apply (drule (1) has_derivative_compose)
- apply (simp add: ac_simps)
- done
+ using has_derivative_compose by fastforce
lemma has_derivative_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"
by simp
@@ -434,11 +422,7 @@
"\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>
\<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x
:> (scaleR (f x) dg + scaleR df (g x))"
- unfolding gderiv_def has_field_derivative_def inner_add_right inner_scaleR_right
- apply (rule has_derivative_subst)
- apply (erule (1) has_derivative_scaleR)
- apply (simp add: ac_simps)
- done
+ by (simp add: DERIV_mult')
lemma GDERIV_mult:
"\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
--- a/src/HOL/Analysis/Product_Vector.thy Fri Apr 11 22:17:06 2025 +0100
+++ b/src/HOL/Analysis/Product_Vector.thy Sat Apr 12 22:42:32 2025 +0100
@@ -90,10 +90,7 @@
end
lemma module_prod_scale_eq_scaleR: "module_prod.scale (*\<^sub>R) (*\<^sub>R) = scaleR"
- apply (rule ext) apply (rule ext)
- apply (subst module_prod.scale_def)
- subgoal by unfold_locales
- by (simp add: scaleR_prod_def)
+ using module_pair_axioms module_prod.scale_def module_prod_def by fastforce
interpretation real_vector?: vector_space_prod "scaleR::_\<Rightarrow>_\<Rightarrow>'a::real_vector" "scaleR::_\<Rightarrow>_\<Rightarrow>'b::real_vector"
rewrites "scale = ((*\<^sub>R)::_\<Rightarrow>_\<Rightarrow>('a \<times> 'b))"
@@ -166,8 +163,8 @@
then have \<open>\<forall>\<^sub>F ((x'1, y1), (x'2, y2)) in uniformity \<times>\<^sub>F uniformity. (x'1,x'2) = x \<longrightarrow> (y1,y2) \<in> U\<close>
by (simp add: uniformity_prod_def eventually_filtermap case_prod_unfold)
then obtain UA UB where \<open>eventually UA uniformity\<close> and \<open>eventually UB uniformity\<close>
- and UA_UB_U: \<open>UA (a1, a2) \<Longrightarrow> UB (b1, b2) \<Longrightarrow> (a1, b1) = x \<Longrightarrow> (a2, b2) \<in> U\<close> for a1 a2 b1 b2
- apply atomize_elim by (simp add: case_prod_beta eventually_prod_filter)
+ and UA_UB_U: \<open>UA (a1, a2) \<Longrightarrow> UB (b1, b2) \<Longrightarrow> (a1, b1) = x \<Longrightarrow> (a2, b2) \<in> U\<close> for a1 a2 b1 b2
+ by (force simp: case_prod_beta eventually_prod_filter)
have \<open>eventually (\<lambda>a. UA (fst x, a)) (nhds (fst x))\<close>
using \<open>eventually UA uniformity\<close> eventually_mono eventually_nhds_uniformity by fastforce
then obtain A where \<open>open A\<close> and A_UA: \<open>A \<subseteq> {a. UA (fst x, a)}\<close> and \<open>fst x \<in> A\<close>
@@ -190,11 +187,13 @@
by (metis surj_pair uniformity_refl)
next
show \<open>eventually E uniformity \<Longrightarrow> \<forall>\<^sub>F (x::'a\<times>'b, y) in uniformity. E (y, x)\<close> for E
- apply (simp only: uniformity_prod_def eventually_filtermap case_prod_unfold eventually_prod_filter)
- apply (erule exE, erule exE, rename_tac Pf Pg)
- apply (rule_tac x=\<open>\<lambda>(x,y). Pf (y,x)\<close> in exI)
- apply (rule_tac x=\<open>\<lambda>(x,y). Pg (y,x)\<close> in exI)
- by (auto simp add: uniformity_sym)
+ unfolding uniformity_prod_def eventually_filtermap case_prod_unfold eventually_prod_filter
+ apply clarify
+ subgoal for Pf Pg
+ apply (rule_tac x=\<open>\<lambda>(x,y). Pf (y,x)\<close> in exI)
+ apply (rule_tac x=\<open>\<lambda>(x,y). Pg (y,x)\<close> in exI)
+ by (auto simp add: uniformity_sym)
+ done
next
show \<open>\<exists>D. eventually D uniformity \<and> (\<forall>x y z. D (x::'a\<times>'b, y) \<longrightarrow> D (y, z) \<longrightarrow> E (x, z))\<close>
if \<open>eventually E uniformity\<close> for E
@@ -224,11 +223,11 @@
proof -
have *: "eventually P (filtercomap (\<lambda>y. (x, y)) F) \<longleftrightarrow>
eventually (\<lambda>z. fst z = x \<longrightarrow> P (snd z)) F" for P :: "'a \<Rightarrow> bool" and F
- unfolding eventually_filtercomap
- by (smt (verit) eventually_elim2 fst_conv prod.collapse snd_conv)
+ unfolding eventually_filtercomap
+ by (smt (verit, best) eventually_mono split_pairs2)
thus ?thesis
- unfolding filter_eq_iff
- by (subst *) (auto simp: eventually_nhds_uniformity case_prod_unfold)
+ unfolding filter_eq_iff *
+ by (auto simp: eventually_nhds_uniformity case_prod_unfold)
qed
lemma uniformity_of_uniform_continuous_invariant:
@@ -356,8 +355,7 @@
have 1: \<open>\<exists>e\<in>{0<..}.
{(x,y). dist x y < e} \<subseteq> {(x,y). dist x y < a} \<and>
{(x,y). dist x y < e} \<subseteq> {(x,y). dist x y < b}\<close> if \<open>a>0\<close> \<open>b>0\<close> for a b
- apply (rule bexI[of _ \<open>min a b\<close>])
- using that by auto
+ using that by (auto intro: bexI[of _ \<open>min a b\<close>])
have 2: \<open>mono (\<lambda>P. eventually (\<lambda>x. P (Q x)) F)\<close> for F :: \<open>'z filter\<close> and Q :: \<open>'z \<Rightarrow> 'y\<close>
unfolding mono_def using eventually_mono le_funD by fastforce
have \<open>\<forall>\<^sub>F ((x1::'a,y1),(x2::'b,y2)) in uniformity \<times>\<^sub>F uniformity. dist x1 y1 < e/2 \<and> dist x2 y2 < e/2\<close> if \<open>e>0\<close> for e
@@ -383,17 +381,18 @@
have \<open>e > 0\<close>
using \<open>0 < e1\<close> \<open>0 < e2\<close> e_def by auto
have \<open>dist (x1,x2) (y1,y2) < e \<Longrightarrow> dist x1 y1 < e1\<close> for x1 y1 :: 'a and x2 y2 :: 'b
- unfolding dist_prod_def e_def apply auto
- by (smt (verit, best) real_sqrt_sum_squares_ge1)
+ unfolding dist_prod_def e_def
+ by (metis real_sqrt_sum_squares_ge1 fst_conv min_less_iff_conj order_le_less_trans snd_conv)
moreover have \<open>dist (x1,x2) (y1,y2) < e \<Longrightarrow> dist x2 y2 < e2\<close> for x1 y1 :: 'a and x2 y2 :: 'b
- unfolding dist_prod_def e_def apply auto
- by (smt (verit, best) real_sqrt_sum_squares_ge1)
+ unfolding dist_prod_def e_def
+ using real_sqrt_sum_squares_ge1 [of "dist x1 y1" "dist x2 y2"]
+ by (metis min_less_iff_conj order_le_less_trans real_sqrt_sum_squares_ge2 snd_conv)
ultimately have *: \<open>dist (x1,x2) (y1,y2) < e \<Longrightarrow> P ((x1, x2), (y1, y2))\<close> for x1 y1 x2 y2
using e1P1 e2P2 P1P2P by auto
show \<open>eventually P (INF e\<in>{0<..}. principal {(x, y). dist x y < e})\<close>
- apply (rule eventually_INF1[where i=e])
- using \<open>e > 0\<close> * by (auto simp: eventually_principal)
+ using \<open>e > 0\<close> *
+ by (auto simp: eventually_principal intro: eventually_INF1)
qed
qed
end
@@ -421,8 +420,8 @@
fix x y z :: "'a \<times> 'b"
show "dist x y \<le> dist x z + dist y z"
unfolding dist_prod_def
- by (intro order_trans [OF _ real_sqrt_sum_squares_triangle_ineq]
- real_sqrt_le_mono add_mono power_mono dist_triangle2 zero_le_dist)
+ by (meson add_mono dist_triangle2 order_trans power_mono real_sqrt_le_iff
+ real_sqrt_sum_squares_triangle_ineq zero_le_dist)
next
fix S :: "('a \<times> 'b) set"
have *: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
@@ -525,8 +524,8 @@
by auto
show \<open>\<exists>d>0. \<forall>x\<in>S\<times>T. \<forall>y\<in>S\<times>T. dist y x < d \<longrightarrow> dist (f y) (f x) < e\<close>
apply (rule exI[of _ d])
- using \<open>d>0\<close> d[rule_format] apply auto
- by (smt (verit, del_insts) dist_fst_le dist_snd_le fst_conv snd_conv)
+ by (metis SigmaE \<open>0 < d\<close> d dist_fst_le dist_snd_le fst_eqD order_le_less_trans
+ snd_conv)
next
fix e :: real
assume \<open>e > 0\<close> and \<open>\<forall>e>0. \<exists>d>0. \<forall>x\<in>S\<times>T. \<forall>x'\<in>S\<times>T. dist x' x < d \<longrightarrow> dist (f x') (f x) < e\<close>
@@ -559,8 +558,9 @@
fix e :: real assume \<open>0 < e\<close>
show \<open>\<exists>d>0. \<forall>x y :: 'a. dist x y < d \<longrightarrow> (\<forall>x' y'. dist x' y' < d \<longrightarrow> dist (x + x') (y + y') < e)\<close>
apply (rule exI[of _ \<open>e/2\<close>])
- using \<open>0 < e\<close> apply auto
- by (smt (verit, ccfv_SIG) dist_add_cancel dist_add_cancel2 dist_commute dist_triangle_lt)
+ using \<open>0 < e\<close>
+ by (smt (verit) dist_add_cancel dist_add_cancel2 dist_commute
+ dist_triangle_lt field_sum_of_halves)
qed
subsection \<open>Product is a Complete Metric Space\<close>
@@ -607,10 +607,7 @@
done
show "norm (scaleR r x) = \<bar>r\<bar> * norm x"
unfolding norm_prod_def
- apply (simp add: power_mult_distrib)
- apply (simp add: distrib_left [symmetric])
- apply (simp add: real_sqrt_mult)
- done
+ by (simp add: power_mult_distrib real_sqrt_mult flip: distrib_left)
show "sgn x = scaleR (inverse (norm x)) x"
by (rule sgn_prod_def)
show "dist x y = norm (x - y)"
@@ -654,13 +651,10 @@
using f.pos_bounded by fast
obtain Kg where "0 < Kg" and norm_g: "\<And>x. norm (g x) \<le> norm x * Kg"
using g.pos_bounded by fast
- have "\<forall>x. norm (f x, g x) \<le> norm x * (Kf + Kg)"
- apply (rule allI)
- apply (simp add: norm_Pair)
- apply (rule order_trans [OF sqrt_add_le_add_sqrt], simp, simp)
- apply (simp add: distrib_left)
- apply (rule add_mono [OF norm_f norm_g])
- done
+ have "\<And>x. sqrt ((norm (f x))\<^sup>2) + sqrt ((norm (g x))\<^sup>2) \<le> norm x * (Kf + Kg)"
+ by (simp add: add_mono distrib_left norm_f norm_g)
+ then have "\<forall>x. norm (f x, g x) \<le> norm x * (Kf + Kg)"
+ by (smt (verit) norm_ge_zero norm_prod_def prod.sel sqrt_add_le_add_sqrt zero_le_power)
then show "\<exists>K. \<forall>x. norm (f x, g x) \<le> norm x * K" ..
qed
@@ -730,44 +724,50 @@
by (metis norm_ge_zero sqrt_sum_squares_le_sum)
lemma (in vector_space_prod) span_Times_sing1: "p.span ({0} \<times> B) = {0} \<times> vs2.span B"
- apply (rule p.span_unique)
- subgoal by (auto intro!: vs1.span_base vs2.span_base)
- subgoal using vs1.subspace_single_0 vs2.subspace_span by (rule subspace_Times)
- subgoal for T
- proof safe
+proof (rule p.span_unique)
+ show "{0} \<times> B \<subseteq> {0} \<times> vs2.span B"
+ by (auto intro!: vs1.span_base vs2.span_base)
+ show "p.subspace ({0} \<times> vs2.span B)"
+ using vs1.subspace_single_0 vs2.subspace_span by (rule subspace_Times)
+ fix T :: "('b \<times> 'c) set"
+ assume subset_T: "{0} \<times> B \<subseteq> T" and subspace: "p.subspace T"
+ show "{0} \<times> vs2.span B \<subseteq> T"
+ proof clarify
fix b
- assume subset_T: "{0} \<times> B \<subseteq> T" and subspace: "p.subspace T" and b_span: "b \<in> vs2.span B"
+ assume b_span: "b \<in> vs2.span B"
then obtain t r where b: "b = (\<Sum>a\<in>t. r a *b a)" and t: "finite t" "t \<subseteq> B"
by (auto simp: vs2.span_explicit)
have "(0, b) = (\<Sum>b\<in>t. scale (r b) (0, b))"
- unfolding b scale_prod sum_prod
- by simp
+ unfolding b scale_prod sum_prod by simp
also have "\<dots> \<in> T"
using \<open>t \<subseteq> B\<close> subset_T
by (auto intro!: p.subspace_sum p.subspace_scale subspace)
finally show "(0, b) \<in> T" .
qed
- done
+qed
lemma (in vector_space_prod) span_Times_sing2: "p.span (A \<times> {0}) = vs1.span A \<times> {0}"
- apply (rule p.span_unique)
- subgoal by (auto intro!: vs1.span_base vs2.span_base)
- subgoal using vs1.subspace_span vs2.subspace_single_0 by (rule subspace_Times)
- subgoal for T
- proof safe
+proof (rule p.span_unique)
+ show "A \<times> {0} \<subseteq> vs1.span A \<times> {0}"
+ by (auto intro!: vs1.span_base vs2.span_base)
+ show "p.subspace (vs1.span A \<times> {0})"
+ using vs1.subspace_span vs2.subspace_single_0 by (rule subspace_Times)
+ fix T :: "('b \<times> 'c) set"
+ assume subset_T: "A \<times> {0} \<subseteq> T" and subspace: "p.subspace T"
+ show "vs1.span A \<times> {0} \<subseteq> T"
+ proof clarify
fix a
- assume subset_T: "A \<times> {0} \<subseteq> T" and subspace: "p.subspace T" and a_span: "a \<in> vs1.span A"
+ assume a_span: "a \<in> vs1.span A"
then obtain t r where a: "a = (\<Sum>a\<in>t. r a *a a)" and t: "finite t" "t \<subseteq> A"
by (auto simp: vs1.span_explicit)
have "(a, 0) = (\<Sum>a\<in>t. scale (r a) (a, 0))"
- unfolding a scale_prod sum_prod
- by simp
+ unfolding a scale_prod sum_prod by simp
also have "\<dots> \<in> T"
using \<open>t \<subseteq> A\<close> subset_T
by (auto intro!: p.subspace_sum p.subspace_scale subspace)
finally show "(a, 0) \<in> T" .
qed
- done
+qed
subsection \<open>Product is Finite Dimensional\<close>