104 using absolutely_integrable_max[of ?f "cube n" ?g] A Suc by (simp add: *) |
110 using absolutely_integrable_max[of ?f "cube n" ?g] A Suc by (simp add: *) |
105 qed auto |
111 qed auto |
106 qed (auto intro: LIMSEQ_indicator_UN simp: cube_def) |
112 qed (auto intro: LIMSEQ_indicator_UN simp: cube_def) |
107 qed simp |
113 qed simp |
108 |
114 |
109 interpretation lebesgue: measure_space lebesgue lmeasure |
115 interpretation lebesgue: measure_space lebesgue |
110 proof |
116 proof |
111 have *: "indicator {} = (\<lambda>x. 0 :: real)" by (simp add: fun_eq_iff) |
117 have *: "indicator {} = (\<lambda>x. 0 :: real)" by (simp add: fun_eq_iff) |
112 show "lmeasure {} = 0" by (simp add: integral_0 * lmeasure_def) |
118 show "measure lebesgue {} = 0" by (simp add: integral_0 * lebesgue_def) |
113 next |
119 next |
114 show "countably_additive lebesgue lmeasure" |
120 show "countably_additive lebesgue (measure lebesgue)" |
115 proof (intro countably_additive_def[THEN iffD2] allI impI) |
121 proof (intro countably_additive_def[THEN iffD2] allI impI) |
116 fix A :: "nat \<Rightarrow> 'b set" assume rA: "range A \<subseteq> sets lebesgue" "disjoint_family A" |
122 fix A :: "nat \<Rightarrow> 'b set" assume rA: "range A \<subseteq> sets lebesgue" "disjoint_family A" |
117 then have A[simp, intro]: "\<And>i n. (indicator (A i) :: _ \<Rightarrow> real) integrable_on cube n" |
123 then have A[simp, intro]: "\<And>i n. (indicator (A i) :: _ \<Rightarrow> real) integrable_on cube n" |
118 by (auto dest: lebesgueD) |
124 by (auto dest: lebesgueD) |
119 let "?m n i" = "integral (cube n) (indicator (A i) :: _\<Rightarrow>real)" |
125 let "?m n i" = "integral (cube n) (indicator (A i) :: _\<Rightarrow>real)" |
120 let "?M n I" = "integral (cube n) (indicator (\<Union>i\<in>I. A i) :: _\<Rightarrow>real)" |
126 let "?M n I" = "integral (cube n) (indicator (\<Union>i\<in>I. A i) :: _\<Rightarrow>real)" |
121 have nn[simp, intro]: "\<And>i n. 0 \<le> ?m n i" by (auto intro!: integral_nonneg) |
127 have nn[simp, intro]: "\<And>i n. 0 \<le> ?m n i" by (auto intro!: integral_nonneg) |
122 assume "(\<Union>i. A i) \<in> sets lebesgue" |
128 assume "(\<Union>i. A i) \<in> sets lebesgue" |
123 then have UN_A[simp, intro]: "\<And>i n. (indicator (\<Union>i. A i) :: _ \<Rightarrow> real) integrable_on cube n" |
129 then have UN_A[simp, intro]: "\<And>i n. (indicator (\<Union>i. A i) :: _ \<Rightarrow> real) integrable_on cube n" |
124 by (auto dest: lebesgueD) |
130 by (auto dest: lebesgueD) |
125 show "(\<Sum>\<^isub>\<infinity>n. lmeasure (A n)) = lmeasure (\<Union>i. A i)" unfolding lmeasure_def |
131 show "(\<Sum>\<^isub>\<infinity>n. measure lebesgue (A n)) = measure lebesgue (\<Union>i. A i)" |
126 proof (subst psuminf_SUP_eq) |
132 proof (simp add: lebesgue_def, subst psuminf_SUP_eq) |
127 fix n i show "Real (?m n i) \<le> Real (?m (Suc n) i)" |
133 fix n i show "Real (?m n i) \<le> Real (?m (Suc n) i)" |
128 using cube_subset[of n "Suc n"] by (auto intro!: integral_subset_le) |
134 using cube_subset[of n "Suc n"] by (auto intro!: integral_subset_le) |
129 next |
135 next |
130 show "(SUP n. \<Sum>\<^isub>\<infinity>i. Real (?m n i)) = (SUP n. Real (?M n UNIV))" |
136 show "(SUP n. \<Sum>\<^isub>\<infinity>i. Real (?m n i)) = (SUP n. Real (?M n UNIV))" |
131 unfolding psuminf_def |
137 unfolding psuminf_def |
211 lemma lebesgueI_negligible[dest]: fixes s::"'a::ordered_euclidean_space set" |
217 lemma lebesgueI_negligible[dest]: fixes s::"'a::ordered_euclidean_space set" |
212 assumes "negligible s" shows "s \<in> sets lebesgue" |
218 assumes "negligible s" shows "s \<in> sets lebesgue" |
213 using assms by (force simp: cube_def integrable_on_def negligible_def intro!: lebesgueI) |
219 using assms by (force simp: cube_def integrable_on_def negligible_def intro!: lebesgueI) |
214 |
220 |
215 lemma lmeasure_eq_0: |
221 lemma lmeasure_eq_0: |
216 fixes S :: "'a::ordered_euclidean_space set" assumes "negligible S" shows "lmeasure S = 0" |
222 fixes S :: "'a::ordered_euclidean_space set" assumes "negligible S" shows "lebesgue.\<mu> S = 0" |
217 proof - |
223 proof - |
218 have "\<And>n. integral (cube n) (indicator S :: 'a\<Rightarrow>real) = 0" |
224 have "\<And>n. integral (cube n) (indicator S :: 'a\<Rightarrow>real) = 0" |
219 unfolding integral_def using assms |
225 unfolding lebesgue_integral_def using assms |
220 by (intro some1_equality ex_ex1I has_integral_unique) |
226 by (intro integral_unique some1_equality ex_ex1I) |
221 (auto simp: cube_def negligible_def intro: ) |
227 (auto simp: cube_def negligible_def) |
222 then show ?thesis unfolding lmeasure_def by auto |
228 then show ?thesis by (auto simp: lebesgue_def) |
223 qed |
229 qed |
224 |
230 |
225 lemma lmeasure_iff_LIMSEQ: |
231 lemma lmeasure_iff_LIMSEQ: |
226 assumes "A \<in> sets lebesgue" "0 \<le> m" |
232 assumes "A \<in> sets lebesgue" "0 \<le> m" |
227 shows "lmeasure A = Real m \<longleftrightarrow> (\<lambda>n. integral (cube n) (indicator A :: _ \<Rightarrow> real)) ----> m" |
233 shows "lebesgue.\<mu> A = Real m \<longleftrightarrow> (\<lambda>n. integral (cube n) (indicator A :: _ \<Rightarrow> real)) ----> m" |
228 unfolding lmeasure_def |
234 proof (simp add: lebesgue_def, intro SUP_eq_LIMSEQ) |
229 proof (intro SUP_eq_LIMSEQ) |
|
230 show "mono (\<lambda>n. integral (cube n) (indicator A::_=>real))" |
235 show "mono (\<lambda>n. integral (cube n) (indicator A::_=>real))" |
231 using cube_subset assms by (intro monoI integral_subset_le) (auto dest!: lebesgueD) |
236 using cube_subset assms by (intro monoI integral_subset_le) (auto dest!: lebesgueD) |
232 fix n show "0 \<le> integral (cube n) (indicator A::_=>real)" |
237 fix n show "0 \<le> integral (cube n) (indicator A::_=>real)" |
233 using assms by (auto dest!: lebesgueD intro!: integral_nonneg) |
238 using assms by (auto dest!: lebesgueD intro!: integral_nonneg) |
234 qed fact |
239 qed fact |
337 then show "(\<lambda>n. integral (cube n) (?I s)) ----> m" |
342 then show "(\<lambda>n. integral (cube n) (?I s)) ----> m" |
338 unfolding integral_unique[OF assms] integral_indicator_UNIV by simp |
343 unfolding integral_unique[OF assms] integral_indicator_UNIV by simp |
339 qed |
344 qed |
340 |
345 |
341 lemma has_integral_iff_lmeasure: |
346 lemma has_integral_iff_lmeasure: |
342 "(indicator A has_integral m) UNIV \<longleftrightarrow> (A \<in> sets lebesgue \<and> 0 \<le> m \<and> lmeasure A = Real m)" |
347 "(indicator A has_integral m) UNIV \<longleftrightarrow> (A \<in> sets lebesgue \<and> 0 \<le> m \<and> lebesgue.\<mu> A = Real m)" |
343 proof |
348 proof |
344 assume "(indicator A has_integral m) UNIV" |
349 assume "(indicator A has_integral m) UNIV" |
345 with has_integral_lmeasure[OF this] has_integral_lebesgue[OF this] |
350 with has_integral_lmeasure[OF this] has_integral_lebesgue[OF this] |
346 show "A \<in> sets lebesgue \<and> 0 \<le> m \<and> lmeasure A = Real m" |
351 show "A \<in> sets lebesgue \<and> 0 \<le> m \<and> lebesgue.\<mu> A = Real m" |
347 by (auto intro: has_integral_nonneg) |
352 by (auto intro: has_integral_nonneg) |
348 next |
353 next |
349 assume "A \<in> sets lebesgue \<and> 0 \<le> m \<and> lmeasure A = Real m" |
354 assume "A \<in> sets lebesgue \<and> 0 \<le> m \<and> lebesgue.\<mu> A = Real m" |
350 then show "(indicator A has_integral m) UNIV" by (intro lmeasure_finite_has_integral) auto |
355 then show "(indicator A has_integral m) UNIV" by (intro lmeasure_finite_has_integral) auto |
351 qed |
356 qed |
352 |
357 |
353 lemma lmeasure_eq_integral: assumes "(indicator s::_\<Rightarrow>real) integrable_on UNIV" |
358 lemma lmeasure_eq_integral: assumes "(indicator s::_\<Rightarrow>real) integrable_on UNIV" |
354 shows "lmeasure s = Real (integral UNIV (indicator s))" |
359 shows "lebesgue.\<mu> s = Real (integral UNIV (indicator s))" |
355 using assms unfolding integrable_on_def |
360 using assms unfolding integrable_on_def |
356 proof safe |
361 proof safe |
357 fix y :: real assume "(indicator s has_integral y) UNIV" |
362 fix y :: real assume "(indicator s has_integral y) UNIV" |
358 from this[unfolded has_integral_iff_lmeasure] integral_unique[OF this] |
363 from this[unfolded has_integral_iff_lmeasure] integral_unique[OF this] |
359 show "lmeasure s = Real (integral UNIV (indicator s))" by simp |
364 show "lebesgue.\<mu> s = Real (integral UNIV (indicator s))" by simp |
360 qed |
365 qed |
361 |
366 |
362 lemma lebesgue_simple_function_indicator: |
367 lemma lebesgue_simple_function_indicator: |
363 fixes f::"'a::ordered_euclidean_space \<Rightarrow> pextreal" |
368 fixes f::"'a::ordered_euclidean_space \<Rightarrow> pextreal" |
364 assumes f:"lebesgue.simple_function f" |
369 assumes f:"simple_function lebesgue f" |
365 shows "f = (\<lambda>x. (\<Sum>y \<in> f ` UNIV. y * indicator (f -` {y}) x))" |
370 shows "f = (\<lambda>x. (\<Sum>y \<in> f ` UNIV. y * indicator (f -` {y}) x))" |
366 apply(rule,subst lebesgue.simple_function_indicator_representation[OF f]) by auto |
371 by (rule, subst lebesgue.simple_function_indicator_representation[OF f]) auto |
367 |
372 |
368 lemma integral_eq_lmeasure: |
373 lemma integral_eq_lmeasure: |
369 "(indicator s::_\<Rightarrow>real) integrable_on UNIV \<Longrightarrow> integral UNIV (indicator s) = real (lmeasure s)" |
374 "(indicator s::_\<Rightarrow>real) integrable_on UNIV \<Longrightarrow> integral UNIV (indicator s) = real (lebesgue.\<mu> s)" |
370 by (subst lmeasure_eq_integral) (auto intro!: integral_nonneg) |
375 by (subst lmeasure_eq_integral) (auto intro!: integral_nonneg) |
371 |
376 |
372 lemma lmeasure_finite: assumes "(indicator s::_\<Rightarrow>real) integrable_on UNIV" shows "lmeasure s \<noteq> \<omega>" |
377 lemma lmeasure_finite: assumes "(indicator s::_\<Rightarrow>real) integrable_on UNIV" shows "lebesgue.\<mu> s \<noteq> \<omega>" |
373 using lmeasure_eq_integral[OF assms] by auto |
378 using lmeasure_eq_integral[OF assms] by auto |
374 |
379 |
375 lemma negligible_iff_lebesgue_null_sets: |
380 lemma negligible_iff_lebesgue_null_sets: |
376 "negligible A \<longleftrightarrow> A \<in> lebesgue.null_sets" |
381 "negligible A \<longleftrightarrow> A \<in> lebesgue.null_sets" |
377 proof |
382 proof |
451 by (subst content_closed_interval) auto |
455 by (subst content_closed_interval) auto |
452 then show ?thesis by simp |
456 then show ?thesis by simp |
453 qed |
457 qed |
454 |
458 |
455 lemma lmeasure_singleton[simp]: |
459 lemma lmeasure_singleton[simp]: |
456 fixes a :: "'a::ordered_euclidean_space" shows "lmeasure {a} = 0" |
460 fixes a :: "'a::ordered_euclidean_space" shows "lebesgue.\<mu> {a} = 0" |
457 using lmeasure_atLeastAtMost[of a a] by simp |
461 using lmeasure_atLeastAtMost[of a a] by simp |
458 |
462 |
459 declare content_real[simp] |
463 declare content_real[simp] |
460 |
464 |
461 lemma |
465 lemma |
462 fixes a b :: real |
466 fixes a b :: real |
463 shows lmeasure_real_greaterThanAtMost[simp]: |
467 shows lmeasure_real_greaterThanAtMost[simp]: |
464 "lmeasure {a <.. b} = Real (if a \<le> b then b - a else 0)" |
468 "lebesgue.\<mu> {a <.. b} = Real (if a \<le> b then b - a else 0)" |
465 proof cases |
469 proof cases |
466 assume "a < b" |
470 assume "a < b" |
467 then have "lmeasure {a <.. b} = lmeasure {a .. b} - lmeasure {a}" |
471 then have "lebesgue.\<mu> {a <.. b} = lebesgue.\<mu> {a .. b} - lebesgue.\<mu> {a}" |
468 by (subst lebesgue.measure_Diff[symmetric]) |
472 by (subst lebesgue.measure_Diff[symmetric]) |
469 (auto intro!: arg_cong[where f=lmeasure]) |
473 (auto intro!: arg_cong[where f=lebesgue.\<mu>]) |
470 then show ?thesis by auto |
474 then show ?thesis by auto |
471 qed auto |
475 qed auto |
472 |
476 |
473 lemma |
477 lemma |
474 fixes a b :: real |
478 fixes a b :: real |
475 shows lmeasure_real_atLeastLessThan[simp]: |
479 shows lmeasure_real_atLeastLessThan[simp]: |
476 "lmeasure {a ..< b} = Real (if a \<le> b then b - a else 0)" |
480 "lebesgue.\<mu> {a ..< b} = Real (if a \<le> b then b - a else 0)" |
477 proof cases |
481 proof cases |
478 assume "a < b" |
482 assume "a < b" |
479 then have "lmeasure {a ..< b} = lmeasure {a .. b} - lmeasure {b}" |
483 then have "lebesgue.\<mu> {a ..< b} = lebesgue.\<mu> {a .. b} - lebesgue.\<mu> {b}" |
480 by (subst lebesgue.measure_Diff[symmetric]) |
484 by (subst lebesgue.measure_Diff[symmetric]) |
481 (auto intro!: arg_cong[where f=lmeasure]) |
485 (auto intro!: arg_cong[where f=lebesgue.\<mu>]) |
482 then show ?thesis by auto |
486 then show ?thesis by auto |
483 qed auto |
487 qed auto |
484 |
488 |
485 lemma |
489 lemma |
486 fixes a b :: real |
490 fixes a b :: real |
487 shows lmeasure_real_greaterThanLessThan[simp]: |
491 shows lmeasure_real_greaterThanLessThan[simp]: |
488 "lmeasure {a <..< b} = Real (if a \<le> b then b - a else 0)" |
492 "lebesgue.\<mu> {a <..< b} = Real (if a \<le> b then b - a else 0)" |
489 proof cases |
493 proof cases |
490 assume "a < b" |
494 assume "a < b" |
491 then have "lmeasure {a <..< b} = lmeasure {a <.. b} - lmeasure {b}" |
495 then have "lebesgue.\<mu> {a <..< b} = lebesgue.\<mu> {a <.. b} - lebesgue.\<mu> {b}" |
492 by (subst lebesgue.measure_Diff[symmetric]) |
496 by (subst lebesgue.measure_Diff[symmetric]) |
493 (auto intro!: arg_cong[where f=lmeasure]) |
497 (auto intro!: arg_cong[where f=lebesgue.\<mu>]) |
494 then show ?thesis by auto |
498 then show ?thesis by auto |
495 qed auto |
499 qed auto |
496 |
500 |
497 interpretation borel: measure_space borel lmeasure |
501 definition "lborel = lebesgue \<lparr> sets := sets borel \<rparr>" |
|
502 |
|
503 lemma |
|
504 shows space_lborel[simp]: "space lborel = UNIV" |
|
505 and sets_lborel[simp]: "sets lborel = sets borel" |
|
506 and measure_lborel[simp]: "measure lborel = lebesgue.\<mu>" |
|
507 and measurable_lborel[simp]: "measurable lborel = measurable borel" |
|
508 by (simp_all add: measurable_def_raw lborel_def) |
|
509 |
|
510 interpretation lborel: measure_space lborel |
|
511 where "space lborel = UNIV" |
|
512 and "sets lborel = sets borel" |
|
513 and "measure lborel = lebesgue.\<mu>" |
|
514 and "measurable lborel = measurable borel" |
|
515 proof - |
|
516 show "measure_space lborel" |
|
517 proof |
|
518 show "countably_additive lborel (measure lborel)" |
|
519 using lebesgue.ca unfolding countably_additive_def lborel_def |
|
520 apply safe apply (erule_tac x=A in allE) by auto |
|
521 qed (auto simp: lborel_def) |
|
522 qed simp_all |
|
523 |
|
524 interpretation lborel: sigma_finite_measure lborel |
|
525 where "space lborel = UNIV" |
|
526 and "sets lborel = sets borel" |
|
527 and "measure lborel = lebesgue.\<mu>" |
|
528 and "measurable lborel = measurable borel" |
|
529 proof - |
|
530 show "sigma_finite_measure lborel" |
|
531 proof (default, intro conjI exI[of _ "\<lambda>n. cube n"]) |
|
532 show "range cube \<subseteq> sets lborel" by (auto intro: borel_closed) |
|
533 { fix x have "\<exists>n. x\<in>cube n" using mem_big_cube by auto } |
|
534 thus "(\<Union>i. cube i) = space lborel" by auto |
|
535 show "\<forall>i. measure lborel (cube i) \<noteq> \<omega>" by (simp add: cube_def) |
|
536 qed |
|
537 qed simp_all |
|
538 |
|
539 interpretation lebesgue: sigma_finite_measure lebesgue |
498 proof |
540 proof |
499 show "countably_additive borel lmeasure" |
541 from lborel.sigma_finite guess A .. |
500 using lebesgue.ca unfolding countably_additive_def |
|
501 apply safe apply (erule_tac x=A in allE) by auto |
|
502 qed auto |
|
503 |
|
504 interpretation borel: sigma_finite_measure borel lmeasure |
|
505 proof (default, intro conjI exI[of _ "\<lambda>n. cube n"]) |
|
506 show "range cube \<subseteq> sets borel" by (auto intro: borel_closed) |
|
507 { fix x have "\<exists>n. x\<in>cube n" using mem_big_cube by auto } |
|
508 thus "(\<Union>i. cube i) = space borel" by auto |
|
509 show "\<forall>i. lmeasure (cube i) \<noteq> \<omega>" unfolding cube_def by auto |
|
510 qed |
|
511 |
|
512 interpretation lebesgue: sigma_finite_measure lebesgue lmeasure |
|
513 proof |
|
514 from borel.sigma_finite guess A .. |
|
515 moreover then have "range A \<subseteq> sets lebesgue" using lebesgueI_borel by blast |
542 moreover then have "range A \<subseteq> sets lebesgue" using lebesgueI_borel by blast |
516 ultimately show "\<exists>A::nat \<Rightarrow> 'b set. range A \<subseteq> sets lebesgue \<and> (\<Union>i. A i) = space lebesgue \<and> (\<forall>i. lmeasure (A i) \<noteq> \<omega>)" |
543 ultimately show "\<exists>A::nat \<Rightarrow> 'b set. range A \<subseteq> sets lebesgue \<and> (\<Union>i. A i) = space lebesgue \<and> (\<forall>i. lebesgue.\<mu> (A i) \<noteq> \<omega>)" |
517 by auto |
544 by auto |
518 qed |
545 qed |
519 |
546 |
520 lemma simple_function_has_integral: |
547 lemma simple_function_has_integral: |
521 fixes f::"'a::ordered_euclidean_space \<Rightarrow> pextreal" |
548 fixes f::"'a::ordered_euclidean_space \<Rightarrow> pextreal" |
522 assumes f:"lebesgue.simple_function f" |
549 assumes f:"simple_function lebesgue f" |
523 and f':"\<forall>x. f x \<noteq> \<omega>" |
550 and f':"\<forall>x. f x \<noteq> \<omega>" |
524 and om:"\<forall>x\<in>range f. lmeasure (f -` {x} \<inter> UNIV) = \<omega> \<longrightarrow> x = 0" |
551 and om:"\<forall>x\<in>range f. lebesgue.\<mu> (f -` {x} \<inter> UNIV) = \<omega> \<longrightarrow> x = 0" |
525 shows "((\<lambda>x. real (f x)) has_integral (real (lebesgue.simple_integral f))) UNIV" |
552 shows "((\<lambda>x. real (f x)) has_integral (real (integral\<^isup>S lebesgue f))) UNIV" |
526 unfolding lebesgue.simple_integral_def |
553 unfolding simple_integral_def |
527 apply(subst lebesgue_simple_function_indicator[OF f]) |
554 apply(subst lebesgue_simple_function_indicator[OF f]) |
528 proof - |
555 proof - |
529 case goal1 |
556 case goal1 |
530 have *:"\<And>x. \<forall>y\<in>range f. y * indicator (f -` {y}) x \<noteq> \<omega>" |
557 have *:"\<And>x. \<forall>y\<in>range f. y * indicator (f -` {y}) x \<noteq> \<omega>" |
531 "\<forall>x\<in>range f. x * lmeasure (f -` {x} \<inter> UNIV) \<noteq> \<omega>" |
558 "\<forall>x\<in>range f. x * lebesgue.\<mu> (f -` {x} \<inter> UNIV) \<noteq> \<omega>" |
532 using f' om unfolding indicator_def by auto |
559 using f' om unfolding indicator_def by auto |
533 show ?case unfolding space_lebesgue real_of_pextreal_setsum'[OF *(1),THEN sym] |
560 show ?case unfolding space_lebesgue real_of_pextreal_setsum'[OF *(1),THEN sym] |
534 unfolding real_of_pextreal_setsum'[OF *(2),THEN sym] |
561 unfolding real_of_pextreal_setsum'[OF *(2),THEN sym] |
535 unfolding real_of_pextreal_setsum space_lebesgue |
562 unfolding real_of_pextreal_setsum space_lebesgue |
536 apply(rule has_integral_setsum) |
563 apply(rule has_integral_setsum) |
537 proof safe show "finite (range f)" using f by (auto dest: lebesgue.simple_functionD) |
564 proof safe show "finite (range f)" using f by (auto dest: lebesgue.simple_functionD) |
538 fix y::'a show "((\<lambda>x. real (f y * indicator (f -` {f y}) x)) has_integral |
565 fix y::'a show "((\<lambda>x. real (f y * indicator (f -` {f y}) x)) has_integral |
539 real (f y * lmeasure (f -` {f y} \<inter> UNIV))) UNIV" |
566 real (f y * lebesgue.\<mu> (f -` {f y} \<inter> UNIV))) UNIV" |
540 proof(cases "f y = 0") case False |
567 proof(cases "f y = 0") case False |
541 have mea:"(indicator (f -` {f y}) ::_\<Rightarrow>real) integrable_on UNIV" |
568 have mea:"(indicator (f -` {f y}) ::_\<Rightarrow>real) integrable_on UNIV" |
542 apply(rule lmeasure_finite_integrable) |
569 apply(rule lmeasure_finite_integrable) |
543 using assms unfolding lebesgue.simple_function_def using False by auto |
570 using assms unfolding simple_function_def using False by auto |
544 have *:"\<And>x. real (indicator (f -` {f y}) x::pextreal) = (indicator (f -` {f y}) x)" |
571 have *:"\<And>x. real (indicator (f -` {f y}) x::pextreal) = (indicator (f -` {f y}) x)" |
545 by (auto simp: indicator_def) |
572 by (auto simp: indicator_def) |
546 show ?thesis unfolding real_of_pextreal_mult[THEN sym] |
573 show ?thesis unfolding real_of_pextreal_mult[THEN sym] |
547 apply(rule has_integral_cmul[where 'b=real, unfolded real_scaleR_def]) |
574 apply(rule has_integral_cmul[where 'b=real, unfolded real_scaleR_def]) |
548 unfolding Int_UNIV_right lmeasure_eq_integral[OF mea,THEN sym] |
575 unfolding Int_UNIV_right lmeasure_eq_integral[OF mea,THEN sym] |
556 unfolding bounded_def dist_real_def apply(rule_tac x=0 in exI) |
583 unfolding bounded_def dist_real_def apply(rule_tac x=0 in exI) |
557 using assms by auto |
584 using assms by auto |
558 |
585 |
559 lemma simple_function_has_integral': |
586 lemma simple_function_has_integral': |
560 fixes f::"'a::ordered_euclidean_space \<Rightarrow> pextreal" |
587 fixes f::"'a::ordered_euclidean_space \<Rightarrow> pextreal" |
561 assumes f:"lebesgue.simple_function f" |
588 assumes f:"simple_function lebesgue f" |
562 and i: "lebesgue.simple_integral f \<noteq> \<omega>" |
589 and i: "integral\<^isup>S lebesgue f \<noteq> \<omega>" |
563 shows "((\<lambda>x. real (f x)) has_integral (real (lebesgue.simple_integral f))) UNIV" |
590 shows "((\<lambda>x. real (f x)) has_integral (real (integral\<^isup>S lebesgue f))) UNIV" |
564 proof- let ?f = "\<lambda>x. if f x = \<omega> then 0 else f x" |
591 proof- let ?f = "\<lambda>x. if f x = \<omega> then 0 else f x" |
565 { fix x have "real (f x) = real (?f x)" by (cases "f x") auto } note * = this |
592 { fix x have "real (f x) = real (?f x)" by (cases "f x") auto } note * = this |
566 have **:"{x. f x \<noteq> ?f x} = f -` {\<omega>}" by auto |
593 have **:"{x. f x \<noteq> ?f x} = f -` {\<omega>}" by auto |
567 have **:"lmeasure {x\<in>space lebesgue. f x \<noteq> ?f x} = 0" |
594 have **:"lebesgue.\<mu> {x\<in>space lebesgue. f x \<noteq> ?f x} = 0" |
568 using lebesgue.simple_integral_omega[OF assms] by(auto simp add:**) |
595 using lebesgue.simple_integral_omega[OF assms] by(auto simp add:**) |
569 show ?thesis apply(subst lebesgue.simple_integral_cong'[OF f _ **]) |
596 show ?thesis apply(subst lebesgue.simple_integral_cong'[OF f _ **]) |
570 apply(rule lebesgue.simple_function_compose1[OF f]) |
597 apply(rule lebesgue.simple_function_compose1[OF f]) |
571 unfolding * defer apply(rule simple_function_has_integral) |
598 unfolding * defer apply(rule simple_function_has_integral) |
572 proof- |
599 proof- |
573 show "lebesgue.simple_function ?f" |
600 show "simple_function lebesgue ?f" |
574 using lebesgue.simple_function_compose1[OF f] . |
601 using lebesgue.simple_function_compose1[OF f] . |
575 show "\<forall>x. ?f x \<noteq> \<omega>" by auto |
602 show "\<forall>x. ?f x \<noteq> \<omega>" by auto |
576 show "\<forall>x\<in>range ?f. lmeasure (?f -` {x} \<inter> UNIV) = \<omega> \<longrightarrow> x = 0" |
603 show "\<forall>x\<in>range ?f. lebesgue.\<mu> (?f -` {x} \<inter> UNIV) = \<omega> \<longrightarrow> x = 0" |
577 proof (safe, simp, safe, rule ccontr) |
604 proof (safe, simp, safe, rule ccontr) |
578 fix y assume "f y \<noteq> \<omega>" "f y \<noteq> 0" |
605 fix y assume "f y \<noteq> \<omega>" "f y \<noteq> 0" |
579 hence "(\<lambda>x. if f x = \<omega> then 0 else f x) -` {if f y = \<omega> then 0 else f y} = f -` {f y}" |
606 hence "(\<lambda>x. if f x = \<omega> then 0 else f x) -` {if f y = \<omega> then 0 else f y} = f -` {f y}" |
580 by (auto split: split_if_asm) |
607 by (auto split: split_if_asm) |
581 moreover assume "lmeasure ((\<lambda>x. if f x = \<omega> then 0 else f x) -` {if f y = \<omega> then 0 else f y}) = \<omega>" |
608 moreover assume "lebesgue.\<mu> ((\<lambda>x. if f x = \<omega> then 0 else f x) -` {if f y = \<omega> then 0 else f y}) = \<omega>" |
582 ultimately have "lmeasure (f -` {f y}) = \<omega>" by simp |
609 ultimately have "lebesgue.\<mu> (f -` {f y}) = \<omega>" by simp |
583 moreover |
610 moreover |
584 have "f y * lmeasure (f -` {f y}) \<noteq> \<omega>" using i f |
611 have "f y * lebesgue.\<mu> (f -` {f y}) \<noteq> \<omega>" using i f |
585 unfolding lebesgue.simple_integral_def setsum_\<omega> lebesgue.simple_function_def |
612 unfolding simple_integral_def setsum_\<omega> simple_function_def |
586 by auto |
613 by auto |
587 ultimately have "f y = 0" by (auto split: split_if_asm) |
614 ultimately have "f y = 0" by (auto split: split_if_asm) |
588 then show False using `f y \<noteq> 0` by simp |
615 then show False using `f y \<noteq> 0` by simp |
589 qed |
616 qed |
590 qed |
617 qed |
607 qed |
634 qed |
608 |
635 |
609 lemma positive_integral_has_integral: |
636 lemma positive_integral_has_integral: |
610 fixes f::"'a::ordered_euclidean_space => pextreal" |
637 fixes f::"'a::ordered_euclidean_space => pextreal" |
611 assumes f:"f \<in> borel_measurable lebesgue" |
638 assumes f:"f \<in> borel_measurable lebesgue" |
612 and int_om:"lebesgue.positive_integral f \<noteq> \<omega>" |
639 and int_om:"integral\<^isup>P lebesgue f \<noteq> \<omega>" |
613 and f_om:"\<forall>x. f x \<noteq> \<omega>" (* TODO: remove this *) |
640 and f_om:"\<forall>x. f x \<noteq> \<omega>" (* TODO: remove this *) |
614 shows "((\<lambda>x. real (f x)) has_integral (real (lebesgue.positive_integral f))) UNIV" |
641 shows "((\<lambda>x. real (f x)) has_integral (real (integral\<^isup>P lebesgue f))) UNIV" |
615 proof- let ?i = "lebesgue.positive_integral f" |
642 proof- let ?i = "integral\<^isup>P lebesgue f" |
616 from lebesgue.borel_measurable_implies_simple_function_sequence[OF f] |
643 from lebesgue.borel_measurable_implies_simple_function_sequence[OF f] |
617 guess u .. note conjunctD2[OF this,rule_format] note u = conjunctD2[OF this(1)] this(2) |
644 guess u .. note conjunctD2[OF this,rule_format] note u = conjunctD2[OF this(1)] this(2) |
618 let ?u = "\<lambda>i x. real (u i x)" and ?f = "\<lambda>x. real (f x)" |
645 let ?u = "\<lambda>i x. real (u i x)" and ?f = "\<lambda>x. real (f x)" |
619 have u_simple:"\<And>k. lebesgue.simple_integral (u k) = lebesgue.positive_integral (u k)" |
646 have u_simple:"\<And>k. integral\<^isup>S lebesgue (u k) = integral\<^isup>P lebesgue (u k)" |
620 apply(subst lebesgue.positive_integral_eq_simple_integral[THEN sym,OF u(1)]) .. |
647 apply(subst lebesgue.positive_integral_eq_simple_integral[THEN sym,OF u(1)]) .. |
621 have int_u_le:"\<And>k. lebesgue.simple_integral (u k) \<le> lebesgue.positive_integral f" |
648 have int_u_le:"\<And>k. integral\<^isup>S lebesgue (u k) \<le> integral\<^isup>P lebesgue f" |
622 unfolding u_simple apply(rule lebesgue.positive_integral_mono) |
649 unfolding u_simple apply(rule lebesgue.positive_integral_mono) |
623 using isoton_Sup[OF u(3)] unfolding le_fun_def by auto |
650 using isoton_Sup[OF u(3)] unfolding le_fun_def by auto |
624 have u_int_om:"\<And>i. lebesgue.simple_integral (u i) \<noteq> \<omega>" |
651 have u_int_om:"\<And>i. integral\<^isup>S lebesgue (u i) \<noteq> \<omega>" |
625 proof- case goal1 thus ?case using int_u_le[of i] int_om by auto qed |
652 proof- case goal1 thus ?case using int_u_le[of i] int_om by auto qed |
626 |
653 |
627 note u_int = simple_function_has_integral'[OF u(1) this] |
654 note u_int = simple_function_has_integral'[OF u(1) this] |
628 have "(\<lambda>x. real (f x)) integrable_on UNIV \<and> |
655 have "(\<lambda>x. real (f x)) integrable_on UNIV \<and> |
629 (\<lambda>k. Integration.integral UNIV (\<lambda>x. real (u k x))) ----> Integration.integral UNIV (\<lambda>x. real (f x))" |
656 (\<lambda>k. Integration.integral UNIV (\<lambda>x. real (u k x))) ----> Integration.integral UNIV (\<lambda>x. real (f x))" |
631 proof safe case goal1 show ?case apply(rule real_of_pextreal_mono) using u(2,3) by auto |
658 proof safe case goal1 show ?case apply(rule real_of_pextreal_mono) using u(2,3) by auto |
632 next case goal2 show ?case using u(3) apply(subst lim_Real[THEN sym]) |
659 next case goal2 show ?case using u(3) apply(subst lim_Real[THEN sym]) |
633 prefer 3 apply(subst Real_real') defer apply(subst Real_real') |
660 prefer 3 apply(subst Real_real') defer apply(subst Real_real') |
634 using isotone_Lim[OF u(3)[unfolded isoton_fun_expand, THEN spec]] using f_om u by auto |
661 using isotone_Lim[OF u(3)[unfolded isoton_fun_expand, THEN spec]] using f_om u by auto |
635 next case goal3 |
662 next case goal3 |
636 show ?case apply(rule bounded_realI[where B="real (lebesgue.positive_integral f)"]) |
663 show ?case apply(rule bounded_realI[where B="real (integral\<^isup>P lebesgue f)"]) |
637 apply safe apply(subst abs_of_nonneg) apply(rule integral_nonneg,rule) apply(rule u_int) |
664 apply safe apply(subst abs_of_nonneg) apply(rule integral_nonneg,rule) apply(rule u_int) |
638 unfolding integral_unique[OF u_int] defer apply(rule real_of_pextreal_mono[OF _ int_u_le]) |
665 unfolding integral_unique[OF u_int] defer apply(rule real_of_pextreal_mono[OF _ int_u_le]) |
639 using u int_om by auto |
666 using u int_om by auto |
640 qed note int = conjunctD2[OF this] |
667 qed note int = conjunctD2[OF this] |
641 |
668 |
642 have "(\<lambda>i. lebesgue.simple_integral (u i)) ----> ?i" unfolding u_simple |
669 have "(\<lambda>i. integral\<^isup>S lebesgue (u i)) ----> ?i" unfolding u_simple |
643 apply(rule lebesgue.positive_integral_monotone_convergence(2)) |
670 apply(rule lebesgue.positive_integral_monotone_convergence(2)) |
644 apply(rule lebesgue.borel_measurable_simple_function[OF u(1)]) |
671 apply(rule lebesgue.borel_measurable_simple_function[OF u(1)]) |
645 using isotone_Lim[OF u(3)[unfolded isoton_fun_expand, THEN spec]] by auto |
672 using isotone_Lim[OF u(3)[unfolded isoton_fun_expand, THEN spec]] by auto |
646 hence "(\<lambda>i. real (lebesgue.simple_integral (u i))) ----> real ?i" apply- |
673 hence "(\<lambda>i. real (integral\<^isup>S lebesgue (u i))) ----> real ?i" apply- |
647 apply(subst lim_Real[THEN sym]) prefer 3 |
674 apply(subst lim_Real[THEN sym]) prefer 3 |
648 apply(subst Real_real') defer apply(subst Real_real') |
675 apply(subst Real_real') defer apply(subst Real_real') |
649 using u f_om int_om u_int_om by auto |
676 using u f_om int_om u_int_om by auto |
650 note * = LIMSEQ_unique[OF this int(2)[unfolded integral_unique[OF u_int]]] |
677 note * = LIMSEQ_unique[OF this int(2)[unfolded integral_unique[OF u_int]]] |
651 show ?thesis unfolding * by(rule integrable_integral[OF int(1)]) |
678 show ?thesis unfolding * by(rule integrable_integral[OF int(1)]) |
652 qed |
679 qed |
653 |
680 |
654 lemma lebesgue_integral_has_integral: |
681 lemma lebesgue_integral_has_integral: |
655 fixes f::"'a::ordered_euclidean_space => real" |
682 fixes f::"'a::ordered_euclidean_space => real" |
656 assumes f:"lebesgue.integrable f" |
683 assumes f:"integrable lebesgue f" |
657 shows "(f has_integral (lebesgue.integral f)) UNIV" |
684 shows "(f has_integral (integral\<^isup>L lebesgue f)) UNIV" |
658 proof- let ?n = "\<lambda>x. - min (f x) 0" and ?p = "\<lambda>x. max (f x) 0" |
685 proof- let ?n = "\<lambda>x. - min (f x) 0" and ?p = "\<lambda>x. max (f x) 0" |
659 have *:"f = (\<lambda>x. ?p x - ?n x)" apply rule by auto |
686 have *:"f = (\<lambda>x. ?p x - ?n x)" apply rule by auto |
660 note f = lebesgue.integrableD[OF f] |
687 note f = integrableD[OF f] |
661 show ?thesis unfolding lebesgue.integral_def apply(subst *) |
688 show ?thesis unfolding lebesgue_integral_def apply(subst *) |
662 proof(rule has_integral_sub) case goal1 |
689 proof(rule has_integral_sub) case goal1 |
663 have *:"\<forall>x. Real (f x) \<noteq> \<omega>" by auto |
690 have *:"\<forall>x. Real (f x) \<noteq> \<omega>" by auto |
664 note lebesgue.borel_measurable_Real[OF f(1)] |
691 note lebesgue.borel_measurable_Real[OF f(1)] |
665 from positive_integral_has_integral[OF this f(2) *] |
692 from positive_integral_has_integral[OF this f(2) *] |
666 show ?case unfolding real_Real_max . |
693 show ?case unfolding real_Real_max . |
672 show ?case unfolding real_Real_max minus_min_eq_max by auto |
699 show ?case unfolding real_Real_max minus_min_eq_max by auto |
673 qed |
700 qed |
674 qed |
701 qed |
675 |
702 |
676 lemma lebesgue_positive_integral_eq_borel: |
703 lemma lebesgue_positive_integral_eq_borel: |
677 "f \<in> borel_measurable borel \<Longrightarrow> lebesgue.positive_integral f = borel.positive_integral f " |
704 "f \<in> borel_measurable borel \<Longrightarrow> integral\<^isup>P lebesgue f = integral\<^isup>P lborel f" |
678 by (auto intro!: lebesgue.positive_integral_subalgebra[symmetric]) default |
705 by (auto intro!: lebesgue.positive_integral_subalgebra[symmetric]) default |
679 |
706 |
680 lemma lebesgue_integral_eq_borel: |
707 lemma lebesgue_integral_eq_borel: |
681 assumes "f \<in> borel_measurable borel" |
708 assumes "f \<in> borel_measurable borel" |
682 shows "lebesgue.integrable f = borel.integrable f" (is ?P) |
709 shows "integrable lebesgue f \<longleftrightarrow> integrable lborel f" (is ?P) |
683 and "lebesgue.integral f = borel.integral f" (is ?I) |
710 and "integral\<^isup>L lebesgue f = integral\<^isup>L lborel f" (is ?I) |
684 proof - |
711 proof - |
685 have *: "sigma_algebra borel" by default |
712 have *: "sigma_algebra lborel" by default |
686 have "sets borel \<subseteq> sets lebesgue" by auto |
713 have "sets lborel \<subseteq> sets lebesgue" by auto |
687 from lebesgue.integral_subalgebra[OF assms this _ *] |
714 from lebesgue.integral_subalgebra[of f lborel, OF _ this _ _ *] assms |
688 show ?P ?I by auto |
715 show ?P ?I by auto |
689 qed |
716 qed |
690 |
717 |
691 lemma borel_integral_has_integral: |
718 lemma borel_integral_has_integral: |
692 fixes f::"'a::ordered_euclidean_space => real" |
719 fixes f::"'a::ordered_euclidean_space => real" |
693 assumes f:"borel.integrable f" |
720 assumes f:"integrable lborel f" |
694 shows "(f has_integral (borel.integral f)) UNIV" |
721 shows "(f has_integral (integral\<^isup>L lborel f)) UNIV" |
695 proof - |
722 proof - |
696 have borel: "f \<in> borel_measurable borel" |
723 have borel: "f \<in> borel_measurable borel" |
697 using f unfolding borel.integrable_def by auto |
724 using f unfolding integrable_def by auto |
698 from f show ?thesis |
725 from f show ?thesis |
699 using lebesgue_integral_has_integral[of f] |
726 using lebesgue_integral_has_integral[of f] |
700 unfolding lebesgue_integral_eq_borel[OF borel] by simp |
727 unfolding lebesgue_integral_eq_borel[OF borel] by simp |
701 qed |
728 qed |
702 |
729 |
749 apply safe apply(rule vimageI[OF _ y(1)]) unfolding y p2e_e2p by auto |
776 apply safe apply(rule vimageI[OF _ y(1)]) unfolding y p2e_e2p by auto |
750 next fix x assume "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}" |
777 next fix x assume "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}" |
751 thus "x \<in> e2p ` A" unfolding image_iff apply(rule_tac x="p2e x" in bexI) apply(subst e2p_p2e) by auto |
778 thus "x \<in> e2p ` A" unfolding image_iff apply(rule_tac x="p2e x" in bexI) apply(subst e2p_p2e) by auto |
752 qed |
779 qed |
753 |
780 |
754 interpretation borel_product: product_sigma_finite "\<lambda>x. borel::real algebra" "\<lambda>x. lmeasure" |
781 interpretation lborel_product: product_sigma_finite "\<lambda>x. lborel::real measure_space" |
755 by default |
782 by default |
756 |
783 |
757 lemma cube_subset_Suc[intro]: "cube n \<subseteq> cube (Suc n)" |
784 interpretation lborel_space: finite_product_sigma_finite "\<lambda>x. lborel::real measure_space" "{..<DIM('a::ordered_euclidean_space)}" |
758 unfolding cube_def_raw subset_eq apply safe unfolding mem_interval by auto |
785 where "space lborel = UNIV" |
759 |
786 and "sets lborel = sets borel" |
760 lemma Pi_iff: "f \<in> Pi I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i)" |
787 and "measure lborel = lebesgue.\<mu>" |
761 unfolding Pi_def by auto |
788 and "measurable lborel = measurable borel" |
762 |
789 proof - |
763 lemma measurable_e2p_on_generator: |
790 show "finite_product_sigma_finite (\<lambda>x. lborel::real measure_space) {..<DIM('a::ordered_euclidean_space)}" |
764 "e2p \<in> measurable \<lparr> space = UNIV::'a set, sets = range lessThan \<rparr> |
791 by default simp |
765 (product_algebra |
792 qed simp_all |
766 (\<lambda>x. \<lparr> space = UNIV::real set, sets = range lessThan \<rparr>) |
793 |
767 {..<DIM('a::ordered_euclidean_space)})" |
794 lemma sets_product_borel: |
768 (is "e2p \<in> measurable ?E ?P") |
795 assumes [intro]: "finite I" |
769 proof (unfold measurable_def, intro CollectI conjI ballI) |
796 shows "sets (\<Pi>\<^isub>M i\<in>I. |
770 show "e2p \<in> space ?E \<rightarrow> space ?P" by (auto simp: e2p_def) |
797 \<lparr> space = UNIV::real set, sets = range lessThan, measure = lebesgue.\<mu> \<rparr>) = |
771 fix A assume "A \<in> sets ?P" |
798 sets (\<Pi>\<^isub>M i\<in>I. lborel)" (is "sets ?G = _") |
772 then obtain E where A: "A = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. E i)" |
799 proof - |
773 and "E \<in> {..<DIM('a)} \<rightarrow> (range lessThan)" |
800 have "sets ?G = sets (\<Pi>\<^isub>M i\<in>I. |
774 by (auto elim!: product_algebraE) |
801 sigma \<lparr> space = UNIV::real set, sets = range lessThan, measure = lebesgue.\<mu> \<rparr>)" |
775 then have "\<forall>i\<in>{..<DIM('a)}. \<exists>xs. E i = {..< xs}" by auto |
802 by (subst sigma_product_algebra_sigma_eq[of I "\<lambda>_ i. {..<real i}" ]) |
776 from this[THEN bchoice] guess xs .. |
803 (auto intro!: measurable_sigma_sigma isotoneI real_arch_lt |
777 then have A_eq: "A = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..< xs i})" |
804 simp: product_algebra_def) |
778 using A by auto |
805 then show ?thesis |
779 have "e2p -` A = {..< (\<chi>\<chi> i. xs i) :: 'a}" |
806 unfolding lborel_def borel_eq_lessThan lebesgue_def sigma_def by simp |
780 using DIM_positive by (auto simp add: Pi_iff set_eq_iff e2p_def A_eq |
|
781 euclidean_eq[where 'a='a] eucl_less[where 'a='a]) |
|
782 then show "e2p -` A \<inter> space ?E \<in> sets ?E" by simp |
|
783 qed |
807 qed |
784 |
808 |
785 lemma measurable_e2p: |
809 lemma measurable_e2p: |
786 "e2p \<in> measurable (borel::'a algebra) |
810 "e2p \<in> measurable (borel::'a::ordered_euclidean_space algebra) |
787 (sigma (product_algebra (\<lambda>x. borel :: real algebra) {..<DIM('a::ordered_euclidean_space)}))" |
811 (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. (lborel :: real measure_space))" |
788 using measurable_e2p_on_generator[where 'a='a] unfolding borel_eq_lessThan |
812 (is "_ \<in> measurable ?E ?P") |
789 by (subst sigma_product_algebra_sigma_eq[where S="\<lambda>_ i. {..<real i}"]) |
813 proof - |
790 (auto intro!: measurable_sigma_sigma isotoneI real_arch_lt |
814 let ?B = "\<lparr> space = UNIV::real set, sets = range lessThan, measure = lebesgue.\<mu> \<rparr>" |
791 simp: product_algebra_def) |
815 let ?G = "product_algebra_generator {..<DIM('a)} (\<lambda>_. ?B)" |
792 |
816 have "e2p \<in> measurable ?E (sigma ?G)" |
793 lemma measurable_p2e_on_generator: |
817 proof (rule borel.measurable_sigma) |
794 "p2e \<in> measurable |
818 show "e2p \<in> space ?E \<rightarrow> space ?G" by (auto simp: e2p_def) |
795 (product_algebra |
819 fix A assume "A \<in> sets ?G" |
796 (\<lambda>x. \<lparr> space = UNIV::real set, sets = range lessThan \<rparr>) |
820 then obtain E where A: "A = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. E i)" |
797 {..<DIM('a::ordered_euclidean_space)}) |
821 and "E \<in> {..<DIM('a)} \<rightarrow> (range lessThan)" |
798 \<lparr> space = UNIV::'a set, sets = range lessThan \<rparr>" |
822 by (auto elim!: product_algebraE simp: ) |
799 (is "p2e \<in> measurable ?P ?E") |
823 then have "\<forall>i\<in>{..<DIM('a)}. \<exists>xs. E i = {..< xs}" by auto |
800 proof (unfold measurable_def, intro CollectI conjI ballI) |
824 from this[THEN bchoice] guess xs .. |
|
825 then have A_eq: "A = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..< xs i})" |
|
826 using A by auto |
|
827 have "e2p -` A = {..< (\<chi>\<chi> i. xs i) :: 'a}" |
|
828 using DIM_positive by (auto simp add: Pi_iff set_eq_iff e2p_def A_eq |
|
829 euclidean_eq[where 'a='a] eucl_less[where 'a='a]) |
|
830 then show "e2p -` A \<inter> space ?E \<in> sets ?E" by simp |
|
831 qed (auto simp: product_algebra_generator_def) |
|
832 with sets_product_borel[of "{..<DIM('a)}"] show ?thesis |
|
833 unfolding measurable_def product_algebra_def by simp |
|
834 qed |
|
835 |
|
836 lemma measurable_p2e: |
|
837 "p2e \<in> measurable (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. (lborel :: real measure_space)) |
|
838 (borel :: 'a::ordered_euclidean_space algebra)" |
|
839 (is "p2e \<in> measurable ?P _") |
|
840 unfolding borel_eq_lessThan |
|
841 proof (intro lborel_space.measurable_sigma) |
|
842 let ?E = "\<lparr> space = UNIV :: 'a set, sets = range lessThan \<rparr>" |
801 show "p2e \<in> space ?P \<rightarrow> space ?E" by simp |
843 show "p2e \<in> space ?P \<rightarrow> space ?E" by simp |
802 fix A assume "A \<in> sets ?E" |
844 fix A assume "A \<in> sets ?E" |
803 then obtain x where "A = {..<x}" by auto |
845 then obtain x where "A = {..<x}" by auto |
804 then have "p2e -` A \<inter> space ?P = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..< x $$ i})" |
846 then have "p2e -` A \<inter> space ?P = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..< x $$ i})" |
805 using DIM_positive |
847 using DIM_positive |
806 by (auto simp: Pi_iff set_eq_iff p2e_def |
848 by (auto simp: Pi_iff set_eq_iff p2e_def |
807 euclidean_eq[where 'a='a] eucl_less[where 'a='a]) |
849 euclidean_eq[where 'a='a] eucl_less[where 'a='a]) |
808 then show "p2e -` A \<inter> space ?P \<in> sets ?P" by auto |
850 then show "p2e -` A \<inter> space ?P \<in> sets ?P" by auto |
809 qed |
851 qed simp |
810 |
|
811 lemma measurable_p2e: |
|
812 "p2e \<in> measurable (sigma (product_algebra (\<lambda>x. borel :: real algebra) {..<DIM('a::ordered_euclidean_space)})) |
|
813 (borel::'a algebra)" |
|
814 using measurable_p2e_on_generator[where 'a='a] unfolding borel_eq_lessThan |
|
815 by (subst sigma_product_algebra_sigma_eq[where S="\<lambda>_ i. {..<real i}"]) |
|
816 (auto intro!: measurable_sigma_sigma isotoneI real_arch_lt |
|
817 simp: product_algebra_def) |
|
818 |
852 |
819 lemma e2p_Int:"e2p ` A \<inter> e2p ` B = e2p ` (A \<inter> B)" (is "?L = ?R") |
853 lemma e2p_Int:"e2p ` A \<inter> e2p ` B = e2p ` (A \<inter> B)" (is "?L = ?R") |
820 apply(rule image_Int[THEN sym]) |
854 apply(rule image_Int[THEN sym]) |
821 using bij_inv_p2e_e2p[THEN bij_inv_bij_betw(2)] |
855 using bij_inv_p2e_e2p[THEN bij_inv_bij_betw(2)] |
822 unfolding bij_betw_def by auto |
856 unfolding bij_betw_def by auto |
838 apply safe unfolding inter_interval by auto |
872 apply safe unfolding inter_interval by auto |
839 |
873 |
840 lemma lmeasure_measure_eq_borel_prod: |
874 lemma lmeasure_measure_eq_borel_prod: |
841 fixes A :: "('a::ordered_euclidean_space) set" |
875 fixes A :: "('a::ordered_euclidean_space) set" |
842 assumes "A \<in> sets borel" |
876 assumes "A \<in> sets borel" |
843 shows "lmeasure A = borel_product.product_measure {..<DIM('a)} (e2p ` A :: (nat \<Rightarrow> real) set)" |
877 shows "lebesgue.\<mu> A = lborel_space.\<mu> TYPE('a) (e2p ` A)" (is "_ = ?m A") |
844 proof (rule measure_unique_Int_stable[where X=A and A=cube]) |
878 proof (rule measure_unique_Int_stable[where X=A and A=cube]) |
845 interpret fprod: finite_product_sigma_finite "\<lambda>x. borel :: real algebra" "\<lambda>x. lmeasure" "{..<DIM('a)}" by default auto |
|
846 show "Int_stable \<lparr> space = UNIV :: 'a set, sets = range (\<lambda>(a,b). {a..b}) \<rparr>" |
879 show "Int_stable \<lparr> space = UNIV :: 'a set, sets = range (\<lambda>(a,b). {a..b}) \<rparr>" |
847 (is "Int_stable ?E" ) using Int_stable_cuboids' . |
880 (is "Int_stable ?E" ) using Int_stable_cuboids' . |
848 show "borel = sigma ?E" using borel_eq_atLeastAtMost . |
881 have [simp]: "sigma ?E = borel" using borel_eq_atLeastAtMost .. |
849 show "\<And>i. lmeasure (cube i) \<noteq> \<omega>" unfolding cube_def by auto |
882 show "\<And>i. lebesgue.\<mu> (cube i) \<noteq> \<omega>" unfolding cube_def by auto |
850 show "\<And>X. X \<in> sets ?E \<Longrightarrow> |
883 show "\<And>X. X \<in> sets ?E \<Longrightarrow> lebesgue.\<mu> X = ?m X" |
851 lmeasure X = borel_product.product_measure {..<DIM('a)} (e2p ` X :: (nat \<Rightarrow> real) set)" |
|
852 proof- case goal1 then obtain a b where X:"X = {a..b}" by auto |
884 proof- case goal1 then obtain a b where X:"X = {a..b}" by auto |
853 { presume *:"X \<noteq> {} \<Longrightarrow> ?case" |
885 { presume *:"X \<noteq> {} \<Longrightarrow> ?case" |
854 show ?case apply(cases,rule *,assumption) by auto } |
886 show ?case apply(cases,rule *,assumption) by auto } |
855 def XX \<equiv> "\<lambda>i. {a $$ i .. b $$ i}" assume "X \<noteq> {}" note X' = this[unfolded X interval_ne_empty] |
887 def XX \<equiv> "\<lambda>i. {a $$ i .. b $$ i}" assume "X \<noteq> {}" note X' = this[unfolded X interval_ne_empty] |
856 have *:"Pi\<^isub>E {..<DIM('a)} XX = e2p ` X" apply(rule set_eqI) |
888 have *:"Pi\<^isub>E {..<DIM('a)} XX = e2p ` X" apply(rule set_eqI) |
859 unfolding Pi_def extensional_def e2p_def restrict_def X mem_interval XX_def by rule auto |
891 unfolding Pi_def extensional_def e2p_def restrict_def X mem_interval XX_def by rule auto |
860 next fix x assume "x \<in> e2p ` X" then guess y unfolding image_iff .. note y = this |
892 next fix x assume "x \<in> e2p ` X" then guess y unfolding image_iff .. note y = this |
861 show "x \<in> Pi\<^isub>E {..<DIM('a)} XX" unfolding y using y(1) |
893 show "x \<in> Pi\<^isub>E {..<DIM('a)} XX" unfolding y using y(1) |
862 unfolding Pi_def extensional_def e2p_def restrict_def X mem_interval XX_def by auto |
894 unfolding Pi_def extensional_def e2p_def restrict_def X mem_interval XX_def by auto |
863 qed |
895 qed |
864 have "lmeasure X = (\<Prod>x<DIM('a). Real (b $$ x - a $$ x))" using X' apply- unfolding X |
896 have "lebesgue.\<mu> X = (\<Prod>x<DIM('a). Real (b $$ x - a $$ x))" using X' apply- unfolding X |
865 unfolding lmeasure_atLeastAtMost content_closed_interval apply(subst Real_setprod) by auto |
897 unfolding lmeasure_atLeastAtMost content_closed_interval apply(subst Real_setprod) by auto |
866 also have "... = (\<Prod>i<DIM('a). lmeasure (XX i))" apply(rule setprod_cong2) |
898 also have "... = (\<Prod>i<DIM('a). lebesgue.\<mu> (XX i))" apply(rule setprod_cong2) |
867 unfolding XX_def lmeasure_atLeastAtMost apply(subst content_real) using X' by auto |
899 unfolding XX_def lmeasure_atLeastAtMost apply(subst content_real) using X' by auto |
868 also have "... = borel_product.product_measure {..<DIM('a)} (e2p ` X)" unfolding *[THEN sym] |
900 also have "... = ?m X" unfolding *[THEN sym] |
869 apply(rule fprod.measure_times[THEN sym]) unfolding XX_def by auto |
901 apply(rule lborel_space.measure_times[symmetric]) unfolding XX_def by auto |
870 finally show ?case . |
902 finally show ?case . |
871 qed |
903 qed |
872 |
904 |
873 show "range cube \<subseteq> sets \<lparr>space = UNIV, sets = range (\<lambda>(a, b). {a..b})\<rparr>" |
905 show "range cube \<subseteq> sets \<lparr>space = UNIV, sets = range (\<lambda>(a, b). {a..b})\<rparr>" |
874 unfolding cube_def_raw by auto |
906 unfolding cube_def_raw by auto |
875 have "\<And>x. \<exists>xa. x \<in> cube xa" apply(rule_tac x=x in mem_big_cube) by fastsimp |
907 have "\<And>x. \<exists>xa. x \<in> cube xa" apply(rule_tac x=x in mem_big_cube) by fastsimp |
876 thus "cube \<up> space \<lparr>space = UNIV, sets = range (\<lambda>(a, b). {a..b})\<rparr>" |
908 thus "cube \<up> space \<lparr>space = UNIV, sets = range (\<lambda>(a, b). {a..b})\<rparr>" |
877 apply-apply(rule isotoneI) apply(rule cube_subset_Suc) by auto |
909 apply-apply(rule isotoneI) apply(rule cube_subset_Suc) by auto |
878 show "A \<in> sets borel " by fact |
910 show "A \<in> sets (sigma ?E)" using assms by simp |
879 show "measure_space borel lmeasure" by default |
911 have "measure_space lborel" by default |
880 show "measure_space borel |
912 then show "measure_space \<lparr> space = space ?E, sets = sets (sigma ?E), measure = measure lebesgue\<rparr>" |
881 (\<lambda>a::'a set. finite_product_sigma_finite.measure (\<lambda>x. borel) (\<lambda>x. lmeasure) {..<DIM('a)} (e2p ` a))" |
913 unfolding lebesgue_def lborel_def by simp |
882 proof (rule fprod.measure_space_vimage) |
914 let ?M = "\<lparr> space = space ?E, sets = sets (sigma ?E), measure = ?m \<rparr>" |
883 show "sigma_algebra borel" by default |
915 show "measure_space ?M" |
884 show "(p2e :: (nat \<Rightarrow> real) \<Rightarrow> 'a) \<in> measurable fprod.P borel" by (rule measurable_p2e) |
916 proof (rule lborel_space.measure_space_vimage) |
885 fix A :: "'a set" assume "A \<in> sets borel" |
917 show "sigma_algebra ?M" by (rule lborel.sigma_algebra_cong) auto |
886 show "fprod.measure (e2p ` A) = fprod.measure (p2e -` A \<inter> space fprod.P)" |
918 show "p2e \<in> measurable (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. lborel) ?M" |
|
919 using measurable_p2e unfolding measurable_def by auto |
|
920 fix A :: "'a set" assume "A \<in> sets ?M" |
|
921 show "measure ?M A = lborel_space.\<mu> TYPE('a) (p2e -` A \<inter> space (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. lborel))" |
887 by (simp add: e2p_image_vimage) |
922 by (simp add: e2p_image_vimage) |
888 qed |
923 qed |
889 qed |
924 qed simp |
890 |
925 |
891 lemma range_e2p:"range (e2p::'a::ordered_euclidean_space \<Rightarrow> _) = extensional {..<DIM('a)}" |
926 lemma range_e2p:"range (e2p::'a::ordered_euclidean_space \<Rightarrow> _) = extensional {..<DIM('a)}" |
892 unfolding e2p_def_raw |
927 unfolding e2p_def_raw |
893 apply auto |
928 apply auto |
894 by (rule_tac x="\<chi>\<chi> i. x i" in image_eqI) (auto simp: fun_eq_iff extensional_def) |
929 by (rule_tac x="\<chi>\<chi> i. x i" in image_eqI) (auto simp: fun_eq_iff extensional_def) |
895 |
930 |
896 lemma borel_fubini_positiv_integral: |
931 lemma borel_fubini_positiv_integral: |
897 fixes f :: "'a::ordered_euclidean_space \<Rightarrow> pextreal" |
932 fixes f :: "'a::ordered_euclidean_space \<Rightarrow> pextreal" |
898 assumes f: "f \<in> borel_measurable borel" |
933 assumes f: "f \<in> borel_measurable borel" |
899 shows "borel.positive_integral f = |
934 shows "integral\<^isup>P lborel f = \<integral>\<^isup>+x. f (p2e x) \<partial>(lborel_space.P TYPE('a))" |
900 borel_product.product_positive_integral {..<DIM('a)} (f \<circ> p2e)" |
935 proof (rule lborel.positive_integral_vimage[symmetric, of _ "e2p :: 'a \<Rightarrow> _" "(\<lambda>x. f (p2e x))", unfolded p2e_e2p]) |
901 proof- def U \<equiv> "extensional {..<DIM('a)} :: (nat \<Rightarrow> real) set" |
936 show "(e2p :: 'a \<Rightarrow> _) \<in> measurable borel (lborel_space.P TYPE('a))" by (rule measurable_e2p) |
902 interpret fprod: finite_product_sigma_finite "\<lambda>x. borel" "\<lambda>x. lmeasure" "{..<DIM('a)}" by default auto |
937 show "sigma_algebra (lborel_space.P TYPE('a))" by default |
903 show ?thesis |
938 from measurable_comp[OF measurable_p2e f] |
904 proof (subst borel.positive_integral_vimage[symmetric, of _ "e2p :: 'a \<Rightarrow> _" "(\<lambda>x. f (p2e x))", unfolded p2e_e2p]) |
939 show "(\<lambda>x. f (p2e x)) \<in> borel_measurable (lborel_space.P TYPE('a))" by (simp add: comp_def) |
905 show "(e2p :: 'a \<Rightarrow> _) \<in> measurable borel fprod.P" by (rule measurable_e2p) |
940 let "?L A" = "lebesgue.\<mu> ((e2p::'a \<Rightarrow> (nat \<Rightarrow> real)) -` A \<inter> UNIV)" |
906 show "sigma_algebra fprod.P" by default |
941 fix A :: "(nat \<Rightarrow> real) set" assume "A \<in> sets (lborel_space.P TYPE('a))" |
907 from measurable_comp[OF measurable_p2e f] |
942 then have A: "(e2p::'a \<Rightarrow> (nat \<Rightarrow> real)) -` A \<inter> space borel \<in> sets borel" |
908 show "(\<lambda>x. f (p2e x)) \<in> borel_measurable fprod.P" by (simp add: comp_def) |
943 by (rule measurable_sets[OF measurable_e2p]) |
909 let "?L A" = "lmeasure ((e2p::'a \<Rightarrow> (nat \<Rightarrow> real)) -` A \<inter> space borel)" |
944 have [simp]: "A \<inter> extensional {..<DIM('a)} = A" |
910 show "measure_space.positive_integral fprod.P ?L (\<lambda>x. f (p2e x)) = |
945 using `A \<in> sets (lborel_space.P TYPE('a))`[THEN lborel_space.sets_into_space] by auto |
911 fprod.positive_integral (f \<circ> p2e)" |
946 show "lborel_space.\<mu> TYPE('a) A = ?L A" |
912 unfolding comp_def |
947 using lmeasure_measure_eq_borel_prod[OF A] by (simp add: range_e2p) |
913 proof (rule fprod.positive_integral_cong_measure) |
|
914 fix A :: "(nat \<Rightarrow> real) set" assume "A \<in> sets fprod.P" |
|
915 then have A: "(e2p::'a \<Rightarrow> (nat \<Rightarrow> real)) -` A \<inter> space borel \<in> sets borel" |
|
916 by (rule measurable_sets[OF measurable_e2p]) |
|
917 have [simp]: "A \<inter> extensional {..<DIM('a)} = A" |
|
918 using `A \<in> sets fprod.P`[THEN fprod.sets_into_space] by auto |
|
919 show "?L A = fprod.measure A" |
|
920 unfolding lmeasure_measure_eq_borel_prod[OF A] |
|
921 by (simp add: range_e2p) |
|
922 qed |
|
923 qed |
|
924 qed |
948 qed |
925 |
949 |
926 lemma borel_fubini: |
950 lemma borel_fubini: |
927 fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real" |
951 fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real" |
928 assumes f: "f \<in> borel_measurable borel" |
952 assumes f: "f \<in> borel_measurable borel" |
929 shows "borel.integral f = borel_product.product_integral {..<DIM('a)} (f \<circ> p2e)" |
953 shows "integral\<^isup>L lborel f = \<integral>x. f (p2e x) \<partial>(lborel_space.P TYPE('a))" |
930 proof- interpret fprod: finite_product_sigma_finite "\<lambda>x. borel" "\<lambda>x. lmeasure" "{..<DIM('a)}" by default auto |
954 proof - |
931 have 1:"(\<lambda>x. Real (f x)) \<in> borel_measurable borel" using f by auto |
955 have 1:"(\<lambda>x. Real (f x)) \<in> borel_measurable borel" using f by auto |
932 have 2:"(\<lambda>x. Real (- f x)) \<in> borel_measurable borel" using f by auto |
956 have 2:"(\<lambda>x. Real (- f x)) \<in> borel_measurable borel" using f by auto |
933 show ?thesis unfolding fprod.integral_def borel.integral_def |
957 show ?thesis unfolding lebesgue_integral_def |
934 unfolding borel_fubini_positiv_integral[OF 1] borel_fubini_positiv_integral[OF 2] |
958 unfolding borel_fubini_positiv_integral[OF 1] borel_fubini_positiv_integral[OF 2] |
935 unfolding o_def .. |
959 unfolding o_def .. |
936 qed |
960 qed |
937 |
961 |
938 end |
962 end |