(* The Lebesgue Integral Stefan Richter 2002 *) section ‹The three-step approach \label{sec:stepwise-approach}› theory Integral imports RealRandVar begin (*simple function integral set*) text ‹Having learnt from my failures, we take the safe and clean way of Heinz Bauer \cite{Bauer}. It proceeds as outlined in the introduction. In three steps, we fix the integral for elementary (``step-'')functions, for limits of these, and finally for differences between such limits. › subsection ‹Simple functions \label{sec:simple-fun}› text ‹ A simple function is a finite sum of characteristic functions, each multiplied with a nonnegative constant. These functions must be parametrized by measurable sets. Note that to check this condition, a tuple consisting of a set of measurable sets and a measure is required as the integral operator's second argument, whereas the measure only is given in informal notation. Usually the tuple will be a measure space, though it is not required so by the definition at this point. It is most natural to declare the value of the integral in this elementary case by simply replacing the characteristic functions with the measures of their respective sets. Uniqueness remains to be shown, for a function may have infinitely many decompositions and these might give rise to more than one integral value. This is why we construct a \emph{simple function integral set} for any function and measurable sets/measure pair by means of an inductive set definition containing but one introduction rule. › inductive_set sfis:: "('a ⇒ real) ⇒ ('a set set * ('a set ⇒ real)) ⇒ real set" for f :: "'a ⇒ real" and M :: "'a set set * ('a set ⇒ real)" where (*This uses normal forms*) base: "⟦f = (λt. ∑i∈(S::nat set). x i * χ (A i) t); ∀i ∈ S. A i ∈ measurable_sets M; nonnegative x; finite S; ∀i∈S. ∀j∈S. i ≠ j ⟶ A i ∩ A j = {}; (⋃i∈S. A i) = UNIV⟧ ⟹ (∑i∈S. x i * measure M (A i)) ∈ sfis f M" (*S may not be polymorphic*) text‹As you can see we require two extra conditions, and they amount to the sets being a partition of the universe. We say that a function is in normal form if it is represented this way. Normal forms are only needed to show additivity and monotonicity of simple function integral sets. These theorems can then be used in turn to get rid of the normality condition. More precisely, normal forms play a central role in the ‹sfis_present› lemma. For two simple functions with different underlying partitions it states the existence of a common finer-grained partition that can be used to represent the functions uniformly. The proof is remarkably lengthy, another case where informal reasoning is more intricate than it seems. The reason it is included anyway, with the exception of the two following lemmata, is that it gives insight into the arising complication and its formal solution. The problem is in the use of informal sum notation, which easily permits for a change in index sets, allowing for a pair of indices. This change has to be rectified in formal reasoning. Luckily, the task is eased by an injective function from $\mathbb{N}^2$ into $\mathbb{N}$, which was developed for the rationals mentioned in \ref{sec:realrandvar}. It might have been still easier if index sets were polymorphic in our integral definition, permitting pairs to be formed when necessary, but the logic doesn't allow for this.› lemma assumes un: "(⋃i∈R. B i) = UNIV" and fin: "finite R" and dis: "∀j1∈R. ∀j2∈R. j1 ≠ j2 ⟶ (B j1) ∩ (B j2) = {}" shows char_split: "χ A t = (∑j∈R. χ (A ∩ B j) t)" (*<*)proof (cases "t ∈ A") case True with un obtain j where jR: "j∈R" and tj: "t ∈ A ∩ B j" by fast from tj have "χ (A ∩ B j) t = 1" by (simp add: characteristic_function_def) with fin jR have "(∑i∈R-{j}. χ (A ∩ B i) t) = (∑i∈R. χ (A ∩ B i) t) - 1" by (simp add: sum_diff1) also from dis jR tj have "R-{j} = R-{j}" and "⋀x. x ∈ R-{j} ⟹ χ (A ∩ B x) t = 0" by (auto simp add: characteristic_function_def) hence "(∑i∈R-{j}. χ (A ∩ B i) t) = (∑i∈R-{j}. 0)" by (rule sum.cong) finally have "1 = (∑i∈R. χ (A ∩ B i) t)" by (simp) with True show ?thesis by (simp add: characteristic_function_def) next case False hence "⋀i. χ (A ∩ B i) t = 0" by (simp add: characteristic_function_def) hence "0 = (∑i∈R. χ (A ∩ B i) t)" by (simp) with False show ?thesis by (simp add: characteristic_function_def) qed lemma assumes ms: "measure_space M" and dis: "∀j1∈(R::nat set). ∀j2∈R. j1 ≠ j2 ⟶ (B j1) ∩ (B j2) = {}" and meas: "∀j∈R. B j ∈ measurable_sets M" shows measure_sums_UNION: "(λn. measure M (if n ∈ R then B n else {})) sums measure M (⋃i∈R. B i)" (*<*)proof - have eq: "(⋃i∈R. B i) = (⋃i. if i∈R then B i else {})" by (auto split: if_splits) from dis have dis2: "(∀i j. i ≠ j ⟶ (if i∈R then B i else {}) ∩ (if j∈R then B j else {}) = {})" by simp from meas have meas2: "range (λi. if i∈R then B i else {}) ⊆ measurable_sets M" using ms by (auto simp add: measure_space_def sigma_algebra_def) hence "∀i. (if i∈R then B i else {})∈ measurable_sets M" by auto with ms have "(⋃i. if i∈R then B i else {}) ∈ measurable_sets M" by (auto simp add: measure_space_def sigma_algebra_def) (use eq in presburger) with meas2 dis2 have "(λn. measure M (if n ∈ R then B n else {})) sums measure M (⋃i. if i∈R then B i else {})" using ms by (simp add: measure_space_def countably_additive_def cong: SUP_cong_simp) with eq show ?thesis by simp qed(*>*) lemma sumr_sum: "(∑i=0..<k::nat. if i ∈ R then f i else (0::real)) = (∑i∈(R∩{..<k}). f i)" (*<*)proof (induct k) case 0 thus ?case by simp case (Suc l) hence "(∑i=0..<Suc l. if i ∈ R then f i else 0) = (if l ∈ R then f l else 0) + (∑i∈(R∩{..<l}). f i)" by simp also have "… = (∑i∈(R ∩ {..<Suc l}). f i)" proof (cases "l ∈ R") case True have "l ∉ (R∩{..<l})" by simp have "f l + (∑i∈(R∩{..<l}). f i) = (∑i∈(insert l (R∩{..<l})). f i)" by simp also from True have "insert l (R∩{..<l}) = (R ∩ {..<Suc l})" by (auto simp add: lessThan_Suc) finally show ?thesis using True by simp next case False hence "(R∩{..<l}) = (R ∩ {..<Suc l})" by (auto simp add: lessThan_Suc) thus ?thesis by auto qed finally show ?case . qed(*>*) lemma assumes ms: "measure_space M" and dis: "∀j1∈(R::nat set). ∀j2∈R. j1 ≠ j2 ⟶ (B j1) ∩ (B j2) = {}" and meas: "∀j∈R. B j ∈ measurable_sets M" and fin: "finite R" shows measure_sum: "measure M (⋃i∈R. B i) = (∑j∈R. measure M (B j))" (*<*)proof (cases "R={}") case False with fin have leR: "∀r∈R. r ≤ Max R" by simp hence "R = R ∩ {..Max R}" by auto also have "… = R ∩ {..<Suc (Max R)}" by (simp add: lessThan_Suc_atMost[THEN sym]) finally have "(∑j∈R. measure M (B j)) = (∑j∈R∩ {..<Suc (Max R)} . measure M (B j))" by simp also have "… = (∑x=0..<Suc(Max R). if x ∈ R then measure M (B x) else 0)" by (rule sumr_sum[THEN sym]) also { fix x from ms have "(if x ∈ R then measure M (B x) else 0) = (measure M (if x∈R then B x else {}))" by (simp add: measure_space_def positive_def) } hence "… = (∑x=0..<Suc(Max R). measure M (if x∈R then B x else {}))" by simp also { fix m assume "Suc (Max R) ≤ m" hence "Max R < m" by simp with leR have "m∉R" by auto with ms have "measure M (if m∈R then B m else {}) = 0" by (simp add: measure_space_def positive_def) } hence "∀m. (Suc (Max R)) ≤ m ⟶ measure M (if m∈R then B m else {}) = 0" by simp hence "(λn. measure M (if n ∈ R then B n else {})) sums (∑x=0..<Suc(Max R). measure M (if x∈R then B x else {}))" by (intro sums_finite) auto hence "(∑x=0..<Suc(Max R). measure M (if x∈R then B x else {})) = suminf (λn. measure M (if n ∈ R then B n else {}))" by (rule sums_unique) also from ms dis meas have "(λn. measure M (if n ∈ R then B n else {})) sums measure M (⋃i∈R. B i)" by (rule measure_sums_UNION) ultimately show ?thesis by (simp add: sums_unique) next case True with ms show ?thesis by (simp add: measure_space_def positive_def) qed(*>*) lemma assumes ms: "measure_space M" and un: "(⋃i∈R. B i) = UNIV" and fin: "finite (R::nat set)" and dis: "∀j1∈R. ∀j2∈R. j1 ≠ j2 ⟶ (B j1) ∩ (B j2) = {}" and meas: "∀j∈R. B j ∈ measurable_sets M" and Ameas: "A ∈ measurable_sets M" shows measure_split: "measure M A = (∑j∈R. measure M (A ∩ B j))" (*<*)proof - note ms moreover from dis have "∀j1∈R. ∀j2∈R. j1 ≠ j2 ⟶ (A ∩ B j1) ∩ (A ∩ B j2) = {}" by fast moreover from ms meas Ameas have "∀j∈R. A ∩ B j ∈ measurable_sets M" by (simp add: measure_space_def sigma_algebra_inter) moreover note fin ultimately have "measure M (⋃i∈R. A ∩ B i) = (∑j∈R. measure M (A ∩ B j))" by (rule measure_sum) also from un have "A = (⋃i∈R. A ∩ B i)" by auto ultimately show ?thesis by simp qed(*>*) lemma prod_encode_fst_inj: "inj (λi. prod_encode(i,j))" using inj_prod_encode by (unfold inj_on_def) blast lemma prod_encode_snd_inj: "inj (λj. prod_encode(i,j))" using inj_prod_encode by (unfold inj_on_def) blast (*>*) lemma assumes (*<*)ms:(*>*) "measure_space M" and (*<*)a:(*>*) "a ∈ sfis f M" and (*<*)b:(*>*) "b ∈ sfis g M" shows sfis_present: "∃ z1 z2 C K. f = (λt. ∑i∈(K::nat set). z1 i * χ (C i) t) ∧ g = (λt. ∑i∈K. z2 i * χ (C i) t) ∧ a = (∑i∈K. z1 i * measure M (C i)) ∧ b = (∑i∈K. z2 i * measure M (C i)) ∧ finite K ∧ (∀i∈K. ∀j∈K. i ≠ j ⟶ C i ∩ C j = {}) ∧ (∀i ∈ K. C i ∈ measurable_sets M) ∧ (⋃i∈K. C i) = UNIV ∧ nonnegative z1 ∧ nonnegative z2" using a proof cases case (base x A R) note base_x = this show ?thesis using b proof cases case (base y B S) with assms base_x have ms: "measure_space M" and f: "f = (λt. ∑i∈(R::nat set). x i * χ (A i) t)" and a: "a = (∑i∈R. x i * measure M (A i))" and Ams: "∀i ∈ R. A i ∈ measurable_sets M" and R: "finite R" and Adis: "∀i∈R. ∀j∈R. i ≠ j ⟶ A i ∩ A j = {}" and Aun: "(⋃i∈R. A i) = UNIV" and g: "g = (λt. ∑i∈(S::nat set). y i * χ (B i) t)" and b: "b = (∑j∈S. y j * measure M (B j))" and Bms: "∀i ∈ S. B i ∈ measurable_sets M" and S: "finite S" and Bdis: "∀i∈S. ∀j∈S. i ≠ j ⟶ B i ∩ B j = {}" and Bun: "(⋃i∈S. B i) = UNIV" and x: "nonnegative x" and y: "nonnegative y" by simp_all txt‹\nopagebreak› define C where "C = (λ(i,j). A i ∩ B j) ∘ prod_decode" define z1 where "z1 k = x (fst (prod_decode k))" for k define z2 where "z2 k = y (snd (prod_decode k))" for k define K where "K = {k. ∃i∈R. ∃j∈S. k = prod_encode (i,j)}" define G where "G i = (λj. prod_encode (i,j)) ` S" for i define H where "H j = (λi. prod_encode (i,j)) ` R" for j { fix t { fix i from Bun S Bdis have "χ (A i) t = (∑j∈S. χ (A i ∩ B j) t)" by (rule char_split) hence "x i * χ (A i) t = (∑j∈S. x i * χ (A i ∩ B j) t)" by (simp add: sum_distrib_left) also { fix j have "S=S" and "x i * χ (A i ∩ B j) t = (let k=prod_encode(i,j) in z1 k * χ (C k) t)" by (auto simp add: C_def z1_def Let_def) } hence "… = (∑j∈S. let k=prod_encode (i,j) in z1 k * χ (C k) t)" by (rule sum.cong) also from S have "… = (∑k∈(G i). z1 k * χ (C k) t)" by (simp add: G_def Let_def o_def sum.reindex[OF subset_inj_on[OF prod_encode_snd_inj]]) finally have eq: "x i * χ (A i) t = (∑k∈ G i. z1 k * χ (C k) t)" . (*Repeat with measure instead of char*) from S have G: "finite (G i)" by (simp add: G_def) { fix k assume "k ∈ G i" then obtain j where kij: "k=prod_encode (i,j)" by (auto simp only: G_def) { fix i2 assume i2: "i2 ≠ i" { fix k2 assume "k2 ∈ G i2" then obtain j2 where kij2: "k2=prod_encode (i2,j2)" by (auto simp only: G_def) from i2 have "(i2,j2) ≠ (i,j)" and "(i2,j2) ∈ UNIV" and "(i,j) ∈ UNIV" by auto with inj_prod_encode have "prod_encode (i2,j2) ≠ prod_encode (i,j)" by (rule inj_on_contraD) with kij kij2 have "k2 ≠ k" by fast } hence "k ∉ G i2" by fast } } hence "⋀j. i ≠ j ⟹ G i ∩ G j = {}" by fast note eq G this } hence eq: "⋀i. x i * χ (A i) t = (∑k∈G i. z1 k * χ (C k) t)" and G: "⋀i. finite (G i)" and Gdis: "⋀i j. i ≠ j ⟹ G i ∩ G j = {}" . { fix i assume "i∈R" with ms Bun S Bdis Bms Ams have "measure M (A i) = (∑j∈S. measure M (A i ∩ B j))" by (simp add: measure_split) hence "x i * measure M (A i) = (∑j∈S. x i * measure M (A i ∩ B j))" by (simp add: sum_distrib_left) also { fix j have "S=S" and "x i * measure M (A i ∩ B j) = (let k=prod_encode(i,j) in z1 k * measure M (C k))" by (auto simp add: C_def z1_def Let_def) } hence "… = (∑j∈S. let k=prod_encode (i,j) in z1 k * measure M (C k))" by (rule sum.cong) also from S have "… = (∑k∈(G i). z1 k * measure M (C k))" by (simp add: G_def Let_def o_def sum.reindex[OF subset_inj_on[OF prod_encode_snd_inj]]) finally have "x i * measure M (A i) = (∑k∈(G i). z1 k * measure M (C k))" . } with refl[of R] have "(∑i∈R. x i * measure M (A i)) = (∑i∈R. (∑k∈(G i). z1 k * measure M (C k)))" by (rule sum.cong) with eq f a have "f t = (∑i∈R. (∑k∈G i. z1 k * χ (C k) t))" and "a = (∑i∈R. (∑k∈(G i). z1 k * measure M (C k)))" by auto also have KG: "K = (⋃i∈R. G i)" by (auto simp add: K_def G_def) moreover note G Gdis R ultimately have f: "f t = (∑k∈K. z1 k * χ (C k) t)" and a: "a = (∑k∈K. z1 k * measure M (C k))" by (auto simp add: sum.UNION_disjoint) (*And now (almost) the same for g*) { fix j from Aun R Adis have "χ (B j) t = (∑i∈R. χ (B j ∩ A i) t)" by (rule char_split) hence "y j * χ (B j) t = (∑i∈R. y j * χ (A i ∩ B j) t)" by (simp add: sum_distrib_left Int_commute) also { fix i have "R=R" and "y j * χ (A i ∩ B j) t = (let k=prod_encode(i,j) in z2 k * χ (C k) t)" by (auto simp add: C_def z2_def Let_def) } hence "… = (∑i∈R. let k=prod_encode (i,j) in z2 k * χ (C k) t)" by (rule sum.cong) also from R have "… = (∑k∈(H j). z2 k * χ (C k) t)" by (simp add: H_def Let_def o_def sum.reindex[OF subset_inj_on[OF prod_encode_fst_inj]]) finally have eq: "y j * χ (B j) t = (∑k∈ H j. z2 k * χ (C k) t)" . from R have H: "finite (H j)" by (simp add: H_def) { fix k assume "k ∈ H j" then obtain i where kij: "k=prod_encode (i,j)" by (auto simp only: H_def) { fix j2 assume j2: "j2 ≠ j" { fix k2 assume "k2 ∈ H j2" then obtain i2 where kij2: "k2=prod_encode (i2,j2)" by (auto simp only: H_def) from j2 have "(i2,j2) ≠ (i,j)" and "(i2,j2) ∈ UNIV" and "(i,j) ∈ UNIV" by auto with inj_prod_encode have "prod_encode (i2,j2) ≠ prod_encode (i,j)" by (rule inj_on_contraD) with kij kij2 have "k2 ≠ k" by fast } hence "k ∉ H j2" by fast } } hence "⋀i. i ≠ j ⟹ H i ∩ H j = {}" by fast note eq H this } hence eq: "⋀j. y j * χ (B j) t = (∑k∈H j. z2 k * χ (C k) t)" and H: "⋀i. finite (H i)" and Hdis: "⋀i j. i ≠ j ⟹ H i ∩ H j = {}" . from eq g have "g t = (∑j∈S. (∑k∈H j. z2 k * χ (C k) t))" by simp also { fix j assume jS: "j∈S" from ms Aun R Adis Ams Bms jS have "measure M (B j) = (∑i∈R. measure M (B j ∩ A i))" by (simp add: measure_split) hence "y j * measure M (B j) = (∑i∈R. y j * measure M (A i ∩ B j))" by (simp add: sum_distrib_left Int_commute) also { fix i have "R=R" and "y j * measure M (A i ∩ B j) = (let k=prod_encode(i,j) in z2 k * measure M (C k))" by (auto simp add: C_def z2_def Let_def) } hence "… = (∑i∈R. let k=prod_encode(i,j) in z2 k * measure M (C k))" by (rule sum.cong) also from R have "… = (∑k∈(H j). z2 k * measure M (C k))" by (simp add: H_def Let_def o_def sum.reindex[OF subset_inj_on[OF prod_encode_fst_inj]]) finally have eq2: "y j * measure M (B j) = (∑k∈(H j). z2 k * measure M (C k))" . } with refl have "(∑j∈S. y j * measure M (B j)) = (∑j∈S. (∑k∈(H j). z2 k * measure M (C k)))" by (rule sum.cong) with b have "b = (∑j∈S. (∑k∈(H j). z2 k * measure M (C k)))" by simp moreover have "K = (⋃j∈S. H j)" by (auto simp add: K_def H_def) moreover note H Hdis S ultimately have g: "g t = (∑k∈K. z2 k * χ (C k) t)" and K: "finite K" and b: "b = (∑k∈K. z2 k * measure M (C k))" by (auto simp add: sum.UNION_disjoint) { fix i from Bun have "(⋃k∈G i. C k) = A i" by (simp add: G_def C_def) } with Aun have "(⋃i∈R. (⋃k∈G i. C k)) = UNIV" by simp hence "(⋃k∈(⋃i∈R. G i). C k) = UNIV" by simp with KG have Kun: "(⋃k∈K. C k) = UNIV" by simp note f g a b Kun K } txt‹\nopagebreak› hence f: "f = (λt. (∑k∈K. z1 k * χ (C k) t))" and g: "g = (λt. (∑k∈K. z2 k * χ (C k) t))" and a: "a = (∑k∈K. z1 k * measure M (C k))" and b: "b = (∑k∈K. z2 k * measure M (C k))" and Kun: "⋃(C ` K) = UNIV" and K: "finite K" by (auto simp add: ext) note f g a b K moreover { fix k1 k2 assume "k1∈K" and "k2∈K" and diff: "k1 ≠ k2" with K_def obtain i1 j1 i2 j2 where RS: "i1 ∈ R ∧ i2 ∈ R ∧ j1 ∈ S ∧ j2 ∈ S" and k1: "k1 = prod_encode (i1,j1)" and k2: "k2 = prod_encode (i2,j2)" by auto with diff have "(i1,j1) ≠ (i2,j2)" by auto with RS Adis Bdis k1 k2 have "C k1 ∩ C k2 = {}" by (simp add: C_def) fast } moreover { fix k assume "k ∈ K" with K_def obtain i j where R: "i ∈ R" and S: "j ∈ S" and k: "k = prod_encode (i,j)" by auto with Ams Bms have "A i ∈ measurable_sets M" and "B j ∈ measurable_sets M" by auto with ms have "A i ∩ B j ∈ measurable_sets M" by (simp add: measure_space_def sigma_algebra_inter) with k have "C k ∈ measurable_sets M" by (simp add: C_def) } moreover note Kun moreover from x have "nonnegative z1" by (simp add: z1_def nonnegative_def) moreover from y have "nonnegative z2" by (simp add: z2_def nonnegative_def) ultimately show ?thesis by blast qed qed text‹Additivity and monotonicity are now almost obvious, the latter trivially implying uniqueness.› lemma assumes ms: "measure_space M" and a: "a ∈ sfis f M" and b: "b ∈ sfis g M" shows sfis_add: "a+b ∈ sfis (λw. f w + g w) M" proof - from assms have "∃ z1 z2 C K. f = (λt. ∑i∈(K::nat set). z1 i * χ (C i) t) ∧ g = (λt. ∑i∈K. z2 i * χ (C i) t) ∧ a = (∑i∈K. z1 i * measure M (C i)) ∧ b = (∑i∈K. z2 i * measure M (C i)) ∧ finite K ∧ (∀i∈K. ∀j∈K. i ≠ j ⟶ C i ∩ C j = {}) ∧ (∀i ∈ K. C i ∈ measurable_sets M) ∧ (⋃i∈K. C i) = UNIV ∧ nonnegative z1 ∧ nonnegative z2" by (rule sfis_present) then obtain z1 z2 C K where f: "f = (λt. ∑i∈(K::nat set). z1 i * χ (C i) t)" and g: "g = (λt. ∑i∈K. z2 i * χ (C i) t)" and a2: "a = (∑i∈K. z1 i * measure M (C i))" and b2: "b = (∑i∈K. z2 i * measure M (C i))" and CK: "finite K ∧ (∀i∈K. ∀j∈K. i ≠ j ⟶ C i ∩ C j = {}) ∧ (∀i∈K. C i ∈ measurable_sets M) ∧ ⋃(C ` K) = UNIV" and z1: "nonnegative z1" and z2: "nonnegative z2" by auto { fix t from f g have "f t + g t = (∑i∈K. z1 i * χ (C i) t) + (∑i∈K. z2 i * χ (C i) t)" by simp also have "… = (∑i∈K. z1 i * χ (C i) t + z2 i * χ (C i) t)" by (rule sum.distrib[THEN sym]) also have "… = (∑i∈K. (z1 i + z2 i) * χ (C i) t)" by (simp add: distrib_right) finally have "f t + g t = (∑i∈K. (z1 i + z2 i) * χ (C i) t)" . } also { fix t from z1 have "0 ≤ z1 t" by (simp add: nonnegative_def) also from z2 have "0 ≤ z2 t" by (simp add: nonnegative_def) ultimately have "0 ≤ z1 t + z2 t" by (rule add_nonneg_nonneg) } hence "nonnegative (λw. z1 w + z2 w)" by (simp add: nonnegative_def ext) moreover note CK ultimately have "(∑i∈K. (z1 i + z2 i) * measure M (C i)) ∈ sfis (λw. f w + g w) M" by (auto simp add: sfis.base) also from a2 b2 have "a+b = (∑i∈K. (z1 i + z2 i) * measure M (C i))" by (simp add: sum.distrib[THEN sym] distrib_right) ultimately show ?thesis by simp qed lemma assumes ms: "measure_space M" and a: "a ∈ sfis f M" and b: "b ∈ sfis g M" and fg: "f≤g" shows sfis_mono: "a ≤ b" proof - txt‹\nopagebreak› from ms a b have "∃ z1 z2 C K. f = (λt. ∑i∈(K::nat set). z1 i * χ (C i) t) ∧ g = (λt. ∑i∈K. z2 i * χ (C i) t) ∧ a = (∑i∈K. z1 i * measure M (C i)) ∧ b = (∑i∈K. z2 i * measure M (C i)) ∧ finite K ∧ (∀i∈K. ∀j∈K. i ≠ j ⟶ C i ∩ C j = {}) ∧ (∀i ∈ K. C i ∈ measurable_sets M) ∧ (⋃i∈K. C i) = UNIV ∧ nonnegative z1 ∧ nonnegative z2" by (rule sfis_present) then obtain z1 z2 C K where f: "f = (λt. ∑i∈(K::nat set). z1 i * χ (C i) t)" and g: "g = (λt. ∑i∈K. z2 i * χ (C i) t)" and a2: "a = (∑i∈K. z1 i * measure M (C i))" and b2: "b = (∑i∈K. z2 i * measure M (C i))" and K: "finite K" and dis: "(∀i∈K. ∀j∈K. i ≠ j ⟶ C i ∩ C j = {})" and Cms: "(∀i∈K. C i ∈ measurable_sets M)" and Cun: "⋃(C ` K) = UNIV" by auto { fix i assume iK: "i ∈ K" { assume "C i ≠ {}" then obtain t where ti: "t ∈ C i" by auto hence "z1 i = z1 i * χ (C i) t" by (simp add: characteristic_function_def) also from dis iK ti have "K-{i} = K-{i}" and "⋀x. x ∈ K-{i} ⟹ z1 x * χ (C x) t = 0" by (auto simp add: characteristic_function_def) hence "0 = (∑k∈K-{i}. z1 k * χ (C k) t)" by (simp only: sum.neutral_const sum.cong) with K iK have "z1 i * χ (C i) t = (∑k∈K. z1 k * χ (C k) t)" by (simp add: sum_diff1) also from fg f g have "(∑i∈K. z1 i * χ (C i) t) ≤ (∑i∈K. z2 i * χ (C i) t)" by (simp add: le_fun_def) also from dis iK ti have "K-{i} = K-{i}" and "⋀x. x ∈ K-{i} ⟹ z2 x * χ (C x) t = 0" by (auto simp add: characteristic_function_def) hence "0 = (∑k∈K-{i}. z2 k * χ (C k) t)" by (simp only: sum.neutral_const sum.cong) with K iK have "(∑k∈K. z2 k * χ (C k) t) = z2 i * χ (C i) t" by (simp add: sum_diff1) also from ti have "… = z2 i" by (simp add: characteristic_function_def) finally have "z1 i ≤ z2 i" . } hence h: "C i ≠ {} ⟹ z1 i ≤ z2 i" . have "z1 i * measure M (C i) ≤ z2 i * measure M (C i)" proof (cases "C i ≠ {}") case False with ms show ?thesis by (auto simp add: measure_space_def positive_def) next case True with h have "z1 i ≤ z2 i" by fast also from iK ms Cms have "0 ≤ measure M (C i)" by (auto simp add: measure_space_def positive_def ) ultimately show ?thesis by (simp add: mult_right_mono) qed } with a2 b2 show ?thesis by (simp add: sum_mono) qed lemma sfis_unique: assumes ms: "measure_space M" and a: "a ∈ sfis f M" and b: "b ∈ sfis f M" shows "a=b" proof - have "f≤f" by (simp add: le_fun_def) with assms have "a≤b" and "b≤a" by (auto simp add: sfis_mono) thus ?thesis by simp qed text ‹The integral of characteristic functions, as well as the effect of multiplication with a constant, follows directly from the definition. Together with a generalization of the addition theorem to sums, a less restrictive introduction rule emerges, making normal forms obsolete. It is only valid in measure spaces though.› lemma sfis_char: assumes ms: "measure_space M" and mA: "A ∈ measurable_sets M" shows "measure M A ∈ sfis χ A M" (*<*)proof - define R :: "nat ⇒ 'a set" where "R i = (if i = 0 then A else if i=1 then -A else {})" for i define x :: "nat ⇒ real" where "x i = (if i = 0 then 1 else 0)" for i define K :: "nat set" where "K = {0,1}" from ms mA have Rms: "∀i∈K. R i ∈ measurable_sets M" by (simp add: K_def R_def measure_space_def sigma_algebra_def) have nn: "nonnegative x" by (simp add: nonnegative_def x_def) have un: "(⋃i∈K. R i) = UNIV" by (simp add: R_def K_def) have fin: "finite K" by (simp add: K_def) have dis: "∀j1∈K. ∀j2∈K. j1 ≠ j2 ⟶ (R j1) ∩ (R j2) = {}" by (auto simp add: R_def K_def) { fix t from un fin dis have "χ A t = (∑i∈K. χ (A ∩ R i) t)" by (rule char_split) also { fix i have "K=K" and "χ (A ∩ R i) t = x i * χ (R i) t" by (auto simp add: R_def x_def characteristic_function_def)} hence "… = (∑i∈K. x i * χ (R i) t)" by (rule sum.cong) finally have "χ A t = (∑i∈K. x i * χ (R i) t)" . } hence "χ A = (λt. ∑i∈K. x i * χ (R i) t)" by (simp add: ext) from this Rms nn fin dis un have "(∑i∈K. x i * measure M (R i)) ∈ sfis χ A M" by (rule sfis.base) also { fix i from ms have "K=K" and "x i * measure M (R i) = measure M (A ∩ R i)" by (auto simp add: R_def x_def measure_space_def positive_def) } hence "(∑i∈K. x i * measure M (R i)) = (∑i∈K. measure M (A ∩ R i))" by (rule sum.cong) also from ms un fin dis Rms mA have "… = measure M A" by (rule measure_split[THEN sym]) finally show ?thesis . qed(*>*) (*Sums are always problematic, since they use informal notation all the time.*) lemma sfis_times: assumes a: "a ∈ sfis f M" and z: "0≤z" shows "z*a ∈ sfis (λw. z*f w) M" (*<*)using a proof cases case (base x A S) { fix t from base have "z*f t = (∑i∈S. z * (x i * χ (A i) t))" by (simp add: sum_distrib_left) also have "… = (∑i∈S. (z * x i) * χ (A i) t)" proof (rule sum.cong) show "S = S" .. fix i show "z * (x i * χ (A i) t) = (z * x i) * χ (A i) t" by auto qed finally have "z * f t = (∑i∈S. z * x i * χ (A i) t)" . } hence zf: "(λw. z*f w) = (λt. ∑i∈S. z * x i * χ (A i) t)" by (simp add: ext) from z base have "nonnegative (λw. z*x w)" by (simp add: nonnegative_def zero_le_mult_iff) with base zf have "(∑i∈S. z * x i * measure M (A i)) ∈ sfis (λw. z*f w) M" by (simp add: sfis.base) also have "(∑i∈S. z * x i * measure M (A i)) = (∑i∈S. z * (x i * measure M (A i)))" proof (rule sum.cong) show "S = S" .. fix i show "(z * x i) * measure M (A i) = z * (x i * measure M (A i))" by auto qed also from base have "… = z*a" by (simp add: sum_distrib_left) finally show ?thesis . qed(*>*) lemma assumes ms: "measure_space M" and a: "∀i∈S. a i ∈ sfis (f i) M" and S: "finite S" shows sfis_sum: "(∑i∈S. a i) ∈ sfis (λt. ∑i∈S. f i t) M" (*<*)using S a proof induct case empty with ms have "measure M {} ∈ sfis χ {} M" by (simp add: measure_space_def sigma_algebra_def sfis_char) with ms show ?case by (simp add: sum.empty measure_space_def positive_def char_empty) next case (insert s S) then have "⋀t. (∑i ∈ insert s S. f i t) = f s t + (∑i∈S. f i t)" by simp moreover from insert have "(∑i ∈ insert s S. a i) = a s + (∑i∈S. a i)" by simp moreover from insert have "a s ∈ sfis (f s) M" by fast moreover from insert have "(∑i∈S. a i) ∈ sfis (λt. ∑i∈S. f i t) M" by fast moreover note ms ultimately show ?case by (simp add: sfis_add ext) qed(*>*) (*The introduction rule without normal forms, only in measure_spaces*) lemma sfis_intro: assumes ms: "measure_space M" and Ams: "∀i ∈ S. A i ∈ measurable_sets M" and nn: "nonnegative x" and S: "finite S" shows "(∑i∈S. x i * measure M (A i)) ∈ sfis (λt. ∑i∈(S::nat set). x i * χ (A i) t) M" proof - { fix i assume iS: "i ∈ S" with ms Ams have "measure M (A i) ∈ sfis χ (A i) M" by (simp add: sfis_char) with nn have "x i * measure M (A i) ∈ sfis (λt. x i * χ (A i) t) M" by (simp add: nonnegative_def sfis_times) } with ms S show ?thesis by (simp add: sfis_sum) qed text‹That is nearly all there is to know about simple function integral sets. It will be useful anyway to have the next two facts available.› lemma sfis_nn: assumes f: "a ∈ sfis f M" shows "nonnegative f" (*<*)using f proof (cases) case (base x A S) { fix t from base have "⋀i. 0 ≤ x i * χ (A i) t" by (simp add: nonnegative_def characteristic_function_def) with base have "(∑i∈S. 0) ≤ f t" by (simp del: sum.neutral_const sum_constant add: sum_mono) hence "0 ≤ f t" by simp } thus ?thesis by (simp add: nonnegative_def) qed(*>*) lemma sum_rv: assumes rvs: "∀k∈K. (f k) ∈ rv M" and ms: "measure_space M" shows "(λt. ∑k∈K. f k t) ∈ rv M" (*<*)proof (cases "finite K") case False hence "(λt. ∑k∈K. f k t) = (λt. 0)" by simp with ms show ?thesis by (simp add: const_rv) next case True from this rvs show ?thesis proof (induct) case empty have "(λt. ∑k∈{}. f k t) = (λt. 0)" by simp with ms show ?case by (simp add: const_rv) next case (insert x F) hence "(λt. ∑k∈insert x F. f k t) = (λt. f x t + (∑k∈F. f k t))" by simp also from insert have "f x ∈ rv M" and "(λt. (∑k∈F. f k t)) ∈ rv M" by simp_all ultimately show ?case by (simp add: rv_plus_rv) qed qed(*>*) lemma sfis_rv: assumes ms: "measure_space M" and f: "a ∈ sfis f M" shows "f ∈ rv M" using f proof (cases) case (base x A S) hence "f = (λt. ∑i∈S. x i * χ (A i) t)" by simp also { fix i assume "i ∈ S" with base have "A i ∈ measurable_sets M" by simp with ms have "(λt. x i * χ (A i) t) ∈ rv M" by (simp add: char_rv const_rv rv_times_rv) } with ms have "… ∈ rv M" by (simp add: sum_rv) ultimately show ?thesis by simp qed(*>*)(*>*)(*nonnegative function integral set*)(*>*) subsection ‹Nonnegative Functions› text ‹ \label{nnfis}There is one more important fact about ‹sfis›, easily the hardest one to see. It is about the relationship with monotone convergence and paves the way for a sensible definition of ‹nnfis›, the nonnegative function integral sets, enabling monotonicity and thus uniqueness. A reasonably concise formal proof could fortunately be achieved in spite of the nontrivial ideas involved --- compared for instance to the intuitive but hard-to-formalize ‹sfis_present›. A small lemma is needed to ensure that the inequation, which depends on an arbitrary $z$ strictly between $0$ and $1$, carries over to $z=1$, thereby eliminating $z$ in the end.› lemma real_le_mult_sustain: assumes zr: "⋀z. ⟦0<z; z<1⟧ ⟹ z * r ≤ y" shows "r ≤ (y::real)"(*<*) proof (cases "0<y") case False have "0<(1::real)" by simp hence "∃z::real. 0<z ∧ z<1" by (rule dense) then obtain z::real where 0: "0<z" and 1: "z<1" by fast with zr have a: "z*r ≤ y" by simp also from False have "y≤0" by simp with a have "z*r ≤ 0" by simp with 0 1 have z1: "z≤1" and r0: "r≤0" by (simp_all add: mult_le_0_iff) hence "1*r ≤ z*r" by (rule mult_right_mono_neg) ultimately show "r≤y" by simp next case True { assume yr: "y < r" then have "∃q. y<q ∧ q<r" by (rule dense) then obtain q where yq: "y<q" and q: "q<r" by fast from yr True have r0: "0<r" by simp with q have "q/r < 1" by (simp add: pos_divide_less_eq) also from True yq r0 have "0<q/r" by (simp add: zero_less_divide_iff) ultimately have "(q/r)*r≤y" using zr by force with r0 have "q≤y" by simp with yq have False by simp } thus ?thesis by force qed(*>*) lemma sfis_mon_conv_mono: assumes uf: "u↑f" and xu: "⋀n. x n ∈ sfis (u n) M" and xy: "x↑y" and sr: "r ∈ sfis s M" and sf: "s ≤ f" and ms: "measure_space M" shows "r ≤ y" (*This is Satz 11.1 in Bauer*) using sr proof cases case (base a A S) note base_a = this { fix z assume znn: "0<(z::real)" and z1: "z<1" define B where "B n = {w. z*s w ≤ u n w}" for n { fix n note ms also from xu have xu: "x n ∈ sfis (u n) M" . hence nnu: "nonnegative (u n)" by (rule sfis_nn) from ms xu have "u n ∈ rv M" by (rule sfis_rv) moreover from ms sr have "s ∈ rv M" by (rule sfis_rv) with ms have "(λw. z*s w) ∈ rv M" by (simp add: const_rv rv_times_rv) ultimately have "B n ∈ measurable_sets M" by (simp add: B_def rv_le_rv_measurable) with ms base have ABms: "∀i∈S. (A i ∩ B n) ∈ measurable_sets M" by (auto simp add: measure_space_def sigma_algebra_inter) from xu have "z*(∑i∈S. a i * measure M (A i ∩ B n)) ≤ x n" proof (cases) case (base c C R) { fix t { fix i have "S=S" and "a i * χ (A i ∩ B n) t = χ (B n) t * (a i * χ (A i) t)" by (auto simp add: characteristic_function_def) } hence "(∑i∈S. a i * χ (A i ∩ B n) t) = (∑i∈S. χ (B n) t * (a i * χ (A i) t))" by (rule sum.cong) hence "z*(∑i∈S. a i * χ (A i ∩ B n) t) = z*(∑i∈S. χ (B n) t * (a i * χ (A i) t))" by simp also have "… = z * χ (B n) t * (∑i∈S. a i * χ (A i) t)" by (simp add: sum_distrib_left[THEN sym]) also from sr have "nonnegative s" by (simp add: sfis_nn) with nnu B_def base_a have "z * χ (B n) t * (∑i∈S. a i * χ (A i) t) ≤ u n t" by (auto simp add: characteristic_function_def nonnegative_def) finally have "z*(∑i∈S. a i * χ (A i ∩ B n) t) ≤ u n t" . } also from ms base_a znn ABms have "z*(∑i∈S. a i * measure M (A i ∩ B n)) ∈ sfis (λt. z*(∑i∈S. a i * χ (A i ∩ B n) t)) M" by (simp add: sfis_intro sfis_times) moreover note xu ms ultimately show ?thesis by (simp add: sfis_mono le_fun_def) qed note this ABms } hence 1: "⋀n. z * (∑i∈S. a i * measure M (A i ∩ B n)) ≤ x n" and ABms: "⋀n. ∀i∈S. A i ∩ B n ∈ measurable_sets M" . have Bun: "(λn. B n)↑UNIV" proof (unfold mon_conv_set_def, rule) { fix n from uf have um: "u n ≤ u (Suc n)" by (simp add: mon_conv_real_fun_def) { fix w assume "z*s w ≤ u n w" also from um have "u n w ≤ u (Suc n) w" by (simp add: le_fun_def) finally have "z*s w ≤ u (Suc n) w" . } hence "B n ≤ B (Suc n)" by (auto simp add: B_def) } thus " ∀n. B n ⊆ B (Suc n)" by fast { fix t have "∃n. z*s t ≤ u n t" proof (cases "s t = 0") case True fix n from True have "z*s t = 0" by simp also from xu have "nonnegative (u n)" by (rule sfis_nn) hence "0 ≤ u n t" by (simp add: nonnegative_def) finally show ?thesis by rule next case False from sr have "nonnegative s" by(rule sfis_nn) hence "0 ≤ s t" by (simp add: nonnegative_def) with False have "0 < s t" by arith with z1 have "z*s t < 1*s t" by (simp only: mult_strict_right_mono) also from sf have "… ≤ f t" by (simp add: le_fun_def) finally have "z * s t < f t" . (*Next we have to prove that u grows beyond z*s t*) also from uf have "(λm. u m t)↑f t" by (simp add: realfun_mon_conv_iff) ultimately have "∃n.∀m. n≤m ⟶ z*s t < u m t" by (simp add: real_mon_conv_outgrow) hence "∃n. z*s t < u n t" by fast thus ?thesis by (auto simp add: order_less_le) qed hence "∃n. t ∈ B n" by (simp add: B_def) hence "t ∈ (⋃n. B n)" by fast } thus "UNIV=(⋃n. B n)" by fast qed { fix j assume jS: "j ∈ S" note ms also from jS ABms have "⋀n. A j ∩ B n ∈ measurable_sets M" by auto moreover from Bun have "(λn. A j ∩ B n)↑(A j)" by (auto simp add: mon_conv_set_def) ultimately have "(λn. measure M (A j ∩ B n)) ⇢ measure M (A j)" by (rule measure_mon_conv) hence "(λn. a j * measure M (A j ∩ B n)) ⇢ a j * measure M (A j)" by (simp add: tendsto_const tendsto_mult) } hence "(λn. ∑j∈S. a j * measure M (A j ∩ B n)) ⇢ (∑j∈S. a j * measure M (A j))" by (rule tendsto_sum) hence "(λn. z* (∑j∈S. a j * measure M (A j ∩ B n))) ⇢ z*(∑j∈S. a j * measure M (A j))" by (simp add: tendsto_const tendsto_mult) with 1 xy base have "z*r ≤ y" by (auto simp add: LIMSEQ_le mon_conv_real_def) } hence zr: "⋀z. 0 < z ⟹ z < 1 ⟹ z * r ≤ y" . thus ?thesis by (rule real_le_mult_sustain) qed text ‹Now we are ready for the second step. The integral of a monotone limit of functions is the limit of their integrals. Note that this last limit has to exist in the first place, since we decided not to use infinite values. Backed by the last theorem and the preexisting knowledge about limits, the usual basic properties are straightforward.› inductive_set nnfis:: "('a ⇒ real) ⇒ ('a set set * ('a set ⇒ real)) ⇒ real set" for f :: "'a ⇒ real" and M :: "'a set set * ('a set ⇒ real)" where base: "⟦u↑f; ⋀n. x n ∈ sfis (u n) M; x↑y⟧ ⟹ y ∈ nnfis f M" lemma sfis_nnfis: assumes s: "a ∈ sfis f M" shows "a ∈ nnfis f M" (*<*)proof - { fix t have "(λn. f t)↑f t" by (simp add: mon_conv_real_def tendsto_const) } hence "(λn. f)↑f" by (simp add: realfun_mon_conv_iff) also from s have "⋀n. a ∈ sfis f M" . moreover have "(λn. a)↑a" by (simp add: mon_conv_real_def tendsto_const) ultimately show ?thesis by (rule nnfis.base) qed(*>*) lemma nnfis_times: assumes ms: "measure_space M" and a: "a ∈ nnfis f M" and nn: "0≤z" shows "z*a ∈ nnfis (λw. z*f w) M" (*<*)using a proof (cases) case (base u x) with nn have "(λm w. z*u m w)↑(λw. z*f w)" by (simp add: realfun_mon_conv_times) also from nn base have "⋀m. z*x m ∈ sfis (λw. z*u m w) M" by (simp add: sfis_times) moreover from a nn base have "(λm. z*x m)↑(z*a)" by (simp add: real_mon_conv_times) ultimately have "z*a ∈ nnfis (λw. z*f w) M" by (rule nnfis.base) with base show ?thesis by simp qed(*>*) lemma nnfis_add: assumes ms: "measure_space M" and a: "a ∈ nnfis f M" and b: "b ∈ nnfis g M" shows "a+b ∈ nnfis (λw. f w + g w) M" (*<*)using a proof (cases) case (base u x) note base_u = this from b show ?thesis proof cases case (base v r) with base_u have "(λm w. u m w + v m w)↑(λw. f w + g w)" by (simp add: realfun_mon_conv_add) also from ms base_u base have "⋀n. x n + r n ∈ sfis (λw. u n w + v n w) M" by (simp add: sfis_add) moreover from ms base_u base have "(λm. x m + r m)↑(a+b)" by (simp add: real_mon_conv_add) ultimately have "a+b ∈ nnfis (λw. f w + g w) M" by (rule nnfis.base) with a b show ?thesis by simp qed qed(*>*) lemma assumes ms: "measure_space M" and a: "a ∈ nnfis f M" and b: "b ∈ nnfis g M" and fg: "f≤g" shows nnfis_mono: "a ≤ b" using a proof (cases) case (base u x) note base_u = this from b show ?thesis proof (cases) case (base v r) { fix m from base_u base have "u m ≤ f" by (simp add: realfun_mon_conv_le) also note fg finally have "u m ≤ g" . with ms base_u base have "v↑g" and "⋀n. r n ∈ sfis (v n) M" and "r↑b" and "x m ∈ sfis (u m) M" and "u m ≤ g" and "measure_space M" by simp_all hence "x m ≤ b" by (rule sfis_mon_conv_mono) } with ms base_u base show "a ≤ b" by (auto simp add: mon_conv_real_def LIMSEQ_le_const2) qed qed corollary nnfis_unique: assumes ms: "measure_space M" and a: "a ∈ nnfis f M" and b: "b ∈ nnfis f M" shows "a=b" (*<*) proof - have "f≤f" .. with assms have "a≤b" and "b≤a" by (auto simp add: nnfis_mono) thus ?thesis by simp qed(*>*) text‹There is much more to prove about nonnegative integration. Next up is a classic theorem by Beppo Levi, the monotone convergence theorem. In essence, it says that the introduction rule for ‹nnfis› holds not only for sequences of simple functions, but for any sequence of nonnegative integrable functions. It should be mentioned that this theorem cannot be formulated for the Riemann integral. We prove it by exhibiting a sequence of simple functions that converges to the same limit as the original one and then applying the introduction rule. The construction and properties of the sequence are slightly intricate. By definition, for any $f_n$ in the original sequence, there is a sequence $(u_{m n})_{m\in\mathbb{N}}$ of simple functions converging to it. The $n$th element of the new sequence is the upper closure of the $n$th elements of the first $n$ sequences.› definition (*The upper closure?*) upclose:: "('a ⇒ real) ⇒ ('a ⇒ real) ⇒ ('a ⇒ real)" where "upclose f g = (λt. max (f t) (g t))" primrec mon_upclose_help :: "nat ⇒ (nat ⇒ nat ⇒ 'a ⇒ real) ⇒ nat ⇒ ('a ⇒ real)" ("muh") where "muh 0 u m = u m 0" | "muh (Suc n) u m = upclose (u m (Suc n)) (muh n u m)" definition mon_upclose (*See Bauer p. 68*) :: "(nat ⇒ nat ⇒ 'a ⇒ real) ⇒ nat ⇒ ('a ⇒ real)" ("mu") where "mu u m = muh m u m" lemma sf_norm_help: assumes fin: "finite K" and jK: "j ∈ K" and tj: "t ∈ C j" and iK: "∀i∈K-{j}. t ∉ C i" shows "(∑i∈K. (z i) * χ (C i) t) = z j" (*<*)proof - from jK have "K = insert j (K-{j})" by blast moreover from fin have finat2: "finite (K-{j})" and "j ∉ (K-{j})" by simp_all hence "(∑i∈insert j (K-{j}). (z i) * χ (C i) t) = (z j * χ (C j) t) + (∑i∈K-{j}. (z i) * χ (C i) t)" by (rule sum.insert) moreover from tj have "… = z j + (∑i∈K-{j}. (z i) * χ (C i) t)" by (simp add: characteristic_function_def) moreover { from iK have "∀i∈K-{j}. (z i) * χ (C i) t = 0" by (auto simp add: characteristic_function_def) } hence "… = z j" by (simp add:sum.neutral) ultimately show ?thesis by simp qed(*>*) lemma upclose_sfis: assumes ms: "measure_space M" and f: "a ∈ sfis f M" and g: "b ∈ sfis g M" shows "∃c. c ∈ sfis (upclose f g) M" (*<*) proof - from assms have "∃ z1 z2 C K. f = (λt. ∑i∈(K::nat set). z1 i * χ (C i) t) ∧ g = (λt. ∑i∈K. z2 i * χ (C i) t) ∧ a = (∑i∈K. z1 i * measure M (C i)) ∧ b = (∑i∈K. z2 i * measure M (C i)) ∧ finite K ∧ (∀i∈K. ∀j∈K. i ≠ j ⟶ C i ∩ C j = {}) ∧ (∀i ∈ K. C i ∈ measurable_sets M) ∧ (⋃i∈K. C i) = UNIV ∧ nonnegative z1 ∧ nonnegative z2" by (rule sfis_present) then obtain z1 z2 C K where f: "f = (λt. ∑i∈(K::nat set). z1 i * χ (C i) t)" and g: "g = (λt. ∑i∈K. z2 i * χ (C i) t)" and a2: "a = (∑i∈K. z1 i * measure M (C i))" and b2: "b = (∑i∈K. z2 i * measure M (C i))" and CK: "finite K ∧ (∀i∈K. ∀j∈K. i ≠ j ⟶ C i ∩ C j = {}) ∧ (∀i∈K. C i ∈ measurable_sets M) ∧ ⋃(C ` K) = UNIV" and z1: "nonnegative z1" and z2: "nonnegative z2" by auto { fix t from CK obtain j where jK: "j ∈ K" and tj: "t ∈ C j" by force with CK have iK: "∀i∈K-{j}. t ∉ C i" by auto from f and g have "max (f t) (g t) = max (∑i∈K. (z1 i) * χ (C i) t) (∑i∈K. (z2 i) * χ (C i) t)" by simp also from CK jK iK tj have "… = max (z1 j) (z2 j)" by (simp add: sf_norm_help) also from CK jK iK tj have "… = (∑i∈K. (max (z1 i) (z2 i)) * χ (C i) t)" by (simp add: sf_norm_help) finally have "max (f t) (g t) = (∑i∈K. max (z1 i) (z2 i) * χ (C i) t)" . } hence "upclose f g = (λt. (∑i∈K. max (z1 i) (z2 i) * χ (C i) t))" by (simp add: upclose_def) also { from z1 z2 have "nonnegative (λi. max (z1 i) (z2 i))" by (simp add: nonnegative_def max_def) } with ms CK have "(∑i∈K. max (z1 i) (z2 i) * measure M (C i)) ∈ sfis … M" by (simp add: sfis_intro) ultimately show ?thesis by auto qed(*>*) lemma mu_sfis: assumes u: "⋀m n. ∃a. a ∈ sfis (u m n) M" and ms: "measure_space M" shows "∃c. ∀m. c m ∈ sfis (mu u m) M" (*<*)proof - { fix m from u ms have "⋀n. ∃c. c ∈ sfis (muh m u n) M" proof (induct m) case 0 from u show ?case by force next case (Suc m) { fix n from Suc obtain a b where "a ∈ sfis (muh m u n) M" and "b ∈ sfis (u n (Suc m)) M" by force with ms u have "∃a. a ∈ sfis (muh (Suc m) u n) M" by (simp add: upclose_sfis) } thus ?case by force qed hence "∃c. c ∈ sfis (mu u m) M" by (simp add: mon_upclose_def) } hence "∀m. ∃c. c ∈ sfis (mu u m) M" by simp thus ?thesis by (rule choice) qed(*>*) lemma mu_help: assumes uf: "⋀n. (λm. u m n)↑(f n)" and fh: "f↑h" shows "(mu u)↑h" and "⋀n. mu u n ≤ f n" proof - show mu_le: "⋀n. mu u n ≤ f n" proof (unfold mon_upclose_def) fix n show "⋀m. muh n u m ≤ f n" proof (induct n) case (0 m) from uf have "u m 0 ≤ f 0" by (rule realfun_mon_conv_le) thus ?case by simp next case (Suc n m) { fix t from Suc have "muh n u m t ≤ f n t" by (simp add: le_fun_def) also from fh have "f n t ≤ f (Suc n) t" by (simp add: realfun_mon_conv_iff mon_conv_real_def) also from uf have "(λm. u m (Suc n) t)↑(f (Suc n) t)" by (simp add: realfun_mon_conv_iff) hence "u m (Suc n) t ≤ f (Suc n) t" by (rule real_mon_conv_le) ultimately have "muh (Suc n) u m t ≤ f (Suc n) t" by (simp add: upclose_def) } thus ?case by (simp add: le_fun_def) qed qed (*isotony (?) of mu u is next to prove*) { fix t { fix m n have "muh n u m t ≤ muh (Suc n) u m t" by (simp add: upclose_def) } hence pos1: "⋀m n. muh n u m t ≤ muh (Suc n) u m t" . from uf have uiso: "⋀m n. u m n t ≤ u (Suc m) n t" by (simp add: realfun_mon_conv_iff mon_conv_real_def) have iso: "⋀n. mu u n t ≤ mu u (Suc n) t" proof (unfold mon_upclose_def) fix n have "⋀m. muh n u m t ≤ muh n u (Suc m) t" proof (induct n) case 0 from uiso show ?case by (simp add: upclose_def le_max_iff_disj) next case (Suc n m) from Suc have "muh n u m t ≤ muh n u (Suc m) t" . also from uiso have "u m (Suc n) t ≤ u (Suc m) (Suc n) t" . ultimately show ?case by (auto simp add: upclose_def le_max_iff_disj) qed note this [of n] also note pos1 [of n "Suc n"] finally show "muh n u n t ≤ muh (Suc n) u (Suc n) t" . qed also { fix n from mu_le [of n] have "mu u n t ≤ f n t" by (simp add: le_fun_def) also from fh have "(λn. f n t)↑h t" by (simp add: realfun_mon_conv_iff) hence "f n t ≤ h t" by (rule real_mon_conv_le) finally have "mu u n t ≤ h t" . } ultimately have "∃l. (λn. mu u n t)↑l ∧ l ≤ h t" by (rule real_mon_conv_bound) then obtain l where conv: "(λn. mu u n t)↑l" and lh: "l ≤ h t" by (force simp add: real_mon_conv_bound) { fix n::nat { fix m assume le: "n ≤ m" hence "u m n t ≤ mu u m t" proof (unfold mon_upclose_def) have "u m n t ≤ muh n u m t" by (induct n) (auto simp add: upclose_def le_max_iff_disj) also from pos1 have "incseq (λn. muh n u m t)" by (simp add: incseq_Suc_iff) hence "muh n u m t ≤ muh (n+(m-n)) u m t" unfolding incseq_def by simp with le have "muh n u m t ≤ muh m u m t" by simp finally show "u m n t ≤ muh m u m t" . qed } hence "∃N. ∀m. N ≤ m ⟶ u m n t ≤ mu u m t" by blast also from uf have "(λm. u m n t) ⇢ f n t" by (simp add: realfun_mon_conv_iff mon_conv_real_def) moreover from conv have "(λn. mu u n t) ⇢ l" by (simp add: mon_conv_real_def) ultimately have "f n t ≤ l" by (simp add: LIMSEQ_le) } also from fh have "(λn. f n t) ⇢ h t" by (simp add: realfun_mon_conv_iff mon_conv_real_def) ultimately have "h t ≤ l" by (simp add: LIMSEQ_le_const2) with lh have "l = h t" by simp with conv have "(λn. mu u n t)↑(h t)" by simp } with mon_upclose_def show "mu u↑h" by (simp add: realfun_mon_conv_iff) qed (* The Beppo Levi - Theorem *) theorem nnfis_mon_conv: assumes fh: "f↑h" and xf: "⋀n. x n ∈ nnfis (f n) M" and xy: "x↑y" and ms: "measure_space M" shows "y ∈ nnfis h M" proof - define u where "u n = (SOME u. u↑(f n) ∧ (∀m. ∃a. a ∈ sfis (u m) M))" for n { fix n from xf[of n] have "∃u. u↑(f n) ∧ (∀m. ∃a. a ∈ sfis (u m) M)" (is "∃x. ?P x") proof (cases) case (base r a) hence "r↑(f n)" and "⋀m. ∃a. a ∈ sfis (r m) M" by auto thus ?thesis by fast qed hence "?P (SOME x. ?P x)" by (rule someI_ex) with u_def have "?P (u n)" by simp } also define urev where "urev m n = u n m" for m n ultimately have uf: "⋀n. (λm. urev m n)↑(f n)" and sf: "⋀n m. ∃a. a ∈ sfis (urev m n) M" by auto from uf fh have up: "mu urev↑h" by (rule mu_help) (*Could split the mu_help lemma in two*) from uf fh have le: "⋀n. mu urev n ≤ f n" by (rule mu_help) from sf ms obtain c where sf2: "⋀m. c m ∈ sfis (mu urev m) M" by (force simp add: mu_sfis) { fix m from sf2 have "c m ∈ nnfis (mu urev m) M" by (rule sfis_nnfis) with ms le[of m] xf[of m] have "c m ≤ x m" by (simp add: nnfis_mono) } hence "c ≤ x" by (simp add: le_fun_def) also { fix m note ms also from up have "mu urev m ≤ mu urev (Suc m)" by (simp add: mon_conv_real_fun_def) moreover from sf2 have "c m ∈ sfis (mu urev m) M" and "c (Suc m) ∈ sfis (mu urev (Suc m)) M" by fast+ ultimately have "c m ≤ c (Suc m)" by (simp add: sfis_mono) } moreover note xy ultimately have "∃l. c↑l ∧ l ≤ y" by (simp add: real_mon_conv_dom) then obtain l where cl: "c↑l" and ly: "l ≤ y" by fast from up sf2 cl have int: "l ∈ nnfis h M" by (rule nnfis.base) { fix n from fh have "f n ≤ h" by (rule realfun_mon_conv_le) with ms xf[of n] int have "x n ≤ l" by (rule nnfis_mono) } with xy have "y ≤ l" by (auto simp add: mon_conv_real_def LIMSEQ_le_const2) with ly have "l=y" by simp with int show ?thesis by simp qed text‹Establishing that only nonnegative functions may arise this way is a triviality.› lemma nnfis_nn: assumes "a ∈ nnfis f M" shows "nonnegative f" (*<*)using assms proof cases case (base u x) {fix t { fix n from base have "x n ∈ sfis (u n) M" by fast hence "nonnegative (u n)" by (rule sfis_nn) hence "0 ≤ u n t" by (simp add: nonnegative_def) } also from base have "(λn. u n t)⇢f t" by (simp add: realfun_mon_conv_iff mon_conv_real_def) ultimately have "0 ≤ f t" by (simp add: LIMSEQ_le_const) } thus ?thesis by (simp add: nonnegative_def) qed(*>*)(*>*) subsection ‹Integrable Functions› text‹ Before we take the final step of defining integrability and the integral operator, we should first clarify what kind of functions we are able to integrate up to now. It is easy to see that all nonnegative integrable functions are random variables.› lemma assumes (*<*)ms:(*>*) "measure_space M" and (*<*)f:(*>*) "a ∈ nnfis f M" shows nnfis_rv: "f ∈ rv M" (*<*)using f proof (cases) case (base u x) { fix n from base have "x n ∈ sfis (u n) M" by simp with ms have "u n ∈ rv M" by (simp add: sfis_rv) } also from base have "u↑f" by simp ultimately show ?thesis by (rule mon_conv_rv) qed(*>*) text‹The converse does not hold of course, since there are measurable functions whose integral is infinite. Regardless, it is possible to approximate any measurable function using simple step-functions. This means that all nonnegative random variables are quasi integrable, as the property is sometimes called, and brings forth the fundamental insight that a nonnegative function is integrable if and only if it is measurable and the integrals of the simple functions that approximate it converge monotonically. Technically, the proof is rather complex, involving many properties of real numbers.›(*<*) declare zero_le_power [simp] (*>*) lemma assumes (*<*)ms:(*>*) "measure_space M" and (*<*)f(*>*): "f ∈ rv M" and (*<*)nn:(*>*) "nonnegative f" shows rv_mon_conv_sfis: "∃u x. u↑f ∧ (∀n. x n ∈ sfis (u n) M)" (*<*)proof (rule+) (*We don't need the greater case in the book, since our functions are real*) define A where "A n i = {w. real i/(2::real)^n ≤ f w} ∩ {w. f w < real (Suc i)/(2::real)^n}" for n i define u where "u n t = (∑i∈{..<(n*2^n)}-{0}. (real i/(2::real)^n)*χ (A n i) t)" for n t define x where "x n = (∑i∈{..<(n*2^n)}-{0}. (real i/(2::real)^n)*measure M (A n i))" for n { fix n note ms also { fix i::nat from ms f have "{w. real i/(2::real)^n ≤ f w} ∈ measurable_sets M" by (simp_all add: rv_ge_iff) also from ms f have "{w. f w < real (Suc i)/(2::real)^n} ∈ measurable_sets M" by (simp add: rv_less_iff) moreover note ms ultimately have "A n i ∈ measurable_sets M" by (simp add: A_def measure_space_def sigma_algebra_inter) } hence "∀i∈{..<(n*2^n)}-{0}. A n i ∈ measurable_sets M" by fast moreover { fix i::nat have "0 ≤ real i" by simp also have "0 ≤ (2::real)^n" by simp ultimately have "0 ≤ real i/(2::real)^n" by (simp add: zero_le_divide_iff) } hence "nonnegative (λi::nat. real i/(2::real)^n)" by (simp add: nonnegative_def) (* This is a little stronger than it has to be, btw.. x i must only be nn for i in S *) moreover have "finite ({..<(n*2^n)}-{0})" by simp ultimately have "x n ∈ sfis (u n) M" by (simp only: u_def [abs_def] x_def sfis_intro) } thus "∀n. x n ∈ sfis (u n) M" by simp show "u↑f" proof - { fix t { fix m i assume tai: "t ∈ A m i" and iS: "i ∈ {..<(m*2^m)}" have usum: "u m t = (∑j∈{..<(m*2^m)}-{0}. real j / (2::real)^m * χ (A m j) t)" by (simp add: u_def) { fix j assume ne: "i ≠ j" have "t ∉ A m j" proof (cases "i < j") case True from tai have "f t < real (Suc i) / (2::real)^m" by (simp add: A_def) also from True have "real (Suc i)/(2::real)^m ≤ real j/(2::real)^m" by (simp add: divide_inverse) finally show ?thesis by (simp add: A_def) next case False with ne have no: "j<i" by arith hence "real (Suc j)/(2::real)^m ≤ real i/(2::real)^m" by (simp add: divide_inverse) also from tai have "real i / (2::real)^m ≤ f t" by (simp add: A_def) finally show ?thesis by (simp add: A_def order_less_le) qed } hence "⋀j. i ≠ j ⟹ χ (A m j) t = 0" by (simp add: characteristic_function_def) hence "⋀j. j∈{..<(m*2^m)}-{0}-{i} ⟹ real j / (2::real)^m * χ (A m j) t = 0" by force with refl have "(∑j∈{..<(m*2^m)}-{0}-{i}. real j / (2::real)^m * χ (A m j) t) = (∑j∈{..<(m*2^m)}-{0}-{i}. 0)" by (rule sum.cong) also have "… = 0" by (rule sum.neutral_const) finally have sum0: "(∑j∈{..<(m*2^m)}-{0}-{i}. real j / (2::real)^m * χ (A m j) t) = 0" . have "u m t = real i / (2::real)^m" proof (cases "i=0") case True hence "i ∉ {..<(m*2^m)}-{0}" by simp hence "{..<(m*2^m)}-{0} = {..<(m*2^m)}-{0}-{i}" by simp with usum sum0 have "u m t = 0" by simp also from True have "… = real i / (2::real)^m * χ (A m i) t" by simp finally show ?thesis using tai by (simp add: characteristic_function_def) next case False with iS have iS: "i ∈ {..<(m*2^m)}-{0}" by simp note usum also have fin: "finite ({..<(m*2^m)}-{0}-{i})" by simp from iS have ins: "{..<(m*2^m)}-{0} = insert i ({..<(m*2^m)}-{0}-{i})" by auto have "i ∉ ({..<(m*2^m)}-{0}-{i})" by simp with fin have "(∑j∈insert i ({..<(m*2^m)}-{0}-{i}). real j / (2::real)^m * χ (A m j) t) = real i / (2::real)^m * χ (A m i) t + (∑j∈{..<(m*2^m)}-{0}-{i}. real j / (2::real)^m * χ (A m j) t)" by (rule sum.insert) with ins tai have "(∑j∈{..<(m*2^m)}-{0}. real j / (2::real)^m * χ (A m j) t) = real i / (2::real)^m + (∑j∈{..<(m*2^m)}-{0}-{i}. real j / (2::real)^m * χ (A m j) t)" by (simp add: characteristic_function_def) also note sum0 finally show ?thesis by simp qed } hence disj: "⋀m i. ⟦t ∈ A m i; i ∈ {..<m * 2 ^ m}⟧ ⟹ u m t = real i / (2::real)^m" . { fix n define a where "a = (f t)*(2::real)^n" define i where "i = (LEAST i. a < real (i::nat)) - 1" from nn have "0 ≤ a" by (simp add: zero_le_mult_iff a_def nonnegative_def) also have "∃i. a < real (i::nat)" by (rule reals_Archimedean2) then obtain k where "a < real (k::nat)" by fast hence less: "a < real (LEAST i. a < real (i::nat))" by (rule LeastI) finally have "0 < (LEAST i. a < real (i::nat))" by simp hence min: "(LEAST i. a < real (i::nat)) - 1 < (LEAST i. a < real (i::nat))" by arith hence "¬ (a < real ((LEAST i. a < real (i::nat)) - 1))" by (rule not_less_Least) hence ia: "real i ≤ a" by (auto simp add: i_def order_less_le) from min less have ai: "a < real (Suc i)" by (simp add: i_def) from ia have ia2: "real i / (2::real)^n ≤ f t" by (simp add: a_def pos_divide_le_eq) also from ai have ai2: "f t < real (Suc i) / (2::real)^n" by (simp add: a_def pos_less_divide_eq[THEN sym]) ultimately have tA: "t ∈ A n i" by (simp add: A_def) { assume ftn: "f t < real n" from ia a_def have "real i ≤ f t * (2::real)^n" by simp also from ftn have "f t * (2::real)^n < real n * (2::real)^n" by simp finally have ni: "i < n * 2 ^ n" by (simp add: of_nat_less_iff[symmetric, where 'a=real]) with tA have un: "u n t = real i / (2::real)^n" using disj by simp with ia2 have lef: "u n t ≤ f t" by simp from un have "real (i+1) / (2::real)^n = (real i + real (1::nat))/(2::real)^n" by (simp only: of_nat_add) with un ai2 have fless: "f t < u n t + 1/(2::real)^n" by (simp add: add_divide_distrib) have uSuc: "u n t ≤ u (Suc n) t" proof (cases "f t < real (2*i+1) / (2*(2::real)^n)") case True from ia2 have "real (2*i)/(2::real)^(n+1) ≤ f t" by simp with True have tA2: "t ∈ A (n+1) (2*i)" by (simp add: A_def) from ni have "2*i < (n+1)*(2^(n+1))" by simp with tA2 have "u (n+1) t = real i / (2::real)^n" using disj by simp with un show ?thesis by simp next case False have "(2::real) ≠ 0" by simp hence "real (2*(Suc i)) / ((2::real)^(Suc n)) = real (Suc i) / (2::real)^n" by (metis mult_divide_mult_cancel_left_if power_Suc of_nat_mult of_nat_numeral) with ai2 have "f t < real (2*(Suc i)) / (2::real)^(n+1)" by simp with False have tA2: "t ∈ A (n+1) (2*i+1)" by (simp add: A_def) from ni have "2*i+1 < (n+1)*(2^(n+1))" by simp with tA2 have "u (Suc n) t = real (2*i+1) / (2 * (2::real)^n)" using disj by simp also have "… = (real (2*i) + real (1::nat))/ (2 * (2::real)^n)" by (simp only: of_nat_add) also have "… = real i / (2::real)^n + real (1::nat) / (2 * (2::real)^n)" by (simp add: add_divide_distrib) finally show ?thesis using un by (simp add: zero_le_divide_iff) qed note this lef fless } hence uSuc: "f t < real n ⟹ u n t ≤ u (Suc n) t" and lef: "f t < real n ⟹ u n t ≤ f t" and fless:"f t < real n ⟹ f t < u n t + 1 / (2::real)^n" by auto have "u n t ≤ u (Suc n) t" proof (cases "real n ≤ f t") case True { fix i assume "i ∈ {..<(n*2^n)}-{0}" hence "Suc i ≤ n*2^n" by simp hence mult: "real (Suc i) ≤ real n * (2::real)^n" by (simp add: of_nat_le_iff[symmetric, where 'a=real]) have "0 < (2::real)^n" by simp with mult have "real (Suc i) / (2::real)^n ≤ real n" by (simp add: pos_divide_le_eq) also note True finally have "¬ f t < real (Suc i) / (2::real)^n" by (simp add: order_less_le) hence "t ∉ A n i" by (simp add: A_def) hence "(real i/(2::real)^n)*χ (A n i) t = 0" by (simp add: characteristic_function_def) } with refl have "(∑i∈{..<n * 2 ^ n} - {0}. real i / (2::real)^n * χ (A n i) t) = (∑i∈{..<n * 2 ^ n} - {0}. 0)" by (rule sum.cong) hence "u n t = 0" by (simp add: u_def) also { fix m have "0 ≤ u m t" by (simp add: u_def characteristic_function_def zero_le_divide_iff sum_nonneg) } hence "0 ≤ u (Suc n) t" . finally show ?thesis . next case False with uSuc show ?thesis by simp qed note this lef fless } hence uSuc: "⋀n. u n t ≤ u (Suc n) t" and lef: "⋀n. f t < real n ⟹ u n t ≤ f t" and fless:"⋀n. f t < real n ⟹ f t < u n t + 1 / (2::real)^n" by auto have "∃n0::nat. f t < real n0" by (rule reals_Archimedean2) then obtain n0::nat where "f t < real n0" .. also have "⋀n. real n0 ≤ real (n+n0)" by simp finally have pro: "⋀n. f t < real (n + n0)" . hence 2: "⋀n. u (n+n0) t ≤ f t" using lef by simp from uSuc have 1: "⋀n. u (n+n0) t ≤ u (Suc n + n0) t" by simp from 1 2 have "∃c. (λn. u (n+n0) t)↑c ∧ c ≤ f t" by (rule real_mon_conv_bound) with uSuc obtain c where n0mc: "(λn. u (n+n0) t)↑c" and cle: "c ≤ f t" by fast from n0mc have "(λn. u (n+n0) t) ⇢ c" by (simp add: mon_conv_real_def) hence lim: "(λn. u n t) ⇢ c" by (subst limseq_shift_iff[THEN sym]) have "∀y. ∃N. ∀n. N ≤ n ⟶ y < (2::real)^n" proof fix y::real have "∃N::nat. y < real N" by (rule reals_Archimedean2) then obtain N::nat where 1: "y < real N" by fast { fix n::nat note 1 also assume "N ≤ n" also have "real n < (2::real)^n" by (rule of_nat_less_two_power) finally have "y < 2 ^ n" by simp } thus "∃N. ∀n. N ≤ n ⟶ y < (2::real)^n" by blast qed hence "(λn. inverse ((2::real)^n)) ⇢ 0" by (intro LIMSEQ_inverse_zero) auto with lim have "(λn. u n t + inverse ((2::real)^n)) ⇢ c+0" by (rule tendsto_add) hence "(λn. u n t + 1/(2::real)^n) ⇢ c" by (simp add: divide_inverse) hence "(λn. u (n+n0) t + 1/(2::real)^(n+n0)) ⇢ c" by (subst limseq_shift_iff) also from pro fless have "⋀n. f t ≤ u (n+n0) t + 1 / 2 ^ (n+n0)" by (simp add: order_le_less) ultimately have "f t ≤ c" by (simp add: LIMSEQ_le_const) with cle have "c = f t" by simp with lim have "(λn. u n t) ⇢ f t" by simp with uSuc have "(λn. u n t)↑ f t" by (simp add: mon_conv_real_def) } thus ?thesis by (simp add: realfun_mon_conv_iff) qed qed(*>*) text‹The following dominated convergence theorem is an easy corollary. It can be effectively applied to show integrability.› corollary assumes ms: "measure_space M" and f: "f ∈ rv M" and b: "b ∈ nnfis g M" and fg: "f≤g" and nn: "nonnegative f" shows nnfis_dom_conv: "∃a. a ∈ nnfis f M ∧ a ≤ b" using b proof (cases) case (base v r) from ms f nn have "∃u x. u↑f ∧ (∀n. x n ∈ sfis (u n) M)" by (rule rv_mon_conv_sfis) then obtain u x where uf: "u↑f" and xu: "⋀n. x n ∈ sfis (u n) M" by fast { fix n from uf have "u n ≤ f" by (rule realfun_mon_conv_le) also note fg also from xu have "x n ∈ nnfis (u n) M" by (rule sfis_nnfis) moreover note b ms ultimately have le: "x n ≤ b" by (simp add: nnfis_mono) from uf have "u n ≤ u (Suc n)" by (simp only: mon_conv_real_fun_def) with ms xu[of n] xu[of "Suc n"] have "x n ≤ x (Suc n)" by (simp add: sfis_mono) note this le } hence "∃a. x↑a ∧ a ≤ b" by (rule real_mon_conv_bound) then obtain a where xa: "x↑a" and ab: "a ≤ b" by auto from uf xu xa have "a ∈ nnfis f M" by (rule nnfis.base) with ab show ?thesis by fast qed text‹Speaking all the time about integrability, it is time to define it at last.› definition integrable:: "('a ⇒ real) ⇒ ('a set set * ('a set ⇒ real)) ⇒ bool" where (*We could also demand that f be in rv M, but measurability is already ensured by construction of the integral/nn_integrable functions*) "integrable f M ⟷ measure_space M ∧ (∃x. x ∈ nnfis (pp f) M) ∧ (∃y. y ∈ nnfis (np f) M)" definition integral:: "('a ⇒ real) ⇒ ('a set set * ('a set ⇒ real)) ⇒ real" ("∫ _ ∂_"(*<*)[60,61] 110(*>*)) where "integrable f M ⟹ ∫ f ∂M = (THE i. i ∈ nnfis (pp f) M) - (THE j. j ∈ nnfis (np f) M)" text‹So the final step is done, the integral defined. The theorems we are already used to prove from the earlier stages are still missing. Only now there are always two properties to be shown: integrability and the value of the integral. Isabelle makes it possible two have both goals in a single theorem, so that the user may derive the statement he desires. Two useful lemmata follow. They help lifting nonnegative function integral sets to integrals proper. Notice how the dominated convergence theorem from above is employed in the latter.› lemma nnfis_integral: assumes nn: "a ∈ nnfis f M" and ms: "measure_space M" shows "integrable f M" and "∫ f ∂ M = a" proof - from nn have "nonnegative f" by (rule nnfis_nn) hence "pp f = f" and 0: "np f = (λt. 0)" by (auto simp add: nn_pp_np) with nn have a: "a ∈ nnfis (pp f) M" by simp have "0≤(0::real)" by (rule order_refl) with ms nn have "0*a ∈ nnfis (λt. 0*f t) M" by (rule nnfis_times) with 0 have 02: "0 ∈ nnfis (np f) M" by simp with ms a show "integrable f M" by (auto simp add: integrable_def) also from a ms have "(THE i. i ∈ nnfis (pp f) M) = a" by (auto simp add: nnfis_unique) moreover from 02 ms have "(THE i. i ∈ nnfis (np f) M) = 0" by (auto simp add: nnfis_unique) ultimately show "∫ f ∂ M = a" by (simp add: integral_def) qed lemma nnfis_minus_nnfis_integral: assumes a: "a ∈ nnfis f M" and b: "b ∈ nnfis g M" and ms: "measure_space M" shows "integrable (λt. f t - g t) M" and "∫ (λt. f t - g t) ∂ M = a - b" proof - from ms a b have "(λt. f t - g t) ∈ rv M" by (auto simp only: nnfis_rv rv_minus_rv) hence prv: "pp (λt. f t - g t) ∈ rv M" and nrv: " np (λt. f t - g t) ∈ rv M" by (auto simp only: pp_np_rv) have nnp: "nonnegative (pp (λt. f t - g t))" and nnn: "nonnegative (np (λt. f t - g t))" by (simp_all add: nonnegative_def positive_part_def negative_part_def) from ms a b have fg: "a+b ∈ nnfis (λt. f t + g t) M" by (rule nnfis_add) from a b have nnf: "nonnegative f" and nng: "nonnegative g" by (simp_all only: nnfis_nn) { fix t from nnf nng have "0 ≤ f t" and "0 ≤ g t" by (simp_all add: nonnegative_def) hence "(pp (λt. f t - g t)) t ≤ f t + g t" and "(np (λt. f t - g t)) t ≤ f t + g t" by (simp_all add: positive_part_def negative_part_def) } hence "(pp (λt. f t - g t)) ≤ (λt. f t + g t)" and "(np (λt. f t - g t)) ≤ (λt. f t + g t)" by (simp_all add: le_fun_def) with fg nnf nng prv nrv nnp nnn ms have "∃l. l ∈ nnfis (pp (λt. f t - g t)) M ∧ l ≤ a+b" and "∃k. k ∈ nnfis (np (λt. f t - g t)) M ∧ k ≤ a+b" by (auto simp only: nnfis_dom_conv) then obtain l k where l: "l ∈ nnfis (pp (λt. f t - g t)) M" and k: "k ∈ nnfis (np (λt. f t - g t)) M" by auto with ms show i: "integrable (λt. f t - g t) M" by (auto simp add: integrable_def) { fix t have "f t - g t = (pp (λt. f t - g t)) t - (np (λt. f t - g t)) t" by (rule f_plus_minus) hence "f t + (np (λt. f t - g t)) t = g t + (pp (λt. f t - g t)) t" by arith } hence "(λt. f t + (np (λt. f t - g t)) t) = (λt. g t + (pp (λt. f t - g t)) t)" by (rule ext) also from ms a k b l have "a+k ∈ nnfis (λt. f t + (np (λt. f t - g t)) t) M" and "b+l ∈ nnfis (λt. g t + (pp (λt. f t - g t)) t) M" by (auto simp add: nnfis_add) moreover note ms ultimately have "a+k = b+l" by (simp add: nnfis_unique) hence "l-k=a-b" by arith also from k l ms have "(THE i. i ∈ nnfis (pp (λt. f t - g t)) M) = l" and "(THE i. i ∈ nnfis (np (λt. f t - g t)) M) = k" by (auto simp add: nnfis_unique) moreover note i ultimately show "∫ (λt. f t - g t) ∂ M = a - b" by (simp add: integral_def) qed text‹Armed with these, the standard integral behavior should not be hard to derive. Mind that integrability always implies a measure space, just like random variables did in \ref{sec:realrandvar}.› theorem assumes (*<*)int:(*>*) "integrable f M" shows integrable_rv: "f ∈ rv M" (*<*)proof - from int have "pp f ∈ rv M ∧ np f ∈ rv M" by (auto simp add: integrable_def nnfis_rv) thus ?thesis by (simp add: pp_np_rv_iff[THEN sym]) qed(*>*) theorem integral_char: assumes ms: "measure_space M" and mA: "A ∈ measurable_sets M" shows "∫ χ A ∂ M = measure M A" and "integrable χ A M" (*<*)proof - from ms mA have "measure M A ∈ sfis χ A M" by (rule sfis_char) hence nnfis: "measure M A ∈ nnfis χ A M" by (rule sfis_nnfis) from this and ms show "∫ χ A ∂ M = measure M A" by (rule nnfis_integral) from nnfis and ms show "integrable χ A M" by (rule nnfis_integral) qed(*>*) theorem integral_add: assumes f: "integrable f M" and g: "integrable g M" shows "integrable (λt. f t + g t) M" and "∫ (λt. f t + g t) ∂M = ∫ f ∂M + ∫ g ∂M" proof - define u where "u = (λt. pp f t + pp g t)" define v where "v = (λt. np f t + np g t)" from f obtain pf nf where pf: "pf ∈ nnfis (pp f) M" and nf: "nf ∈ nnfis (np f) M" and ms: "measure_space M" by (auto simp add: integrable_def) from g obtain pg ng where pg: "pg ∈ nnfis (pp g) M" and ng: "ng ∈ nnfis (np g) M" by (auto simp add: integrable_def) from ms pf pg u_def have u: "pf+pg ∈ nnfis u M" by (simp add: nnfis_add) from ms nf ng v_def have v: "nf+ng ∈ nnfis v M" by (simp add: nnfis_add) { fix t from u_def v_def have "f t + g t = u t - v t" by (simp add: positive_part_def negative_part_def) } hence uvf: "(λt. u t - v t) = (λt. f t + g t)" by (simp add: ext) from u v ms have "integrable (λt. u t - v t) M" by (rule nnfis_minus_nnfis_integral) with u_def v_def uvf show "integrable (λt. f t + g t) M" by simp from pf nf ms have "∫ (λt. pp f t - np f t) ∂M = pf-nf" by (rule nnfis_minus_nnfis_integral) hence "∫ f ∂M = pf-nf" by (simp add: f_plus_minus[THEN sym]) also from pg ng ms have "∫ (λt. pp g t - np g t) ∂M = pg-ng" by (rule nnfis_minus_nnfis_integral) hence "∫ g ∂M = pg-ng" by (simp add: f_plus_minus[THEN sym]) moreover from u v ms have "∫ (λt. u t - v t) ∂M = pf + pg - (nf + ng)" by (rule nnfis_minus_nnfis_integral) with uvf have "∫ (λt. f t + g t) ∂M = pf-nf + pg-ng" by simp ultimately show "∫ (λt. f t + g t) ∂M = ∫ f ∂M + ∫ g ∂M" by simp qed theorem integral_mono: assumes f: "integrable f M" and g: "integrable g M" and fg: "f≤g" shows "∫ f ∂M ≤ ∫ g ∂M" proof - from f obtain pf nf where pf: "pf ∈ nnfis (pp f) M" and nf: "nf ∈ nnfis (np f) M" and ms: "measure_space M" by (auto simp add: integrable_def) from g obtain pg ng where pg: "pg ∈ nnfis (pp g) M" and ng: "ng ∈ nnfis (np g) M" by (auto simp add: integrable_def) { fix t from fg have "f t ≤ g t" by (simp add: le_fun_def) hence "pp f t ≤ pp g t" and "np g t ≤ np f t" by (auto simp add: positive_part_def negative_part_def) } hence "pp f ≤ pp g" and "np g ≤ np f" by (simp_all add: le_fun_def) with ms pf pg ng nf have "pf ≤ pg" and "ng ≤ nf" by (simp_all add: nnfis_mono) also from ms pf pg ng nf have "(THE i. i ∈ nnfis (pp f) M) = pf" and "(THE i. i ∈ nnfis (np f) M) = nf" and "(THE i. i ∈ nnfis (pp g) M) = pg" and "(THE i. i ∈ nnfis (np g) M) = ng" by (auto simp add: nnfis_unique) with f g have "∫ f ∂M = pf - nf" and "∫ g ∂M = pg - ng" by (auto simp add: integral_def) ultimately show ?thesis by simp qed theorem integral_times: assumes int: "integrable f M" shows "integrable (λt. a*f t) M" and "∫ (λt. a*f t) ∂M = a*∫ f ∂M" (*<*)proof - from int have "∫ f ∂M = (THE i. i ∈ nnfis (pp f) M) - (THE j. j ∈ nnfis (np f) M)" by (simp only: integral_def) also from int obtain k l where k: "k ∈ nnfis (pp f) M" and l: "l ∈ nnfis (np f) M" and ms: "measure_space M" by (auto simp add: integrable_def) from k l ms have "(THE i. i ∈ nnfis (pp f) M) = k" and "(THE i. i ∈ nnfis (np f) M) = l" by (auto simp add: nnfis_unique) with int have uni: "k-l = ∫ f ∂M" by (simp add: integral_def) have "integrable (λt. a*f t) M ∧ ∫ (λt. a*f t) ∂M = a*∫ f ∂M" proof (cases "0≤a") case True hence pp: "pp (λt. a * f t) = (λt. a * pp f t)" and np: "np (λt. a * f t) = (λt. a * np f t)" by (auto simp add: real_pp_np_pos_times) from ms k True have "a*k ∈ nnfis (λt. a * pp f t) M" by (rule nnfis_times) with pp have 1: "a*k ∈ nnfis (pp (λt. a * f t)) M" by simp from np ms l True have 2: "a*l ∈ nnfis (np (λt. a * f t)) M" by (simp add: nnfis_times) from ms 1 2 have i: "integrable (λt. a*f t) M" by (auto simp add: integrable_def) also from 1 ms have "(THE i. i ∈ nnfis (pp (λt. a * f t)) M) = a*k" by (auto simp add: nnfis_unique) moreover from 2 ms have "(THE i. i ∈ nnfis (np (λt. a * f t)) M) = a*l" by (auto simp add: nnfis_unique) ultimately have "∫ (λt. a*f t) ∂M = a*k-a*l" by (simp add: integral_def) also have "… = a*(k-l)" by (simp add: right_diff_distrib) also note uni also note i ultimately show ?thesis by simp next case False hence pp: "pp (λt. a*f t) = (λt. -a*np f t)" and np: "np (λt. a*f t) = (λt. -a*pp f t)" by (auto simp add: real_pp_np_neg_times) from False have le: "0 ≤ -a" by simp with ms l have "-a*l ∈ nnfis (λt. -a * np f t) M" by (rule nnfis_times) with pp have 1: "-a*l ∈ nnfis (pp (λt. a * f t)) M" by simp from ms k le have "-a*k ∈ nnfis (λt. -a * pp f t) M" by (rule nnfis_times) with np have 2: "-a*k ∈ nnfis (np (λt. a * f t)) M" by simp from ms 1 2 have i: "integrable (λt. a*f t) M" by (auto simp add: integrable_def) also from 1 ms have "(THE i. i ∈ nnfis (pp (λt. a * f t)) M) = -a*l" by (auto simp add: nnfis_unique) moreover from 2 ms have "(THE i. i ∈ nnfis (np (λt. a * f t)) M) = -a*k" by (auto simp add: nnfis_unique) ultimately have "∫ (λt. a*f t) ∂M = -a*l-(-a*k)" by (simp add: integral_def) also have "… = a*(k-l)" by (simp add: right_diff_distrib) also note uni also note i ultimately show ?thesis by simp qed thus "integrable (λt. a*f t) M" and "∫ (λt. a*f t) ∂M = a*∫ f ∂M" by simp_all qed(*>*) (* Left out for lack of time theorem sf_integral: assumes M: "measure_space M" and f: "f = (λt. ∑i∈(S::nat set). x i * χ (A i) t)" and A: "∀i∈S. A i ∈ measurable_sets M" and S: "finite S" shows "∫ f ∂ M = (∑i∈S. x i * measure M (A i))" and "integrable f M" oops constdefs The probabilistic Quantifiers as in Hurd: p. 53 could be defined as a special case of this almost_everywhere:: "('a set set * ('a set ⇒ real)) ⇒ ('a ⇒ bool) ⇒ bool" ("_-a.e. _") "M-a.e. P == measure_space M ∧ (∃N. N ∈ measurable_sets M ∧ measure M N = 0 ∧ (∀w ∈ -N. P w))" theorem assumes ae0: "M-a.e. (λw. f w = 0)" shows ae0_nn_integ: "∫ f ∂ M = 0" oops theorem assumes "integrable f M" and "integrable g M" and "M-a.e. (λw. f w ≤ g w)" shows ae_integ_monotone: "∫ f ∂ M ≤ ∫ g ∂ M" oops theorem assumes aeq: "M-a.e. (λw. f w = g w)" shows aeq_nn_integ: "integrable f M ⟹ ∫ f ∂ M = ∫ g ∂ M" oops *) text‹To try out our definitions in an application, only one more theorem is missing. The famous Markov--Chebyshev inequation is not difficult to arrive at using the basic integral properties.› theorem assumes int: "integrable f M" and a: "0<a" and intp: "integrable (λx. ¦f x¦ ^ n) M" shows markov_ineq: "law M f {a..} ≤ ∫ (λx. ¦f x¦ ^ n) ∂M / (a^n)" proof - from int have rv: "f ∈ rv M" by (rule integrable_rv) hence ms: "measure_space M" by (simp add: rv_def) from ms rv have ams: "{w. a ≤ f w} ∈ measurable_sets M" by (simp add: rv_ge_iff) from rv have "(a^n)*law M f {a..} = (a^n)*measure M {w. a ≤ f w}" by (simp add: distribution_def vimage_def) also from ms ams have int2: "integrable χ {w. a ≤ f w} M" and eq2: "… = (a^n)*∫ χ {w. a ≤ f w} ∂ M" by (auto simp add: integral_char) note eq2 also from int2 have int3: "integrable (λt. (a^n)*χ {w. a ≤ f w} t) M" and eq3: "… = ∫ (λt. (a^n)*χ {w. a ≤ f w} t) ∂ M" by (auto simp add: integral_times) note eq3 also { fix t from a have "(a^n)*χ {w. a ≤ f w} t ≤ ¦f t¦ ^ n" proof (cases "a ≤ f t") case False thus ?thesis by (simp add: characteristic_function_def) next case True with a have "a ^ n ≤ (f t)^ n" by (simp add: power_mono) also have "(f t)^ n ≤ ¦(f t) ^ n¦" by arith hence "(f t)^ n ≤ ¦f t¦ ^ n" by (simp add: power_abs) finally show ?thesis by (simp add: characteristic_function_def) qed } with int3 intp have "… ≤ ∫ (λx. ¦f x¦ ^ n) ∂M" by (simp add: le_fun_def integral_mono) also from a have "0 < a^n" by (rule zero_less_power) ultimately show ?thesis by (simp add: pos_le_divide_eq mult.commute) qed end