equal
deleted
inserted
replaced
6 header {*Lebesgue Integration*} |
6 header {*Lebesgue Integration*} |
7 |
7 |
8 theory Lebesgue_Integration |
8 theory Lebesgue_Integration |
9 imports Measure_Space Borel_Space |
9 imports Measure_Space Borel_Space |
10 begin |
10 begin |
11 |
|
12 lemma ereal_minus_eq_PInfty_iff: |
|
13 fixes x y :: ereal shows "x - y = \<infinity> \<longleftrightarrow> y = -\<infinity> \<or> x = \<infinity>" |
|
14 by (cases x y rule: ereal2_cases) simp_all |
|
15 |
|
16 lemma real_ereal_1[simp]: "real (1::ereal) = 1" |
|
17 unfolding one_ereal_def by simp |
|
18 |
|
19 lemma ereal_indicator_pos[simp,intro]: "0 \<le> (indicator A x ::ereal)" |
|
20 unfolding indicator_def by auto |
|
21 |
11 |
22 lemma tendsto_real_max: |
12 lemma tendsto_real_max: |
23 fixes x y :: real |
13 fixes x y :: real |
24 assumes "(X ---> x) net" |
14 assumes "(X ---> x) net" |
25 assumes "(Y ---> y) net" |
15 assumes "(Y ---> y) net" |
39 proof - |
29 proof - |
40 have "f -` A \<inter> g -` B \<inter> space M = (f -` A \<inter> space M) \<inter> (g -` B \<inter> space M)" |
30 have "f -` A \<inter> g -` B \<inter> space M = (f -` A \<inter> space M) \<inter> (g -` B \<inter> space M)" |
41 by auto |
31 by auto |
42 then show ?thesis using assms by (auto intro: measurable_sets) |
32 then show ?thesis using assms by (auto intro: measurable_sets) |
43 qed |
33 qed |
44 |
|
45 lemma incseq_Suc_iff: "incseq f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))" |
|
46 proof |
|
47 assume "\<forall>n. f n \<le> f (Suc n)" then show "incseq f" by (auto intro!: incseq_SucI) |
|
48 qed (auto simp: incseq_def) |
|
49 |
34 |
50 section "Simple function" |
35 section "Simple function" |
51 |
36 |
52 text {* |
37 text {* |
53 |
38 |