--- a/src/HOL/Probability/Central_Limit_Theorem.thy Tue Jun 21 10:53:43 2016 +0200
+++ b/src/HOL/Probability/Central_Limit_Theorem.thy Tue Jun 14 12:18:45 2016 +0200
@@ -1,5 +1,5 @@
-(* Theory: Central_Limit_Theorem.thy
- Authors: Jeremy Avigad, Luke Serafin
+(* Title: HOL/Probability/Central_Limit_Theorem.thy
+ Authors: Jeremy Avigad (CMU), Luke Serafin (CMU)
*)
section \<open>The Central Limit Theorem\<close>
@@ -73,20 +73,20 @@
using \<sigma>_pos by (simp add: power_divide)
also have "t^2 / n / 2 = (t^2 / 2) / n"
by simp
- finally have **: "norm (\<psi> n t - (1 + (-(t^2) / 2) / n)) \<le>
+ finally have **: "norm (\<psi> n t - (1 + (-(t^2) / 2) / n)) \<le>
?t\<^sup>2 / 6 * (LINT x|\<mu>. min (6 * x\<^sup>2) (\<bar>?t\<bar> * \<bar>x\<bar> ^ 3))" by simp
- have "norm (\<phi> n t - (complex_of_real (1 + (-(t^2) / 2) / n))^n) \<le>
+ have "norm (\<phi> n t - (complex_of_real (1 + (-(t^2) / 2) / n))^n) \<le>
n * norm (\<psi> n t - (complex_of_real (1 + (-(t^2) / 2) / n)))"
using n
by (auto intro!: norm_power_diff \<mu>.cmod_char_le_1 abs_leI
simp del: of_real_diff simp: of_real_diff[symmetric] divide_le_eq \<phi>_eq \<psi>_def)
also have "\<dots> \<le> n * (?t\<^sup>2 / 6 * (LINT x|\<mu>. min (6 * x\<^sup>2) (\<bar>?t\<bar> * \<bar>x\<bar> ^ 3)))"
by (rule mult_left_mono [OF **], simp)
- also have "\<dots> = (t\<^sup>2 / (6 * \<sigma>\<^sup>2) * (LINT x|\<mu>. min (6 * x\<^sup>2) (\<bar>?t\<bar> * \<bar>x\<bar> ^ 3)))"
+ also have "\<dots> = (t\<^sup>2 / (6 * \<sigma>\<^sup>2) * (LINT x|\<mu>. min (6 * x\<^sup>2) (\<bar>?t\<bar> * \<bar>x\<bar> ^ 3)))"
using \<sigma>_pos by (simp add: field_simps min_absorb2)
- finally show "norm (\<phi> n t - (1 + (-(t^2) / 2) / n)^n) \<le>
- (t\<^sup>2 / (6 * \<sigma>\<^sup>2) * (LINT x|\<mu>. min (6 * x\<^sup>2) (\<bar>?t\<bar> * \<bar>x\<bar> ^ 3)))"
+ finally show "norm (\<phi> n t - (1 + (-(t^2) / 2) / n)^n) \<le>
+ (t\<^sup>2 / (6 * \<sigma>\<^sup>2) * (LINT x|\<mu>. min (6 * x\<^sup>2) (\<bar>?t\<bar> * \<bar>x\<bar> ^ 3)))"
by simp
qed
@@ -95,7 +95,7 @@
fix t
let ?t = "\<lambda>n. t / sqrt (\<sigma>\<^sup>2 * n)"
have "\<And>x. (\<lambda>n. min (6 * x\<^sup>2) (\<bar>t\<bar> * \<bar>x\<bar> ^ 3 / \<bar>sqrt (\<sigma>\<^sup>2 * real n)\<bar>)) \<longlonglongrightarrow> 0"
- using \<sigma>_pos
+ using \<sigma>_pos
by (auto simp: real_sqrt_mult min_absorb2
intro!: tendsto_min[THEN tendsto_eq_rhs] sqrt_at_top[THEN filterlim_compose]
filterlim_tendsto_pos_mult_at_top filterlim_at_top_imp_at_infinity
--- a/src/HOL/Probability/Characteristic_Functions.thy Tue Jun 21 10:53:43 2016 +0200
+++ b/src/HOL/Probability/Characteristic_Functions.thy Tue Jun 14 12:18:45 2016 +0200
@@ -1,6 +1,5 @@
-(*
- Theory: Characteristic_Functions.thy
- Authors: Jeremy Avigad, Luke Serafin
+(* Title: Characteristic_Functions.thy
+ Authors: Jeremy Avigad (CMU), Luke Serafin (CMU), Johannes Hölzl (TUM)
*)
section \<open>Characteristic Functions\<close>
@@ -29,7 +28,7 @@
qed
qed
-lemma limseq_even_odd:
+lemma limseq_even_odd:
assumes "(\<lambda>n. f (2 * n)) \<longlonglongrightarrow> (l :: 'a :: topological_space)"
and "(\<lambda>n. f (2 * n + 1)) \<longlonglongrightarrow> l"
shows "f \<longlonglongrightarrow> l"
@@ -63,7 +62,7 @@
lemma (in real_distribution) char_zero: "char M 0 = 1"
unfolding char_def by (simp del: space_eq_univ add: prob_space)
-lemma (in prob_space) integrable_iexp:
+lemma (in prob_space) integrable_iexp:
assumes f: "f \<in> borel_measurable M" "\<And>x. Im (f x) = 0"
shows "integrable M (\<lambda>x. exp (ii * (f x)))"
proof (intro integrable_const_bound [of _ 1])
@@ -96,7 +95,7 @@
subsection \<open>Independence\<close>
-(* the automation can probably be improved *)
+(* the automation can probably be improved *)
lemma (in prob_space) char_distr_sum:
fixes X1 X2 :: "'a \<Rightarrow> real" and t :: real
assumes "indep_var borel X1 borel X2"
@@ -145,13 +144,13 @@
let ?F = "\<lambda>s. complex_of_real(-((x - s) ^ (Suc n) / (Suc n))) * iexp s"
have "x^(Suc n) / (Suc n) = (CLBINT s=0..x. (f s n * iexp s + (ii * iexp s) * -(f s (Suc n) / (Suc n))))" (is "?LHS = ?RHS")
proof -
- have "?RHS = (CLBINT s=0..x. (f s n * iexp s + (ii * iexp s) *
+ have "?RHS = (CLBINT s=0..x. (f s n * iexp s + (ii * iexp s) *
complex_of_real(-((x - s) ^ (Suc n) / (Suc n)))))"
by (cases "0 \<le> x") (auto intro!: simp: f_def[abs_def])
also have "... = ?F x - ?F 0"
unfolding zero_ereal_def using 1
by (intro interval_integral_FTC_finite)
- (auto simp: f_def add_nonneg_eq_0_iff complex_eq_iff
+ (auto simp: f_def add_nonneg_eq_0_iff complex_eq_iff
intro!: continuous_at_imp_continuous_on continuous_intros)
finally show ?thesis
by auto
@@ -184,7 +183,7 @@
lemma iexp_eq2:
fixes x :: real
- defines "f s m \<equiv> complex_of_real ((x - s) ^ m)"
+ defines "f s m \<equiv> complex_of_real ((x - s) ^ m)"
shows "iexp x = (\<Sum>k\<le>Suc n. (ii*x)^k/fact k) + ii^Suc n/fact n * (CLBINT s=0..x. f s n*(iexp s - 1))"
proof -
have isCont_f: "isCont (\<lambda>s. f s n) x" for n x
@@ -224,7 +223,7 @@
intro!: interval_integral_cong)
then show ?thesis by simp
next
- assume "\<not> (0 \<le> x \<or> even n)"
+ assume "\<not> (0 \<le> x \<or> even n)"
then have "(LBINT s=0..x. \<bar>(x - s)^n\<bar>) = LBINT s=0..x. -((x - s)^n)"
by (auto simp add: zero_ereal_def power_abs min_absorb1 max_absorb2
ereal_min[symmetric] ereal_max[symmetric] power_minus_odd[symmetric]
@@ -307,11 +306,11 @@
proof -
have integ_iexp: "integrable M (\<lambda>x. iexp (t * x))"
by (intro integrable_const_bound) auto
-
+
define c where [abs_def]: "c k x = (ii * t)^k / fact k * complex_of_real (x^k)" for k x
have integ_c: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. c k x)"
unfolding c_def by (intro integrable_mult_right integrable_of_real integrable_moments)
-
+
have "k \<le> n \<Longrightarrow> expectation (c k) = (\<i>*t) ^ k * (expectation (\<lambda>x. x ^ k)) / fact k" for k
unfolding c_def integral_mult_right_zero integral_complex_of_real by simp
then have "norm (char M t - ?t1) = norm (char M t - (CLINT x | M. (\<Sum>k \<le> n. c k x)))"
@@ -342,7 +341,7 @@
proof -
have integ_iexp: "integrable M (\<lambda>x. iexp (t * x))"
by (intro integrable_const_bound) auto
-
+
define c where [abs_def]: "c k x = (ii * t)^k / fact k * complex_of_real (x^k)" for k x
have integ_c: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. c k x)"
unfolding c_def by (intro integrable_mult_right integrable_of_real integrable_moments)
@@ -355,7 +354,7 @@
apply (simp_all add: field_simps abs_mult del: fact_Suc)
apply (simp_all add: field_simps)
done
-
+
have "k \<le> n \<Longrightarrow> expectation (c k) = (\<i>*t) ^ k * (expectation (\<lambda>x. x ^ k)) / fact k" for k
unfolding c_def integral_mult_right_zero integral_complex_of_real by simp
then have "norm (char M t - ?t1) = norm (char M t - (CLINT x | M. (\<Sum>k \<le> n. c k x)))"
@@ -399,9 +398,9 @@
proof -
note real_distribution.char_approx2 [of M 2 t, simplified]
have [simp]: "prob UNIV = 1" by (metis prob_space space_eq_univ)
- from integral_2 have [simp]: "expectation (\<lambda>x. x * x) = \<sigma>2"
+ from integral_2 have [simp]: "expectation (\<lambda>x. x * x) = \<sigma>2"
by (simp add: integral_1 numeral_eq_Suc)
- have 1: "k \<le> 2 \<Longrightarrow> integrable M (\<lambda>x. x^k)" for k
+ have 1: "k \<le> 2 \<Longrightarrow> integrable M (\<lambda>x. x^k)" for k
using assms by (auto simp: eval_nat_numeral le_Suc_eq)
note char_approx1
note 2 = char_approx1 [of 2 t, OF 1, simplified]
@@ -417,7 +416,7 @@
qed
text \<open>
- This is a more familiar textbook formulation in terms of random variables, but
+ This is a more familiar textbook formulation in terms of random variables, but
we will use the previous version for the CLT.
\<close>
--- a/src/HOL/Probability/Distribution_Functions.thy Tue Jun 21 10:53:43 2016 +0200
+++ b/src/HOL/Probability/Distribution_Functions.thy Tue Jun 14 12:18:45 2016 +0200
@@ -1,6 +1,5 @@
-(*
- Title : Distribution_Functions.thy
- Authors : Jeremy Avigad and Luke Serafin
+(* Title: Distribution_Functions.thy
+ Authors: Jeremy Avigad (CMU) and Luke Serafin (CMU)
*)
section \<open>Distribution Functions\<close>
--- a/src/HOL/Probability/Helly_Selection.thy Tue Jun 21 10:53:43 2016 +0200
+++ b/src/HOL/Probability/Helly_Selection.thy Tue Jun 14 12:18:45 2016 +0200
@@ -1,6 +1,6 @@
-(*
- Theory: Helly_Selection.thy
- Authors: Jeremy Avigad, Luke Serafin
+(* Title: HOL/Probability/Helly_Selection.thy
+ Authors: Jeremy Avigad (CMU), Luke Serafin (CMU)
+ Authors: Johannes Hölzl, TU München
*)
section \<open>Helly's selection theorem\<close>
@@ -36,7 +36,7 @@
fix n :: nat and s :: "nat \<Rightarrow> nat" assume s: "subseq s"
have "bounded {-M..M}"
using bounded_closed_interval by auto
- moreover have "\<And>k. f (s k) (r n) \<in> {-M..M}"
+ moreover have "\<And>k. f (s k) (r n) \<in> {-M..M}"
using bdd by (simp add: abs_le_iff minus_le_iff)
ultimately have "\<exists>l s'. subseq s' \<and> ((\<lambda>k. f (s k) (r n)) \<circ> s') \<longlonglongrightarrow> l"
using compact_Icc compact_imp_seq_compact seq_compactE by metis
--- a/src/HOL/Probability/Interval_Integral.thy Tue Jun 21 10:53:43 2016 +0200
+++ b/src/HOL/Probability/Interval_Integral.thy Tue Jun 14 12:18:45 2016 +0200
@@ -1,5 +1,5 @@
(* Title: HOL/Probability/Interval_Integral.thy
- Author: Jeremy Avigad, Johannes Hölzl, Luke Serafin
+ Author: Jeremy Avigad (CMU), Johannes Hölzl (TUM), Luke Serafin (CMU)
Lebesgue integral over an interval (with endpoints possibly +-\<infinity>)
*)
@@ -15,7 +15,7 @@
lemma has_vector_derivative_weaken:
fixes x D and f g s t
assumes f: "(f has_vector_derivative D) (at x within t)"
- and "x \<in> s" "s \<subseteq> t"
+ and "x \<in> s" "s \<subseteq> t"
and "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
shows "(g has_vector_derivative D) (at x within s)"
proof -
@@ -51,7 +51,7 @@
lemma borel_einterval[measurable]: "einterval a b \<in> sets borel"
unfolding einterval_def by measurable
-(*
+(*
Approximating a (possibly infinite) interval
*)
@@ -61,7 +61,7 @@
lemma ereal_incseq_approx:
fixes a b :: ereal
assumes "a < b"
- obtains X :: "nat \<Rightarrow> real" where
+ obtains X :: "nat \<Rightarrow> real" where
"incseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> b"
proof (cases b)
case PInf
@@ -104,7 +104,7 @@
lemma ereal_decseq_approx:
fixes a b :: ereal
assumes "a < b"
- obtains X :: "nat \<Rightarrow> real" where
+ obtains X :: "nat \<Rightarrow> real" where
"decseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> a"
proof -
have "-b < -a" using \<open>a < b\<close> by simp
@@ -120,7 +120,7 @@
lemma einterval_Icc_approximation:
fixes a b :: ereal
assumes "a < b"
- obtains u l :: "nat \<Rightarrow> real" where
+ obtains u l :: "nat \<Rightarrow> real" where
"einterval a b = (\<Union>i. {l i .. u i})"
"incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
"l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b"
@@ -134,7 +134,7 @@
fix x assume "a < ereal x" "ereal x < b"
have "eventually (\<lambda>i. ereal (l i) < ereal x) sequentially"
using l(4) \<open>a < ereal x\<close> by (rule order_tendstoD)
- moreover
+ moreover
have "eventually (\<lambda>i. ereal x < ereal (u i)) sequentially"
using u(4) \<open>ereal x< b\<close> by (rule order_tendstoD)
ultimately have "eventually (\<lambda>i. l i < x \<and> x < u i) sequentially"
@@ -142,7 +142,7 @@
then show "\<exists>i. l i \<le> x \<and> x \<le> u i"
by (auto intro: less_imp_le simp: eventually_sequentially)
next
- fix x i assume "l i \<le> x" "x \<le> u i"
+ fix x i assume "l i \<le> x" "x \<le> u i"
with \<open>a < ereal (l i)\<close> \<open>ereal (u i) < b\<close>
show "a < ereal x" "ereal x < b"
by (auto simp del: ereal_less_eq(3) simp add: ereal_less_eq(3)[symmetric])
@@ -151,7 +151,7 @@
by (intro that) fact+
qed
-(* TODO: in this definition, it would be more natural if einterval a b included a and b when
+(* TODO: in this definition, it would be more natural if einterval a b included a and b when
they are real. *)
definition interval_lebesgue_integral :: "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> 'a::{banach, second_countable_topology}" where
"interval_lebesgue_integral M a b f =
@@ -203,23 +203,23 @@
by (simp add: *)
qed
-lemma interval_lebesgue_integral_add [intro, simp]:
- fixes M a b f
+lemma interval_lebesgue_integral_add [intro, simp]:
+ fixes M a b f
assumes "interval_lebesgue_integrable M a b f" "interval_lebesgue_integrable M a b g"
- shows "interval_lebesgue_integrable M a b (\<lambda>x. f x + g x)" and
- "interval_lebesgue_integral M a b (\<lambda>x. f x + g x) =
+ shows "interval_lebesgue_integrable M a b (\<lambda>x. f x + g x)" and
+ "interval_lebesgue_integral M a b (\<lambda>x. f x + g x) =
interval_lebesgue_integral M a b f + interval_lebesgue_integral M a b g"
-using assms by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def
+using assms by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def
field_simps)
-lemma interval_lebesgue_integral_diff [intro, simp]:
- fixes M a b f
+lemma interval_lebesgue_integral_diff [intro, simp]:
+ fixes M a b f
assumes "interval_lebesgue_integrable M a b f"
"interval_lebesgue_integrable M a b g"
- shows "interval_lebesgue_integrable M a b (\<lambda>x. f x - g x)" and
- "interval_lebesgue_integral M a b (\<lambda>x. f x - g x) =
+ shows "interval_lebesgue_integrable M a b (\<lambda>x. f x - g x)" and
+ "interval_lebesgue_integral M a b (\<lambda>x. f x - g x) =
interval_lebesgue_integral M a b f - interval_lebesgue_integral M a b g"
-using assms by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def
+using assms by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def
field_simps)
lemma interval_lebesgue_integrable_mult_right [intro, simp]:
@@ -268,13 +268,13 @@
unfolding interval_lebesgue_integral_def
by (auto simp add: interval_lebesgue_integral_def set_integral_complex_of_real)
-lemma interval_lebesgue_integral_le_eq:
+lemma interval_lebesgue_integral_le_eq:
fixes a b f
assumes "a \<le> b"
shows "interval_lebesgue_integral M a b f = (LINT x : einterval a b | M. f x)"
using assms by (auto simp add: interval_lebesgue_integral_def)
-lemma interval_lebesgue_integral_gt_eq:
+lemma interval_lebesgue_integral_gt_eq:
fixes a b f
assumes "a > b"
shows "interval_lebesgue_integral M a b f = -(LINT x : einterval b a | M. f x)"
@@ -318,13 +318,13 @@
lemma interval_lebesgue_integral_0_infty:
"interval_lebesgue_integrable M 0 \<infinity> f \<longleftrightarrow> set_integrable M {0<..} f"
"interval_lebesgue_integral M 0 \<infinity> f = (LINT x:{0<..}|M. f x)"
- unfolding zero_ereal_def
+ unfolding zero_ereal_def
by (auto simp: interval_lebesgue_integral_le_eq interval_lebesgue_integrable_def)
lemma interval_integral_to_infinity_eq: "(LINT x=ereal a..\<infinity> | M. f x) = (LINT x : {a<..} | M. f x)"
unfolding interval_lebesgue_integral_def by auto
-lemma interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a \<infinity> f) =
+lemma interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a \<infinity> f) =
(set_integrable M {a<..} f)"
unfolding interval_lebesgue_integrable_def by auto
@@ -334,14 +334,14 @@
lemma interval_integral_zero [simp]:
fixes a b :: ereal
- shows"LBINT x=a..b. 0 = 0"
-unfolding interval_lebesgue_integral_def einterval_eq
+ shows"LBINT x=a..b. 0 = 0"
+unfolding interval_lebesgue_integral_def einterval_eq
by simp
lemma interval_integral_const [intro, simp]:
fixes a b c :: real
- shows "interval_lebesgue_integrable lborel a b (\<lambda>x. c)" and "LBINT x=a..b. c = c * (b - a)"
-unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq
+ shows "interval_lebesgue_integrable lborel a b (\<lambda>x. c)" and "LBINT x=a..b. c = c * (b - a)"
+unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq
by (auto simp add: less_imp_le field_simps measure_def)
lemma interval_integral_cong_AE:
@@ -359,7 +359,7 @@
qed
lemma interval_integral_cong:
- assumes "\<And>x. x \<in> einterval (min a b) (max a b) \<Longrightarrow> f x = g x"
+ assumes "\<And>x. x \<in> einterval (min a b) (max a b) \<Longrightarrow> f x = g x"
shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
using assms
proof (induct a b rule: linorder_wlog)
@@ -434,9 +434,9 @@
apply (auto simp: eq anti_eq einterval_iff split: split_indicator)
done
-lemma interval_integral_sum:
+lemma interval_integral_sum:
fixes a b c :: ereal
- assumes integrable: "interval_lebesgue_integrable lborel (min a (min b c)) (max a (max b c)) f"
+ assumes integrable: "interval_lebesgue_integrable lborel (min a (min b c)) (max a (max b c)) f"
shows "(LBINT x=a..b. f x) + (LBINT x=b..c. f x) = (LBINT x=a..c. f x)"
proof -
let ?I = "\<lambda>a b. LBINT x=a..b. f x"
@@ -487,16 +487,16 @@
using assms unfolding interval_lebesgue_integrable_def apply simp
by (rule set_integrable_subset, rule borel_integrable_atLeastAtMost' [of a b], auto)
-lemma interval_integral_eq_integral:
+lemma interval_integral_eq_integral:
fixes f :: "real \<Rightarrow> 'a::euclidean_space"
shows "a \<le> b \<Longrightarrow> set_integrable lborel {a..b} f \<Longrightarrow> LBINT x=a..b. f x = integral {a..b} f"
by (subst interval_integral_Icc, simp) (rule set_borel_integral_eq_integral)
-lemma interval_integral_eq_integral':
+lemma interval_integral_eq_integral':
fixes f :: "real \<Rightarrow> 'a::euclidean_space"
shows "a \<le> b \<Longrightarrow> set_integrable lborel (einterval a b) f \<Longrightarrow> LBINT x=a..b. f x = integral (einterval a b) f"
by (subst interval_lebesgue_integral_le_eq, simp) (rule set_borel_integral_eq_integral)
-
+
(*
General limit approximation arguments
*)
@@ -513,7 +513,7 @@
assumes f_nonneg: "AE x in lborel. a < ereal x \<longrightarrow> ereal x < b \<longrightarrow> 0 \<le> f x"
assumes f_measurable: "set_borel_measurable lborel (einterval a b) f"
assumes lbint_lim: "(\<lambda>i. LBINT x=l i.. u i. f x) \<longlonglongrightarrow> C"
- shows
+ shows
"set_integrable lborel (einterval a b) f"
"(LBINT x=a..b. f x) = C"
proof -
@@ -551,7 +551,7 @@
also have "... = C" by (rule integral_monotone_convergence [OF 1 2 3 4 5])
finally show "(LBINT x=a..b. f x) = C" .
- show "set_integrable lborel (einterval a b) f"
+ show "set_integrable lborel (einterval a b) f"
by (rule integrable_monotone_convergence[OF 1 2 3 4 5])
qed
@@ -578,7 +578,7 @@
show "AE x in lborel. (\<lambda>i. indicator {l i..u i} x *\<^sub>R f x) \<longlonglongrightarrow> indicator (einterval a b) x *\<^sub>R f x"
proof (intro AE_I2 tendsto_intros Lim_eventually)
fix x
- { fix i assume "l i \<le> x" "x \<le> u i"
+ { fix i assume "l i \<le> x" "x \<le> u i"
with \<open>incseq u\<close>[THEN incseqD, of i] \<open>decseq l\<close>[THEN decseqD, of i]
have "eventually (\<lambda>i. l i \<le> x \<and> x \<le> u i) sequentially"
by (auto simp: eventually_sequentially decseq_def incseq_def intro: order_trans) }
@@ -592,7 +592,7 @@
qed
(*
- A slightly stronger version of integral_FTC_atLeastAtMost and related facts,
+ A slightly stronger version of integral_FTC_atLeastAtMost and related facts,
with continuous_on instead of isCont
TODO: make the older versions corollaries of these (using continuous_at_imp_continuous_on, etc.)
@@ -615,8 +615,8 @@
lemma interval_integral_FTC_finite:
fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: real
assumes f: "continuous_on {min a b..max a b} f"
- assumes F: "\<And>x. min a b \<le> x \<Longrightarrow> x \<le> max a b \<Longrightarrow> (F has_vector_derivative (f x)) (at x within
- {min a b..max a b})"
+ assumes F: "\<And>x. min a b \<le> x \<Longrightarrow> x \<le> max a b \<Longrightarrow> (F has_vector_derivative (f x)) (at x within
+ {min a b..max a b})"
shows "(LBINT x=a..b. f x) = F b - F a"
apply (case_tac "a \<le> b")
apply (subst interval_integral_Icc, simp)
@@ -632,13 +632,13 @@
lemma interval_integral_FTC_nonneg:
fixes f F :: "real \<Rightarrow> real" and a b :: ereal
assumes "a < b"
- assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV F x :> f x"
- assumes f: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f x"
+ assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV F x :> f x"
+ assumes f: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f x"
assumes f_nonneg: "AE x in lborel. a < ereal x \<longrightarrow> ereal x < b \<longrightarrow> 0 \<le> f x"
assumes A: "((F \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)"
assumes B: "((F \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)"
shows
- "set_integrable lborel (einterval a b) f"
+ "set_integrable lborel (einterval a b) f"
"(LBINT x=a..b. f x) = B - A"
proof -
from einterval_Icc_approximation[OF \<open>a < b\<close>] guess u l . note approx = this
@@ -660,7 +660,7 @@
(auto simp del: ereal_less_eq simp add: ereal_less_eq(3)[symmetric])
qed
have 2: "set_borel_measurable lborel (einterval a b) f"
- by (auto simp del: real_scaleR_def intro!: set_borel_measurable_continuous
+ by (auto simp del: real_scaleR_def intro!: set_borel_measurable_continuous
simp: continuous_on_eq_continuous_at einterval_iff f)
have 3: "(\<lambda>i. LBINT x=l i..u i. f x) \<longlonglongrightarrow> B - A"
apply (subst FTCi)
@@ -672,15 +672,15 @@
by (elim allE[of _ "\<lambda>i. ereal (l i)"], auto)
show "(LBINT x=a..b. f x) = B - A"
by (rule interval_integral_Icc_approx_nonneg [OF \<open>a < b\<close> approx 1 f_nonneg 2 3])
- show "set_integrable lborel (einterval a b) f"
+ show "set_integrable lborel (einterval a b) f"
by (rule interval_integral_Icc_approx_nonneg [OF \<open>a < b\<close> approx 1 f_nonneg 2 3])
qed
lemma interval_integral_FTC_integrable:
fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: ereal
assumes "a < b"
- assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> (F has_vector_derivative f x) (at x)"
- assumes f: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f x"
+ assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> (F has_vector_derivative f x) (at x)"
+ assumes f: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f x"
assumes f_integrable: "set_integrable lborel (einterval a b) f"
assumes A: "((F \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)"
assumes B: "((F \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)"
@@ -709,7 +709,7 @@
by (elim LIMSEQ_unique)
qed
-(*
+(*
The second Fundamental Theorem of Calculus and existence of antiderivatives on an
einterval.
*)
@@ -746,12 +746,12 @@
qed (insert assms, auto)
qed
-lemma einterval_antiderivative:
+lemma einterval_antiderivative:
fixes a b :: ereal and f :: "real \<Rightarrow> 'a::euclidean_space"
assumes "a < b" and contf: "\<And>x :: real. a < x \<Longrightarrow> x < b \<Longrightarrow> isCont f x"
shows "\<exists>F. \<forall>x :: real. a < x \<longrightarrow> x < b \<longrightarrow> (F has_vector_derivative f x) (at x)"
proof -
- from einterval_nonempty [OF \<open>a < b\<close>] obtain c :: real where [simp]: "a < c" "c < b"
+ from einterval_nonempty [OF \<open>a < b\<close>] obtain c :: real where [simp]: "a < c" "c < b"
by (auto simp add: einterval_def)
let ?F = "(\<lambda>u. LBINT y=c..u. f y)"
show ?thesis
@@ -759,10 +759,10 @@
fix x :: real
assume [simp]: "a < x" "x < b"
have 1: "a < min c x" by simp
- from einterval_nonempty [OF 1] obtain d :: real where [simp]: "a < d" "d < c" "d < x"
+ from einterval_nonempty [OF 1] obtain d :: real where [simp]: "a < d" "d < c" "d < x"
by (auto simp add: einterval_def)
have 2: "max c x < b" by simp
- from einterval_nonempty [OF 2] obtain e :: real where [simp]: "c < e" "x < e" "e < b"
+ from einterval_nonempty [OF 2] obtain e :: real where [simp]: "c < e" "x < e" "e < b"
by (auto simp add: einterval_def)
show "(?F has_vector_derivative f x) (at x)"
(* TODO: factor out the next three lines to has_field_derivative_within_open *)
@@ -785,7 +785,7 @@
Once again, three versions: first, for finite intervals, and then two versions for
arbitrary intervals.
*)
-
+
lemma interval_integral_substitution_finite:
fixes a b :: real and f :: "real \<Rightarrow> 'a::euclidean_space"
assumes "a \<le> b"
@@ -798,7 +798,7 @@
using derivg unfolding has_field_derivative_iff_has_vector_derivative .
then have contg [simp]: "continuous_on {a..b} g"
by (rule continuous_on_vector_derivative) auto
- have 1: "\<And>u. min (g a) (g b) \<le> u \<Longrightarrow> u \<le> max (g a) (g b) \<Longrightarrow>
+ have 1: "\<And>u. min (g a) (g b) \<le> u \<Longrightarrow> u \<le> max (g a) (g b) \<Longrightarrow>
\<exists>x\<in>{a..b}. u = g x"
apply (case_tac "g a \<le> g b")
apply (auto simp add: min_def max_def less_imp_le)
@@ -814,7 +814,7 @@
apply (rule continuous_on_subset [OF contf])
using g_im by auto
then guess F ..
- then have derivF: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow>
+ then have derivF: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow>
(F has_vector_derivative (f (g x))) (at (g x) within (g ` {a..b}))" by auto
have contf2: "continuous_on {min (g a) (g b)..max (g a) (g b)} f"
apply (rule continuous_on_subset [OF contf])
@@ -842,7 +842,7 @@
lemma interval_integral_substitution_integrable:
fixes f :: "real \<Rightarrow> 'a::euclidean_space" and a b u v :: ereal
- assumes "a < b"
+ assumes "a < b"
and deriv_g: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV g x :> g' x"
and contf: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f (g x)"
and contg': "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont g' x"
@@ -859,10 +859,10 @@
by (rule order_less_le_trans, rule approx, force)
have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
- have [simp]: "\<And>i. l i < b"
- apply (rule order_less_trans) prefer 2
+ have [simp]: "\<And>i. l i < b"
+ apply (rule order_less_trans) prefer 2
by (rule approx, auto, rule approx)
- have [simp]: "\<And>i. a < u i"
+ have [simp]: "\<And>i. a < u i"
by (rule order_less_trans, rule approx, auto, rule approx)
have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx)
have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx)
@@ -875,7 +875,7 @@
apply (rule less_imp_le, erule order_less_le_trans, auto)
by (rule less_imp_le, rule le_less_trans, subst ereal_less_eq(3), assumption, auto)
have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
- proof -
+ proof -
have A2: "(\<lambda>i. g (l i)) \<longlonglongrightarrow> A"
using A apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
@@ -891,7 +891,7 @@
apply (rule order_trans [OF _ B3 [of 0]])
by auto
{ fix x :: real
- assume "A < x" and "x < B"
+ assume "A < x" and "x < B"
then have "eventually (\<lambda>i. ereal (g (l i)) < x \<and> x < ereal (g (u i))) sequentially"
apply (intro eventually_conj order_tendstoD)
by (rule A2, assumption, rule B2, assumption)
@@ -903,7 +903,7 @@
apply (erule (1) AB)
apply (rule order_le_less_trans, rule A3, simp)
apply (rule order_less_le_trans) prefer 2
- by (rule B3, simp)
+ by (rule B3, simp)
qed
(* finally, the main argument *)
{
@@ -942,7 +942,7 @@
lemma interval_integral_substitution_nonneg:
fixes f g g':: "real \<Rightarrow> real" and a b u v :: ereal
- assumes "a < b"
+ assumes "a < b"
and deriv_g: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV g x :> g' x"
and contf: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f (g x)"
and contg': "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont g' x"
@@ -951,7 +951,7 @@
and A: "((ereal \<circ> g \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)"
and B: "((ereal \<circ> g \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)"
and integrable_fg: "set_integrable lborel (einterval a b) (\<lambda>x. f (g x) * g' x)"
- shows
+ shows
"set_integrable lborel (einterval A B) f"
"(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))"
proof -
@@ -961,10 +961,10 @@
by (rule order_less_le_trans, rule approx, force)
have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
- have [simp]: "\<And>i. l i < b"
- apply (rule order_less_trans) prefer 2
+ have [simp]: "\<And>i. l i < b"
+ apply (rule order_less_trans) prefer 2
by (rule approx, auto, rule approx)
- have [simp]: "\<And>i. a < u i"
+ have [simp]: "\<And>i. a < u i"
by (rule order_less_trans, rule approx, auto, rule approx)
have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx)
have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx)
@@ -977,7 +977,7 @@
apply (rule less_imp_le, erule order_less_le_trans, auto)
by (rule less_imp_le, rule le_less_trans, subst ereal_less_eq(3), assumption, auto)
have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
- proof -
+ proof -
have A2: "(\<lambda>i. g (l i)) \<longlonglongrightarrow> A"
using A apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
@@ -993,7 +993,7 @@
apply (rule order_trans [OF _ B3 [of 0]])
by auto
{ fix x :: real
- assume "A < x" and "x < B"
+ assume "A < x" and "x < B"
then have "eventually (\<lambda>i. ereal (g (l i)) < x \<and> x < ereal (g (u i))) sequentially"
apply (intro eventually_conj order_tendstoD)
by (rule A2, assumption, rule B2, assumption)
@@ -1005,7 +1005,7 @@
apply (erule (1) AB)
apply (rule order_le_less_trans, rule A3, simp)
apply (rule order_less_le_trans) prefer 2
- by (rule B3, simp)
+ by (rule B3, simp)
qed
(* finally, the main argument *)
{
@@ -1031,7 +1031,7 @@
apply (rule g_nondec, auto)
by (erule order_less_le_trans, rule g_nondec, auto)
have img: "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> \<exists>c \<ge> l i. c \<le> u i \<and> x = g c"
- apply (frule (1) IVT' [of g], auto)
+ apply (frule (1) IVT' [of g], auto)
apply (rule continuous_at_imp_continuous_on, auto)
by (rule DERIV_isCont, rule deriv_g, auto)
have nonneg_f2: "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> 0 \<le> f x"
@@ -1076,11 +1076,11 @@
translations
"CLBINT x:A. f" == "CONST complex_set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
-abbreviation complex_interval_lebesgue_integral ::
+abbreviation complex_interval_lebesgue_integral ::
"real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> complex" where
"complex_interval_lebesgue_integral M a b f \<equiv> interval_lebesgue_integral M a b f"
-abbreviation complex_interval_lebesgue_integrable ::
+abbreviation complex_interval_lebesgue_integrable ::
"real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> bool" where
"complex_interval_lebesgue_integrable M a b f \<equiv> interval_lebesgue_integrable M a b f"
@@ -1099,14 +1099,14 @@
by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def)
lemma interval_integral_norm2:
- "interval_lebesgue_integrable lborel a b f \<Longrightarrow>
+ "interval_lebesgue_integrable lborel a b f \<Longrightarrow>
norm (LBINT t=a..b. f t) \<le> \<bar>LBINT t=a..b. norm (f t)\<bar>"
proof (induct a b rule: linorder_wlog)
case (sym a b) then show ?case
by (simp add: interval_integral_endpoints_reverse[of a b] interval_integrable_endpoints_reverse[of a b])
next
- case (le a b)
- then have "\<bar>LBINT t=a..b. norm (f t)\<bar> = LBINT t=a..b. norm (f t)"
+ case (le a b)
+ then have "\<bar>LBINT t=a..b. norm (f t)\<bar> = LBINT t=a..b. norm (f t)"
using integrable_norm[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"]
by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def
intro!: integral_nonneg_AE abs_of_nonneg)
--- a/src/HOL/Probability/Levy.thy Tue Jun 21 10:53:43 2016 +0200
+++ b/src/HOL/Probability/Levy.thy Tue Jun 14 12:18:45 2016 +0200
@@ -1,5 +1,5 @@
-(* Theory: Levy.thy
- Author: Jeremy Avigad
+(* Title: HOL/Probability/Levy.thy
+ Authors: Jeremy Avigad (CMU)
*)
section \<open>The Levy inversion theorem, and the Levy continuity theorem.\<close>
--- a/src/HOL/Probability/Radon_Nikodym.thy Tue Jun 21 10:53:43 2016 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy Tue Jun 14 12:18:45 2016 +0200
@@ -8,8 +8,9 @@
imports Bochner_Integration
begin
-definition "diff_measure M N =
- measure_of (space M) (sets M) (\<lambda>A. emeasure M A - emeasure N A)"
+definition diff_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
+where
+ "diff_measure M N = measure_of (space M) (sets M) (\<lambda>A. emeasure M A - emeasure N A)"
lemma
shows space_diff_measure[simp]: "space (diff_measure M N) = space M"
@@ -36,7 +37,7 @@
(\<Sum>i. emeasure M (A i)) - (\<Sum>i. emeasure N (A i))"
using fin pos[of "A _"]
by (intro ennreal_suminf_minus)
- (auto simp: sets_eq finite_measure.emeasure_eq_measure suminf_emeasure measure_nonneg)
+ (auto simp: sets_eq finite_measure.emeasure_eq_measure suminf_emeasure)
then show "(\<Sum>i. emeasure M (A i) - emeasure N (A i)) =
emeasure M (\<Union>i. A i) - emeasure N (\<Union>i. A i) "
by (simp add: suminf)
@@ -53,6 +54,8 @@
disjoint: "disjoint_family A"
using sigma_finite_disjoint by blast
let ?B = "\<lambda>i. 2^Suc i * emeasure M (A i)"
+ have [measurable]: "\<And>i. A i \<in> sets M"
+ using range by fastforce+
have "\<forall>i. \<exists>x. 0 < x \<and> x < inverse (?B i)"
proof
fix i show "\<exists>x. 0 < x \<and> x < inverse (?B i)"
@@ -65,9 +68,7 @@
let ?h = "\<lambda>x. \<Sum>i. n i * indicator (A i) x"
show ?thesis
proof (safe intro!: bexI[of _ ?h] del: notI)
- have "\<And>i. A i \<in> sets M"
- using range by fastforce+
- then have "integral\<^sup>N M ?h = (\<Sum>i. n i * emeasure M (A i))" using pos
+ have "integral\<^sup>N M ?h = (\<Sum>i. n i * emeasure M (A i))" using pos
by (simp add: nn_integral_suminf nn_integral_cmult_indicator)
also have "\<dots> \<le> (\<Sum>i. ennreal ((1/2)^Suc i))"
proof (intro suminf_le allI)
@@ -81,10 +82,8 @@
del: power_Suc)
also have "\<dots> \<le> inverse (ennreal 2) ^ Suc N"
using measure[of N]
- apply (cases "emeasure M (A N)" rule: ennreal_cases)
- apply (cases "emeasure M (A N) = 0")
- apply (auto simp: inverse_ennreal ennreal_mult[symmetric] divide_ennreal_def simp del: power_Suc)
- done
+ by (cases "emeasure M (A N)"; cases "emeasure M (A N) = 0")
+ (auto simp: inverse_ennreal ennreal_mult[symmetric] divide_ennreal_def simp del: power_Suc)
also have "\<dots> = ennreal (inverse 2 ^ Suc N)"
by (subst ennreal_power[symmetric], simp) (simp add: inverse_ennreal)
finally show "n N * emeasure M (A N) \<le> ennreal ((1/2)^Suc N)"
@@ -92,11 +91,8 @@
qed auto
also have "\<dots> < top"
unfolding less_top[symmetric]
- apply (rule ennreal_suminf_neq_top)
- apply (subst summable_Suc_iff)
- apply (subst summable_geometric)
- apply auto
- done
+ by (rule ennreal_suminf_neq_top)
+ (auto simp: summable_geometric summable_Suc_iff simp del: power_Suc)
finally show "integral\<^sup>N M ?h \<noteq> \<infinity>"
by (auto simp: top_unique)
next
@@ -214,7 +210,7 @@
by (auto simp add: not_less)
{ fix n have "?d (A n) \<le> - real n * e"
proof (induct n)
- case (Suc n) with dA_epsilon[of n, OF B] show ?case by (simp del: A_simps add: of_nat_Suc field_simps)
+ case (Suc n) with dA_epsilon[of n, OF B] show ?case by (simp del: A_simps add: field_simps)
next
case 0 with measure_empty show ?case by (simp add: zero_ennreal_def)
qed } note dA_less = this
@@ -236,8 +232,7 @@
lemma (in finite_measure) Radon_Nikodym_aux:
assumes "finite_measure N" and sets_eq: "sets N = sets M"
- shows "\<exists>A\<in>sets M. measure M (space M) - measure N (space M) \<le>
- measure M A - measure N A \<and>
+ shows "\<exists>A\<in>sets M. measure M (space M) - measure N (space M) \<le> measure M A - measure N A \<and>
(\<forall>B\<in>sets M. B \<subseteq> A \<longrightarrow> 0 \<le> measure M B - measure N B)"
proof -
interpret N: finite_measure N by fact
@@ -293,24 +288,20 @@
lemma (in finite_measure) Radon_Nikodym_finite_measure:
assumes "finite_measure N" and sets_eq: "sets N = sets M"
assumes "absolutely_continuous M N"
- shows "\<exists>f \<in> borel_measurable M. (\<forall>x. 0 \<le> f x) \<and> density M f = N"
+ shows "\<exists>f \<in> borel_measurable M. density M f = N"
proof -
interpret N: finite_measure N by fact
- define G where "G =
- {g \<in> borel_measurable M. (\<forall>x. 0 \<le> g x) \<and> (\<forall>A\<in>sets M. (\<integral>\<^sup>+x. g x * indicator A x \<partial>M) \<le> N A)}"
+ define G where "G = {g \<in> borel_measurable M. \<forall>A\<in>sets M. (\<integral>\<^sup>+x. g x * indicator A x \<partial>M) \<le> N A}"
{ fix f have "f \<in> G \<Longrightarrow> f \<in> borel_measurable M" by (auto simp: G_def) }
note this[measurable_dest]
have "(\<lambda>x. 0) \<in> G" unfolding G_def by auto
hence "G \<noteq> {}" by auto
- { fix f g assume f: "f \<in> G" and g: "g \<in> G"
+ { fix f g assume f[measurable]: "f \<in> G" and g[measurable]: "g \<in> G"
have "(\<lambda>x. max (g x) (f x)) \<in> G" (is "?max \<in> G") unfolding G_def
proof safe
- show "?max \<in> borel_measurable M" using f g unfolding G_def by auto
let ?A = "{x \<in> space M. f x \<le> g x}"
have "?A \<in> sets M" using f g unfolding G_def by auto
- fix A assume "A \<in> sets M"
- hence sets: "?A \<inter> A \<in> sets M" "(space M - ?A) \<inter> A \<in> sets M" using \<open>?A \<in> sets M\<close> by auto
- hence sets': "?A \<inter> A \<in> sets N" "(space M - ?A) \<inter> A \<in> sets N" by (auto simp: sets_eq)
+ fix A assume [measurable]: "A \<in> sets M"
have union: "((?A \<inter> A) \<union> ((space M - ?A) \<inter> A)) = A"
using sets.sets_into_space[OF \<open>A \<in> sets M\<close>] by auto
have "\<And>x. x \<in> space M \<Longrightarrow> max (g x) (f x) * indicator A x =
@@ -319,24 +310,19 @@
hence "(\<integral>\<^sup>+x. max (g x) (f x) * indicator A x \<partial>M) =
(\<integral>\<^sup>+x. g x * indicator (?A \<inter> A) x \<partial>M) +
(\<integral>\<^sup>+x. f x * indicator ((space M - ?A) \<inter> A) x \<partial>M)"
- using f g sets unfolding G_def
by (auto cong: nn_integral_cong intro!: nn_integral_add)
also have "\<dots> \<le> N (?A \<inter> A) + N ((space M - ?A) \<inter> A)"
- using f g sets unfolding G_def by (auto intro!: add_mono)
+ using f g unfolding G_def by (auto intro!: add_mono)
also have "\<dots> = N A"
- using plus_emeasure[OF sets'] union by auto
+ using union by (subst plus_emeasure) (auto simp: sets_eq)
finally show "(\<integral>\<^sup>+x. max (g x) (f x) * indicator A x \<partial>M) \<le> N A" .
- next
- fix x show "0 \<le> max (g x) (f x)" using f g by (auto simp: G_def split: split_max)
- qed }
+ qed auto }
note max_in_G = this
{ fix f assume "incseq f" and f: "\<And>i. f i \<in> G"
then have [measurable]: "\<And>i. f i \<in> borel_measurable M" by (auto simp: G_def)
have "(\<lambda>x. SUP i. f i x) \<in> G" unfolding G_def
proof safe
show "(\<lambda>x. SUP i. f i x) \<in> borel_measurable M" by measurable
- { fix x show "0 \<le> (SUP i. f i x)"
- using f by (auto simp: G_def intro: SUP_upper2) }
next
fix A assume "A \<in> sets M"
have "(\<integral>\<^sup>+x. (SUP i. f i x) * indicator A x \<partial>M) =
@@ -394,9 +380,6 @@
by (auto intro!: SUP_mono nn_integral_mono Max_ge)
qed
finally have int_f_eq_y: "integral\<^sup>N M f = ?y" .
- have "\<And>x. 0 \<le> f x"
- unfolding f_def using \<open>\<And>i. gs i \<in> G\<close>
- by (auto intro!: SUP_upper2 Max_ge_iff[THEN iffD2] simp: G_def)
let ?t = "\<lambda>A. N A - (\<integral>\<^sup>+x. ?F A x \<partial>M)"
let ?M = "diff_measure N (density M f)"
have f_le_N: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>\<^sup>+x. ?F A x \<partial>M) \<le> N A"
@@ -445,9 +428,9 @@
using M'.finite_emeasure_space by (auto simp: top_unique)
moreover
define b where "b = ?M (space M) / emeasure M (space M) / 2"
- ultimately have b: "b \<noteq> 0 \<and> 0 \<le> b \<and> b \<noteq> \<infinity>"
+ ultimately have b: "b \<noteq> 0 \<and> b \<noteq> \<infinity>"
by (auto simp: ennreal_divide_eq_top_iff)
- then have b: "b \<noteq> 0" "0 \<le> b" "0 < b" "b \<noteq> \<infinity>"
+ then have b: "b \<noteq> 0" "0 < b" "b \<noteq> \<infinity>"
by (auto simp: less_le)
let ?Mb = "density M (\<lambda>_. b)"
have Mb: "finite_measure ?Mb" "sets ?Mb = sets ?M"
@@ -460,7 +443,7 @@
{ fix B assume B: "B \<in> sets M" "B \<subseteq> A0"
with *[OF this] have "b * emeasure M B \<le> ?M B"
using b unfolding M'.emeasure_eq_measure emeasure_eq_measure
- by (cases b rule: ennreal_cases) (auto simp: ennreal_mult[symmetric] measure_nonneg) }
+ by (cases b rule: ennreal_cases) (auto simp: ennreal_mult[symmetric]) }
note bM_le_t = this
let ?f0 = "\<lambda>x. f x + b * indicator A0 x"
{ fix A assume A: "A \<in> sets M"
@@ -487,7 +470,7 @@
unfolding emeasure_M[OF \<open>A \<in> sets M\<close>]
using f_le_v N.emeasure_eq_measure[of A]
by (cases "\<integral>\<^sup>+x. ?F A x \<partial>M" "N A" rule: ennreal2_cases)
- (auto simp: top_unique measure_nonneg ennreal_minus ennreal_plus[symmetric] simp del: ennreal_plus)
+ (auto simp: top_unique ennreal_minus ennreal_plus[symmetric] simp del: ennreal_plus)
finally have "(\<integral>\<^sup>+x. ?f0 x * indicator A x \<partial>M) \<le> N A" . }
hence "?f0 \<in> G" using \<open>A0 \<in> sets M\<close> b \<open>f \<in> G\<close> by (auto simp: G_def)
have int_f_finite: "integral\<^sup>N M f \<noteq> \<infinity>"
@@ -501,7 +484,7 @@
by simp
with b have "?M A0 \<noteq> 0"
by (cases b rule: ennreal_cases)
- (auto simp: M'.emeasure_eq_measure measure_nonneg mult_less_0_iff not_le[symmetric])
+ (auto simp: M'.emeasure_eq_measure mult_less_0_iff not_le[symmetric])
then have "emeasure M A0 \<noteq> 0"
using ac \<open>A0 \<in> sets M\<close> by (auto simp: absolutely_continuous_def null_sets_def)
then have "0 < emeasure M A0"
@@ -661,7 +644,7 @@
lemma (in finite_measure) Radon_Nikodym_finite_measure_infinite:
assumes "absolutely_continuous M N" and sets_eq: "sets N = sets M"
- shows "\<exists>f\<in>borel_measurable M. (\<forall>x. 0 \<le> f x) \<and> density M f = N"
+ shows "\<exists>f\<in>borel_measurable M. density M f = N"
proof -
from split_space_into_finite_sets_and_rest[OF assms]
obtain Q0 and Q :: "nat \<Rightarrow> 'a set"
@@ -671,7 +654,7 @@
and Q_fin: "\<And>i. N (Q i) \<noteq> \<infinity>" by force
from Q have Q_sets: "\<And>i. Q i \<in> sets M" by auto
let ?N = "\<lambda>i. density N (indicator (Q i))" and ?M = "\<lambda>i. density M (indicator (Q i))"
- have "\<forall>i. \<exists>f\<in>borel_measurable (?M i). (\<forall>x. 0 \<le> f x) \<and> density (?M i) f = ?N i"
+ have "\<forall>i. \<exists>f\<in>borel_measurable (?M i). density (?M i) f = ?N i"
proof (intro allI finite_measure.Radon_Nikodym_finite_measure)
fix i
from Q show "finite_measure (?M i)"
@@ -705,7 +688,6 @@
proof (safe intro!: bexI[of _ ?f])
show "?f \<in> borel_measurable M" using Q0 borel Q_sets
by (auto intro!: measurable_If)
- show "\<And>x. 0 \<le> ?f x" using borel by (auto intro!: suminf_0_le simp: indicator_def)
show "density M ?f = N"
proof (rule measure_eqI)
fix A assume "A \<in> sets (density M ?f)"
@@ -745,7 +727,7 @@
lemma (in sigma_finite_measure) Radon_Nikodym:
assumes ac: "absolutely_continuous M N" assumes sets_eq: "sets N = sets M"
- shows "\<exists>f \<in> borel_measurable M. (\<forall>x. 0 \<le> f x) \<and> density M f = N"
+ shows "\<exists>f \<in> borel_measurable M. density M f = N"
proof -
from Ex_finite_integrable_function
obtain h where finite: "integral\<^sup>N M h \<noteq> \<infinity>" and
@@ -770,7 +752,7 @@
by (auto simp: absolutely_continuous_def)
qed (auto simp add: sets_eq)
from T.Radon_Nikodym_finite_measure_infinite[OF this]
- obtain f where f_borel: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x" "density ?MT f = N" by auto
+ obtain f where f_borel: "f \<in> borel_measurable M" "density ?MT f = N" by auto
with nn borel show ?thesis
by (auto intro!: bexI[of _ "\<lambda>x. h x * f x"] simp: density_density_eq)
qed
--- a/src/HOL/Probability/Set_Integral.thy Tue Jun 21 10:53:43 2016 +0200
+++ b/src/HOL/Probability/Set_Integral.thy Tue Jun 14 12:18:45 2016 +0200
@@ -1,5 +1,5 @@
(* Title: HOL/Probability/Set_Integral.thy
- Author: Jeremy Avigad, Johannes Hölzl, Luke Serafin
+ Author: Jeremy Avigad (CMU), Johannes Hölzl (TUM), Luke Serafin (CMU)
Notation and useful facts for working with integrals over a set.
--- a/src/HOL/Probability/Sinc_Integral.thy Tue Jun 21 10:53:43 2016 +0200
+++ b/src/HOL/Probability/Sinc_Integral.thy Tue Jun 14 12:18:45 2016 +0200
@@ -1,6 +1,6 @@
-(*
- Theory: Sinc_Integral.thy
- Authors: Jeremy Avigad, Luke Serafin, Johannes Hölzl
+(* Title: HOL/Probability/Sinc_Integral.thy
+ Authors: Jeremy Avigad (CMU), Luke Serafin (CMU)
+ Authors: Johannes Hölzl, TU München
*)
section \<open>Integral of sinc\<close>
--- a/src/HOL/Probability/Weak_Convergence.thy Tue Jun 21 10:53:43 2016 +0200
+++ b/src/HOL/Probability/Weak_Convergence.thy Tue Jun 14 12:18:45 2016 +0200
@@ -1,6 +1,5 @@
-(*
- Theory: Weak_Convergence.thy
- Authors: Jeremy Avigad, Luke Serafin
+(* Title: HOL/Probability/Weak_Convergence.thy
+ Authors: Jeremy Avigad (CMU), Johannes Hölzl (TUM)
*)
section \<open>Weak Convergence of Functions and Distributions\<close>