moved lemmas to appropriate places
authorhoelzl
Wed Apr 25 19:26:00 2012 +0200 (2012-04-25)
changeset 47761dfe747e72fa8
parent 47760 b9840d8fca43
child 47762 d31085f07f60
moved lemmas to appropriate places
src/HOL/Library/FuncSet.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Caratheodory.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Series.thy
     1.1 --- a/src/HOL/Library/FuncSet.thy	Wed Apr 25 17:15:10 2012 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Wed Apr 25 19:26:00 2012 +0200
     1.3 @@ -63,6 +63,9 @@
     1.4  lemma Pi_mem: "[|f: Pi A B; x \<in> A|] ==> f x \<in> B x"
     1.5    by (simp add: Pi_def)
     1.6  
     1.7 +lemma Pi_iff: "f \<in> Pi I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i)"
     1.8 +  unfolding Pi_def by auto
     1.9 +
    1.10  lemma PiE [elim]:
    1.11    "f : Pi A B ==> (f x : B x ==> Q) ==> (x ~: A ==> Q) ==> Q"
    1.12  by(auto simp: Pi_def)
     2.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Apr 25 17:15:10 2012 +0200
     2.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Apr 25 19:26:00 2012 +0200
     2.3 @@ -1129,22 +1129,6 @@
     2.4      using assms real by (simp add: ereal_le_minus)
     2.5  qed (insert assms, auto)
     2.6  
     2.7 -lemma sums_finite:
     2.8 -  assumes "\<forall>N\<ge>n. f N = 0"
     2.9 -  shows "f sums (\<Sum>N<n. f N)"
    2.10 -proof -
    2.11 -  { fix i have "(\<Sum>N<i + n. f N) = (\<Sum>N<n. f N)"
    2.12 -      by (induct i) (insert assms, auto) }
    2.13 -  note this[simp]
    2.14 -  show ?thesis unfolding sums_def
    2.15 -    by (rule LIMSEQ_offset[of _ n]) (auto simp add: atLeast0LessThan intro: tendsto_const)
    2.16 -qed
    2.17 -
    2.18 -lemma suminf_finite:
    2.19 -  fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add,t2_space}" assumes "\<forall>N\<ge>n. f N = 0"
    2.20 -  shows "suminf f = (\<Sum>N<n. f N)"
    2.21 -  using sums_finite[OF assms, THEN sums_unique] by simp
    2.22 -
    2.23  lemma suminf_upper:
    2.24    fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>n. 0 \<le> f n"
    2.25    shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
    2.26 @@ -1294,4 +1278,13 @@
    2.27      apply (subst SUP_commute) ..
    2.28  qed
    2.29  
    2.30 +lemma suminf_setsum_ereal:
    2.31 +  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> ereal"
    2.32 +  assumes nonneg: "\<And>i a. a \<in> A \<Longrightarrow> 0 \<le> f i a"
    2.33 +  shows "(\<Sum>i. \<Sum>a\<in>A. f i a) = (\<Sum>a\<in>A. \<Sum>i. f i a)"
    2.34 +proof cases
    2.35 +  assume "finite A" from this nonneg show ?thesis
    2.36 +    by induct (simp_all add: suminf_add_ereal setsum_nonneg)
    2.37 +qed simp
    2.38 +
    2.39  end
     3.1 --- a/src/HOL/Probability/Borel_Space.thy	Wed Apr 25 17:15:10 2012 +0200
     3.2 +++ b/src/HOL/Probability/Borel_Space.thy	Wed Apr 25 19:26:00 2012 +0200
     3.3 @@ -943,6 +943,28 @@
     3.4    using measurable_comp[OF f borel_measurable_borel_log[OF `1 < b`]]
     3.5    by (simp add: comp_def)
     3.6  
     3.7 +lemma borel_measurable_real_floor:
     3.8 +  "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
     3.9 +  unfolding borel_measurable_iff_ge
    3.10 +proof (intro allI)
    3.11 +  fix a :: real
    3.12 +  { fix x have "a \<le> real \<lfloor>x\<rfloor> \<longleftrightarrow> real \<lceil>a\<rceil> \<le> x"
    3.13 +      using le_floor_eq[of "\<lceil>a\<rceil>" x] ceiling_le_iff[of a "\<lfloor>x\<rfloor>"]
    3.14 +      unfolding real_eq_of_int by simp }
    3.15 +  then have "{w::real \<in> space borel. a \<le> real \<lfloor>w\<rfloor>} = {real \<lceil>a\<rceil>..}" by auto
    3.16 +  then show "{w::real \<in> space borel. a \<le> real \<lfloor>w\<rfloor>} \<in> sets borel" by auto
    3.17 +qed
    3.18 +
    3.19 +lemma borel_measurable_real_natfloor[intro, simp]:
    3.20 +  assumes "f \<in> borel_measurable M"
    3.21 +  shows "(\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
    3.22 +proof -
    3.23 +  have "\<And>x. real (natfloor (f x)) = max 0 (real \<lfloor>f x\<rfloor>)"
    3.24 +    by (auto simp: max_def natfloor_def)
    3.25 +  with borel_measurable_max[OF measurable_comp[OF assms borel_measurable_real_floor] borel_measurable_const]
    3.26 +  show ?thesis by (simp add: comp_def)
    3.27 +qed
    3.28 +
    3.29  subsection "Borel space on the extended reals"
    3.30  
    3.31  lemma borel_measurable_ereal_borel:
     4.1 --- a/src/HOL/Probability/Caratheodory.thy	Wed Apr 25 17:15:10 2012 +0200
     4.2 +++ b/src/HOL/Probability/Caratheodory.thy	Wed Apr 25 19:26:00 2012 +0200
     4.3 @@ -357,7 +357,7 @@
     4.4  proof -
     4.5    let ?A = "\<lambda>i::nat. (if i = 0 then b else {})"
     4.6    have "(\<Sum>i. f (?A i)) = (\<Sum>i<1::nat. f (?A i))"
     4.7 -    by (rule suminf_finite) (simp add: f[unfolded positive_def])
     4.8 +    by (rule suminf_finite) (simp_all add: f[unfolded positive_def])
     4.9    also have "... = f b"
    4.10      by simp
    4.11    finally show ?thesis using assms
     5.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Wed Apr 25 17:15:10 2012 +0200
     5.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Wed Apr 25 19:26:00 2012 +0200
     5.3 @@ -11,9 +11,6 @@
     5.4  lemma split_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
     5.5    by auto
     5.6  
     5.7 -lemma Pi_iff: "f \<in> Pi I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i)"
     5.8 -  unfolding Pi_def by auto
     5.9 -
    5.10  abbreviation
    5.11    "Pi\<^isub>E A B \<equiv> Pi A B \<inter> extensional A"
    5.12  
     6.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Wed Apr 25 17:15:10 2012 +0200
     6.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Wed Apr 25 19:26:00 2012 +0200
     6.3 @@ -32,16 +32,6 @@
     6.4      by (intro tendsto_add assms tendsto_divide tendsto_norm tendsto_diff) auto
     6.5  qed
     6.6  
     6.7 -lemma measure_Union:
     6.8 -  assumes "finite S" "S \<subseteq> sets M" "\<And>A B. A \<in> S \<Longrightarrow> B \<in> S \<Longrightarrow> A \<noteq> B \<Longrightarrow> A \<inter> B = {}"
     6.9 -  shows "setsum (emeasure M) S = (emeasure M) (\<Union>S)"
    6.10 -proof -
    6.11 -  have "setsum (emeasure M) S = (emeasure M) (\<Union>i\<in>S. i)"
    6.12 -    using assms by (intro setsum_emeasure[OF _ _ `finite S`]) (auto simp: disjoint_family_on_def)
    6.13 -  also have "\<dots> = (emeasure M) (\<Union>S)" by (auto intro!: arg_cong[where f="emeasure M"])
    6.14 -  finally show ?thesis .
    6.15 -qed
    6.16 -
    6.17  lemma measurable_sets2[intro]:
    6.18    assumes "f \<in> measurable M M'" "g \<in> measurable M M''"
    6.19    and "A \<in> sets M'" "B \<in> sets M''"
    6.20 @@ -57,55 +47,6 @@
    6.21    assume "\<forall>n. f n \<le> f (Suc n)" then show "incseq f" by (auto intro!: incseq_SucI)
    6.22  qed (auto simp: incseq_def)
    6.23  
    6.24 -lemma borel_measurable_real_floor:
    6.25 -  "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
    6.26 -  unfolding borel_measurable_iff_ge
    6.27 -proof (intro allI)
    6.28 -  fix a :: real
    6.29 -  { fix x have "a \<le> real \<lfloor>x\<rfloor> \<longleftrightarrow> real \<lceil>a\<rceil> \<le> x"
    6.30 -      using le_floor_eq[of "\<lceil>a\<rceil>" x] ceiling_le_iff[of a "\<lfloor>x\<rfloor>"]
    6.31 -      unfolding real_eq_of_int by simp }
    6.32 -  then have "{w::real \<in> space borel. a \<le> real \<lfloor>w\<rfloor>} = {real \<lceil>a\<rceil>..}" by auto
    6.33 -  then show "{w::real \<in> space borel. a \<le> real \<lfloor>w\<rfloor>} \<in> sets borel" by auto
    6.34 -qed
    6.35 -
    6.36 -lemma borel_measurable_real_natfloor[intro, simp]:
    6.37 -  assumes "f \<in> borel_measurable M"
    6.38 -  shows "(\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
    6.39 -proof -
    6.40 -  have "\<And>x. real (natfloor (f x)) = max 0 (real \<lfloor>f x\<rfloor>)"
    6.41 -    by (auto simp: max_def natfloor_def)
    6.42 -  with borel_measurable_max[OF measurable_comp[OF assms borel_measurable_real_floor] borel_measurable_const]
    6.43 -  show ?thesis by (simp add: comp_def)
    6.44 -qed
    6.45 -
    6.46 -lemma AE_not_in:
    6.47 -  assumes N: "N \<in> null_sets M" shows "AE x in M. x \<notin> N"
    6.48 -  using N by (rule AE_I') auto
    6.49 -
    6.50 -lemma sums_If_finite:
    6.51 -  fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
    6.52 -  assumes finite: "finite {r. P r}"
    6.53 -  shows "(\<lambda>r. if P r then f r else 0) sums (\<Sum>r\<in>{r. P r}. f r)" (is "?F sums _")
    6.54 -proof cases
    6.55 -  assume "{r. P r} = {}" hence "\<And>r. \<not> P r" by auto
    6.56 -  thus ?thesis by (simp add: sums_zero)
    6.57 -next
    6.58 -  assume not_empty: "{r. P r} \<noteq> {}"
    6.59 -  have "?F sums (\<Sum>r = 0..< Suc (Max {r. P r}). ?F r)"
    6.60 -    by (rule series_zero)
    6.61 -       (auto simp add: Max_less_iff[OF finite not_empty] less_eq_Suc_le[symmetric])
    6.62 -  also have "(\<Sum>r = 0..< Suc (Max {r. P r}). ?F r) = (\<Sum>r\<in>{r. P r}. f r)"
    6.63 -    by (subst setsum_cases)
    6.64 -       (auto intro!: setsum_cong simp: Max_ge_iff[OF finite not_empty] less_Suc_eq_le)
    6.65 -  finally show ?thesis .
    6.66 -qed
    6.67 -
    6.68 -lemma sums_single:
    6.69 -  fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
    6.70 -  shows "(\<lambda>r. if r = i then f r else 0) sums f i"
    6.71 -  using sums_If_finite[of "\<lambda>r. r = i" f] by simp
    6.72 -
    6.73  section "Simple function"
    6.74  
    6.75  text {*
    6.76 @@ -526,7 +467,7 @@
    6.77    { fix x assume "x \<in> space M"
    6.78      have "\<Union>(?sub (f x)) = (f -` {f x} \<inter> space M)" by auto
    6.79      with sets have "(emeasure M) (f -` {f x} \<inter> space M) = setsum (emeasure M) (?sub (f x))"
    6.80 -      by (subst measure_Union) auto }
    6.81 +      by (subst setsum_emeasure) (auto simp: disjoint_family_on_def) }
    6.82    hence "integral\<^isup>S M f = (\<Sum>(x,A)\<in>?SIGMA. x * (emeasure M) A)"
    6.83      unfolding simple_integral_def using f sets
    6.84      by (subst setsum_Sigma[symmetric])
     7.1 --- a/src/HOL/Probability/Measure_Space.thy	Wed Apr 25 17:15:10 2012 +0200
     7.2 +++ b/src/HOL/Probability/Measure_Space.thy	Wed Apr 25 19:26:00 2012 +0200
     7.3 @@ -12,22 +12,6 @@
     7.4    "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
     7.5  begin
     7.6  
     7.7 -lemma suminf_eq_setsum:
     7.8 -  fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add, t2_space}"
     7.9 -  assumes "finite {i. f i \<noteq> 0}" (is "finite ?P")
    7.10 -  shows "(\<Sum>i. f i) = (\<Sum>i | f i \<noteq> 0. f i)"
    7.11 -proof cases
    7.12 -  assume "?P \<noteq> {}"
    7.13 -  have [dest!]: "\<And>i. Suc (Max ?P) \<le> i \<Longrightarrow> f i = 0"
    7.14 -    using `finite ?P` `?P \<noteq> {}` by (auto simp: Suc_le_eq) 
    7.15 -  have "(\<Sum>i. f i) = (\<Sum>i<Suc (Max ?P). f i)"
    7.16 -    by (rule suminf_finite) auto
    7.17 -  also have "\<dots> = (\<Sum>i | f i \<noteq> 0. f i)"
    7.18 -    using `finite ?P` `?P \<noteq> {}`
    7.19 -    by (intro setsum_mono_zero_right) (auto simp: less_Suc_eq_le)
    7.20 -  finally show ?thesis .
    7.21 -qed simp
    7.22 -
    7.23  lemma suminf_cmult_indicator:
    7.24    fixes f :: "nat \<Rightarrow> ereal"
    7.25    assumes "disjoint_family A" "x \<in> A i" "\<And>i. 0 \<le> f i"
    7.26 @@ -246,7 +230,7 @@
    7.27      using disj by (auto simp: disjoint_family_on_def)
    7.28  
    7.29    from fin_not_0 have "(\<Sum>i. \<mu> (F i)) = (\<Sum>i | \<mu> (F i) \<noteq> 0. \<mu> (F i))"
    7.30 -    by (rule suminf_eq_setsum)
    7.31 +    by (rule suminf_finite) auto
    7.32    also have "\<dots> = (\<Sum>i | F i \<noteq> {}. \<mu> (F i))"
    7.33      using fin_not_empty F_subset by (rule setsum_mono_zero_left) auto
    7.34    also have "\<dots> = \<mu> (\<Union>i\<in>{i. F i \<noteq> {}}. F i)"
    7.35 @@ -791,6 +775,10 @@
    7.36    using Int_absorb1[OF sets_into_space, of N M]
    7.37    by (subst AE_iff_null) (auto simp: Int_def[symmetric])
    7.38  
    7.39 +lemma AE_not_in:
    7.40 +  "N \<in> null_sets M \<Longrightarrow> AE x in M. x \<notin> N"
    7.41 +  by (metis AE_iff_null_sets null_setsD2)
    7.42 +
    7.43  lemma AE_iff_measurable:
    7.44    "N \<in> sets M \<Longrightarrow> {x\<in>space M. \<not> P x} = N \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> emeasure M N = 0"
    7.45    using AE_iff_null[of _ P] by auto
    7.46 @@ -1357,7 +1345,7 @@
    7.47            with finite_F have "finite {i. ?M (F i) \<noteq> 0} "
    7.48              by (simp add: fin_eq)
    7.49            then have "(\<Sum>i. ?M (F i)) = (\<Sum>i | ?M (F i) \<noteq> 0. ?M (F i))"
    7.50 -            by (rule suminf_eq_setsum)
    7.51 +            by (rule suminf_finite) auto
    7.52            also have "\<dots> = ereal (\<Sum>i | F i \<noteq> {}. card (F i))"
    7.53              using finite_F by simp
    7.54            also have "\<dots> = ereal (card (\<Union>i \<in> {i. F i \<noteq> {}}. F i))"
     8.1 --- a/src/HOL/Series.thy	Wed Apr 25 17:15:10 2012 +0200
     8.2 +++ b/src/HOL/Series.thy	Wed Apr 25 19:26:00 2012 +0200
     8.3 @@ -120,6 +120,50 @@
     8.4    shows "f sums x \<longleftrightarrow> summable f \<and> (suminf f = x)"
     8.5    by (metis summable_sums sums_summable sums_unique)
     8.6  
     8.7 +lemma sums_finite:
     8.8 +  assumes [simp]: "finite N"
     8.9 +  assumes f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
    8.10 +  shows "f sums (\<Sum>n\<in>N. f n)"
    8.11 +proof -
    8.12 +  { fix n
    8.13 +    have "setsum f {..<n + Suc (Max N)} = setsum f N"
    8.14 +    proof cases
    8.15 +      assume "N = {}"
    8.16 +      with f have "f = (\<lambda>x. 0)" by auto
    8.17 +      then show ?thesis by simp
    8.18 +    next
    8.19 +      assume [simp]: "N \<noteq> {}"
    8.20 +      show ?thesis
    8.21 +      proof (safe intro!: setsum_mono_zero_right f)
    8.22 +        fix i assume "i \<in> N"
    8.23 +        then have "i \<le> Max N" by simp
    8.24 +        then show "i < n + Suc (Max N)" by simp
    8.25 +      qed
    8.26 +    qed }
    8.27 +  note eq = this
    8.28 +  show ?thesis unfolding sums_def
    8.29 +    by (rule LIMSEQ_offset[of _ "Suc (Max N)"])
    8.30 +       (simp add: eq atLeast0LessThan tendsto_const del: add_Suc_right)
    8.31 +qed
    8.32 +
    8.33 +lemma suminf_finite:
    8.34 +  fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add,t2_space}"
    8.35 +  assumes N: "finite N" and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
    8.36 +  shows "suminf f = (\<Sum>n\<in>N. f n)"
    8.37 +  using sums_finite[OF assms, THEN sums_unique] by simp
    8.38 +
    8.39 +lemma sums_If_finite_set:
    8.40 +  "finite A \<Longrightarrow> (\<lambda>r. if r \<in> A then f r else 0 :: 'a::{comm_monoid_add,t2_space}) sums (\<Sum>r\<in>A. f r)"
    8.41 +  using sums_finite[of A "(\<lambda>r. if r \<in> A then f r else 0)"] by simp
    8.42 +
    8.43 +lemma sums_If_finite:
    8.44 +  "finite {r. P r} \<Longrightarrow> (\<lambda>r. if P r then f r else 0 :: 'a::{comm_monoid_add,t2_space}) sums (\<Sum>r | P r. f r)"
    8.45 +  using sums_If_finite_set[of "{r. P r}" f] by simp
    8.46 +
    8.47 +lemma sums_single:
    8.48 +  "(\<lambda>r. if r = i then f r else 0::'a::{comm_monoid_add,t2_space}) sums f i"
    8.49 +  using sums_If_finite[of "\<lambda>r. r = i" f] by simp
    8.50 +
    8.51  lemma sums_split_initial_segment:
    8.52    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
    8.53    shows "f sums s ==> (\<lambda>n. f(n + k)) sums (s - (SUM i = 0..< k. f i))"