--- a/src/HOL/Analysis/Complex_Transcendental.thy Thu Dec 29 16:44:45 2022 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Thu Dec 29 22:14:25 2022 +0000
@@ -660,15 +660,10 @@
lemma norm_sin_squared:
"norm(sin z) ^ 2 = (exp(2 * Im z) + inverse(exp(2 * Im z)) - 2 * cos(2 * Re z)) / 4"
-proof (cases z)
- case (Complex x1 x2)
- then show ?thesis
- apply (simp only: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double Complex_eq)
- apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide)
- apply (simp only: left_diff_distrib [symmetric] power_mult_distrib cos_squared_eq)
- apply (simp add: power2_eq_square field_split_simps)
- done
-qed
+ using cos_double_sin [of "Re z"]
+ apply (simp add: sin_cos_eq norm_cos_squared exp_minus mult.commute [of _ 2] exp_double)
+ apply (simp add: algebra_simps power2_eq_square)
+ done
lemma exp_uminus_Im: "exp (- Im z) \<le> exp (cmod z)"
using abs_Im_le_cmod linear order_trans by fastforce
@@ -1002,17 +997,14 @@
lemma Arg2pi_times_of_real [simp]:
assumes "0 < r" shows "Arg2pi (of_real r * z) = Arg2pi z"
-proof (cases "z=0")
- case False
- show ?thesis
- by (rule Arg2pi_unique [of "r * norm z"]) (use Arg2pi False assms is_Arg_def in auto)
-qed auto
+ by (metis (no_types, lifting) Arg2pi Arg2pi_eq Arg2pi_unique assms mult.assoc
+ mult_eq_0_iff mult_pos_pos of_real_mult zero_less_norm_iff)
lemma Arg2pi_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg2pi (z * of_real r) = Arg2pi z"
by (metis Arg2pi_times_of_real mult.commute)
lemma Arg2pi_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg2pi (z / of_real r) = Arg2pi z"
- by (metis Arg2pi_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)
+ by (metis Arg2pi_times_of_real2 less_irrefl nonzero_eq_divide_eq of_real_eq_0_iff)
lemma Arg2pi_le_pi: "Arg2pi z \<le> pi \<longleftrightarrow> 0 \<le> Im z"
proof (cases "z=0")
@@ -1095,12 +1087,14 @@
lemma Arg2pi_eq_iff:
assumes "w \<noteq> 0" "z \<noteq> 0"
- shows "Arg2pi w = Arg2pi z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)"
- using assms Arg2pi_eq [of z] Arg2pi_eq [of w]
- apply auto
- apply (rule_tac x="norm w / norm z" in exI)
- apply (simp add: field_split_simps)
- by (metis mult.commute mult.left_commute)
+ shows "Arg2pi w = Arg2pi z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)" (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then have "(cmod w) * (z / cmod z) = w"
+ by (metis Arg2pi_eq assms(2) mult_eq_0_iff nonzero_mult_div_cancel_left)
+ then show ?rhs
+ by (metis assms divide_pos_pos of_real_divide times_divide_eq_left times_divide_eq_right zero_less_norm_iff)
+qed auto
lemma Arg2pi_inverse_eq_0: "Arg2pi(inverse z) = 0 \<longleftrightarrow> Arg2pi z = 0"
by (metis Arg2pi_eq_0 Arg2pi_inverse inverse_inverse_eq)
@@ -1142,19 +1136,20 @@
using Arg2pi_add [OF assms]
by auto
-lemma Arg2pi_cnj_eq_inverse: "z\<noteq>0 \<Longrightarrow> Arg2pi (cnj z) = Arg2pi (inverse z)"
- apply (simp add: Arg2pi_eq_iff field_split_simps complex_norm_square [symmetric])
- by (metis of_real_power zero_less_norm_iff zero_less_power)
+lemma Arg2pi_cnj_eq_inverse:
+ assumes "z \<noteq> 0" shows "Arg2pi (cnj z) = Arg2pi (inverse z)"
+proof -
+ have "\<exists>r>0. of_real r / z = cnj z"
+ by (metis assms complex_norm_square nonzero_mult_div_cancel_left zero_less_norm_iff zero_less_power)
+ then show ?thesis
+ by (metis Arg2pi_times_of_real2 divide_inverse_commute)
+qed
lemma Arg2pi_cnj: "Arg2pi(cnj z) = (if z \<in> \<real> then Arg2pi z else 2*pi - Arg2pi z)"
-proof (cases "z=0")
- case False
- then show ?thesis
- by (simp add: Arg2pi_cnj_eq_inverse Arg2pi_inverse)
-qed auto
+ by (metis Arg2pi_cnj_eq_inverse Arg2pi_inverse Reals_cnj_iff complex_cnj_zero)
lemma Arg2pi_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg2pi(exp z) = Im z"
- by (rule Arg2pi_unique [of "exp(Re z)"]) (auto simp: exp_eq_polar)
+ by (simp add: Arg2pi_unique exp_eq_polar)
lemma complex_split_polar:
obtains r a::real where "z = complex_of_real r * (cos a + \<i> * sin a)" "0 \<le> r" "0 \<le> a" "a < 2*pi"
@@ -2215,21 +2210,13 @@
lemma Arg_times_of_real [simp]:
assumes "0 < r" shows "Arg (of_real r * z) = Arg z"
-proof (cases "z=0")
- case True
- then show ?thesis
- by (simp add: Arg_def)
-next
- case False
- with Arg_eq assms show ?thesis
- by (auto simp: mpi_less_Arg Arg_le_pi intro!: Arg_unique [of "r * norm z"])
-qed
+ using Arg_def Ln_times_of_real assms by auto
lemma Arg_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg (z * of_real r) = Arg z"
by (metis Arg_times_of_real mult.commute)
lemma Arg_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg (z / of_real r) = Arg z"
- by (metis Arg_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)
+ by (metis Arg_times_of_real2 less_irrefl nonzero_eq_divide_eq of_real_eq_0_iff)
lemma Arg_less_0: "0 \<le> Arg z \<longleftrightarrow> 0 \<le> Im z"
using Im_Ln_le_pi Im_Ln_pos_le
@@ -2243,18 +2230,13 @@
by (auto simp: order.order_iff_strict Arg_def)
lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re z"
- using complex_is_Real_iff
- by (simp add: Arg_def Im_Ln_eq_0) (metis less_eq_real_def of_real_Re of_real_def scale_zero_left)
+ using Arg_def Im_Ln_eq_0 complex_eq_iff complex_is_Real_iff by auto
corollary\<^marker>\<open>tag unimportant\<close> Arg_ne_0: assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0" shows "Arg z \<noteq> 0"
using assms by (auto simp: nonneg_Reals_def Arg_eq_0)
lemma Arg_eq_pi_iff: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
-proof (cases "z=0")
- case False
- then show ?thesis
- using Arg_eq_0 [of "-z"] Arg_eq_pi complex_is_Real_iff by blast
-qed (simp add: Arg_def)
+ using Arg_eq_pi complex_is_Real_iff by blast
lemma Arg_eq_0_pi: "Arg z = 0 \<or> Arg z = pi \<longleftrightarrow> z \<in> \<real>"
using Arg_eq_pi_iff Arg_eq_0 by force
@@ -2266,15 +2248,11 @@
proof (cases "z \<in> \<real>")
case True
then show ?thesis
- by simp (metis Arg2pi_inverse Arg2pi_real Arg_real Reals_inverse)
+ by (metis Arg2pi_inverse Arg2pi_real Arg_real Reals_inverse)
next
case False
- then have z: "Arg z < pi" "z \<noteq> 0"
- using Arg_eq_0_pi Arg_le_pi by (auto simp: less_eq_real_def)
- show ?thesis
- apply (rule Arg_unique [of "inverse (norm z)"])
- using False z mpi_less_Arg [of z] Arg_eq [of z]
- by (auto simp: exp_minus field_simps)
+ then show ?thesis
+ by (simp add: Arg_def Ln_inverse complex_is_Real_iff complex_nonpos_Reals_iff)
qed
lemma Arg_eq_iff:
@@ -2282,7 +2260,7 @@
shows "Arg w = Arg z \<longleftrightarrow> (\<exists>x. 0 < x \<and> w = of_real x * z)" (is "?lhs = ?rhs")
proof
assume ?lhs
- then have "w = complex_of_real (cmod w / cmod z) * z"
+ then have "w = (cmod w / cmod z) * z"
by (metis Arg_eq assms divide_divide_eq_right eq_divide_eq exp_not_eq_zero of_real_divide)
then show ?rhs
using assms divide_pos_pos zero_less_norm_iff by blast
@@ -2307,14 +2285,11 @@
assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
shows "continuous (at z) Arg"
proof -
- have [simp]: "(\<lambda>z. Im (Ln z)) \<midarrow>z\<rightarrow> Arg z"
+ have "(\<lambda>z. Im (Ln z)) \<midarrow>z\<rightarrow> Arg z"
using Arg_def assms continuous_at by fastforce
- show ?thesis
+ then show ?thesis
unfolding continuous_at
- proof (rule Lim_transform_within_open)
- show "\<And>w. \<lbrakk>w \<in> - \<real>\<^sub>\<le>\<^sub>0; w \<noteq> z\<rbrakk> \<Longrightarrow> Im (Ln w) = Arg w"
- by (metis Arg_def Compl_iff nonpos_Reals_zero_I)
- qed (use assms in auto)
+ by (smt (verit, del_insts) Arg_eq_Im_Ln Lim_transform_away_at assms nonpos_Reals_zero_I)
qed
lemma continuous_within_Arg: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z within S) Arg"
@@ -2388,44 +2363,17 @@
qed
next
show "arctan (Im z / Re z) > -pi"
- by (rule le_less_trans[OF _ arctan_lbound]) auto
+ by (smt (verit, ccfv_SIG) arctan field_sum_of_halves)
next
- have "arctan (Im z / Re z) < pi / 2"
- by (rule arctan_ubound)
- also have "\<dots> \<le> pi" by simp
- finally show "arctan (Im z / Re z) \<le> pi"
- by simp
+ show "arctan (Im z / Re z) \<le> pi"
+ by (smt (verit, best) arctan field_sum_of_halves)
qed
subsection\<^marker>\<open>tag unimportant\<close>\<open>Relation between Ln and Arg2pi, and hence continuity of Arg2pi\<close>
-lemma Arg2pi_Ln:
- assumes "0 < Arg2pi z" shows "Arg2pi z = Im(Ln(-z)) + pi"
-proof (cases "z = 0")
- case True
- with assms show ?thesis
- by simp
-next
- case False
- then have "z / of_real(norm z) = exp(\<i> * of_real(Arg2pi z))"
- using Arg2pi [of z]
- by (metis is_Arg_def abs_norm_cancel nonzero_mult_div_cancel_left norm_of_real zero_less_norm_iff)
- then have "- z / of_real(norm z) = exp (\<i> * (of_real (Arg2pi z) - pi))"
- using cis_conv_exp cis_pi
- by (auto simp: exp_diff algebra_simps)
- then have "ln (- z / of_real(norm z)) = ln (exp (\<i> * (of_real (Arg2pi z) - pi)))"
- by simp
- also have "\<dots> = \<i> * (of_real(Arg2pi z) - pi)"
- using Arg2pi [of z] assms pi_not_less_zero
- by auto
- finally have "Arg2pi z = Im (Ln (- z / of_real (cmod z))) + pi"
- by simp
- also have "\<dots> = Im (Ln (-z) - ln (cmod z)) + pi"
- by (metis diff_0_right minus_diff_eq zero_less_norm_iff Ln_divide_of_real False)
- also have "\<dots> = Im (Ln (-z)) + pi"
- by simp
- finally show ?thesis .
-qed
+lemma Arg2pi_Ln: "0 < Arg2pi z \<Longrightarrow> Arg2pi z = Im(Ln(-z)) + pi"
+ by (smt (verit, best) Arg2pi_0 Arg2pi_exp Arg2pi_minus Arg_exp Arg_minus Im_Ln_le_pi
+ exp_Ln mpi_less_Im_Ln neg_equal_0_iff_equal)
lemma continuous_at_Arg2pi:
assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0"
@@ -2433,18 +2381,14 @@
proof -
have *: "isCont (\<lambda>z. Im (Ln (- z)) + pi) z"
by (rule Complex.isCont_Im isCont_Ln' continuous_intros | simp add: assms complex_is_Real_iff)+
- have [simp]: "Im x \<noteq> 0 \<Longrightarrow> Im (Ln (- x)) + pi = Arg2pi x" for x
- using Arg2pi_Ln by (simp add: Arg2pi_gt_0 complex_nonneg_Reals_iff)
consider "Re z < 0" | "Im z \<noteq> 0" using assms
using complex_nonneg_Reals_iff not_le by blast
- then have [simp]: "(\<lambda>z. Im (Ln (- z)) + pi) \<midarrow>z\<rightarrow> Arg2pi z"
+ then have "(\<lambda>z. Im (Ln (- z)) + pi) \<midarrow>z\<rightarrow> Arg2pi z"
using "*" by (simp add: Arg2pi_Ln Arg2pi_gt_0 assms continuous_within)
- show ?thesis
+ then show ?thesis
unfolding continuous_at
- proof (rule Lim_transform_within_open)
- show "\<And>x. \<lbrakk>x \<in> - \<real>\<^sub>\<ge>\<^sub>0; x \<noteq> z\<rbrakk> \<Longrightarrow> Im (Ln (- x)) + pi = Arg2pi x"
- by (auto simp add: Arg2pi_Ln [OF Arg2pi_gt_0] complex_nonneg_Reals_iff)
- qed (use assms in auto)
+ by (metis (mono_tags, lifting) Arg2pi_Ln Arg2pi_gt_0 Compl_iff Lim_transform_within_open assms
+ closed_nonneg_Reals_complex open_Compl)
qed
@@ -2467,18 +2411,7 @@
lemma Arg2pi_eq_Im_Ln:
assumes "0 \<le> Im z" "0 < Re z"
shows "Arg2pi z = Im (Ln z)"
-proof (cases "Im z = 0")
- case True then show ?thesis
- using Arg2pi_eq_0 Ln_in_Reals assms(2) complex_is_Real_iff by auto
-next
- case False
- then have *: "Arg2pi z > 0"
- using Arg2pi_gt_0 complex_is_Real_iff by blast
- then have "z \<noteq> 0"
- by auto
- with * assms False show ?thesis
- by (subst Arg2pi_Ln) (auto simp: Ln_minus)
-qed
+ by (smt (verit, ccfv_SIG) Arg2pi_exp Im_Ln_pos_le assms exp_Ln pi_neq_zero zero_complex.simps(1))
lemma continuous_within_upperhalf_Arg2pi:
assumes "z \<noteq> 0"
@@ -2681,9 +2614,7 @@
also have "\<dots> \<longleftrightarrow> ((\<lambda>z. g z ^ nat n) has_field_derivative dd') (at z within S)"
proof (rule has_field_derivative_cong_eventually)
show "\<forall>\<^sub>F x in at z within S. g x powr of_int n = g x ^ nat n"
- unfolding eventually_at
- apply (rule exI[where x=e])
- using powr_of_int that \<open>e>0\<close> e_dist by (simp add: dist_commute)
+ unfolding eventually_at by (metis e_dist \<open>e>0\<close> dist_commute powr_of_int that)
qed (use powr_of_int \<open>g z\<noteq>0\<close> that in simp)
also have "\<dots>" unfolding dd'_def using gderiv that
by (auto intro!: derivative_eq_intros)
@@ -2707,8 +2638,7 @@
proof (rule has_field_derivative_cong_eventually)
show "\<forall>\<^sub>F x in at z within S. g x powr of_int n = inverse (g x ^ nat (- n))"
unfolding eventually_at
- apply (rule exI[where x=e])
- using powr_of_int that \<open>e>0\<close> e_dist by (simp add: dist_commute)
+ by (metis \<open>e>0\<close> e_dist dist_commute linorder_not_le powr_of_int that)
qed (use powr_of_int \<open>g z\<noteq>0\<close> that in simp)
also have "\<dots>"
proof -
@@ -2759,8 +2689,8 @@
using field_differentiable_def has_field_derivative_powr_right by blast
lemma holomorphic_on_powr_right [holomorphic_intros]:
- assumes "f holomorphic_on s"
- shows "(\<lambda>z. w powr (f z)) holomorphic_on s"
+ assumes "f holomorphic_on S"
+ shows "(\<lambda>z. w powr (f z)) holomorphic_on S"
proof (cases "w = 0")
case False
with assms show ?thesis
@@ -2769,21 +2699,9 @@
qed simp
lemma holomorphic_on_divide_gen [holomorphic_intros]:
- assumes f: "f holomorphic_on s" and g: "g holomorphic_on s" and 0: "\<And>z z'. \<lbrakk>z \<in> s; z' \<in> s\<rbrakk> \<Longrightarrow> g z = 0 \<longleftrightarrow> g z' = 0"
-shows "(\<lambda>z. f z / g z) holomorphic_on s"
-proof (cases "\<exists>z\<in>s. g z = 0")
- case True
- with 0 have "g z = 0" if "z \<in> s" for z
- using that by blast
- then show ?thesis
- using g holomorphic_transform by auto
-next
- case False
- with 0 have "g z \<noteq> 0" if "z \<in> s" for z
- using that by blast
- with holomorphic_on_divide show ?thesis
- using f g by blast
-qed
+ assumes "f holomorphic_on S" "g holomorphic_on S" and "\<And>z z'. \<lbrakk>z \<in> S; z' \<in> S\<rbrakk> \<Longrightarrow> g z = 0 \<longleftrightarrow> g z' = 0"
+ shows "(\<lambda>z. f z / g z) holomorphic_on S"
+ by (metis (no_types, lifting) assms division_ring_divide_zero holomorphic_on_divide holomorphic_transform)
lemma norm_powr_real_powr:
"w \<in> \<real> \<Longrightarrow> 0 \<le> Re w \<Longrightarrow> cmod (w powr z) = Re w powr Re z"
@@ -2879,6 +2797,7 @@
lemma tendsto_neg_powr_complex_of_nat:
assumes "filterlim f at_top F" and "Re s < 0"
shows "((\<lambda>x. of_nat (f x) powr s) \<longlongrightarrow> 0) F"
+ using tendsto_neg_powr_complex_of_real [of "real o f" F s]
proof -
have "((\<lambda>x. of_real (real (f x)) powr s) \<longlongrightarrow> 0) F" using assms(2)
by (intro filterlim_compose[OF _ tendsto_neg_powr_complex_of_real]
@@ -3093,29 +3012,18 @@
also have "\<dots> = exp (Ln z / 2)"
apply (rule csqrt_square)
using cos_gt_zero_pi [of "(Im (Ln z) / 2)"] Im_Ln_le_pi mpi_less_Im_Ln assms
- by (fastforce simp: Re_exp Im_exp )
+ by (fastforce simp: Re_exp Im_exp)
finally show ?thesis using assms csqrt_square
by simp
qed
lemma csqrt_inverse:
- assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
- shows "csqrt (inverse z) = inverse (csqrt z)"
-proof (cases "z=0")
- case False
- then show ?thesis
- using assms csqrt_exp_Ln Ln_inverse exp_minus
- by (simp add: csqrt_exp_Ln Ln_inverse exp_minus)
-qed auto
-
-lemma cnj_csqrt:
- assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
- shows "cnj(csqrt z) = csqrt(cnj z)"
-proof (cases "z=0")
- case False
- then show ?thesis
- by (simp add: assms cnj_Ln csqrt_exp_Ln exp_cnj)
-qed auto
+ "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> csqrt (inverse z) = inverse (csqrt z)"
+ by (metis Ln_inverse csqrt_eq_0 csqrt_exp_Ln divide_minus_left exp_minus
+ inverse_nonzero_iff_nonzero)
+
+lemma cnj_csqrt: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> cnj(csqrt z) = csqrt(cnj z)"
+ by (metis cnj_Ln complex_cnj_divide complex_cnj_numeral complex_cnj_zero_iff csqrt_eq_0 csqrt_exp_Ln exp_cnj)
lemma has_field_derivative_csqrt:
assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
@@ -3175,8 +3083,8 @@
"continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt"
proof (cases "z \<in> \<real>\<^sub>\<le>\<^sub>0")
case True
- have [simp]: "Im z = 0" and 0: "Re z < 0 \<or> z = 0"
- using True cnj.code complex_cnj_zero_iff by (auto simp: Complex_eq complex_nonpos_Reals_iff) fastforce
+ then have [simp]: "Im z = 0" and 0: "Re z < 0 \<or> z = 0"
+ using complex_nonpos_Reals_iff complex_eq_iff by force+
show ?thesis
using 0
proof
@@ -3296,11 +3204,7 @@
have nzi: "((1 - \<i>*z) * inverse (1 + \<i>*z)) \<noteq> 0"
using nz1 nz2 by auto
have "Im ((1 - \<i>*z) / (1 + \<i>*z)) = 0 \<Longrightarrow> 0 < Re ((1 - \<i>*z) / (1 + \<i>*z))"
- apply (simp add: divide_complex_def)
- apply (simp add: divide_simps split: if_split_asm)
- using assms
- apply (auto simp: algebra_simps abs_square_less_1 [unfolded power2_eq_square])
- done
+ by (simp add: Im_complex_div_lemma Re_complex_div_lemma assms cmod_eq_Im)
then have *: "((1 - \<i>*z) / (1 + \<i>*z)) \<notin> \<real>\<^sub>\<le>\<^sub>0"
by (auto simp add: complex_nonpos_Reals_iff)
show "\<bar>Re(Arctan z)\<bar> < pi/2"
@@ -3483,7 +3387,7 @@
also have "\<dots> = x"
proof -
have "(complex_of_real x)\<^sup>2 \<noteq> - 1"
- by (metis diff_0_right minus_diff_eq mult_zero_left not_le of_real_1 of_real_eq_iff of_real_minus of_real_power power2_eq_square real_minus_mult_self_le zero_less_one)
+ by (smt (verit, best) Im_complex_of_real imaginary_unit.sel(2) of_real_minus power2_eq_iff power2_i)
then show ?thesis
by simp
qed
@@ -3526,22 +3430,8 @@
qed
lemma arctan_inverse:
- assumes "0 < x"
- shows "arctan(inverse x) = pi/2 - arctan x"
-proof -
- have "arctan(inverse x) = arctan(inverse(tan(arctan x)))"
- by (simp add: arctan)
- also have "\<dots> = arctan (tan (pi / 2 - arctan x))"
- by (simp add: tan_cot)
- also have "\<dots> = pi/2 - arctan x"
- proof -
- have "0 < pi - arctan x"
- using arctan_ubound [of x] pi_gt_zero by linarith
- with assms show ?thesis
- by (simp add: Transcendental.arctan_tan)
- qed
- finally show ?thesis .
-qed
+ "0 < x \<Longrightarrow>arctan(inverse x) = pi/2 - arctan x"
+ by (smt (verit, del_insts) arctan arctan_unique tan_cot zero_less_arctan_iff)
lemma arctan_add_small:
assumes "\<bar>x * y\<bar> < 1"
@@ -3590,7 +3480,7 @@
show "(\<lambda>k. 1 / real (k * 2 + 1) * x ^ (k * 2 + 1)) \<longlonglongrightarrow> 0 * 0"
using assms
by (intro tendsto_mult real_tendsto_divide_at_top)
- (auto simp: filterlim_real_sequentially filterlim_sequentially_iff_filterlim_real
+ (auto simp: filterlim_sequentially_iff_filterlim_real
intro!: real_tendsto_divide_at_top tendsto_power_zero filterlim_real_sequentially
tendsto_eq_intros filterlim_at_top_mult_tendsto_pos filterlim_tendsto_add_at_top)
qed simp
@@ -3705,7 +3595,7 @@
ultimately show ?thesis
apply (simp add: sin_exp_eq Arcsin_def Arcsin_body_lemma exp_minus divide_simps)
apply (simp add: algebra_simps)
- apply (simp add: power2_eq_square [symmetric] algebra_simps)
+ apply (simp add: right_diff_distrib flip: power2_eq_square)
done
qed
@@ -3748,13 +3638,13 @@
by (metis Arcsin_sin)
lemma Arcsin_0 [simp]: "Arcsin 0 = 0"
- by (metis Arcsin_sin norm_zero pi_half_gt_zero real_norm_def sin_zero zero_complex.simps(1))
+ by (simp add: Arcsin_unique)
lemma Arcsin_1 [simp]: "Arcsin 1 = pi/2"
- by (metis Arcsin_sin Im_complex_of_real Re_complex_of_real numeral_One of_real_numeral pi_half_ge_zero real_sqrt_abs real_sqrt_pow2 real_sqrt_power sin_of_real sin_pi_half)
+ using Arcsin_unique sin_of_real_pi_half by fastforce
lemma Arcsin_minus_1 [simp]: "Arcsin(-1) = - (pi/2)"
- by (metis Arcsin_1 Arcsin_sin Im_complex_of_real Re_complex_of_real abs_of_nonneg of_real_minus pi_half_ge_zero power2_minus real_sqrt_abs sin_Arcsin sin_minus)
+ by (simp add: Arcsin_unique)
lemma has_field_derivative_Arcsin:
assumes "Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1"
@@ -3800,8 +3690,7 @@
using Arcsin_range_lemma [of "-z"] by simp
lemma Arccos_body_lemma: "z + \<i> * csqrt(1 - z\<^sup>2) \<noteq> 0"
- using Arcsin_body_lemma [of z]
- by (metis Arcsin_body_lemma complex_i_mult_minus diff_minus_eq_add power2_minus right_minus_eq)
+ by (metis Arcsin_body_lemma complex_i_mult_minus diff_0 diff_eq_eq power2_minus)
lemma Re_Arccos: "Re(Arccos z) = Im (Ln (z + \<i> * csqrt(1 - z\<^sup>2)))"
by (simp add: Arccos_def)
@@ -3811,7 +3700,7 @@
text\<open>A very tricky argument to find!\<close>
lemma isCont_Arccos_lemma:
- assumes eq0: "Im (z + \<i> * csqrt (1 - z\<^sup>2)) = 0" and "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
+ assumes eq0: "Im (z + \<i> * csqrt (1 - z\<^sup>2)) = 0" and "Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1"
shows False
proof (cases "Im z = 0")
case True
@@ -3987,8 +3876,7 @@
have "Arccos w \<bullet> Arccos w \<le> pi\<^sup>2 + (cmod w)\<^sup>2"
using Re by (simp add: dot_square_norm cmod_power2 [of "Arccos w"])
then have "cmod (Arccos w) \<le> pi + cmod (cos (Arccos w))"
- apply (simp add: norm_le_square)
- by (metis dot_square_norm norm_ge_zero norm_le_square pi_ge_zero triangle_lemma)
+ by (smt (verit) Im_Arccos_bound Re_Arccos_bound cmod_le cos_Arccos)
then show "cmod (Arccos w) \<le> pi + cmod w"
by auto
qed
@@ -3996,68 +3884,11 @@
subsection\<^marker>\<open>tag unimportant\<close>\<open>Interrelations between Arcsin and Arccos\<close>
-lemma cos_Arcsin_nonzero:
- assumes "z\<^sup>2 \<noteq> 1" shows "cos(Arcsin z) \<noteq> 0"
-proof -
- have eq: "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = z\<^sup>2 * (z\<^sup>2 - 1)"
- by (simp add: algebra_simps)
- have "\<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> z\<^sup>2 - 1"
- proof
- assume "\<i> * z * (csqrt (1 - z\<^sup>2)) = z\<^sup>2 - 1"
- then have "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = (z\<^sup>2 - 1)\<^sup>2"
- by simp
- then have "z\<^sup>2 * (z\<^sup>2 - 1) = (z\<^sup>2 - 1)*(z\<^sup>2 - 1)"
- using eq power2_eq_square by auto
- then show False
- using assms by simp
- qed
- then have "1 + \<i> * z * (csqrt (1 - z * z)) \<noteq> z\<^sup>2"
- by (metis add_minus_cancel power2_eq_square uminus_add_conv_diff)
- then have "2*(1 + \<i> * z * (csqrt (1 - z * z))) \<noteq> 2*z\<^sup>2" (*FIXME cancel_numeral_factor*)
- by (metis mult_cancel_left zero_neq_numeral)
- then have "(\<i> * z + csqrt (1 - z\<^sup>2))\<^sup>2 \<noteq> -1"
- using assms
- apply (simp add: power2_sum)
- apply (simp add: power2_eq_square algebra_simps)
- done
- then show ?thesis
- apply (simp add: cos_exp_eq Arcsin_def exp_minus)
- apply (simp add: divide_simps Arcsin_body_lemma)
- apply (metis add.commute minus_unique power2_eq_square)
- done
-qed
-
-lemma sin_Arccos_nonzero:
- assumes "z\<^sup>2 \<noteq> 1" shows "sin(Arccos z) \<noteq> 0"
-proof -
- have eq: "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = -(z\<^sup>2) * (1 - z\<^sup>2)"
- by (simp add: algebra_simps)
- have "\<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> 1 - z\<^sup>2"
- proof
- assume "\<i> * z * (csqrt (1 - z\<^sup>2)) = 1 - z\<^sup>2"
- then have "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = (1 - z\<^sup>2)\<^sup>2"
- by simp
- then have "-(z\<^sup>2) * (1 - z\<^sup>2) = (1 - z\<^sup>2)*(1 - z\<^sup>2)"
- using eq power2_eq_square by auto
- then have "-(z\<^sup>2) = (1 - z\<^sup>2)"
- using assms
- by (metis add.commute add.right_neutral diff_add_cancel mult_right_cancel)
- then show False
- using assms by simp
- qed
- then have "z\<^sup>2 + \<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> 1"
- by (simp add: algebra_simps)
- then have "2*(z\<^sup>2 + \<i> * z * (csqrt (1 - z\<^sup>2))) \<noteq> 2*1"
- by (metis mult_cancel_left2 zero_neq_numeral) (*FIXME cancel_numeral_factor*)
- then have "(z + \<i> * csqrt (1 - z\<^sup>2))\<^sup>2 \<noteq> 1"
- using assms
- by (metis Arccos_def add.commute add.left_neutral cancel_comm_monoid_add_class.diff_cancel cos_Arccos csqrt_0 mult_zero_right)
- then show ?thesis
- apply (simp add: sin_exp_eq Arccos_def exp_minus)
- apply (simp add: divide_simps Arccos_body_lemma)
- apply (simp add: power2_eq_square)
- done
-qed
+lemma cos_Arcsin_nonzero: "z\<^sup>2 \<noteq> 1 \<Longrightarrow>cos(Arcsin z) \<noteq> 0"
+ by (metis diff_0_right power_zero_numeral sin_Arcsin sin_squared_eq)
+
+lemma sin_Arccos_nonzero: "z\<^sup>2 \<noteq> 1 \<Longrightarrow>sin(Arccos z) \<noteq> 0"
+ by (metis add.right_neutral cos_Arccos power2_eq_square power_zero_numeral sin_cos_squared_add3)
lemma cos_sin_csqrt:
assumes "0 < cos(Re z) \<or> cos(Re z) = 0 \<and> Im z * sin(Re z) \<le> 0"
@@ -4076,185 +3907,51 @@
qed (use assms in \<open>auto simp: Re_sin Im_sin add_pos_pos mult_le_0_iff zero_le_mult_iff\<close>)
lemma Arcsin_Arccos_csqrt_pos:
- "(0 < Re z | Re z = 0 & 0 \<le> Im z) \<Longrightarrow> Arcsin z = Arccos(csqrt(1 - z\<^sup>2))"
+ "(0 < Re z \<or> Re z = 0 \<and> 0 \<le> Im z) \<Longrightarrow> Arcsin z = Arccos(csqrt(1 - z\<^sup>2))"
by (simp add: Arcsin_def Arccos_def Complex.csqrt_square add.commute)
lemma Arccos_Arcsin_csqrt_pos:
- "(0 < Re z | Re z = 0 & 0 \<le> Im z) \<Longrightarrow> Arccos z = Arcsin(csqrt(1 - z\<^sup>2))"
+ "(0 < Re z \<or> Re z = 0 \<and> 0 \<le> Im z) \<Longrightarrow> Arccos z = Arcsin(csqrt(1 - z\<^sup>2))"
by (simp add: Arcsin_def Arccos_def Complex.csqrt_square add.commute)
lemma sin_Arccos:
- "0 < Re z | Re z = 0 & 0 \<le> Im z \<Longrightarrow> sin(Arccos z) = csqrt(1 - z\<^sup>2)"
+ "0 < Re z \<or> Re z = 0 \<and> 0 \<le> Im z \<Longrightarrow> sin(Arccos z) = csqrt(1 - z\<^sup>2)"
by (simp add: Arccos_Arcsin_csqrt_pos)
lemma cos_Arcsin:
- "0 < Re z | Re z = 0 & 0 \<le> Im z \<Longrightarrow> cos(Arcsin z) = csqrt(1 - z\<^sup>2)"
+ "0 < Re z \<or> Re z = 0 \<and> 0 \<le> Im z \<Longrightarrow> cos(Arcsin z) = csqrt(1 - z\<^sup>2)"
by (simp add: Arcsin_Arccos_csqrt_pos)
subsection\<^marker>\<open>tag unimportant\<close>\<open>Relationship with Arcsin on the Real Numbers\<close>
-lemma Im_Arcsin_of_real:
- assumes "\<bar>x\<bar> \<le> 1"
- shows "Im (Arcsin (of_real x)) = 0"
-proof -
- have "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
- by (simp add: of_real_sqrt del: csqrt_of_real_nonneg)
- then have "cmod (\<i> * of_real x + csqrt (1 - (of_real x)\<^sup>2))^2 = 1"
- using assms abs_square_le_1
- by (force simp add: Complex.cmod_power2)
- then have "cmod (\<i> * of_real x + csqrt (1 - (of_real x)\<^sup>2)) = 1"
- by (simp add: norm_complex_def)
- then show ?thesis
- by (simp add: Im_Arcsin exp_minus)
-qed
+lemma of_real_arcsin: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arcsin x) = Arcsin(of_real x)"
+ by (smt (verit, best) Arcsin_sin Im_complex_of_real Re_complex_of_real arcsin sin_of_real)
+
+lemma Im_Arcsin_of_real: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> Im (Arcsin (of_real x)) = 0"
+ by (metis Im_complex_of_real of_real_arcsin)
corollary\<^marker>\<open>tag unimportant\<close> Arcsin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arcsin z \<in> \<real>"
by (metis Im_Arcsin_of_real Re_complex_of_real Reals_cases complex_is_Real_iff)
-lemma arcsin_eq_Re_Arcsin:
- assumes "\<bar>x\<bar> \<le> 1"
- shows "arcsin x = Re (Arcsin (of_real x))"
-unfolding arcsin_def
-proof (rule the_equality, safe)
- show "- (pi / 2) \<le> Re (Arcsin (complex_of_real x))"
- using Re_Ln_pos_le [OF Arcsin_body_lemma, of "of_real x"]
- by (auto simp: Complex.in_Reals_norm Re_Arcsin)
-next
- show "Re (Arcsin (complex_of_real x)) \<le> pi / 2"
- using Re_Ln_pos_le [OF Arcsin_body_lemma, of "of_real x"]
- by (auto simp: Complex.in_Reals_norm Re_Arcsin)
-next
- show "sin (Re (Arcsin (complex_of_real x))) = x"
- using Re_sin [of "Arcsin (of_real x)"] Arcsin_body_lemma [of "of_real x"]
- by (simp add: Im_Arcsin_of_real assms)
-next
- fix x'
- assume "- (pi / 2) \<le> x'" "x' \<le> pi / 2" "x = sin x'"
- then show "x' = Re (Arcsin (complex_of_real (sin x')))"
- unfolding sin_of_real [symmetric]
- by (subst Arcsin_sin) auto
-qed
-
-lemma of_real_arcsin: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arcsin x) = Arcsin(of_real x)"
- by (metis Im_Arcsin_of_real add.right_neutral arcsin_eq_Re_Arcsin complex_eq mult_zero_right of_real_0)
+lemma arcsin_eq_Re_Arcsin: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> arcsin x = Re (Arcsin (of_real x))"
+ by (metis Re_complex_of_real of_real_arcsin)
subsection\<^marker>\<open>tag unimportant\<close>\<open>Relationship with Arccos on the Real Numbers\<close>
-lemma Im_Arccos_of_real:
- assumes "\<bar>x\<bar> \<le> 1"
- shows "Im (Arccos (of_real x)) = 0"
-proof -
- have "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
- by (simp add: of_real_sqrt del: csqrt_of_real_nonneg)
- then have "cmod (of_real x + \<i> * csqrt (1 - (of_real x)\<^sup>2))^2 = 1"
- using assms abs_square_le_1
- by (force simp add: Complex.cmod_power2)
- then have "cmod (of_real x + \<i> * csqrt (1 - (of_real x)\<^sup>2)) = 1"
- by (simp add: norm_complex_def)
- then show ?thesis
- by (simp add: Im_Arccos exp_minus)
-qed
+lemma of_real_arccos: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)"
+ by (smt (verit, del_insts) Arccos_unique Im_complex_of_real Re_complex_of_real arccos_lbound
+ arccos_ubound cos_arccos_abs cos_of_real)
+
+lemma Im_Arccos_of_real: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> Im (Arccos (of_real x)) = 0"
+ by (metis Im_complex_of_real of_real_arccos)
corollary\<^marker>\<open>tag unimportant\<close> Arccos_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arccos z \<in> \<real>"
- by (metis Im_Arccos_of_real Re_complex_of_real Reals_cases complex_is_Real_iff)
-
-lemma arccos_eq_Re_Arccos:
- assumes "\<bar>x\<bar> \<le> 1"
- shows "arccos x = Re (Arccos (of_real x))"
-unfolding arccos_def
-proof (rule the_equality, safe)
- show "0 \<le> Re (Arccos (complex_of_real x))"
- using Im_Ln_pos_le [OF Arccos_body_lemma, of "of_real x"]
- by (auto simp: Complex.in_Reals_norm Re_Arccos)
-next
- show "Re (Arccos (complex_of_real x)) \<le> pi"
- using Im_Ln_pos_le [OF Arccos_body_lemma, of "of_real x"]
- by (auto simp: Complex.in_Reals_norm Re_Arccos)
-next
- show "cos (Re (Arccos (complex_of_real x))) = x"
- using Re_cos [of "Arccos (of_real x)"] Arccos_body_lemma [of "of_real x"]
- by (simp add: Im_Arccos_of_real assms)
-next
- fix x'
- assume "0 \<le> x'" "x' \<le> pi" "x = cos x'"
- then show "x' = Re (Arccos (complex_of_real (cos x')))"
- unfolding cos_of_real [symmetric]
- by (subst Arccos_cos) auto
-qed
-
-lemma of_real_arccos: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)"
- by (metis Im_Arccos_of_real add.right_neutral arccos_eq_Re_Arccos complex_eq mult_zero_right of_real_0)
-
-subsection\<^marker>\<open>tag unimportant\<close>\<open>Some interrelationships among the real inverse trig functions\<close>
-
-lemma arccos_arctan:
- assumes "-1 < x" "x < 1"
- shows "arccos x = pi/2 - arctan(x / sqrt(1 - x\<^sup>2))"
-proof -
- have "arctan(x / sqrt(1 - x\<^sup>2)) - (pi/2 - arccos x) = 0"
- proof (rule sin_eq_0_pi)
- show "- pi < arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)"
- using arctan_lbound [of "x / sqrt(1 - x\<^sup>2)"] arccos_bounded [of x] assms
- by (simp add: algebra_simps)
- next
- show "arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x) < pi"
- using arctan_ubound [of "x / sqrt(1 - x\<^sup>2)"] arccos_bounded [of x] assms
- by (simp add: algebra_simps)
- next
- show "sin (arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)) = 0"
- using assms
- by (simp add: algebra_simps sin_diff cos_add sin_arccos sin_arctan cos_arctan
- power2_eq_square square_eq_1_iff)
- qed
- then show ?thesis
- by simp
-qed
-
-lemma arcsin_plus_arccos:
- assumes "-1 \<le> x" "x \<le> 1"
- shows "arcsin x + arccos x = pi/2"
-proof -
- have "arcsin x = pi/2 - arccos x"
- apply (rule sin_inj_pi)
- using assms arcsin [OF assms] arccos [OF assms]
- by (auto simp: algebra_simps sin_diff)
- then show ?thesis
- by (simp add: algebra_simps)
-qed
-
-lemma arcsin_arccos_eq: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = pi/2 - arccos x"
- using arcsin_plus_arccos by force
-
-lemma arccos_arcsin_eq: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = pi/2 - arcsin x"
- using arcsin_plus_arccos by force
-
-lemma arcsin_arctan: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> arcsin x = arctan(x / sqrt(1 - x\<^sup>2))"
- by (simp add: arccos_arctan arcsin_arccos_eq)
-
-lemma csqrt_1_diff_eq: "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
- by ( simp add: of_real_sqrt del: csqrt_of_real_nonneg)
-
-lemma arcsin_arccos_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = arccos(sqrt(1 - x\<^sup>2))"
- apply (simp add: abs_square_le_1 arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
- apply (subst Arcsin_Arccos_csqrt_pos)
- apply (auto simp: power_le_one csqrt_1_diff_eq)
- done
-
-lemma arcsin_arccos_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arcsin x = -arccos(sqrt(1 - x\<^sup>2))"
- using arcsin_arccos_sqrt_pos [of "-x"]
- by (simp add: arcsin_minus)
-
-lemma arccos_arcsin_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = arcsin(sqrt(1 - x\<^sup>2))"
- apply (simp add: abs_square_le_1 arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
- apply (subst Arccos_Arcsin_csqrt_pos)
- apply (auto simp: power_le_one csqrt_1_diff_eq)
- done
-
-lemma arccos_arcsin_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arccos x = pi - arcsin(sqrt(1 - x\<^sup>2))"
- using arccos_arcsin_sqrt_pos [of "-x"]
- by (simp add: arccos_minus)
+ by (metis Im_Arccos_of_real complex_is_Real_iff of_real_Re)
+
+lemma arccos_eq_Re_Arccos: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> arccos x = Re (Arccos (of_real x))"
+ by (metis Re_complex_of_real of_real_arccos)
subsection\<^marker>\<open>tag unimportant\<close>\<open>Continuity results for arcsin and arccos\<close>
--- a/src/HOL/Analysis/Function_Topology.thy Thu Dec 29 16:44:45 2022 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy Thu Dec 29 22:14:25 2022 +0000
@@ -118,12 +118,7 @@
have *: "f \<in> U"
if "U \<in> \<U>" and "\<forall>V\<in>\<U>. \<forall>i. i \<in> I \<and> Y V i \<noteq> topspace (X i) \<longrightarrow> f i \<in> Y V i"
and "\<forall>i\<in>I. f i \<in> topspace (X i)" and "f \<in> extensional I" for f U
- proof -
- have "Pi\<^sub>E I (Y U) = U"
- using Y \<open>U \<in> \<U>\<close> by blast
- then show "f \<in> U"
- using that unfolding PiE_def Pi_def by blast
- qed
+ by (smt (verit) PiE_iff Y that)
show "?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U) \<subseteq> \<Inter>\<U>"
by (auto simp: PiE_iff *)
show "\<Inter>\<U> \<subseteq> ?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U)"
@@ -158,18 +153,16 @@
using Y by force
show "?G ` \<U> \<subseteq> {Pi\<^sub>E I Y |Y. (\<forall>i. openin (X i) (Y i)) \<and> finite {i. Y i \<noteq> topspace (X i)}}"
apply clarsimp
- apply (rule_tac x=" (\<lambda>i. if i = J U then Y U else topspace (X i))" in exI)
+ apply (rule_tac x= "(\<lambda>i. if i = J U then Y U else topspace (X i))" in exI)
apply (auto simp: *)
done
next
show "(\<Inter>U\<in>\<U>. ?G U) = ?TOP \<inter> \<Inter>\<U>"
proof
have "(\<Pi>\<^sub>E i\<in>I. if i = J U then Y U else topspace (X i)) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
- apply (clarsimp simp: PiE_iff Ball_def all_conj_distrib split: if_split_asm)
- using Y \<open>U \<in> \<U>\<close> openin_subset by blast+
+ by (simp add: PiE_mono Y \<open>U \<in> \<U>\<close> openin_subset)
then have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP"
- using \<open>U \<in> \<U>\<close>
- by fastforce
+ using \<open>U \<in> \<U>\<close> by fastforce
moreover have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> \<Inter>\<U>"
using PiE_mem Y by fastforce
ultimately show "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP \<inter> \<Inter>\<U>"
@@ -211,24 +204,25 @@
assumes "openin (product_topology T I) U" "x \<in> U"
shows "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
proof -
- have "generate_topology_on {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}} U"
- using assms unfolding product_topology_def by (intro openin_topology_generated_by) auto
- then have "\<And>x. x\<in>U \<Longrightarrow> \<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
+ define IT where "IT \<equiv> \<lambda>X. {i. X i \<noteq> topspace (T i)}"
+ have "generate_topology_on {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite (IT X)} U"
+ using assms unfolding product_topology_def IT_def by (intro openin_topology_generated_by) auto
+ then have "\<And>x. x\<in>U \<Longrightarrow> \<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite (IT X) \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
proof induction
case (Int U V x)
then obtain XU XV where H:
- "x \<in> Pi\<^sub>E I XU" "(\<forall>i. openin (T i) (XU i))" "finite {i. XU i \<noteq> topspace (T i)}" "Pi\<^sub>E I XU \<subseteq> U"
- "x \<in> Pi\<^sub>E I XV" "(\<forall>i. openin (T i) (XV i))" "finite {i. XV i \<noteq> topspace (T i)}" "Pi\<^sub>E I XV \<subseteq> V"
- by auto meson
+ "x \<in> Pi\<^sub>E I XU" "\<And>i. openin (T i) (XU i)" "finite (IT XU)" "Pi\<^sub>E I XU \<subseteq> U"
+ "x \<in> Pi\<^sub>E I XV" "\<And>i. openin (T i) (XV i)" "finite (IT XV)" "Pi\<^sub>E I XV \<subseteq> V"
+ by (meson Int_iff)
define X where "X = (\<lambda>i. XU i \<inter> XV i)"
have "Pi\<^sub>E I X \<subseteq> Pi\<^sub>E I XU \<inter> Pi\<^sub>E I XV"
- unfolding X_def by (auto simp add: PiE_iff)
+ by (auto simp add: PiE_iff X_def)
then have "Pi\<^sub>E I X \<subseteq> U \<inter> V" using H by auto
moreover have "\<forall>i. openin (T i) (X i)"
unfolding X_def using H by auto
- moreover have "finite {i. X i \<noteq> topspace (T i)}"
- apply (rule rev_finite_subset[of "{i. XU i \<noteq> topspace (T i)} \<union> {i. XV i \<noteq> topspace (T i)}"])
- unfolding X_def using H by auto
+ moreover have "finite (IT X)"
+ apply (rule rev_finite_subset[of "IT XU \<union> IT XV"])
+ using H by (auto simp: X_def IT_def)
moreover have "x \<in> Pi\<^sub>E I X"
unfolding X_def using H by auto
ultimately show ?case
@@ -236,16 +230,10 @@
next
case (UN K x)
then obtain k where "k \<in> K" "x \<in> k" by auto
- with UN have "\<exists>X. x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> k"
- by simp
- then obtain X where "x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> k"
- by blast
- then have "x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> (\<Union>K)"
- using \<open>k \<in> K\<close> by auto
- then show ?case
- by auto
+ with \<open>k \<in> K\<close> UN show ?case
+ by (meson Sup_upper2)
qed auto
- then show ?thesis using \<open>x \<in> U\<close> by auto
+ then show ?thesis using \<open>x \<in> U\<close> IT_def by blast
qed
lemma product_topology_empty_discrete:
@@ -257,9 +245,7 @@
arbitrary union_of
((finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U)))
relative_to topspace (product_topology X I))"
- apply (subst product_topology)
- apply (simp add: topology_inverse' [OF istopology_subbase])
- done
+ by (simp add: istopology_subbase product_topology)
lemma subtopology_PiE:
"subtopology (product_topology X I) (\<Pi>\<^sub>E i\<in>I. (S i)) = product_topology (\<lambda>i. subtopology (X i) (S i)) I"
@@ -349,6 +335,7 @@
"openin (product_topology X I) S \<longleftrightarrow>
(\<forall>x \<in> S. \<exists>U. finite {i \<in> I. U i \<noteq> topspace(X i)} \<and>
(\<forall>i \<in> I. openin (X i) (U i)) \<and> x \<in> Pi\<^sub>E I U \<and> Pi\<^sub>E I U \<subseteq> S)"
+sledgehammer [isar_proofs, provers = "cvc4 z3 spass e vampire verit", timeout = 77]
unfolding openin_product_topology arbitrary_union_of_alt product_topology_base_alt topspace_product_topology
apply safe
apply (drule bspec; blast)+
@@ -438,9 +425,7 @@
corollary closedin_product_topology:
"closedin (product_topology X I) (PiE I S) \<longleftrightarrow> PiE I S = {} \<or> (\<forall>i \<in> I. closedin (X i) (S i))"
- apply (simp add: PiE_eq PiE_eq_empty_iff closure_of_product_topology flip: closure_of_eq)
- apply (metis closure_of_empty)
- done
+ by (smt (verit, best) PiE_eq closedin_empty closure_of_eq closure_of_product_topology)
corollary closedin_product_topology_singleton:
"f \<in> extensional I \<Longrightarrow> closedin (product_topology X I) {f} \<longleftrightarrow> (\<forall>i \<in> I. closedin (X i) {f i})"
@@ -501,17 +486,13 @@
also have "... = (\<Inter>i\<in>J. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
using * \<open>J \<subseteq> I\<close> by auto
also have "openin T1 (...)"
- apply (rule openin_INT)
- apply (simp add: \<open>finite J\<close>)
- using H(2) assms(1) \<open>J \<subseteq> I\<close> by auto
+ using H(2) \<open>J \<subseteq> I\<close> \<open>finite J\<close> assms(1) by blast
ultimately show "openin T1 (f-`U \<inter> topspace T1)" by simp
next
- show "f `topspace T1 \<subseteq> \<Union>{Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
- apply (subst topology_generated_by_topspace[symmetric])
- apply (subst product_topology_def[symmetric])
- apply (simp only: topspace_product_topology)
- apply (auto simp add: PiE_iff)
- using assms unfolding continuous_map_def by auto
+ have "f ` topspace T1 \<subseteq> topspace (product_topology T I)"
+ using assms continuous_map_def by fastforce
+ then show "f `topspace T1 \<subseteq> \<Union>{Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
+ by (simp add: product_topology_def)
qed
lemma continuous_map_product_then_coordinatewise [intro]:
@@ -522,8 +503,7 @@
fix i assume "i \<in> I"
have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f" by auto
also have "continuous_map T1 (T i) (...)"
- apply (rule continuous_map_compose[of _ "product_topology T I"])
- using assms \<open>i \<in> I\<close> by auto
+ by (metis \<open>i \<in> I\<close> assms continuous_map_compose continuous_map_product_coordinates)
ultimately show "continuous_map T1 (T i) (\<lambda>x. f x i)"
by simp
next
@@ -583,28 +563,14 @@
assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
shows "open {f. \<forall>i\<in>I. f (x i) \<in> U i}"
proof -
- define J where "J = x`I"
- define V where "V = (\<lambda>y. if y \<in> J then \<Inter>{U i|i. i\<in>I \<and> x i = y} else UNIV)"
- define X where "X = (\<lambda>y. if y \<in> J then V y else UNIV)"
+ define V where "V \<equiv> (\<lambda>y. if y \<in> x`I then \<Inter>{U i|i. i\<in>I \<and> x i = y} else UNIV)"
+ define X where "X \<equiv> (\<lambda>y. if y \<in> x`I then V y else UNIV)"
have *: "open (X i)" for i
unfolding X_def V_def using assms by auto
- have **: "finite {i. X i \<noteq> UNIV}"
- unfolding X_def V_def J_def using assms(1) by auto
- have "open (Pi\<^sub>E UNIV X)"
- by (simp add: "*" "**" open_PiE)
+ then have "open (Pi\<^sub>E UNIV X)"
+ by (simp add: X_def assms(1) open_PiE)
moreover have "Pi\<^sub>E UNIV X = {f. \<forall>i\<in>I. f (x i) \<in> U i}"
- apply (auto simp add: PiE_iff) unfolding X_def V_def J_def
- proof (auto)
- fix f :: "'a \<Rightarrow> 'b" and i :: 'i
- assume a1: "i \<in> I"
- assume a2: "\<forall>i. f i \<in> (if i \<in> x`I then if i \<in> x`I then \<Inter>{U ia |ia. ia \<in> I \<and> x ia = i} else UNIV else UNIV)"
- have f3: "x i \<in> x`I"
- using a1 by blast
- have "U i \<in> {U ia |ia. ia \<in> I \<and> x ia = x i}"
- using a1 by blast
- then show "f (x i) \<in> U i"
- using f3 a2 by (meson Inter_iff)
- qed
+ by (fastforce simp add: PiE_iff X_def V_def split: if_split_asm)
ultimately show ?thesis by simp
qed
@@ -620,25 +586,13 @@
fixes f :: "'a::topological_space \<Rightarrow> 'b \<Rightarrow> 'c::topological_space"
assumes "\<And>i. continuous_on S (\<lambda>x. f x i)"
shows "continuous_on S f"
- using continuous_map_coordinatewise_then_product [of UNIV, where T = "\<lambda>i. euclidean"]
- by (metis UNIV_I assms continuous_map_iff_continuous euclidean_product_topology)
-
-lemma continuous_on_product_then_coordinatewise_UNIV:
- assumes "continuous_on UNIV f"
- shows "continuous_on UNIV (\<lambda>x. f x i)"
- unfolding continuous_map_iff_continuous2 [symmetric]
- by (rule continuous_map_product_then_coordinatewise [where I=UNIV]) (use assms in \<open>auto simp: euclidean_product_topology\<close>)
+ by (metis UNIV_I assms continuous_map_iff_continuous euclidean_product_topology
+ continuous_map_coordinatewise_then_product)
lemma continuous_on_product_then_coordinatewise:
assumes "continuous_on S f"
shows "continuous_on S (\<lambda>x. f x i)"
-proof -
- have "continuous_on S ((\<lambda>q. q i) \<circ> f)"
- by (metis assms continuous_on_compose continuous_on_id
- continuous_on_product_then_coordinatewise_UNIV continuous_on_subset subset_UNIV)
- then show ?thesis
- by auto
-qed
+ by (metis UNIV_I assms continuous_map_iff_continuous continuous_map_product_then_coordinatewise(1) euclidean_product_topology)
lemma continuous_on_coordinatewise_iff:
fixes f :: "('a \<Rightarrow> real) \<Rightarrow> 'b \<Rightarrow> real"
@@ -679,16 +633,15 @@
next
case (Suc N)
define f::"((nat \<Rightarrow> 'a) \<times> 'a) \<Rightarrow> (nat \<Rightarrow> 'a)"
- where "f = (\<lambda>(x, b). (\<lambda>i. if i = N then b else x i))"
+ where "f = (\<lambda>(x, b). x(N:=b))"
have "{x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>Suc N. x i = a)} \<subseteq> f`({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
proof (auto)
fix x assume H: "\<forall>i::nat. x i \<in> F" "\<forall>i\<ge>Suc N. x i = a"
- define y where "y = (\<lambda>i. if i = N then a else x i)"
- have "f (y, x N) = x"
- unfolding f_def y_def by auto
- moreover have "(y, x N) \<in> {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F"
- unfolding y_def using H \<open>a \<in> F\<close> by auto
- ultimately show "x \<in> f`({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
+ have "f (x(N:=a), x N) = x"
+ unfolding f_def by auto
+ moreover have "(x(N:=a), x N) \<in> {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F"
+ using H \<open>a \<in> F\<close> by auto
+ ultimately show "x \<in> f ` ({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
by (metis (no_types, lifting) image_eqI)
qed
moreover have "countable ({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
@@ -742,7 +695,7 @@
by metis
text \<open>\<open>B i\<close> is a countable basis of neighborhoods of \<open>x\<^sub>i\<close>.\<close>
define B where "B = (\<lambda>i. (A (x i))`UNIV \<union> {UNIV})"
- have "countable (B i)" for i unfolding B_def by auto
+ have countB: "countable (B i)" for i unfolding B_def by auto
have open_B: "\<And>X i. X \<in> B i \<Longrightarrow> open X"
by (auto simp: B_def A)
define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
@@ -750,14 +703,14 @@
unfolding K_def B_def by auto
then have "K \<noteq> {}" by auto
have "countable {X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
- apply (rule countable_product_event_const) using \<open>\<And>i. countable (B i)\<close> by auto
+ by (simp add: countB countable_product_event_const)
moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X)`{X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
unfolding K_def by auto
ultimately have "countable K" by auto
- have "x \<in> k" if "k \<in> K" for k
+ have I: "x \<in> k" if "k \<in> K" for k
using that unfolding K_def B_def apply auto using A(1) by auto
- have "open k" if "k \<in> K" for k
- using that unfolding K_def by (blast intro: open_B open_PiE elim: )
+ have II: "open k" if "k \<in> K" for k
+ using that unfolding K_def by (blast intro: open_B open_PiE)
have Inc: "\<exists>k\<in>K. k \<subseteq> U" if "open U \<and> x \<in> U" for U
proof -
have "openin (product_topology (\<lambda>i. euclidean) UNIV) U" "x \<in> U"
@@ -775,31 +728,28 @@
have *: "\<exists>y. y \<in> B i \<and> y \<subseteq> X i" for i
unfolding B_def using A(3)[OF H(2)] H(1) by (metis PiE_E UNIV_I UnCI image_iff)
have **: "Y i \<in> B i \<and> Y i \<subseteq> X i" for i
- apply (cases "i \<in> I")
- unfolding Y_def using * that apply (auto)
- apply (metis (no_types, lifting) someI, metis (no_types, lifting) someI_ex subset_iff)
- unfolding B_def apply simp
- unfolding I_def apply auto
- done
+ proof (cases "i \<in> I")
+ case True
+ then show ?thesis
+ by (metis (mono_tags, lifting) "*" Nitpick.Eps_psimp Y_def)
+ next
+ case False
+ then show ?thesis by (simp add: B_def I_def Y_def)
+ qed
have "{i. Y i \<noteq> UNIV} \<subseteq> I"
unfolding Y_def by auto
- then have ***: "finite {i. Y i \<noteq> UNIV}"
- unfolding I_def using H(3) rev_finite_subset by blast
- have "(\<forall>i. Y i \<in> B i) \<and> finite {i. Y i \<noteq> UNIV}"
- using ** *** by auto
+ with ** have "(\<forall>i. Y i \<in> B i) \<and> finite {i. Y i \<noteq> UNIV}"
+ using H(3) I_def finite_subset by blast
then have "Pi\<^sub>E UNIV Y \<in> K"
unfolding K_def by auto
-
have "Y i \<subseteq> X i" for i
- apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto
- then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto
- then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto
+ using "**" by auto
+ then have "Pi\<^sub>E UNIV Y \<subseteq> U"
+ by (metis H(4) PiE_mono subset_trans)
then show ?thesis using \<open>Pi\<^sub>E UNIV Y \<in> K\<close> by auto
qed
-
show "\<exists>L. (\<forall>(i::nat). x \<in> L i \<and> open (L i)) \<and> (\<forall>U. open U \<and> x \<in> U \<longrightarrow> (\<exists>i. L i \<subseteq> U))"
- apply (rule first_countableI[of K])
- using \<open>countable K\<close> \<open>\<And>k. k \<in> K \<Longrightarrow> x \<in> k\<close> \<open>\<And>k. k \<in> K \<Longrightarrow> open k\<close> Inc by auto
+ using \<open>countable K\<close> I II Inc by (simp add: first_countableI)
qed
proposition product_topology_countable_basis:
@@ -821,7 +771,7 @@
unfolding K_def using \<open>\<And>U. U \<in> B2 \<Longrightarrow> open U\<close> by auto
have "countable {X. (\<forall>(i::'a). X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
- apply (rule countable_product_event_const) using \<open>countable B2\<close> by auto
+ using \<open>countable B2\<close> by (intro countable_product_event_const) auto
moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X)`{X. (\<forall>i. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
unfolding K_def by auto
ultimately have ii: "countable K" by auto
@@ -832,9 +782,7 @@
then have "openin (product_topology (\<lambda>i. euclidean) UNIV) U"
unfolding open_fun_def by auto
with product_topology_open_contains_basis[OF this \<open>x \<in> U\<close>]
- have "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV} \<and> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
- by simp
- then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
+ obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
"\<And>i. open (X i)"
"finite {i. X i \<noteq> UNIV}"
"(\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
@@ -845,29 +793,15 @@
have *: "\<exists>y. y \<in> B2 \<and> y \<subseteq> X i \<and> x i \<in> y" for i
unfolding B2_def using B \<open>open (X i)\<close> \<open>x i \<in> X i\<close> by (meson UnCI topological_basisE)
have **: "Y i \<in> B2 \<and> Y i \<subseteq> X i \<and> x i \<in> Y i" for i
- using someI_ex[OF *]
- apply (cases "i \<in> I")
- unfolding Y_def using * apply (auto)
- unfolding B2_def I_def by auto
+ using someI_ex[OF *] by (simp add: B2_def I_def Y_def)
have "{i. Y i \<noteq> UNIV} \<subseteq> I"
unfolding Y_def by auto
- then have ***: "finite {i. Y i \<noteq> UNIV}"
- unfolding I_def using H(3) rev_finite_subset by blast
- have "(\<forall>i. Y i \<in> B2) \<and> finite {i. Y i \<noteq> UNIV}"
- using ** *** by auto
+ then have "(\<forall>i. Y i \<in> B2) \<and> finite {i. Y i \<noteq> UNIV}"
+ using "**" H(3) I_def finite_subset by blast
then have "Pi\<^sub>E UNIV Y \<in> K"
unfolding K_def by auto
-
- have "Y i \<subseteq> X i" for i
- apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto
- then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto
- then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto
-
- have "x \<in> Pi\<^sub>E UNIV Y"
- using ** by auto
-
- show "\<exists>V\<in>K. x \<in> V \<and> V \<subseteq> U"
- using \<open>Pi\<^sub>E UNIV Y \<in> K\<close> \<open>Pi\<^sub>E UNIV Y \<subseteq> U\<close> \<open>x \<in> Pi\<^sub>E UNIV Y\<close> by auto
+ then show "\<exists>V\<in>K. x \<in> V \<and> V \<subseteq> U"
+ by (meson "**" H(4) PiE_I PiE_mono UNIV_I order.trans)
next
fix U assume "U \<in> K"
show "open U"
@@ -878,9 +812,11 @@
qed
instance "fun" :: (countable, second_countable_topology) second_countable_topology
- apply standard
- using product_topology_countable_basis topological_basis_imp_subbasis by auto
-
+proof
+ show "\<exists>B::('a \<Rightarrow> 'b) set set. countable B \<and> open = generate_topology B"
+ using product_topology_countable_basis topological_basis_imp_subbasis
+ by auto
+qed
subsection\<open>The Alexander subbase theorem\<close>
@@ -1106,11 +1042,7 @@
qed
ultimately show ?thesis
by metis
-next
- case False
- then show ?thesis
- by (auto simp: continuous_map_def PiE_def)
-qed
+qed (auto simp: continuous_map_def PiE_def)
lemma continuous_map_componentwise_UNIV:
@@ -1147,8 +1079,7 @@
fix x f
assume "f \<in> V"
let ?T = "{a \<in> topspace(Y i).
- (\<lambda>j. if j = i then a
- else if j \<in> I then f j else undefined) \<in> (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> \<Inter>\<F>}"
+ (\<lambda>j\<in>I. f j)(i:=a) \<in> (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> \<Inter>\<F>}"
show "\<exists>T. openin (Y i) T \<and> f i \<in> T \<and> T \<subseteq> (\<lambda>f. f i) ` V"
proof (intro exI conjI)
show "openin (Y i) ?T"
@@ -1164,8 +1095,8 @@
by simp (metis IntD1 PiE_iff V \<open>f \<in> V\<close> that)
qed
then show "continuous_map (Y i) (product_topology Y I)
- (\<lambda>x j. if j = i then x else if j \<in> I then f j else undefined)"
- by (auto simp: continuous_map_componentwise assms extensional_def)
+ (\<lambda>x. (\<lambda>j\<in>I. f j)(i:=x))"
+ by (auto simp: continuous_map_componentwise assms extensional_def restrict_def)
next
have "openin (product_topology Y I) (\<Pi>\<^sub>E i\<in>I. topspace (Y i))"
by (metis openin_topspace topspace_product_topology)
@@ -1177,18 +1108,15 @@
show "\<And>X. X \<in> (\<inter>) (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) ` \<F> \<Longrightarrow> openin (product_topology Y I) X"
unfolding openin_product_topology relative_to_def
apply (clarify intro!: arbitrary_union_of_inc)
- apply (rename_tac F)
- apply (rule_tac x=F in exI)
using subsetD [OF \<F>]
- apply (force intro: finite_intersection_of_inc)
- done
+ by (metis (mono_tags, lifting) finite_intersection_of_inc mem_Collect_eq topspace_product_topology)
qed (use \<open>finite \<F>\<close> \<open>\<F> \<noteq> {}\<close> in auto)
qed
ultimately show "openin (product_topology Y I) ((\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> \<Inter>\<F>)"
by (auto simp only: Int_Inter_eq split: if_split)
qed
next
- have eqf: "(\<lambda>j. if j = i then f i else if j \<in> I then f j else undefined) = f"
+ have eqf: "(\<lambda>j\<in>I. f j)(i:=f i) = f"
using PiE_arb V \<open>f \<in> V\<close> by force
show "f i \<in> ?T"
using V assms \<open>f \<in> V\<close> by (auto simp: PiE_iff eqf)
@@ -1273,10 +1201,8 @@
next
assume ?rhs
then show ?lhs
- apply (simp only: openin_product_topology)
- apply (rule arbitrary_union_of_inc)
- apply (auto simp: product_topology_base_alt)
- done
+ unfolding openin_product_topology
+ by (intro arbitrary_union_of_inc) (auto simp: product_topology_base_alt)
qed
ultimately show ?thesis
by simp
@@ -1306,9 +1232,7 @@
by (simp add: continuous_map_product_projection)
moreover
have "\<And>x. x \<in> topspace (X i) \<Longrightarrow> x \<in> (\<lambda>f. f i) ` (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
- using \<open>i \<in> I\<close> z
- apply (rule_tac x="\<lambda>j. if j = i then x else if j \<in> I then z j else undefined" in image_eqI, auto)
- done
+ using \<open>i \<in> I\<close> z by (rule_tac x="z(i:=x)" in image_eqI) auto
then have "(\<lambda>f. f i) ` (\<Pi>\<^sub>E i\<in>I. topspace (X i)) = topspace (X i)"
using \<open>i \<in> I\<close> z by auto
ultimately show "compactin (X i) (topspace (X i))"
@@ -1461,7 +1385,7 @@
then have "(\<lambda>x. x k) ` {x. x j \<in> V} = UNIV" if "k \<noteq> j" for k
using that
apply (clarsimp simp add: set_eq_iff)
- apply (rule_tac x="\<lambda>m. if m = k then x else f m" in image_eqI, auto)
+ apply (rule_tac x="f(k:=x)" in image_eqI, auto)
done
then have "{i. (\<lambda>x. x i) ` C \<subset> topspace (X i)} \<subseteq> {j}"
using Ceq by auto
@@ -1493,7 +1417,7 @@
using PiE_ext \<open>g \<in> U\<close> gin by force
next
case (insert i M)
- define f where "f \<equiv> \<lambda>j. if j = i then g i else h j"
+ define f where "f \<equiv> h(i:=g i)"
have fin: "f \<in> PiE I (topspace \<circ> X)"
unfolding f_def using gin insert.prems(1) by auto
have subM: "{j \<in> I. f j \<noteq> g j} \<subseteq> M"
@@ -1506,13 +1430,13 @@
show ?thesis
proof (cases "i \<in> I")
case True
- let ?U = "{x \<in> topspace(X i). (\<lambda>j. if j = i then x else h j) \<in> U}"
- let ?V = "{x \<in> topspace(X i). (\<lambda>j. if j = i then x else h j) \<in> V}"
+ let ?U = "{x \<in> topspace(X i). h(i:=x) \<in> U}"
+ let ?V = "{x \<in> topspace(X i). h(i:=x) \<in> V}"
have False
proof (rule connected_spaceD [OF cs [OF \<open>i \<in> I\<close>]])
have "\<And>k. k \<in> I \<Longrightarrow> continuous_map (X i) (X k) (\<lambda>x. if k = i then x else h k)"
using continuous_map_eq_topcontinuous_at insert.prems(1) topcontinuous_at_def by fastforce
- then have cm: "continuous_map (X i) (product_topology X I) (\<lambda>x j. if j = i then x else h j)"
+ then have cm: "continuous_map (X i) (product_topology X I) (\<lambda>x. h(i:=x))"
using \<open>i \<in> I\<close> insert.prems(1)
by (auto simp: continuous_map_componentwise extensional_def)
show "openin (X i) ?U"
@@ -1522,45 +1446,23 @@
show "topspace (X i) \<subseteq> ?U \<union> ?V"
proof clarsimp
fix x
- assume "x \<in> topspace (X i)" and "(\<lambda>j. if j = i then x else h j) \<notin> V"
+ assume "x \<in> topspace (X i)" and "h(i:=x) \<notin> V"
with True subUV \<open>h \<in> Pi\<^sub>E I (topspace \<circ> X)\<close>
- show "(\<lambda>j. if j = i then x else h j) \<in> U"
- by (drule_tac c="(\<lambda>j. if j = i then x else h j)" in subsetD) auto
+ show "h(i:=x) \<in> U"
+ by (force dest: subsetD [where c="h(i:=x)"])
qed
show "?U \<inter> ?V = {}"
using disj by blast
show "?U \<noteq> {}"
- using \<open>U \<noteq> {}\<close> f_def
- proof -
- have "(\<lambda>j. if j = i then g i else h j) \<in> U"
- using \<open>f \<in> U\<close> f_def by blast
- moreover have "f i \<in> topspace (X i)"
- by (metis PiE_iff True comp_apply fin)
- ultimately have "\<exists>b. b \<in> topspace (X i) \<and> (\<lambda>a. if a = i then b else h a) \<in> U"
- using f_def by auto
- then show ?thesis
- by blast
- qed
- have "(\<lambda>j. if j = i then h i else h j) = h"
- by force
- moreover have "h i \<in> topspace (X i)"
- using True insert.prems(1) by auto
- ultimately show "?V \<noteq> {}"
- using \<open>h \<in> V\<close> by force
+ using True \<open>f \<in> U\<close> f_def gin by auto
+ show "?V \<noteq> {}"
+ using True \<open>h \<in> V\<close> V openin_subset by fastforce
qed
then show ?thesis ..
next
case False
show ?thesis
- proof (cases "h = f")
- case True
- show ?thesis
- by (rule insert.IH [OF insert.prems(1)]) (simp add: True subM)
- next
- case False
- then show ?thesis
- using gin insert.prems(1) \<open>i \<notin> I\<close> unfolding f_def by fastforce
- qed
+ using insert.prems(1) by (metis False gin PiE_E \<open>f \<in> U\<close> f_def fun_upd_triv)
qed
next
case False
@@ -1640,14 +1542,8 @@
assumes "i \<in> I"
shows "quotient_map(product_topology X I) (X i) (\<lambda>x. x i) \<longleftrightarrow>
(topspace(product_topology X I) = {} \<longrightarrow> topspace(X i) = {})"
- (is "?lhs = ?rhs")
-proof
- assume ?lhs with assms show ?rhs
- by (auto simp: continuous_open_quotient_map open_map_product_projection)
-next
- assume ?rhs with assms show ?lhs
- by (auto simp: Abstract_Topology.retraction_imp_quotient_map retraction_map_product_projection)
-qed
+ by (metis assms image_empty quotient_imp_surjective_map retraction_imp_quotient_map
+ retraction_map_product_projection)
lemma product_topology_homeomorphic_component:
assumes "i \<in> I" "\<And>j. \<lbrakk>j \<in> I; j \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>a. topspace(X j) = {a}"
@@ -1676,9 +1572,8 @@
from that obtain f where f: "f \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
by force
have "?SX f i homeomorphic_space X i"
- apply (simp add: subtopology_PiE )
- using product_topology_homeomorphic_component [OF \<open>i \<in> I\<close>, of "\<lambda>j. subtopology (X j) (if j = i then topspace (X i) else {f j})"]
- using f by fastforce
+ using f product_topology_homeomorphic_component [OF \<open>i \<in> I\<close>, of "\<lambda>j. subtopology (X j) (if j = i then topspace (X i) else {f j})"]
+ by (force simp add: subtopology_PiE)
then show ?thesis
using minor [OF f major \<open>i \<in> I\<close>] PQ by auto
qed
--- a/src/HOL/Analysis/Measure_Space.thy Thu Dec 29 16:44:45 2022 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy Thu Dec 29 22:14:25 2022 +0000
@@ -26,9 +26,9 @@
proof (rule SUP_eqI)
fix y :: ennreal assume "\<And>n. n \<in> UNIV \<Longrightarrow> (if i < n then f i else 0) \<le> y"
from this[of "Suc i"] show "f i \<le> y" by auto
- qed (insert assms, simp)
+ qed (use assms in simp)
ultimately show ?thesis using assms
- by (subst suminf_eq_SUP) (auto simp: indicator_def)
+ by (simp add: suminf_eq_SUP)
qed
lemma suminf_indicator:
@@ -71,11 +71,8 @@
by (induct n) (auto simp add: binaryset_def f)
qed
moreover
- have "... \<longlonglongrightarrow> f A + f B" by (rule tendsto_const)
- ultimately
- have "(\<lambda>n. \<Sum>i< Suc (Suc n). f (binaryset A B i)) \<longlonglongrightarrow> f A + f B"
- by metis
- hence "(\<lambda>n. \<Sum>i< n+2. f (binaryset A B i)) \<longlonglongrightarrow> f A + f B"
+ have "\<dots> \<longlonglongrightarrow> f A + f B" by (rule tendsto_const)
+ ultimately have "(\<lambda>n. \<Sum>i< n+2. f (binaryset A B i)) \<longlonglongrightarrow> f A + f B"
by simp
thus ?thesis by (rule LIMSEQ_offset [where k=2])
qed
@@ -83,7 +80,7 @@
lemma binaryset_sums:
assumes f: "f {} = 0"
shows "(\<lambda>n. f (binaryset A B n)) sums (f A + f B)"
- by (simp add: sums_def LIMSEQ_binaryset [where f=f, OF f] atLeast0LessThan)
+ using LIMSEQ_binaryset f sums_def by blast
lemma suminf_binaryset_eq:
fixes f :: "'a set \<Rightarrow> 'b::{comm_monoid_add, t2_space}"
@@ -148,7 +145,7 @@
by (auto simp add: increasing_def)
lemma countably_additiveI[case_names countably]:
- "(\<And>A. range A \<subseteq> M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i. A i) \<in> M \<Longrightarrow> (\<Sum>i. f (A i)) = f (\<Union>i. A i))
+ "(\<And>A. \<lbrakk>range A \<subseteq> M; disjoint_family A; (\<Union>i. A i) \<in> M\<rbrakk> \<Longrightarrow> (\<Sum>i. f(A i)) = f(\<Union>i. A i))
\<Longrightarrow> countably_additive M f"
by (simp add: countably_additive_def)
@@ -198,9 +195,9 @@
assume xy: "x \<in> M" "y \<in> M" "x \<subseteq> y"
then have "y - x \<in> M" by auto
then have "f x + 0 \<le> f x + f (y-x)" by (intro add_left_mono zero_le)
- also have "... = f (x \<union> (y-x))" using addf
- by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy(1,2))
- also have "... = f y"
+ also have "\<dots> = f (x \<union> (y-x))"
+ by (metis addf Diff_disjoint \<open>y - x \<in> M\<close> additiveD xy(1))
+ also have "\<dots> = f y"
by (metis Un_Diff_cancel Un_absorb1 xy(3))
finally show "f x \<le> f y" by simp
qed
@@ -222,9 +219,12 @@
also have "\<dots> = f (A x) + f ((\<Union>i\<in>F. A i) - A x)"
using f(2) by (rule additiveD) (insert in_M, auto)
also have "\<dots> \<le> f (A x) + f (\<Union>i\<in>F. A i)"
- using additive_increasing[OF f] in_M subs by (auto simp: increasing_def intro: add_left_mono)
- also have "\<dots> \<le> f (A x) + (\<Sum>i\<in>F. f (A i))" using insert by (auto intro: add_left_mono)
- finally show "f (\<Union>i\<in>(insert x F). A i) \<le> (\<Sum>i\<in>(insert x F). f (A i))" using insert by simp
+ using additive_increasing[OF f] in_M subs
+ by (simp add: increasingD)
+ also have "\<dots> \<le> f (A x) + (\<Sum>i\<in>F. f (A i))"
+ using insert by (auto intro: add_left_mono)
+ finally show "f (\<Union>i\<in>(insert x F). A i) \<le> (\<Sum>i\<in>(insert x F). f (A i))"
+ by (simp add: insert)
qed
lemma (in ring_of_sets) countably_additive_additive:
@@ -239,10 +239,8 @@
hence "range (binaryset x y) \<subseteq> M \<longrightarrow>
(\<Union>i. binaryset x y i) \<in> M \<longrightarrow>
f (\<Union>i. binaryset x y i) = (\<Sum> n. f (binaryset x y n))"
- using ca
- by (simp add: countably_additive_def)
- hence "{x,y,{}} \<subseteq> M \<longrightarrow> x \<union> y \<in> M \<longrightarrow>
- f (x \<union> y) = (\<Sum>n. f (binaryset x y n))"
+ using ca by (simp add: countably_additive_def)
+ hence "{x,y,{}} \<subseteq> M \<longrightarrow> x \<union> y \<in> M \<longrightarrow> f (x \<union> y) = (\<Sum>n. f (binaryset x y n))"
by (simp add: range_binaryset_eq UN_binaryset_eq)
thus "f (x \<union> y) = f x + f y" using posf x y
by (auto simp add: Un suminf_binaryset_eq positive_def)
@@ -259,8 +257,8 @@
fix N
note disj_N = disjoint_family_on_mono[OF _ disj, of "{..<N}"]
have "(\<Sum>i<N. f (A i)) = f (\<Union>i\<in>{..<N}. A i)"
- using A by (intro additive_sum [OF f ad _ _]) (auto simp: disj_N)
- also have "... \<le> f \<Omega>" using space_closed A
+ using A by (intro additive_sum [OF f ad]) (auto simp: disj_N)
+ also have "\<dots> \<le> f \<Omega>" using space_closed A
by (intro increasingD[OF inc] finite_UN) auto
finally show "(\<Sum>i<N. f (A i)) \<le> f \<Omega>" by simp
qed (insert f A, auto simp: positive_def)
@@ -272,16 +270,10 @@
proof (rule countably_additiveI)
fix F :: "nat \<Rightarrow> 'a set" assume F: "range F \<subseteq> M" "(\<Union>i. F i) \<in> M" and disj: "disjoint_family F"
- have "\<forall>i\<in>{i. F i \<noteq> {}}. \<exists>x. x \<in> F i" by auto
- from bchoice[OF this] obtain f where f: "\<And>i. F i \<noteq> {} \<Longrightarrow> f i \<in> F i" by auto
-
- have inj_f: "inj_on f {i. F i \<noteq> {}}"
- proof (rule inj_onI, simp)
- fix i j a b assume *: "f i = f j" "F i \<noteq> {}" "F j \<noteq> {}"
- then have "f i \<in> F i" "f j \<in> F j" using f by force+
- with disj * show "i = j" by (auto simp: disjoint_family_on_def)
- qed
- have "finite (\<Union>i. F i)"
+ have "\<forall>i. F i \<noteq> {} \<longrightarrow> (\<exists>x. x \<in> F i)" by auto
+ then obtain f where f: "\<And>i. F i \<noteq> {} \<Longrightarrow> f i \<in> F i" by metis
+
+ have finU: "finite (\<Union>i. F i)"
by (metis F(2) assms(1) infinite_super sets_into_space)
have F_subset: "{i. \<mu> (F i) \<noteq> 0} \<subseteq> {i. F i \<noteq> {}}"
@@ -290,8 +282,11 @@
proof (rule finite_imageD)
from f have "f`{i. F i \<noteq> {}} \<subseteq> (\<Union>i. F i)" by auto
then show "finite (f`{i. F i \<noteq> {}})"
- by (rule finite_subset) fact
- qed fact
+ by (simp add: finU finite_subset)
+ show inj_f: "inj_on f {i. F i \<noteq> {}}"
+ using f disj
+ by (simp add: inj_on_def disjoint_family_on_def disjoint_iff) metis
+ qed
ultimately have fin_not_0: "finite {i. \<mu> (F i) \<noteq> 0}"
by (rule finite_subset)
@@ -323,8 +318,7 @@
have f_UN: "(\<Sum>i. f (disjointed A i)) = f (\<Union>i. A i)"
by (auto simp: UN_disjointed_eq disjoint_family_disjointed)
moreover have "(\<lambda>n. (\<Sum>i<n. f (disjointed A i))) \<longlonglongrightarrow> (\<Sum>i. f (disjointed A i))"
- using f(1)[unfolded positive_def] dA
- by (auto intro!: summable_LIMSEQ)
+ by (simp add: summable_LIMSEQ)
from LIMSEQ_Suc[OF this]
have "(\<lambda>n. (\<Sum>i\<le>n. f (disjointed A i))) \<longlonglongrightarrow> (\<Sum>i. f (disjointed A i))"
unfolding lessThan_Suc_atMost .
@@ -332,23 +326,21 @@
using disjointed_additive[OF f A(1,2)] .
ultimately show "(\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Union>i. A i)" by simp
next
- assume cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Union>i. A i)"
+ assume cont[rule_format]: "\<forall>A. range A \<subseteq> M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Union>i. A i)"
fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "disjoint_family A" "(\<Union>i. A i) \<in> M"
have *: "(\<Union>n. (\<Union>i<n. A i)) = (\<Union>i. A i)" by auto
- have "(\<lambda>n. f (\<Union>i<n. A i)) \<longlonglongrightarrow> f (\<Union>i. A i)"
- proof (unfold *[symmetric], intro cont[rule_format])
- show "range (\<lambda>i. \<Union>i<i. A i) \<subseteq> M" "(\<Union>i. \<Union>i<i. A i) \<in> M"
- using A * by auto
- qed (force intro!: incseq_SucI)
+ have "range (\<lambda>i. \<Union>i<i. A i) \<subseteq> M" "(\<Union>i. \<Union>i<i. A i) \<in> M"
+ using A * by auto
+ then have "(\<lambda>n. f (\<Union>i<n. A i)) \<longlonglongrightarrow> f (\<Union>i. A i)"
+ unfolding *[symmetric] by (force intro!: cont incseq_SucI)+
moreover have "\<And>n. f (\<Union>i<n. A i) = (\<Sum>i<n. f (A i))"
using A
- by (intro additive_sum[OF f, of _ A, symmetric])
- (auto intro: disjoint_family_on_mono[where B=UNIV])
+ by (intro additive_sum[OF f, symmetric]) (auto intro: disjoint_family_on_mono)
ultimately
have "(\<lambda>i. f (A i)) sums f (\<Union>i. A i)"
unfolding sums_def by simp
- from sums_unique[OF this]
- show "(\<Sum>i. f (A i)) = f (\<Union>i. A i)" by simp
+ then show "(\<Sum>i. f (A i)) = f (\<Union>i. A i)"
+ by (metis sums_unique)
qed
lemma (in ring_of_sets) continuous_from_above_iff_empty_continuous:
@@ -357,13 +349,15 @@
shows "(\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Inter>i. A i))
\<longleftrightarrow> (\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> 0)"
proof safe
- assume cont: "(\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Inter>i. A i))"
- fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "decseq A" "(\<Inter>i. A i) = {}" "\<forall>i. f (A i) \<noteq> \<infinity>"
- with cont[THEN spec, of A] show "(\<lambda>i. f (A i)) \<longlonglongrightarrow> 0"
+ assume cont[rule_format]: "(\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Inter>i. A i))"
+ fix A :: "nat \<Rightarrow> 'a set"
+ assume A: "range A \<subseteq> M" "decseq A" "(\<Inter>i. A i) = {}" "\<forall>i. f (A i) \<noteq> \<infinity>"
+ with cont[of A] show "(\<lambda>i. f (A i)) \<longlonglongrightarrow> 0"
using \<open>positive M f\<close>[unfolded positive_def] by auto
next
- assume cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> 0"
- fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "decseq A" "(\<Inter>i. A i) \<in> M" "\<forall>i. f (A i) \<noteq> \<infinity>"
+ assume cont[rule_format]: "\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> 0"
+ fix A :: "nat \<Rightarrow> 'a set"
+ assume A: "range A \<subseteq> M" "decseq A" "(\<Inter>i. A i) \<in> M" "\<forall>i. f (A i) \<noteq> \<infinity>"
have f_mono: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<subseteq> b \<Longrightarrow> f a \<le> f b"
using additive_increasing[OF f] unfolding increasing_def by simp
@@ -378,23 +372,19 @@
using A by (auto intro!: f_mono)
then have f_Int_fin: "f (\<Inter>x. A x) \<noteq> \<infinity>"
using A by (auto simp: top_unique)
- { fix i
- have "f (A i - (\<Inter>i. A i)) \<le> f (A i)" using A by (auto intro!: f_mono)
- then have "f (A i - (\<Inter>i. A i)) \<noteq> \<infinity>"
- using A by (auto simp: top_unique) }
- note f_fin = this
+ have f_fin: "f (A i - (\<Inter>i. A i)) \<noteq> \<infinity>" for i
+ using A by (metis Diff Diff_subset f_mono infinity_ennreal_def range_subsetD top_unique)
have "(\<lambda>i. f (A i - (\<Inter>i. A i))) \<longlonglongrightarrow> 0"
- proof (intro cont[rule_format, OF _ decseq _ f_fin])
+ proof (intro cont[ OF _ decseq _ f_fin])
show "range (\<lambda>i. A i - (\<Inter>i. A i)) \<subseteq> M" "(\<Inter>i. A i - (\<Inter>i. A i)) = {}"
using A by auto
qed
- from INF_Lim[OF decseq_f this]
- have "(INF n. f (A n - (\<Inter>i. A i))) = 0" .
+ with INF_Lim decseq_f have "(INF n. f (A n - (\<Inter>i. A i))) = 0" by metis
moreover have "(INF n. f (\<Inter>i. A i)) = f (\<Inter>i. A i)"
by auto
ultimately have "(INF n. f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i)) = 0 + f (\<Inter>i. A i)"
using A(4) f_fin f_Int_fin
- by (subst INF_ennreal_add_const) (auto simp: decseq_f)
+ using INF_ennreal_add_const by presburger
moreover {
fix n
have "f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i) = f ((A n - (\<Inter>i. A i)) \<union> (\<Inter>i. A i))"
@@ -424,7 +414,8 @@
also have "((\<Union>i. A i) - A i) \<union> A i = (\<Union>i. A i)"
by auto
finally have "f ((\<Union>i. A i) - A i) = f (\<Union>i. A i) - f (A i)"
- using f(3)[rule_format, of "A i"] A by (auto simp: ennreal_add_diff_cancel subset_eq) }
+ using assms f by fastforce
+ }
moreover have "\<forall>\<^sub>F i in sequentially. f (A i) \<le> f (\<Union>i. A i)"
using increasingD[OF additive_increasing[OF f(1, 2)], of "A _" "\<Union>i. A i"] A
by (auto intro!: always_eventually simp: subset_eq)
@@ -502,17 +493,11 @@
by (metis emeasure_mono emeasure_notin_sets sets.sets_into_space sets.top zero_le)
lemma emeasure_Diff:
- assumes finite: "emeasure M B \<noteq> \<infinity>"
- and [measurable]: "A \<in> sets M" "B \<in> sets M" and "B \<subseteq> A"
+ assumes "emeasure M B \<noteq> \<infinity>"
+ and "A \<in> sets M" "B \<in> sets M" and "B \<subseteq> A"
shows "emeasure M (A - B) = emeasure M A - emeasure M B"
-proof -
- have "(A - B) \<union> B = A" using \<open>B \<subseteq> A\<close> by auto
- then have "emeasure M A = emeasure M ((A - B) \<union> B)" by simp
- also have "\<dots> = emeasure M (A - B) + emeasure M B"
- by (subst plus_emeasure[symmetric]) auto
- finally show "emeasure M (A - B) = emeasure M A - emeasure M B"
- using finite by simp
-qed
+ by (smt (verit, best) add_diff_self_ennreal assms emeasure_Un emeasure_mono
+ ennreal_add_left_cancel le_iff_sup)
lemma emeasure_compl:
"s \<in> sets M \<Longrightarrow> emeasure M s \<noteq> \<infinity> \<Longrightarrow> emeasure M (space M - s) = emeasure M (space M) - emeasure M s"
@@ -563,8 +548,7 @@
also have "\<dots> = emeasure M (A 0) - emeasure M (\<Inter>i. A i)"
using A finite * by (simp, subst emeasure_Diff) auto
finally show ?thesis
- by (rule ennreal_minus_cancel[rotated 3])
- (insert finite A, auto intro: INF_lower emeasure_mono)
+ by (smt (verit, best) Inf_lower diff_diff_ennreal le_MI finite range_eqI)
qed
lemma INF_emeasure_decseq':
@@ -580,7 +564,7 @@
have "(INF n. emeasure M (A n)) = (INF n. emeasure M (A (n + i)))"
proof (rule INF_eq)
show "\<exists>j\<in>UNIV. emeasure M (A (j + i)) \<le> emeasure M (A i')" for i'
- by (intro bexI[of _ i'] emeasure_mono decseqD[OF \<open>decseq A\<close>] A) auto
+ by (meson A \<open>decseq A\<close> decseq_def emeasure_mono iso_tuple_UNIV_I nat_le_iff_add)
qed auto
also have "\<dots> = emeasure M (INF n. (A (n + i)))"
using A \<open>decseq A\<close> fin by (intro INF_emeasure_decseq) (auto simp: decseq_def less_top)
@@ -1118,7 +1102,7 @@
text \<open>The next lemma is convenient to combine with a lemma whose conclusion is of the
form \<open>AE x in M. P x = Q x\<close>: for such a lemma, there is no \<open>[symmetric]\<close> variant,
-but using \<open>AE_symmetric[OF...]\<close> will replace it.\<close>
+but using \<open>AE_symmetric[OF\<dots>]\<close> will replace it.\<close>
(* depricated replace by laws about eventually *)
lemma
@@ -1645,11 +1629,9 @@
have "emeasure M (A \<union> B) \<noteq> \<infinity>"
using emeasure_subadditive[OF measurable] fin by (auto simp: top_unique)
then show "(measure M (A \<union> B)) \<le> (measure M A) + (measure M B)"
- using emeasure_subadditive[OF measurable] fin
- apply simp
- apply (subst (asm) (2 3 4) emeasure_eq_ennreal_measure)
- apply (auto simp flip: ennreal_plus)
- done
+ unfolding measure_def
+ by (metis emeasure_subadditive[OF measurable] fin enn2real_mono enn2real_plus
+ ennreal_add_less_top infinity_ennreal_def less_top)
qed
lemma measure_subadditive_finite:
@@ -1672,13 +1654,13 @@
assumes A: "range A \<subseteq> sets M" and fin: "(\<Sum>i. emeasure M (A i)) \<noteq> \<infinity>"
shows "measure M (\<Union>i. A i) \<le> (\<Sum>i. measure M (A i))"
proof -
- from fin have **: "\<And>i. emeasure M (A i) \<noteq> top"
- using ennreal_suminf_lessD[of "\<lambda>i. emeasure M (A i)"] by (simp add: less_top)
- { have "emeasure M (\<Union>i. A i) \<le> (\<Sum>i. emeasure M (A i))"
- using emeasure_subadditive_countably[OF A] .
- also have "\<dots> < \<infinity>"
- using fin by (simp add: less_top)
- finally have "emeasure M (\<Union>i. A i) \<noteq> top" by simp }
+ have **: "\<And>i. emeasure M (A i) \<noteq> top"
+ using fin ennreal_suminf_lessD[of "\<lambda>i. emeasure M (A i)"] by (simp add: less_top)
+ have ge0: "(\<Sum>i. Sigma_Algebra.measure M (A i)) \<ge> 0"
+ using fin emeasure_eq_ennreal_measure[OF **]
+ by (metis infinity_ennreal_def measure_nonneg suminf_cong suminf_nonneg summable_suminf_not_top)
+ have "emeasure M (\<Union>i. A i) \<noteq> top"
+ by (metis A emeasure_subadditive_countably fin infinity_ennreal_def neq_top_trans)
then have "ennreal (measure M (\<Union>i. A i)) = emeasure M (\<Union>i. A i)"
by (rule emeasure_eq_ennreal_measure[symmetric])
also have "\<dots> \<le> (\<Sum>i. emeasure M (A i))"
@@ -1687,11 +1669,7 @@
using fin unfolding emeasure_eq_ennreal_measure[OF **]
by (subst suminf_ennreal) (auto simp: **)
finally show ?thesis
- apply (rule ennreal_le_iff[THEN iffD1, rotated])
- apply (intro suminf_nonneg allI measure_nonneg summable_suminf_not_top)
- using fin
- apply (simp add: emeasure_eq_ennreal_measure[OF **])
- done
+ using ge0 ennreal_le_iff by blast
qed
lemma measure_Un_null_set: "A \<in> sets M \<Longrightarrow> B \<in> null_sets M \<Longrightarrow> measure M (A \<union> B) = measure M A"
@@ -2038,11 +2016,11 @@
have "emeasure M (B N) \<le> (\<Sum>n\<in>{..<N}. emeasure M (A n))"
unfolding B_def by (rule emeasure_subadditive_finite, auto)
- also have "... = (\<Sum>n\<in>{..<N}. ennreal(measure M (A n)))"
+ also have "\<dots> = (\<Sum>n\<in>{..<N}. ennreal(measure M (A n)))"
using assms(2) by (simp add: emeasure_eq_ennreal_measure less_top)
- also have "... = ennreal (\<Sum>n\<in>{..<N}. measure M (A n))"
+ also have "\<dots> = ennreal (\<Sum>n\<in>{..<N}. measure M (A n))"
by auto
- also have "... \<le> ennreal (\<Sum>n. measure M (A n))"
+ also have "\<dots> \<le> ennreal (\<Sum>n. measure M (A n))"
using * by (auto simp: ennreal_leI)
finally show ?thesis by simp
qed
@@ -2069,9 +2047,9 @@
have I: "(\<Union>k\<in>{n..}. A k) = (\<Union>k. A (k+n))" by (auto, metis le_add_diff_inverse2, fastforce)
have "emeasure M (limsup A) \<le> emeasure M (\<Union>k\<in>{n..}. A k)"
by (rule emeasure_mono, auto simp add: limsup_INF_SUP)
- also have "... = emeasure M (\<Union>k. A (k+n))"
+ also have "\<dots> = emeasure M (\<Union>k. A (k+n))"
using I by auto
- also have "... \<le> (\<Sum>k. measure M (A (k+n)))"
+ also have "\<dots> \<le> (\<Sum>k. measure M (A (k+n)))"
apply (rule emeasure_union_summable)
using assms summable_ignore_initial_segment[OF assms(3), of n] by auto
finally show ?thesis by simp
--- a/src/HOL/Transcendental.thy Thu Dec 29 16:44:45 2022 +0100
+++ b/src/HOL/Transcendental.thy Thu Dec 29 22:14:25 2022 +0000
@@ -5477,6 +5477,64 @@
using that by metis
qed
+lemma arccos_arctan:
+ assumes "-1 < x" "x < 1"
+ shows "arccos x = pi/2 - arctan(x / sqrt(1 - x\<^sup>2))"
+proof -
+ have "arctan(x / sqrt(1 - x\<^sup>2)) - (pi/2 - arccos x) = 0"
+ proof (rule sin_eq_0_pi)
+ show "- pi < arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)"
+ using arctan_lbound [of "x / sqrt(1 - x\<^sup>2)"] arccos_bounded [of x] assms
+ by (simp add: algebra_simps)
+ next
+ show "arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x) < pi"
+ using arctan_ubound [of "x / sqrt(1 - x\<^sup>2)"] arccos_bounded [of x] assms
+ by (simp add: algebra_simps)
+ next
+ show "sin (arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)) = 0"
+ using assms
+ by (simp add: algebra_simps sin_diff cos_add sin_arccos sin_arctan cos_arctan
+ power2_eq_square square_eq_1_iff)
+ qed
+ then show ?thesis
+ by simp
+qed
+
+lemma arcsin_plus_arccos:
+ assumes "-1 \<le> x" "x \<le> 1"
+ shows "arcsin x + arccos x = pi/2"
+proof -
+ have "arcsin x = pi/2 - arccos x"
+ apply (rule sin_inj_pi)
+ using assms arcsin [OF assms] arccos [OF assms]
+ by (auto simp: algebra_simps sin_diff)
+ then show ?thesis
+ by (simp add: algebra_simps)
+qed
+
+lemma arcsin_arccos_eq: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = pi/2 - arccos x"
+ using arcsin_plus_arccos by force
+
+lemma arccos_arcsin_eq: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = pi/2 - arcsin x"
+ using arcsin_plus_arccos by force
+
+lemma arcsin_arctan: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> arcsin x = arctan(x / sqrt(1 - x\<^sup>2))"
+ by (simp add: arccos_arctan arcsin_arccos_eq)
+
+lemma arcsin_arccos_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = arccos(sqrt(1 - x\<^sup>2))"
+ by (smt (verit, del_insts) arccos_cos arcsin_0 arcsin_le_arcsin arcsin_pi cos_arcsin)
+
+lemma arcsin_arccos_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arcsin x = -arccos(sqrt(1 - x\<^sup>2))"
+ using arcsin_arccos_sqrt_pos [of "-x"]
+ by (simp add: arcsin_minus)
+
+lemma arccos_arcsin_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = arcsin(sqrt(1 - x\<^sup>2))"
+ by (smt (verit, del_insts) arccos_lbound arccos_le_pi2 arcsin_sin sin_arccos)
+
+lemma arccos_arcsin_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arccos x = pi - arcsin(sqrt(1 - x\<^sup>2))"
+ using arccos_arcsin_sqrt_pos [of "-x"]
+ by (simp add: arccos_minus)
+
lemma cos_limit_1:
assumes "(\<lambda>j. cos (\<theta> j)) \<longlonglongrightarrow> 1"
shows "\<exists>k. (\<lambda>j. \<theta> j - of_int (k j) * (2 * pi)) \<longlonglongrightarrow> 0"