# HG changeset patch # User hoelzl # Date 1465899525 -7200 # Node ID 6b26c378ab35f5fc67d915afd2c6db4c947854b4 # Parent 7a8515c58271f8ae383bc8474426fe2ed470f2f3 Probability: tuned headers; cleanup Radon_Nikodym diff -r 7a8515c58271 -r 6b26c378ab35 src/HOL/Probability/Central_Limit_Theorem.thy --- 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 \The Central Limit Theorem\ @@ -73,20 +73,20 @@ using \_pos by (simp add: power_divide) also have "t^2 / n / 2 = (t^2 / 2) / n" by simp - finally have **: "norm (\ n t - (1 + (-(t^2) / 2) / n)) \ + finally have **: "norm (\ n t - (1 + (-(t^2) / 2) / n)) \ ?t\<^sup>2 / 6 * (LINT x|\. min (6 * x\<^sup>2) (\?t\ * \x\ ^ 3))" by simp - have "norm (\ n t - (complex_of_real (1 + (-(t^2) / 2) / n))^n) \ + have "norm (\ n t - (complex_of_real (1 + (-(t^2) / 2) / n))^n) \ n * norm (\ n t - (complex_of_real (1 + (-(t^2) / 2) / n)))" using n by (auto intro!: norm_power_diff \.cmod_char_le_1 abs_leI simp del: of_real_diff simp: of_real_diff[symmetric] divide_le_eq \_eq \_def) also have "\ \ n * (?t\<^sup>2 / 6 * (LINT x|\. min (6 * x\<^sup>2) (\?t\ * \x\ ^ 3)))" by (rule mult_left_mono [OF **], simp) - also have "\ = (t\<^sup>2 / (6 * \\<^sup>2) * (LINT x|\. min (6 * x\<^sup>2) (\?t\ * \x\ ^ 3)))" + also have "\ = (t\<^sup>2 / (6 * \\<^sup>2) * (LINT x|\. min (6 * x\<^sup>2) (\?t\ * \x\ ^ 3)))" using \_pos by (simp add: field_simps min_absorb2) - finally show "norm (\ n t - (1 + (-(t^2) / 2) / n)^n) \ - (t\<^sup>2 / (6 * \\<^sup>2) * (LINT x|\. min (6 * x\<^sup>2) (\?t\ * \x\ ^ 3)))" + finally show "norm (\ n t - (1 + (-(t^2) / 2) / n)^n) \ + (t\<^sup>2 / (6 * \\<^sup>2) * (LINT x|\. min (6 * x\<^sup>2) (\?t\ * \x\ ^ 3)))" by simp qed @@ -95,7 +95,7 @@ fix t let ?t = "\n. t / sqrt (\\<^sup>2 * n)" have "\x. (\n. min (6 * x\<^sup>2) (\t\ * \x\ ^ 3 / \sqrt (\\<^sup>2 * real n)\)) \ 0" - using \_pos + using \_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 diff -r 7a8515c58271 -r 6b26c378ab35 src/HOL/Probability/Characteristic_Functions.thy --- 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 \Characteristic Functions\ @@ -29,7 +28,7 @@ qed qed -lemma limseq_even_odd: +lemma limseq_even_odd: assumes "(\n. f (2 * n)) \ (l :: 'a :: topological_space)" and "(\n. f (2 * n + 1)) \ l" shows "f \ 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 \ borel_measurable M" "\x. Im (f x) = 0" shows "integrable M (\x. exp (ii * (f x)))" proof (intro integrable_const_bound [of _ 1]) @@ -96,7 +95,7 @@ subsection \Independence\ -(* the automation can probably be improved *) +(* the automation can probably be improved *) lemma (in prob_space) char_distr_sum: fixes X1 X2 :: "'a \ real" and t :: real assumes "indep_var borel X1 borel X2" @@ -145,13 +144,13 @@ let ?F = "\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 \ 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 \ complex_of_real ((x - s) ^ m)" + defines "f s m \ complex_of_real ((x - s) ^ m)" shows "iexp x = (\k\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 (\s. f s n) x" for n x @@ -224,7 +223,7 @@ intro!: interval_integral_cong) then show ?thesis by simp next - assume "\ (0 \ x \ even n)" + assume "\ (0 \ x \ even n)" then have "(LBINT s=0..x. \(x - s)^n\) = 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 (\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: "\k. k \ n \ integrable M (\x. c k x)" unfolding c_def by (intro integrable_mult_right integrable_of_real integrable_moments) - + have "k \ n \ expectation (c k) = (\*t) ^ k * (expectation (\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. (\k \ n. c k x)))" @@ -342,7 +341,7 @@ proof - have integ_iexp: "integrable M (\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: "\k. k \ n \ integrable M (\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 \ n \ expectation (c k) = (\*t) ^ k * (expectation (\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. (\k \ 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 (\x. x * x) = \2" + from integral_2 have [simp]: "expectation (\x. x * x) = \2" by (simp add: integral_1 numeral_eq_Suc) - have 1: "k \ 2 \ integrable M (\x. x^k)" for k + have 1: "k \ 2 \ integrable M (\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 \ - 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. \ diff -r 7a8515c58271 -r 6b26c378ab35 src/HOL/Probability/Distribution_Functions.thy --- 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 \Distribution Functions\ diff -r 7a8515c58271 -r 6b26c378ab35 src/HOL/Probability/Helly_Selection.thy --- 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 \Helly's selection theorem\ @@ -36,7 +36,7 @@ fix n :: nat and s :: "nat \ nat" assume s: "subseq s" have "bounded {-M..M}" using bounded_closed_interval by auto - moreover have "\k. f (s k) (r n) \ {-M..M}" + moreover have "\k. f (s k) (r n) \ {-M..M}" using bdd by (simp add: abs_le_iff minus_le_iff) ultimately have "\l s'. subseq s' \ ((\k. f (s k) (r n)) \ s') \ l" using compact_Icc compact_imp_seq_compact seq_compactE by metis diff -r 7a8515c58271 -r 6b26c378ab35 src/HOL/Probability/Interval_Integral.thy --- 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 +-\) *) @@ -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 \ s" "s \ t" + and "x \ s" "s \ t" and "\x. x \ s \ 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 \ 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 \ real" where + obtains X :: "nat \ real" where "incseq X" "\i. a < X i" "\i. X i < b" "X \ b" proof (cases b) case PInf @@ -104,7 +104,7 @@ lemma ereal_decseq_approx: fixes a b :: ereal assumes "a < b" - obtains X :: "nat \ real" where + obtains X :: "nat \ real" where "decseq X" "\i. a < X i" "\i. X i < b" "X \ a" proof - have "-b < -a" using \a < b\ by simp @@ -120,7 +120,7 @@ lemma einterval_Icc_approximation: fixes a b :: ereal assumes "a < b" - obtains u l :: "nat \ real" where + obtains u l :: "nat \ real" where "einterval a b = (\i. {l i .. u i})" "incseq u" "decseq l" "\i. l i < u i" "\i. a < l i" "\i. u i < b" "l \ a" "u \ b" @@ -134,7 +134,7 @@ fix x assume "a < ereal x" "ereal x < b" have "eventually (\i. ereal (l i) < ereal x) sequentially" using l(4) \a < ereal x\ by (rule order_tendstoD) - moreover + moreover have "eventually (\i. ereal x < ereal (u i)) sequentially" using u(4) \ereal x< b\ by (rule order_tendstoD) ultimately have "eventually (\i. l i < x \ x < u i) sequentially" @@ -142,7 +142,7 @@ then show "\i. l i \ x \ x \ u i" by (auto intro: less_imp_le simp: eventually_sequentially) next - fix x i assume "l i \ x" "x \ u i" + fix x i assume "l i \ x" "x \ u i" with \a < ereal (l i)\ \ereal (u i) < b\ 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 \ ereal \ ereal \ (real \ 'a) \ '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 (\x. f x + g x)" and - "interval_lebesgue_integral M a b (\x. f x + g x) = + shows "interval_lebesgue_integrable M a b (\x. f x + g x)" and + "interval_lebesgue_integral M a b (\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 (\x. f x - g x)" and - "interval_lebesgue_integral M a b (\x. f x - g x) = + shows "interval_lebesgue_integrable M a b (\x. f x - g x)" and + "interval_lebesgue_integral M a b (\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 \ 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 \ f \ set_integrable M {0<..} f" "interval_lebesgue_integral M 0 \ 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..\ | 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 \ f) = +lemma interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a \ 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 (\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 (\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 "\x. x \ einterval (min a b) (max a b) \ f x = g x" + assumes "\x. x \ einterval (min a b) (max a b) \ 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 = "\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 \ 'a::euclidean_space" shows "a \ b \ set_integrable lborel {a..b} f \ 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 \ 'a::euclidean_space" shows "a \ b \ set_integrable lborel (einterval a b) f \ 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 \ ereal x < b \ 0 \ f x" assumes f_measurable: "set_borel_measurable lborel (einterval a b) f" assumes lbint_lim: "(\i. LBINT x=l i.. u i. f x) \ 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. (\i. indicator {l i..u i} x *\<^sub>R f x) \ indicator (einterval a b) x *\<^sub>R f x" proof (intro AE_I2 tendsto_intros Lim_eventually) fix x - { fix i assume "l i \ x" "x \ u i" + { fix i assume "l i \ x" "x \ u i" with \incseq u\[THEN incseqD, of i] \decseq l\[THEN decseqD, of i] have "eventually (\i. l i \ x \ x \ 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 \ 'a::euclidean_space" and a b :: real assumes f: "continuous_on {min a b..max a b} f" - assumes F: "\x. min a b \ x \ x \ max a b \ (F has_vector_derivative (f x)) (at x within - {min a b..max a b})" + assumes F: "\x. min a b \ x \ x \ max a b \ (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 \ b") apply (subst interval_integral_Icc, simp) @@ -632,13 +632,13 @@ lemma interval_integral_FTC_nonneg: fixes f F :: "real \ real" and a b :: ereal assumes "a < b" - assumes F: "\x. a < ereal x \ ereal x < b \ DERIV F x :> f x" - assumes f: "\x. a < ereal x \ ereal x < b \ isCont f x" + assumes F: "\x. a < ereal x \ ereal x < b \ DERIV F x :> f x" + assumes f: "\x. a < ereal x \ ereal x < b \ isCont f x" assumes f_nonneg: "AE x in lborel. a < ereal x \ ereal x < b \ 0 \ f x" assumes A: "((F \ real_of_ereal) \ A) (at_right a)" assumes B: "((F \ real_of_ereal) \ 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 \a < b\] 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: "(\i. LBINT x=l i..u i. f x) \ B - A" apply (subst FTCi) @@ -672,15 +672,15 @@ by (elim allE[of _ "\i. ereal (l i)"], auto) show "(LBINT x=a..b. f x) = B - A" by (rule interval_integral_Icc_approx_nonneg [OF \a < b\ 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 \a < b\ approx 1 f_nonneg 2 3]) qed lemma interval_integral_FTC_integrable: fixes f F :: "real \ 'a::euclidean_space" and a b :: ereal assumes "a < b" - assumes F: "\x. a < ereal x \ ereal x < b \ (F has_vector_derivative f x) (at x)" - assumes f: "\x. a < ereal x \ ereal x < b \ isCont f x" + assumes F: "\x. a < ereal x \ ereal x < b \ (F has_vector_derivative f x) (at x)" + assumes f: "\x. a < ereal x \ ereal x < b \ isCont f x" assumes f_integrable: "set_integrable lborel (einterval a b) f" assumes A: "((F \ real_of_ereal) \ A) (at_right a)" assumes B: "((F \ real_of_ereal) \ 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 \ 'a::euclidean_space" assumes "a < b" and contf: "\x :: real. a < x \ x < b \ isCont f x" shows "\F. \x :: real. a < x \ x < b \ (F has_vector_derivative f x) (at x)" proof - - from einterval_nonempty [OF \a < b\] obtain c :: real where [simp]: "a < c" "c < b" + from einterval_nonempty [OF \a < b\] obtain c :: real where [simp]: "a < c" "c < b" by (auto simp add: einterval_def) let ?F = "(\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 \ 'a::euclidean_space" assumes "a \ 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: "\u. min (g a) (g b) \ u \ u \ max (g a) (g b) \ + have 1: "\u. min (g a) (g b) \ u \ u \ max (g a) (g b) \ \x\{a..b}. u = g x" apply (case_tac "g a \ 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: "\x. a \ x \ x \ b \ + then have derivF: "\x. a \ x \ x \ b \ (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 \ 'a::euclidean_space" and a b u v :: ereal - assumes "a < b" + assumes "a < b" and deriv_g: "\x. a < ereal x \ ereal x < b \ DERIV g x :> g' x" and contf: "\x. a < ereal x \ ereal x < b \ isCont f (g x)" and contg': "\x. a < ereal x \ ereal x < b \ isCont g' x" @@ -859,10 +859,10 @@ by (rule order_less_le_trans, rule approx, force) have [simp]: "\x i. x \ u i \ ereal x < b" by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx) - have [simp]: "\i. l i < b" - apply (rule order_less_trans) prefer 2 + have [simp]: "\i. l i < b" + apply (rule order_less_trans) prefer 2 by (rule approx, auto, rule approx) - have [simp]: "\i. a < u i" + have [simp]: "\i. a < u i" by (rule order_less_trans, rule approx, auto, rule approx) have [simp]: "\i j. i \ j \ l j \ l i" by (rule decseqD, rule approx) have [simp]: "\i j. i \ j \ u i \ 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 \ B" and un: "einterval A B = (\i. {g(l i)<..i. g (l i)) \ A" using A apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def) by (drule_tac x = "\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 (\i. ereal (g (l i)) < x \ 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 \ real" and a b u v :: ereal - assumes "a < b" + assumes "a < b" and deriv_g: "\x. a < ereal x \ ereal x < b \ DERIV g x :> g' x" and contf: "\x. a < ereal x \ ereal x < b \ isCont f (g x)" and contg': "\x. a < ereal x \ ereal x < b \ isCont g' x" @@ -951,7 +951,7 @@ and A: "((ereal \ g \ real_of_ereal) \ A) (at_right a)" and B: "((ereal \ g \ real_of_ereal) \ B) (at_left b)" and integrable_fg: "set_integrable lborel (einterval a b) (\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]: "\x i. x \ u i \ ereal x < b" by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx) - have [simp]: "\i. l i < b" - apply (rule order_less_trans) prefer 2 + have [simp]: "\i. l i < b" + apply (rule order_less_trans) prefer 2 by (rule approx, auto, rule approx) - have [simp]: "\i. a < u i" + have [simp]: "\i. a < u i" by (rule order_less_trans, rule approx, auto, rule approx) have [simp]: "\i j. i \ j \ l j \ l i" by (rule decseqD, rule approx) have [simp]: "\i j. i \ j \ u i \ 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 \ B" and un: "einterval A B = (\i. {g(l i)<..i. g (l i)) \ A" using A apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def) by (drule_tac x = "\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 (\i. ereal (g (l i)) < x \ 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: "\x i. g (l i) \ x \ x \ g (u i) \ \c \ l i. c \ u i \ 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: "\x i. g (l i) \ x \ x \ g (u i) \ 0 \ f x" @@ -1076,11 +1076,11 @@ translations "CLBINT x:A. f" == "CONST complex_set_lebesgue_integral CONST lborel A (\x. f)" -abbreviation complex_interval_lebesgue_integral :: +abbreviation complex_interval_lebesgue_integral :: "real measure \ ereal \ ereal \ (real \ complex) \ complex" where "complex_interval_lebesgue_integral M a b f \ interval_lebesgue_integral M a b f" -abbreviation complex_interval_lebesgue_integrable :: +abbreviation complex_interval_lebesgue_integrable :: "real measure \ ereal \ ereal \ (real \ complex) \ bool" where "complex_interval_lebesgue_integrable M a b f \ 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 \ + "interval_lebesgue_integrable lborel a b f \ norm (LBINT t=a..b. f t) \ \LBINT t=a..b. norm (f t)\" 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 "\LBINT t=a..b. norm (f t)\ = LBINT t=a..b. norm (f t)" + case (le a b) + then have "\LBINT t=a..b. norm (f t)\ = LBINT t=a..b. norm (f t)" using integrable_norm[of lborel "\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) diff -r 7a8515c58271 -r 6b26c378ab35 src/HOL/Probability/Levy.thy --- 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 \The Levy inversion theorem, and the Levy continuity theorem.\ diff -r 7a8515c58271 -r 6b26c378ab35 src/HOL/Probability/Radon_Nikodym.thy --- 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) (\A. emeasure M A - emeasure N A)" +definition diff_measure :: "'a measure \ 'a measure \ 'a measure" +where + "diff_measure M N = measure_of (space M) (sets M) (\A. emeasure M A - emeasure N A)" lemma shows space_diff_measure[simp]: "space (diff_measure M N) = space M" @@ -36,7 +37,7 @@ (\i. emeasure M (A i)) - (\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 "(\i. emeasure M (A i) - emeasure N (A i)) = emeasure M (\i. A i) - emeasure N (\i. A i) " by (simp add: suminf) @@ -53,6 +54,8 @@ disjoint: "disjoint_family A" using sigma_finite_disjoint by blast let ?B = "\i. 2^Suc i * emeasure M (A i)" + have [measurable]: "\i. A i \ sets M" + using range by fastforce+ have "\i. \x. 0 < x \ x < inverse (?B i)" proof fix i show "\x. 0 < x \ x < inverse (?B i)" @@ -65,9 +68,7 @@ let ?h = "\x. \i. n i * indicator (A i) x" show ?thesis proof (safe intro!: bexI[of _ ?h] del: notI) - have "\i. A i \ sets M" - using range by fastforce+ - then have "integral\<^sup>N M ?h = (\i. n i * emeasure M (A i))" using pos + have "integral\<^sup>N M ?h = (\i. n i * emeasure M (A i))" using pos by (simp add: nn_integral_suminf nn_integral_cmult_indicator) also have "\ \ (\i. ennreal ((1/2)^Suc i))" proof (intro suminf_le allI) @@ -81,10 +82,8 @@ del: power_Suc) also have "\ \ 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 "\ = ennreal (inverse 2 ^ Suc N)" by (subst ennreal_power[symmetric], simp) (simp add: inverse_ennreal) finally show "n N * emeasure M (A N) \ ennreal ((1/2)^Suc N)" @@ -92,11 +91,8 @@ qed auto also have "\ < 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 \ \" by (auto simp: top_unique) next @@ -214,7 +210,7 @@ by (auto simp add: not_less) { fix n have "?d (A n) \ - 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 "\A\sets M. measure M (space M) - measure N (space M) \ - measure M A - measure N A \ + shows "\A\sets M. measure M (space M) - measure N (space M) \ measure M A - measure N A \ (\B\sets M. B \ A \ 0 \ 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 "\f \ borel_measurable M. (\x. 0 \ f x) \ density M f = N" + shows "\f \ borel_measurable M. density M f = N" proof - interpret N: finite_measure N by fact - define G where "G = - {g \ borel_measurable M. (\x. 0 \ g x) \ (\A\sets M. (\\<^sup>+x. g x * indicator A x \M) \ N A)}" + define G where "G = {g \ borel_measurable M. \A\sets M. (\\<^sup>+x. g x * indicator A x \M) \ N A}" { fix f have "f \ G \ f \ borel_measurable M" by (auto simp: G_def) } note this[measurable_dest] have "(\x. 0) \ G" unfolding G_def by auto hence "G \ {}" by auto - { fix f g assume f: "f \ G" and g: "g \ G" + { fix f g assume f[measurable]: "f \ G" and g[measurable]: "g \ G" have "(\x. max (g x) (f x)) \ G" (is "?max \ G") unfolding G_def proof safe - show "?max \ borel_measurable M" using f g unfolding G_def by auto let ?A = "{x \ space M. f x \ g x}" have "?A \ sets M" using f g unfolding G_def by auto - fix A assume "A \ sets M" - hence sets: "?A \ A \ sets M" "(space M - ?A) \ A \ sets M" using \?A \ sets M\ by auto - hence sets': "?A \ A \ sets N" "(space M - ?A) \ A \ sets N" by (auto simp: sets_eq) + fix A assume [measurable]: "A \ sets M" have union: "((?A \ A) \ ((space M - ?A) \ A)) = A" using sets.sets_into_space[OF \A \ sets M\] by auto have "\x. x \ space M \ max (g x) (f x) * indicator A x = @@ -319,24 +310,19 @@ hence "(\\<^sup>+x. max (g x) (f x) * indicator A x \M) = (\\<^sup>+x. g x * indicator (?A \ A) x \M) + (\\<^sup>+x. f x * indicator ((space M - ?A) \ A) x \M)" - using f g sets unfolding G_def by (auto cong: nn_integral_cong intro!: nn_integral_add) also have "\ \ N (?A \ A) + N ((space M - ?A) \ 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 "\ = N A" - using plus_emeasure[OF sets'] union by auto + using union by (subst plus_emeasure) (auto simp: sets_eq) finally show "(\\<^sup>+x. max (g x) (f x) * indicator A x \M) \ N A" . - next - fix x show "0 \ 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: "\i. f i \ G" then have [measurable]: "\i. f i \ borel_measurable M" by (auto simp: G_def) have "(\x. SUP i. f i x) \ G" unfolding G_def proof safe show "(\x. SUP i. f i x) \ borel_measurable M" by measurable - { fix x show "0 \ (SUP i. f i x)" - using f by (auto simp: G_def intro: SUP_upper2) } next fix A assume "A \ sets M" have "(\\<^sup>+x. (SUP i. f i x) * indicator A x \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 "\x. 0 \ f x" - unfolding f_def using \\i. gs i \ G\ - by (auto intro!: SUP_upper2 Max_ge_iff[THEN iffD2] simp: G_def) let ?t = "\A. N A - (\\<^sup>+x. ?F A x \M)" let ?M = "diff_measure N (density M f)" have f_le_N: "\A. A \ sets M \ (\\<^sup>+x. ?F A x \M) \ 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 \ 0 \ 0 \ b \ b \ \" + ultimately have b: "b \ 0 \ b \ \" by (auto simp: ennreal_divide_eq_top_iff) - then have b: "b \ 0" "0 \ b" "0 < b" "b \ \" + then have b: "b \ 0" "0 < b" "b \ \" by (auto simp: less_le) let ?Mb = "density M (\_. b)" have Mb: "finite_measure ?Mb" "sets ?Mb = sets ?M" @@ -460,7 +443,7 @@ { fix B assume B: "B \ sets M" "B \ A0" with *[OF this] have "b * emeasure M B \ ?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 = "\x. f x + b * indicator A0 x" { fix A assume A: "A \ sets M" @@ -487,7 +470,7 @@ unfolding emeasure_M[OF \A \ sets M\] using f_le_v N.emeasure_eq_measure[of A] by (cases "\\<^sup>+x. ?F A x \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 "(\\<^sup>+x. ?f0 x * indicator A x \M) \ N A" . } hence "?f0 \ G" using \A0 \ sets M\ b \f \ G\ by (auto simp: G_def) have int_f_finite: "integral\<^sup>N M f \ \" @@ -501,7 +484,7 @@ by simp with b have "?M A0 \ 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 \ 0" using ac \A0 \ sets M\ 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 "\f\borel_measurable M. (\x. 0 \ f x) \ density M f = N" + shows "\f\borel_measurable M. density M f = N" proof - from split_space_into_finite_sets_and_rest[OF assms] obtain Q0 and Q :: "nat \ 'a set" @@ -671,7 +654,7 @@ and Q_fin: "\i. N (Q i) \ \" by force from Q have Q_sets: "\i. Q i \ sets M" by auto let ?N = "\i. density N (indicator (Q i))" and ?M = "\i. density M (indicator (Q i))" - have "\i. \f\borel_measurable (?M i). (\x. 0 \ f x) \ density (?M i) f = ?N i" + have "\i. \f\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 \ borel_measurable M" using Q0 borel Q_sets by (auto intro!: measurable_If) - show "\x. 0 \ ?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 \ 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 "\f \ borel_measurable M. (\x. 0 \ f x) \ density M f = N" + shows "\f \ borel_measurable M. density M f = N" proof - from Ex_finite_integrable_function obtain h where finite: "integral\<^sup>N M h \ \" 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 \ borel_measurable M" "\x. 0 \ f x" "density ?MT f = N" by auto + obtain f where f_borel: "f \ borel_measurable M" "density ?MT f = N" by auto with nn borel show ?thesis by (auto intro!: bexI[of _ "\x. h x * f x"] simp: density_density_eq) qed diff -r 7a8515c58271 -r 6b26c378ab35 src/HOL/Probability/Set_Integral.thy --- 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. diff -r 7a8515c58271 -r 6b26c378ab35 src/HOL/Probability/Sinc_Integral.thy --- 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 \Integral of sinc\ diff -r 7a8515c58271 -r 6b26c378ab35 src/HOL/Probability/Weak_Convergence.thy --- 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 \Weak Convergence of Functions and Distributions\