author hoelzl Wed Apr 25 19:26:00 2012 +0200 (2012-04-25) changeset 47761 dfe747e72fa8 parent 47760 b9840d8fca43 child 47762 d31085f07f60
moved lemmas to appropriate places
```     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.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.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.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.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.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))"
```