# HG changeset patch # User hoelzl # Date 1450721306 -3600 # Node ID bc0fc54990851e6cb42f1b97d28fa35d4b391ff6 # Parent f833208ff7c1ef9e806a3579fefd676d5df69695 Bochner integral: prove dominated convergence at_top diff -r f833208ff7c1 -r bc0fc5499085 src/HOL/Probability/Bochner_Integration.thy --- a/src/HOL/Probability/Bochner_Integration.thy Mon Dec 21 23:24:05 2015 +0100 +++ b/src/HOL/Probability/Bochner_Integration.thy Mon Dec 21 19:08:26 2015 +0100 @@ -1520,6 +1520,56 @@ show "(\i. integral\<^sup>L M (s i)) ----> integral\<^sup>L M f" by simp qed +context + fixes s :: "real \ 'a \ 'b::{banach, second_countable_topology}" and w :: "'a \ real" + and f :: "'a \ 'b" and M + assumes "f \ borel_measurable M" "\t. s t \ borel_measurable M" "integrable M w" + assumes lim: "AE x in M. ((\i. s i x) ---> f x) at_top" + assumes bound: "\\<^sub>F i in at_top. AE x in M. norm (s i x) \ w x" +begin + +lemma integral_dominated_convergence_at_top: "((\t. integral\<^sup>L M (s t)) ---> integral\<^sup>L M f) at_top" +proof (rule tendsto_at_topI_sequentially) + fix X :: "nat \ real" assume X: "filterlim X at_top sequentially" + from filterlim_iff[THEN iffD1, OF this, rule_format, OF bound] + obtain N where w: "\n. N \ n \ AE x in M. norm (s (X n) x) \ w x" + by (auto simp: eventually_sequentially) + + show "(\n. integral\<^sup>L M (s (X n))) ----> integral\<^sup>L M f" + proof (rule LIMSEQ_offset, rule integral_dominated_convergence) + show "AE x in M. norm (s (X (n + N)) x) \ w x" for n + by (rule w) auto + show "AE x in M. (\n. s (X (n + N)) x) ----> f x" + using lim + proof eventually_elim + fix x assume "((\i. s i x) ---> f x) at_top" + then show "(\n. s (X (n + N)) x) ----> f x" + by (intro LIMSEQ_ignore_initial_segment filterlim_compose[OF _ X]) + qed + qed fact+ +qed + +lemma integrable_dominated_convergence_at_top: "integrable M f" +proof - + from bound obtain N where w: "\n. N \ n \ AE x in M. norm (s n x) \ w x" + by (auto simp: eventually_at_top_linorder) + show ?thesis + proof (rule integrable_dominated_convergence) + show "AE x in M. norm (s (N + i) x) \ w x" for i :: nat + by (intro w) auto + show "AE x in M. (\i. s (N + real i) x) ----> f x" + using lim + proof eventually_elim + fix x assume "((\i. s i x) ---> f x) at_top" + then show "(\n. s (N + n) x) ----> f x" + by (rule filterlim_compose) + (auto intro!: filterlim_tendsto_add_at_top filterlim_real_sequentially) + qed + qed fact+ +qed + +end + lemma integrable_mult_left_iff: fixes f :: "'a \ real" shows "integrable M (\x. c * f x) \ c = 0 \ integrable M f" diff -r f833208ff7c1 -r bc0fc5499085 src/HOL/Probability/Interval_Integral.thy --- a/src/HOL/Probability/Interval_Integral.thy Mon Dec 21 23:24:05 2015 +0100 +++ b/src/HOL/Probability/Interval_Integral.thy Mon Dec 21 19:08:26 2015 +0100 @@ -302,6 +302,19 @@ split: split_indicator) qed +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 + 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) = + (set_integrable M {a<..} f)" + unfolding interval_lebesgue_integrable_def by auto + (* Basic properties of integration over an interval wrt lebesgue measure. *)