765 shows "(\<lambda>x. g (f x)) \<in> measurable (vimage_algebra S f) M2" |
765 shows "(\<lambda>x. g (f x)) \<in> measurable (vimage_algebra S f) M2" |
766 proof - |
766 proof - |
767 note measurable_vimage_algebra[OF assms(2)] |
767 note measurable_vimage_algebra[OF assms(2)] |
768 from measurable_comp[OF this assms(1)] |
768 from measurable_comp[OF this assms(1)] |
769 show ?thesis by (simp add: comp_def) |
769 show ?thesis by (simp add: comp_def) |
770 qed |
|
771 |
|
772 lemma (in sigma_algebra) vimage_vimage_inv: |
|
773 assumes f: "bij_betw f S (space M)" |
|
774 assumes [simp]: "\<And>x. x \<in> space M \<Longrightarrow> f (g x) = x" and g: "g \<in> space M \<rightarrow> S" |
|
775 shows "sigma_algebra.vimage_algebra (vimage_algebra S f) (space M) g = M" |
|
776 proof - |
|
777 interpret T: sigma_algebra "vimage_algebra S f" |
|
778 using f by (safe intro!: sigma_algebra_vimage bij_betw_imp_funcset) |
|
779 |
|
780 have inj: "inj_on f S" and [simp]: "f`S = space M" |
|
781 using f unfolding bij_betw_def by auto |
|
782 |
|
783 { fix A assume A: "A \<in> sets M" |
|
784 have "g -` f -` A \<inter> g -` S \<inter> space M = (f \<circ> g) -` A \<inter> space M" |
|
785 using g by auto |
|
786 also have "\<dots> = A" |
|
787 using `A \<in> sets M`[THEN sets_into_space] by auto |
|
788 finally have "g -` f -` A \<inter> g -` S \<inter> space M = A" . } |
|
789 note X = this |
|
790 show ?thesis |
|
791 unfolding T.vimage_algebra_def unfolding vimage_algebra_def |
|
792 by (simp add: image_compose[symmetric] comp_def X cong: image_cong) |
|
793 qed |
|
794 |
|
795 lemma (in sigma_algebra) measurable_vimage_iff: |
|
796 fixes f :: "'b \<Rightarrow> 'a" assumes f: "bij_betw f S (space M)" |
|
797 shows "g \<in> measurable M M' \<longleftrightarrow> (g \<circ> f) \<in> measurable (vimage_algebra S f) M'" |
|
798 proof |
|
799 assume "g \<in> measurable M M'" |
|
800 from measurable_vimage[OF this f[THEN bij_betw_imp_funcset]] |
|
801 show "(g \<circ> f) \<in> measurable (vimage_algebra S f) M'" unfolding comp_def . |
|
802 next |
|
803 interpret v: sigma_algebra "vimage_algebra S f" |
|
804 using f[THEN bij_betw_imp_funcset] by (rule sigma_algebra_vimage) |
|
805 note f' = f[THEN bij_betw_the_inv_into] |
|
806 assume "g \<circ> f \<in> measurable (vimage_algebra S f) M'" |
|
807 from v.measurable_vimage[OF this, unfolded space_vimage_algebra, OF f'[THEN bij_betw_imp_funcset]] |
|
808 show "g \<in> measurable M M'" |
|
809 using f f'[THEN bij_betw_imp_funcset] f[unfolded bij_betw_def] |
|
810 by (subst (asm) vimage_vimage_inv) |
|
811 (simp_all add: f_the_inv_into_f cong: measurable_cong) |
|
812 qed |
770 qed |
813 |
771 |
814 lemma sigma_sets_vimage: |
772 lemma sigma_sets_vimage: |
815 assumes "f \<in> S' \<rightarrow> S" and "A \<subseteq> Pow S" |
773 assumes "f \<in> S' \<rightarrow> S" and "A \<subseteq> Pow S" |
816 shows "sigma_sets S' ((\<lambda>X. f -` X \<inter> S') ` A) = (\<lambda>X. f -` X \<inter> S') ` sigma_sets S A" |
774 shows "sigma_sets S' ((\<lambda>X. f -` X \<inter> S') ` A) = (\<lambda>X. f -` X \<inter> S') ` sigma_sets S A" |
1415 by (auto simp: subset_image_iff sets_eq_Pow image_space_def) |
1373 by (auto simp: subset_image_iff sets_eq_Pow image_space_def) |
1416 then show "S \<in> sets (image_space X)" |
1374 then show "S \<in> sets (image_space X)" |
1417 by (auto simp: image_space_def) |
1375 by (auto simp: image_space_def) |
1418 qed |
1376 qed |
1419 |
1377 |
1420 subsection "Bijective functions with inverse" |
|
1421 |
|
1422 definition "bij_inv A B f g \<longleftrightarrow> |
|
1423 f \<in> A \<rightarrow> B \<and> g \<in> B \<rightarrow> A \<and> (\<forall>x\<in>A. g (f x) = x) \<and> (\<forall>x\<in>B. f (g x) = x)" |
|
1424 |
|
1425 lemma bij_inv_symmetric[sym]: "bij_inv A B f g \<Longrightarrow> bij_inv B A g f" |
|
1426 unfolding bij_inv_def by auto |
|
1427 |
|
1428 lemma bij_invI: |
|
1429 assumes "f \<in> A \<rightarrow> B" "g \<in> B \<rightarrow> A" |
|
1430 and "\<And>x. x \<in> A \<Longrightarrow> g (f x) = x" |
|
1431 and "\<And>x. x \<in> B \<Longrightarrow> f (g x) = x" |
|
1432 shows "bij_inv A B f g" |
|
1433 using assms unfolding bij_inv_def by auto |
|
1434 |
|
1435 lemma bij_invE: |
|
1436 assumes "bij_inv A B f g" |
|
1437 "\<lbrakk> f \<in> A \<rightarrow> B ; g \<in> B \<rightarrow> A ; |
|
1438 (\<And>x. x \<in> A \<Longrightarrow> g (f x) = x) ; |
|
1439 (\<And>x. x \<in> B \<Longrightarrow> f (g x) = x) \<rbrakk> \<Longrightarrow> P" |
|
1440 shows P |
|
1441 using assms unfolding bij_inv_def by auto |
|
1442 |
|
1443 lemma bij_inv_bij_betw: |
|
1444 assumes "bij_inv A B f g" |
|
1445 shows "bij_betw f A B" "bij_betw g B A" |
|
1446 using assms by (auto intro: bij_betwI elim!: bij_invE) |
|
1447 |
|
1448 lemma bij_inv_vimage_vimage: |
|
1449 assumes "bij_inv A B f e" |
|
1450 shows "f -` (e -` X \<inter> B) \<inter> A = X \<inter> A" |
|
1451 using assms by (auto elim!: bij_invE) |
|
1452 |
|
1453 lemma (in sigma_algebra) measurable_vimage_iff_inv: |
|
1454 fixes f :: "'b \<Rightarrow> 'a" assumes "bij_inv S (space M) f g" |
|
1455 shows "h \<in> measurable (vimage_algebra S f) M' \<longleftrightarrow> (\<lambda>x. h (g x)) \<in> measurable M M'" |
|
1456 unfolding measurable_vimage_iff[OF bij_inv_bij_betw(1), OF assms] |
|
1457 proof (rule measurable_cong) |
|
1458 fix w assume "w \<in> space (vimage_algebra S f)" |
|
1459 then have "w \<in> S" by auto |
|
1460 then show "h w = ((\<lambda>x. h (g x)) \<circ> f) w" |
|
1461 using assms by (auto elim: bij_invE) |
|
1462 qed |
|
1463 |
|
1464 lemma vimage_algebra_sigma: |
|
1465 assumes bi: "bij_inv (space (sigma F)) (space (sigma E)) f e" |
|
1466 and "sets E \<subseteq> Pow (space E)" and F: "sets F \<subseteq> Pow (space F)" |
|
1467 and "more E = more F" |
|
1468 and "f \<in> measurable F E" "e \<in> measurable E F" |
|
1469 shows "sigma_algebra.vimage_algebra (sigma E) (space (sigma F)) f = sigma F" |
|
1470 proof - |
|
1471 interpret sigma_algebra "sigma E" |
|
1472 using assms by (intro sigma_algebra_sigma) auto |
|
1473 have eq: "sets F = (\<lambda>X. f -` X \<inter> space F) ` sets E" |
|
1474 proof safe |
|
1475 fix X assume "X \<in> sets F" |
|
1476 then have "e -` X \<inter> space E \<in> sets E" |
|
1477 using `e \<in> measurable E F` unfolding measurable_def by auto |
|
1478 then show "X \<in>(\<lambda>Y. f -` Y \<inter> space F) ` sets E" |
|
1479 apply (rule rev_image_eqI) |
|
1480 unfolding bij_inv_vimage_vimage[OF bi[simplified]] |
|
1481 using F `X \<in> sets F` by auto |
|
1482 next |
|
1483 fix X assume "X \<in> sets E" then show "f -` X \<inter> space F \<in> sets F" |
|
1484 using `f \<in> measurable F E` unfolding measurable_def by auto |
|
1485 qed |
|
1486 show "vimage_algebra (space (sigma F)) f = sigma F" |
|
1487 unfolding vimage_algebra_def using assms |
|
1488 by (auto simp: bij_inv_def eq sigma_sets_vimage[symmetric] sigma_def) |
|
1489 qed |
|
1490 |
|
1491 lemma measurable_sigma_sigma: |
1378 lemma measurable_sigma_sigma: |
1492 assumes M: "sets M \<subseteq> Pow (space M)" and N: "sets N \<subseteq> Pow (space N)" |
1379 assumes M: "sets M \<subseteq> Pow (space M)" and N: "sets N \<subseteq> Pow (space N)" |
1493 shows "f \<in> measurable M N \<Longrightarrow> f \<in> measurable (sigma M) (sigma N)" |
1380 shows "f \<in> measurable M N \<Longrightarrow> f \<in> measurable (sigma M) (sigma N)" |
1494 using sigma_algebra.measurable_subset[OF sigma_algebra_sigma[OF M], of N] |
1381 using sigma_algebra.measurable_subset[OF sigma_algebra_sigma[OF M], of N] |
1495 using measurable_up_sigma[of M N] N by auto |
1382 using measurable_up_sigma[of M N] N by auto |
1496 |
1383 |
1497 lemma bij_inv_the_inv_into: |
|
1498 assumes "bij_betw f A B" shows "bij_inv A B f (the_inv_into A f)" |
|
1499 proof (rule bij_invI) |
|
1500 show "the_inv_into A f \<in> B \<rightarrow> A" |
|
1501 using bij_betw_the_inv_into[OF assms] by (rule bij_betw_imp_funcset) |
|
1502 show "f \<in> A \<rightarrow> B" using assms by (rule bij_betw_imp_funcset) |
|
1503 show "\<And>x. x \<in> A \<Longrightarrow> the_inv_into A f (f x) = x" |
|
1504 "\<And>x. x \<in> B \<Longrightarrow> f (the_inv_into A f x) = x" |
|
1505 using the_inv_into_f_f[of f A] f_the_inv_into_f[of f A] |
|
1506 using assms by (auto simp: bij_betw_def) |
|
1507 qed |
|
1508 |
|
1509 end |
1384 end |