equal
deleted
inserted
replaced
2024 moreover have "integrable M (\<lambda>x. min (f j x) (Min {f i x |i. i \<in> F}))" |
2024 moreover have "integrable M (\<lambda>x. min (f j x) (Min {f i x |i. i \<in> F}))" |
2025 by (rule integrable_min, auto simp add: H) |
2025 by (rule integrable_min, auto simp add: H) |
2026 ultimately show "integrable M (\<lambda>x. Min {f i x |i. i = j \<or> i \<in> F})" by simp |
2026 ultimately show "integrable M (\<lambda>x. Min {f i x |i. i = j \<or> i \<in> F})" by simp |
2027 qed |
2027 qed |
2028 |
2028 |
|
2029 lemma integrable_MIN: |
|
2030 fixes f:: "_ \<Rightarrow> _ \<Rightarrow> real" |
|
2031 assumes "finite I" "I \<noteq> {}" |
|
2032 "\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)" |
|
2033 shows "integrable M (\<lambda>x. MIN i\<in>I. f i x)" |
|
2034 using integrable_Min[of I M f, OF assms] |
|
2035 by(simp add: Setcompr_eq_image) |
|
2036 |
2029 lemma integrable_Max: |
2037 lemma integrable_Max: |
2030 fixes f:: "_ \<Rightarrow> _ \<Rightarrow> real" |
2038 fixes f:: "_ \<Rightarrow> _ \<Rightarrow> real" |
2031 assumes "finite I" "I \<noteq> {}" |
2039 assumes "finite I" "I \<noteq> {}" |
2032 "\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)" |
2040 "\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)" |
2033 shows "integrable M (\<lambda>x. Max {f i x|i. i \<in> I})" |
2041 shows "integrable M (\<lambda>x. Max {f i x|i. i \<in> I})" |
2040 using H(1) H(2) Max_insert by simp |
2048 using H(1) H(2) Max_insert by simp |
2041 moreover have "integrable M (\<lambda>x. max (f j x) (Max {f i x |i. i \<in> F}))" |
2049 moreover have "integrable M (\<lambda>x. max (f j x) (Max {f i x |i. i \<in> F}))" |
2042 by (rule integrable_max, auto simp add: H) |
2050 by (rule integrable_max, auto simp add: H) |
2043 ultimately show "integrable M (\<lambda>x. Max {f i x |i. i = j \<or> i \<in> F})" by simp |
2051 ultimately show "integrable M (\<lambda>x. Max {f i x |i. i = j \<or> i \<in> F})" by simp |
2044 qed |
2052 qed |
|
2053 |
|
2054 lemma integrable_MAX: |
|
2055 fixes f:: "_ \<Rightarrow> _ \<Rightarrow> real" |
|
2056 assumes "finite I" "I \<noteq> {}" |
|
2057 "\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)" |
|
2058 shows "integrable M (\<lambda>x. MAX i\<in>I. f i x)" |
|
2059 using integrable_Max[of I M f, OF assms] |
|
2060 by(simp add: Setcompr_eq_image) |
2045 |
2061 |
2046 lemma integral_Markov_inequality: |
2062 lemma integral_Markov_inequality: |
2047 assumes [measurable]: "integrable M u" and "AE x in M. 0 \<le> u x" "0 < (c::real)" |
2063 assumes [measurable]: "integrable M u" and "AE x in M. 0 \<le> u x" "0 < (c::real)" |
2048 shows "(emeasure M) {x\<in>space M. u x \<ge> c} \<le> (1/c) * (\<integral>x. u x \<partial>M)" |
2064 shows "(emeasure M) {x\<in>space M. u x \<ge> c} \<le> (1/c) * (\<integral>x. u x \<partial>M)" |
2049 proof - |
2065 proof - |