# HG changeset patch # User nipkow # Date 1535035519 -7200 # Node ID 63e84bd8e1f68f1ef32b15ca3cc61f76db6a183e # Parent 462226db648aef8aa75267f5d034f60d6bf02a6e moved lemma from AFP diff -r 462226db648a -r 63e84bd8e1f6 src/HOL/Analysis/Bochner_Integration.thy --- a/src/HOL/Analysis/Bochner_Integration.thy Thu Aug 23 14:49:36 2018 +0200 +++ b/src/HOL/Analysis/Bochner_Integration.thy Thu Aug 23 16:45:19 2018 +0200 @@ -2026,6 +2026,14 @@ ultimately show "integrable M (\x. Min {f i x |i. i = j \ i \ F})" by simp qed +lemma integrable_MIN: + fixes f:: "_ \ _ \ real" + assumes "finite I" "I \ {}" + "\i. i \ I \ integrable M (f i)" + shows "integrable M (\x. MIN i\I. f i x)" +using integrable_Min[of I M f, OF assms] +by(simp add: Setcompr_eq_image) + lemma integrable_Max: fixes f:: "_ \ _ \ real" assumes "finite I" "I \ {}" @@ -2043,6 +2051,14 @@ ultimately show "integrable M (\x. Max {f i x |i. i = j \ i \ F})" by simp qed +lemma integrable_MAX: + fixes f:: "_ \ _ \ real" + assumes "finite I" "I \ {}" + "\i. i \ I \ integrable M (f i)" + shows "integrable M (\x. MAX i\I. f i x)" +using integrable_Max[of I M f, OF assms] +by(simp add: Setcompr_eq_image) + lemma integral_Markov_inequality: assumes [measurable]: "integrable M u" and "AE x in M. 0 \ u x" "0 < (c::real)" shows "(emeasure M) {x\space M. u x \ c} \ (1/c) * (\x. u x \M)"