--- a/NEWS Wed Mar 01 21:05:09 2023 +0000
+++ b/NEWS Thu Mar 02 11:34:54 2023 +0000
@@ -231,6 +231,13 @@
totalp_on_multpDM
totalp_on_multpHO
+* HOL-Algebra: new theories SimpleGroups (simple groups)
+ and SndIsomorphismGrp (second isomorphism theorem for groups),
+ by Jakob von Raumer
+
+* HOL-Analysis and HOL-Complex_Analysis: much new material, due to
+ Manuel Eberl and Wenda Li.
+
* Mirabelle:
- Added session to output directory structure. Minor INCOMPATIBILITY.
--- a/src/HOL/Analysis/Further_Topology.thy Wed Mar 01 21:05:09 2023 +0000
+++ b/src/HOL/Analysis/Further_Topology.thy Thu Mar 02 11:34:54 2023 +0000
@@ -3333,7 +3333,7 @@
then have "z \<noteq> 0" by auto
have "(w/z)^n = 1"
by (metis False divide_self_if eq power_divide power_one)
- then obtain j where j: "w / z = exp (2 * of_real pi * \<i> * j / n)" and "j < n"
+ then obtain j::nat where j: "w / z = exp (2 * of_real pi * \<i> * j / n)" and "j < n"
using Suc_leI assms \<open>2 \<le> n\<close> complex_roots_unity [THEN eqset_imp_iff, of n "w/z"]
by force
have "cmod (w/z - 1) < 2 * sin (pi / real n)"
--- a/src/HOL/Analysis/Uniform_Limit.thy Wed Mar 01 21:05:09 2023 +0000
+++ b/src/HOL/Analysis/Uniform_Limit.thy Thu Mar 02 11:34:54 2023 +0000
@@ -6,7 +6,7 @@
section \<open>Uniform Limit and Uniform Convergence\<close>
theory Uniform_Limit
-imports Connected Summation_Tests
+imports Connected Summation_Tests Infinite_Sum
begin
@@ -560,12 +560,67 @@
shows "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"
unfolding uniformly_convergent_on_def by (rule exI, rule Weierstrass_m_test[OF assms])
-lemma uniform_limit_eq_rhs: "uniform_limit X f l F \<Longrightarrow> l = m \<Longrightarrow> uniform_limit X f m F"
- by simp
+
+lemma Weierstrass_m_test_general:
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: banach"
+ fixes M :: "'a \<Rightarrow> real"
+ assumes norm_le: "\<And>x y. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> norm (f x y) \<le> M x"
+ assumes summable: "M summable_on X"
+ shows "uniform_limit Y (\<lambda>X y. \<Sum>x\<in>X. f x y) (\<lambda>y. \<Sum>\<^sub>\<infinity>x\<in>X. f x y) (finite_subsets_at_top X)"
+proof (rule uniform_limitI)
+ fix \<epsilon> :: real
+ assume "\<epsilon> > 0"
+ define S where "S = (\<lambda>y. \<Sum>\<^sub>\<infinity>x\<in>X. f x y)"
+ have S: "((\<lambda>x. f x y) has_sum S y) X" if y: "y \<in> Y" for y
+ unfolding S_def
+ proof (rule has_sum_infsum)
+ have "(\<lambda>x. norm (f x y)) summable_on X"
+ by (rule abs_summable_on_comparison_test'[OF summable norm_le]) (use y in auto)
+ thus "(\<lambda>x. f x y) summable_on X"
+ by (metis abs_summable_summable)
+ qed
+
+ define T where "T = (\<Sum>\<^sub>\<infinity>x\<in>X. M x)"
+ have T: "(M has_sum T) X"
+ unfolding T_def by (simp add: local.summable)
+ have M_summable: "M summable_on X'" if "X' \<subseteq> X" for X'
+ using local.summable summable_on_subset_banach that by blast
+
+ have f_summable: "(\<lambda>x. f x y) summable_on X'" if "X' \<subseteq> X" "y \<in> Y" for X' y
+ using S summable_on_def summable_on_subset_banach that by blast
+ have "eventually (\<lambda>X'. dist (\<Sum>x\<in>X'. M x) T < \<epsilon>) (finite_subsets_at_top X)"
+ using T \<open>\<epsilon> > 0\<close> unfolding T_def has_sum_def tendsto_iff by blast
+ moreover have "eventually (\<lambda>X'. finite X' \<and> X' \<subseteq> X) (finite_subsets_at_top X)"
+ by (simp add: eventually_finite_subsets_at_top_weakI)
+ ultimately show "\<forall>\<^sub>F X' in finite_subsets_at_top X. \<forall>y\<in>Y. dist (\<Sum>x\<in>X'. f x y) (\<Sum>\<^sub>\<infinity>x\<in>X. f x y) < \<epsilon>"
+ proof eventually_elim
+ case X': (elim X')
+ show "\<forall>y\<in>Y. dist (\<Sum>x\<in>X'. f x y) (\<Sum>\<^sub>\<infinity>x\<in>X. f x y) < \<epsilon>"
+ proof
+ fix y assume y: "y \<in> Y"
+ have 1: "((\<lambda>x. f x y) has_sum (S y - (\<Sum>x\<in>X'. f x y))) (X - X')"
+ using X' y by (intro has_sum_Diff S has_sum_finite[of X'] f_summable) auto
+ have 2: "(M has_sum (T - (\<Sum>x\<in>X'. M x))) (X - X')"
+ using X' y by (intro has_sum_Diff T has_sum_finite[of X'] M_summable) auto
+ have "dist (\<Sum>x\<in>X'. f x y) (\<Sum>\<^sub>\<infinity>x\<in>X. f x y) = norm (S y - (\<Sum>x\<in>X'. f x y))"
+ by (simp add: dist_norm norm_minus_commute S_def)
+ also have "norm (S y - (\<Sum>x\<in>X'. f x y)) \<le> (\<Sum>\<^sub>\<infinity>x\<in>X-X'. M x)"
+ using 2 y by (intro norm_infsum_le[OF 1 _ norm_le]) (auto simp: infsumI)
+ also have "\<dots> = T - (\<Sum>x\<in>X'. M x)"
+ using 2 by (auto simp: infsumI)
+ also have "\<dots> < \<epsilon>"
+ using X' by (simp add: dist_norm)
+ finally show "dist (\<Sum>x\<in>X'. f x y) (\<Sum>\<^sub>\<infinity>x\<in>X. f x y) < \<epsilon>" .
+ qed
+ qed
+qed
subsection\<^marker>\<open>tag unimportant\<close> \<open>Structural introduction rules\<close>
+lemma uniform_limit_eq_rhs: "uniform_limit X f l F \<Longrightarrow> l = m \<Longrightarrow> uniform_limit X f m F"
+ by simp
+
named_theorems uniform_limit_intros "introduction rules for uniform_limit"
setup \<open>
Global_Theory.add_thms_dynamic (\<^binding>\<open>uniform_limit_eq_intros\<close>,
--- a/src/HOL/Probability/Probability_Mass_Function.thy Wed Mar 01 21:05:09 2023 +0000
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Thu Mar 02 11:34:54 2023 +0000
@@ -12,6 +12,9 @@
"HOL-Library.Multiset"
begin
+text \<open>Conflicting notation from \<^theory>\<open>HOL-Analysis.Infinite_Sum\<close>\<close>
+no_notation Infinite_Sum.abs_summable_on (infixr "abs'_summable'_on" 46)
+
lemma AE_emeasure_singleton:
assumes x: "emeasure M {x} \<noteq> 0" and ae: "AE x in M. P x" shows "P x"
proof -
--- a/src/HOL/Probability/Product_PMF.thy Wed Mar 01 21:05:09 2023 +0000
+++ b/src/HOL/Probability/Product_PMF.thy Thu Mar 02 11:34:54 2023 +0000
@@ -7,6 +7,9 @@
imports Probability_Mass_Function Independent_Family
begin
+text \<open>Conflicting notation from \<^theory>\<open>HOL-Analysis.Infinite_Sum\<close>\<close>
+no_notation Infinite_Sum.abs_summable_on (infixr "abs'_summable'_on" 46)
+
subsection \<open>Preliminaries\<close>
lemma pmf_expectation_eq_infsetsum: "measure_pmf.expectation p f = infsetsum (\<lambda>x. pmf p x * f x) UNIV"
--- a/src/HOL/Probability/SPMF.thy Wed Mar 01 21:05:09 2023 +0000
+++ b/src/HOL/Probability/SPMF.thy Thu Mar 02 11:34:54 2023 +0000
@@ -2338,20 +2338,23 @@
lemma scale_scale_spmf:
"scale_spmf r (scale_spmf r' p) = scale_spmf (r * max 0 (min (inverse (weight_spmf p)) r')) p"
(is "?lhs = ?rhs")
-proof(rule spmf_eqI)
- fix i
- have "max 0 (min (1 / weight_spmf p) r') *
- max 0 (min (1 / min 1 (weight_spmf p * max 0 r')) r) =
- max 0 (min (1 / weight_spmf p) (r * max 0 (min (1 / weight_spmf p) r')))"
- proof(cases "weight_spmf p > 0")
- case False
- thus ?thesis by(simp add: not_less weight_spmf_le_0)
- next
- case True
- thus ?thesis by(simp add: field_simps max_def min.absorb_iff2[symmetric])(auto simp add: min_def field_simps zero_le_mult_iff)
+proof(cases "weight_spmf p > 0")
+ case False
+ thus ?thesis
+ by (simp add: weight_spmf_eq_0 zero_less_measure_iff)
+next
+ case True
+ show ?thesis
+ proof(rule spmf_eqI)
+ fix i
+ have "max 0 (min (1 / weight_spmf p) r') * max 0 (min (1 / min 1 (weight_spmf p * max 0 r')) r) =
+ max 0 (min (1 / weight_spmf p) (r * max 0 (min (1 / weight_spmf p) r')))"
+ using True
+ by(simp add: field_simps max_def min.absorb_iff2[symmetric])(auto simp add: min_def field_simps zero_le_mult_iff)
+ then show "spmf ?lhs i = spmf ?rhs i"
+ apply (subst spmf_scale_spmf)+ (*FOR SOME REASON we now get linarith_split_limit exceeded if simp is used*)
+ by (metis (no_types, opaque_lifting) inverse_eq_divide mult.commute mult.left_commute weight_scale_spmf)
qed
- then show "spmf ?lhs i = spmf ?rhs i"
- by(simp add: spmf_scale_spmf field_simps weight_scale_spmf)
qed
lemma scale_scale_spmf' [simp]: