8 section \<open>Lebesgue measure\<close> |
8 section \<open>Lebesgue measure\<close> |
9 |
9 |
10 theory Lebesgue_Measure |
10 theory Lebesgue_Measure |
11 imports Finite_Product_Measure Bochner_Integration Caratheodory Complete_Measure Summation_Tests Regularity |
11 imports Finite_Product_Measure Bochner_Integration Caratheodory Complete_Measure Summation_Tests Regularity |
12 begin |
12 begin |
|
13 |
|
14 lemma measure_eqI_lessThan: |
|
15 fixes M N :: "real measure" |
|
16 assumes sets: "sets M = sets borel" "sets N = sets borel" |
|
17 assumes fin: "\<And>x. emeasure M {x <..} < \<infinity>" |
|
18 assumes "\<And>x. emeasure M {x <..} = emeasure N {x <..}" |
|
19 shows "M = N" |
|
20 proof (rule measure_eqI_generator_eq_countable) |
|
21 let ?LT = "\<lambda>a::real. {a <..}" let ?E = "range ?LT" |
|
22 show "Int_stable ?E" |
|
23 by (auto simp: Int_stable_def lessThan_Int_lessThan) |
|
24 |
|
25 show "?E \<subseteq> Pow UNIV" "sets M = sigma_sets UNIV ?E" "sets N = sigma_sets UNIV ?E" |
|
26 unfolding sets borel_Ioi by auto |
|
27 |
|
28 show "?LT`Rats \<subseteq> ?E" "(\<Union>i\<in>Rats. ?LT i) = UNIV" "\<And>a. a \<in> ?LT`Rats \<Longrightarrow> emeasure M a \<noteq> \<infinity>" |
|
29 using fin by (auto intro: Rats_no_bot_less simp: less_top) |
|
30 qed (auto intro: assms countable_rat) |
13 |
31 |
14 subsection \<open>Every right continuous and nondecreasing function gives rise to a measure\<close> |
32 subsection \<open>Every right continuous and nondecreasing function gives rise to a measure\<close> |
15 |
33 |
16 definition interval_measure :: "(real \<Rightarrow> real) \<Rightarrow> real measure" where |
34 definition interval_measure :: "(real \<Rightarrow> real) \<Rightarrow> real measure" where |
17 "interval_measure F = extend_measure UNIV {(a, b). a \<le> b} (\<lambda>(a, b). {a <.. b}) (\<lambda>(a, b). ennreal (F b - F a))" |
35 "interval_measure F = extend_measure UNIV {(a, b). a \<le> b} (\<lambda>(a, b). {a <.. b}) (\<lambda>(a, b). ennreal (F b - F a))" |