(* Title: HOL/Analysis/Embed_Measure.thy Author: Manuel Eberl, TU München Defines measure embeddings with injective functions, i.e. lifting a measure on some values to a measure on "tagged" values (e.g. embed_measure M Inl lifts a measure on values 'a to a measure on the left part of the sum type 'a + 'b) *) section ‹Embedding Measure Spaces with a Function› theory Embed_Measure imports Binary_Product_Measure begin text ‹ Given a measure space on some carrier set ‹Ω› and a function ‹f›, we can define a push-forward measure on the carrier set ‹f(Ω)› whose ‹σ›-algebra is the one generated by mapping ‹f› over the original sigma algebra. This is useful e.\,g.\ when ‹f› is injective, i.\,e.\ it is some kind of ``tagging'' function. For instance, suppose we have some algebraaic datatype of values with various constructors, including a constructor ‹RealVal› for real numbers. Then ‹embed_measure› allows us to lift a measure on real numbers to the appropriate subset of that algebraic datatype. › definition✐‹tag important› embed_measure :: "'a measure ⇒ ('a ⇒ 'b) ⇒ 'b measure" where "embed_measure M f = measure_of (f ` space M) {f ` A |A. A ∈ sets M} (λA. emeasure M (f -` A ∩ space M))" lemma space_embed_measure: "space (embed_measure M f) = f ` space M" unfolding embed_measure_def by (subst space_measure_of) (auto dest: sets.sets_into_space) lemma sets_embed_measure': assumes inj: "inj_on f (space M)" shows "sets (embed_measure M f) = {f ` A |A. A ∈ sets M}" unfolding embed_measure_def proof (intro sigma_algebra.sets_measure_of_eq sigma_algebra_iff2[THEN iffD2] conjI allI ballI impI) fix s assume "s ∈ {f ` A |A. A ∈ sets M}" then obtain s' where s'_props: "s = f ` s'" "s' ∈ sets M" by auto hence "f ` space M - s = f ` (space M - s')" using inj by (auto dest: inj_onD sets.sets_into_space) also have "... ∈ {f ` A |A. A ∈ sets M}" using s'_props by auto finally show "f ` space M - s ∈ {f ` A |A. A ∈ sets M}" . next fix A :: "nat ⇒ _" assume "range A ⊆ {f ` A |A. A ∈ sets M}" then obtain A' where A': "⋀i. A i = f ` A' i" "⋀i. A' i ∈ sets M" by (auto simp: subset_eq choice_iff) then have "(⋃x. f ` A' x) = f ` (⋃x. A' x)" by blast with A' show "(⋃i. A i) ∈ {f ` A |A. A ∈ sets M}" by simp blast qed (auto dest: sets.sets_into_space) lemma the_inv_into_vimage: "inj_on f X ⟹ A ⊆ X ⟹ the_inv_into X f -` A ∩ (f`X) = f ` A" by (auto simp: the_inv_into_f_f) lemma sets_embed_eq_vimage_algebra: assumes "inj_on f (space M)" shows "sets (embed_measure M f) = sets (vimage_algebra (f`space M) (the_inv_into (space M) f) M)" by (auto simp: sets_embed_measure'[OF assms] Pi_iff the_inv_into_f_f assms sets_vimage_algebra2 Setcompr_eq_image dest: sets.sets_into_space intro!: image_cong the_inv_into_vimage[symmetric]) lemma sets_embed_measure: assumes inj: "inj f" shows "sets (embed_measure M f) = {f ` A |A. A ∈ sets M}" using assms by (subst sets_embed_measure') (auto intro!: inj_onI dest: injD) lemma in_sets_embed_measure: "A ∈ sets M ⟹ f ` A ∈ sets (embed_measure M f)" unfolding embed_measure_def by (intro in_measure_of) (auto dest: sets.sets_into_space) lemma measurable_embed_measure1: assumes g: "(λx. g (f x)) ∈ measurable M N" shows "g ∈ measurable (embed_measure M f) N" unfolding measurable_def proof safe fix A assume "A ∈ sets N" with g have "(λx. g (f x)) -` A ∩ space M ∈ sets M" by (rule measurable_sets) then have "f ` ((λx. g (f x)) -` A ∩ space M) ∈ sets (embed_measure M f)" by (rule in_sets_embed_measure) also have "f ` ((λx. g (f x)) -` A ∩ space M) = g -` A ∩ space (embed_measure M f)" by (auto simp: space_embed_measure) finally show "g -` A ∩ space (embed_measure M f) ∈ sets (embed_measure M f)" . qed (insert measurable_space[OF assms], auto simp: space_embed_measure) lemma measurable_embed_measure2': assumes "inj_on f (space M)" shows "f ∈ measurable M (embed_measure M f)" proof- { fix A assume A: "A ∈ sets M" also from A have "A = A ∩ space M" by auto also have "... = f -` f ` A ∩ space M" using A assms by (auto dest: inj_onD sets.sets_into_space) finally have "f -` f ` A ∩ space M ∈ sets M" . } thus ?thesis using assms unfolding embed_measure_def by (intro measurable_measure_of) (auto dest: sets.sets_into_space) qed lemma measurable_embed_measure2: assumes [simp]: "inj f" shows "f ∈ measurable M (embed_measure M f)" by (auto simp: inj_vimage_image_eq embed_measure_def intro!: measurable_measure_of dest: sets.sets_into_space) lemma embed_measure_eq_distr': assumes "inj_on f (space M)" shows "embed_measure M f = distr M (embed_measure M f) f" proof- have "distr M (embed_measure M f) f = measure_of (f ` space M) {f ` A |A. A ∈ sets M} (λA. emeasure M (f -` A ∩ space M))" unfolding distr_def by (simp add: space_embed_measure sets_embed_measure'[OF assms]) also have "... = embed_measure M f" unfolding embed_measure_def .. finally show ?thesis .. qed lemma embed_measure_eq_distr: "inj f ⟹ embed_measure M f = distr M (embed_measure M f) f" by (rule embed_measure_eq_distr') (auto intro!: inj_onI dest: injD) lemma nn_integral_embed_measure': "inj_on f (space M) ⟹ g ∈ borel_measurable (embed_measure M f) ⟹ nn_integral (embed_measure M f) g = nn_integral M (λx. g (f x))" apply (subst embed_measure_eq_distr', simp) apply (subst nn_integral_distr) apply (simp_all add: measurable_embed_measure2') done lemma nn_integral_embed_measure: "inj f ⟹ g ∈ borel_measurable (embed_measure M f) ⟹ nn_integral (embed_measure M f) g = nn_integral M (λx. g (f x))" by(erule nn_integral_embed_measure'[OF subset_inj_on]) simp lemma emeasure_embed_measure': assumes "inj_on f (space M)" "A ∈ sets (embed_measure M f)" shows "emeasure (embed_measure M f) A = emeasure M (f -` A ∩ space M)" by (subst embed_measure_eq_distr'[OF assms(1)]) (simp add: emeasure_distr[OF measurable_embed_measure2'[OF assms(1)] assms(2)]) lemma emeasure_embed_measure: assumes "inj f" "A ∈ sets (embed_measure M f)" shows "emeasure (embed_measure M f) A = emeasure M (f -` A ∩ space M)" using assms by (intro emeasure_embed_measure') (auto intro!: inj_onI dest: injD) lemma embed_measure_comp: assumes [simp]: "inj f" "inj g" shows "embed_measure (embed_measure M f) g = embed_measure M (g ∘ f)" proof- have [simp]: "inj (λx. g (f x))" by (subst o_def[symmetric]) (auto intro: inj_compose) note measurable_embed_measure2[measurable] have "embed_measure (embed_measure M f) g = distr M (embed_measure (embed_measure M f) g) (g ∘ f)" by (subst (1 2) embed_measure_eq_distr) (simp_all add: distr_distr sets_embed_measure cong: distr_cong) also have "... = embed_measure M (g ∘ f)" by (subst (3) embed_measure_eq_distr, simp add: o_def, rule distr_cong) (auto simp: sets_embed_measure o_def image_image[symmetric] intro: inj_compose cong: distr_cong) finally show ?thesis . qed lemma sigma_finite_embed_measure: assumes "sigma_finite_measure M" and inj: "inj f" shows "sigma_finite_measure (embed_measure M f)" proof - from assms(1) interpret sigma_finite_measure M . from sigma_finite_countable obtain A where A_props: "countable A" "A ⊆ sets M" "⋃A = space M" "⋀X. X∈A ⟹ emeasure M X ≠ ∞" by blast from A_props have "countable ((`) f`A)" by auto moreover from inj and A_props have "(`) f`A ⊆ sets (embed_measure M f)" by (auto simp: sets_embed_measure) moreover from A_props and inj have "⋃((`) f`A) = space (embed_measure M f)" by (auto simp: space_embed_measure intro!: imageI) moreover from A_props and inj have "∀a∈(`) f ` A. emeasure (embed_measure M f) a ≠ ∞" by (intro ballI, subst emeasure_embed_measure) (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure) ultimately show ?thesis by - (standard, blast) qed lemma embed_measure_count_space': "inj_on f A ⟹ embed_measure (count_space A) f = count_space (f`A)" apply (subst distr_bij_count_space[of f A "f`A", symmetric]) apply (simp add: inj_on_def bij_betw_def) apply (subst embed_measure_eq_distr') apply simp apply(auto 4 3 intro!: measure_eqI imageI simp add: sets_embed_measure' subset_image_iff) apply (subst (1 2) emeasure_distr) apply (auto simp: space_embed_measure sets_embed_measure') done lemma embed_measure_count_space: "inj f ⟹ embed_measure (count_space A) f = count_space (f`A)" by(rule embed_measure_count_space')(erule subset_inj_on, simp) lemma sets_embed_measure_alt: "inj f ⟹ sets (embed_measure M f) = ((`) f) ` sets M" by (auto simp: sets_embed_measure) lemma emeasure_embed_measure_image': assumes "inj_on f (space M)" "X ∈ sets M" shows "emeasure (embed_measure M f) (f`X) = emeasure M X" proof- from assms have "emeasure (embed_measure M f) (f`X) = emeasure M (f -` f ` X ∩ space M)" by (subst emeasure_embed_measure') (auto simp: sets_embed_measure') also from assms have "f -` f ` X ∩ space M = X" by (auto dest: inj_onD sets.sets_into_space) finally show ?thesis . qed lemma emeasure_embed_measure_image: "inj f ⟹ X ∈ sets M ⟹ emeasure (embed_measure M f) (f`X) = emeasure M X" by (simp_all add: emeasure_embed_measure in_sets_embed_measure inj_vimage_image_eq) lemma embed_measure_eq_iff: assumes "inj f" shows "embed_measure A f = embed_measure B f ⟷ A = B" (is "?M = ?N ⟷ _") proof from assms have I: "inj ((`) f)" by (auto intro: injI dest: injD) assume asm: "?M = ?N" hence "sets (embed_measure A f) = sets (embed_measure B f)" by simp with assms have "sets A = sets B" by (simp only: I inj_image_eq_iff sets_embed_measure_alt) moreover { fix X assume "X ∈ sets A" from asm have "emeasure ?M (f`X) = emeasure ?N (f`X)" by simp with ‹X ∈ sets A› and ‹sets A = sets B› and assms have "emeasure A X = emeasure B X" by (simp add: emeasure_embed_measure_image) } ultimately show "A = B" by (rule measure_eqI) qed simp lemma the_inv_into_in_Pi: "inj_on f A ⟹ the_inv_into A f ∈ f ` A → A" by (auto simp: the_inv_into_f_f) lemma map_prod_image: "map_prod f g ` (A × B) = (f`A) × (g`B)" using map_prod_surj_on[OF refl refl] . lemma map_prod_vimage: "map_prod f g -` (A × B) = (f-`A) × (g-`B)" by auto lemma embed_measure_prod: assumes f: "inj f" and g: "inj g" and [simp]: "sigma_finite_measure M" "sigma_finite_measure N" shows "embed_measure M f ⨂⇩_{M}embed_measure N g = embed_measure (M ⨂⇩_{M}N) (λ(x, y). (f x, g y))" (is "?L = _") unfolding map_prod_def[symmetric] proof (rule pair_measure_eqI) have fg[simp]: "⋀A. inj_on (map_prod f g) A" "⋀A. inj_on f A" "⋀A. inj_on g A" using f g by (auto simp: inj_on_def) note complete_lattice_class.Sup_insert[simp del] ccSup_insert[simp del] SUP_insert[simp del] ccSUP_insert[simp del] show sets: "sets ?L = sets (embed_measure (M ⨂⇩_{M}N) (map_prod f g))" unfolding map_prod_def[symmetric] apply (simp add: sets_pair_eq_sets_fst_snd sets_embed_eq_vimage_algebra cong: vimage_algebra_cong) apply (subst sets_vimage_Sup_eq[where Y="space (M ⨂⇩_{M}N)"]) apply (simp_all add: space_pair_measure[symmetric]) apply (auto simp add: the_inv_into_f_f simp del: map_prod_simp del: prod_fun_imageE) [] apply auto [] apply (subst (1 2 3 4 ) vimage_algebra_vimage_algebra_eq) apply (simp_all add: the_inv_into_in_Pi Pi_iff[of snd] Pi_iff[of fst] space_pair_measure) apply (simp_all add: Pi_iff[of snd] Pi_iff[of fst] the_inv_into_in_Pi vimage_algebra_vimage_algebra_eq space_pair_measure[symmetric] map_prod_image[symmetric]) apply (intro arg_cong[where f=sets] arg_cong[where f=Sup] arg_cong2[where f=insert] vimage_algebra_cong) apply (auto simp: map_prod_image the_inv_into_f_f simp del: map_prod_simp del: prod_fun_imageE) apply (simp_all add: the_inv_into_f_f space_pair_measure) done note measurable_embed_measure2[measurable] fix A B assume AB: "A ∈ sets (embed_measure M f)" "B ∈ sets (embed_measure N g)" moreover have "f -` A × g -` B ∩ space (M ⨂⇩_{M}N) = (f -` A ∩ space M) × (g -` B ∩ space N)" by (auto simp: space_pair_measure) ultimately show "emeasure (embed_measure M f) A * emeasure (embed_measure N g) B = emeasure (embed_measure (M ⨂⇩_{M}N) (map_prod f g)) (A × B)" by (simp add: map_prod_vimage sets[symmetric] emeasure_embed_measure sigma_finite_measure.emeasure_pair_measure_Times) qed (insert assms, simp_all add: sigma_finite_embed_measure) lemma mono_embed_measure: "space M = space M' ⟹ sets M ⊆ sets M' ⟹ sets (embed_measure M f) ⊆ sets (embed_measure M' f)" unfolding embed_measure_def apply (subst (1 2) sets_measure_of) apply (blast dest: sets.sets_into_space) apply (blast dest: sets.sets_into_space) apply simp apply (intro sigma_sets_mono') apply safe apply (simp add: subset_eq) apply metis done lemma density_embed_measure: assumes inj: "inj f" and Mg[measurable]: "g ∈ borel_measurable (embed_measure M f)" shows "density (embed_measure M f) g = embed_measure (density M (g ∘ f)) f" (is "?M1 = ?M2") proof (rule measure_eqI) fix X assume X: "X ∈ sets ?M1" from inj have Mf[measurable]: "f ∈ measurable M (embed_measure M f)" by (rule measurable_embed_measure2) from Mg and X have "emeasure ?M1 X = ∫⇧^{+}x. g x * indicator X x ∂embed_measure M f" by (subst emeasure_density) simp_all also from X have "... = ∫⇧^{+}x. g (f x) * indicator X (f x) ∂M" by (subst embed_measure_eq_distr[OF inj], subst nn_integral_distr) auto also have "... = ∫⇧^{+}x. g (f x) * indicator (f -` X ∩ space M) x ∂M" by (intro nn_integral_cong) (auto split: split_indicator) also from X have "... = emeasure (density M (g ∘ f)) (f -` X ∩ space M)" by (subst emeasure_density) (simp_all add: measurable_comp[OF Mf Mg] measurable_sets[OF Mf]) also from X and inj have "... = emeasure ?M2 X" by (subst emeasure_embed_measure) (simp_all add: sets_embed_measure) finally show "emeasure ?M1 X = emeasure ?M2 X" . qed (simp_all add: sets_embed_measure inj) lemma density_embed_measure': assumes inj: "inj f" and inv: "⋀x. f' (f x) = x" and Mg[measurable]: "g ∈ borel_measurable M" shows "density (embed_measure M f) (g ∘ f') = embed_measure (density M g) f" proof- have "density (embed_measure M f) (g ∘ f') = embed_measure (density M (g ∘ f' ∘ f)) f" by (rule density_embed_measure[OF inj]) (rule measurable_comp, rule measurable_embed_measure1, subst measurable_cong, rule inv, rule measurable_ident_sets, simp, rule Mg) also have "density M (g ∘ f' ∘ f) = density M g" by (intro density_cong) (subst measurable_cong, simp add: o_def inv, simp_all add: Mg inv) finally show ?thesis . qed lemma inj_on_image_subset_iff: assumes "inj_on f C" "A ⊆ C" "B ⊆ C" shows "f ` A ⊆ f ` B ⟷ A ⊆ B" proof (intro iffI subsetI) fix x assume A: "f ` A ⊆ f ` B" and B: "x ∈ A" from B have "f x ∈ f ` A" by blast with A have "f x ∈ f ` B" by blast then obtain y where "f x = f y" and "y ∈ B" by blast with assms and B have "x = y" by (auto dest: inj_onD) with ‹y ∈ B› show "x ∈ B" by simp qed auto lemma AE_embed_measure': assumes inj: "inj_on f (space M)" shows "(AE x in embed_measure M f. P x) ⟷ (AE x in M. P (f x))" proof let ?M = "embed_measure M f" assume "AE x in ?M. P x" then obtain A where A_props: "A ∈ sets ?M" "emeasure ?M A = 0" "{x∈space ?M. ¬P x} ⊆ A" by (force elim: AE_E) then obtain A' where A'_props: "A = f ` A'" "A' ∈ sets M" by (auto simp: sets_embed_measure' inj) moreover have B: "{x∈space ?M. ¬P x} = f ` {x∈space M. ¬P (f x)}" by (auto simp: inj space_embed_measure) from A_props(3) have "{x∈space M. ¬P (f x)} ⊆ A'" by (subst (asm) B, subst (asm) A'_props, subst (asm) inj_on_image_subset_iff[OF inj]) (insert A'_props, auto dest: sets.sets_into_space) moreover from A_props A'_props have "emeasure M A' = 0" by (simp add: emeasure_embed_measure_image' inj) ultimately show "AE x in M. P (f x)" by (intro AE_I) next let ?M = "embed_measure M f" assume "AE x in M. P (f x)" then obtain A where A_props: "A ∈ sets M" "emeasure M A = 0" "{x∈space M. ¬P (f x)} ⊆ A" by (force elim: AE_E) hence "f`A ∈ sets ?M" "emeasure ?M (f`A) = 0" "{x∈space ?M. ¬P x} ⊆ f`A" by (auto simp: space_embed_measure emeasure_embed_measure_image' sets_embed_measure' inj) thus "AE x in ?M. P x" by (intro AE_I) qed lemma AE_embed_measure: assumes inj: "inj f" shows "(AE x in embed_measure M f. P x) ⟷ (AE x in M. P (f x))" using assms by (intro AE_embed_measure') (auto intro!: inj_onI dest: injD) lemma nn_integral_monotone_convergence_SUP_countable: fixes f :: "'a ⇒ 'b ⇒ ennreal" assumes nonempty: "Y ≠ {}" and chain: "Complete_Partial_Order.chain (≤) (f ` Y)" and countable: "countable B" shows "(∫⇧^{+}x. (SUP i∈Y. f i x) ∂count_space B) = (SUP i∈Y. (∫⇧^{+}x. f i x ∂count_space B))" (is "?lhs = ?rhs") proof - let ?f = "(λi x. f i (from_nat_into B x) * indicator (to_nat_on B ` B) x)" have "?lhs = ∫⇧^{+}x. (SUP i∈Y. f i (from_nat_into B (to_nat_on B x))) ∂count_space B" by(rule nn_integral_cong)(simp add: countable) also have "… = ∫⇧^{+}x. (SUP i∈Y. f i (from_nat_into B x)) ∂count_space (to_nat_on B ` B)" by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1) also have "… = ∫⇧^{+}x. (SUP i∈Y. ?f i x) ∂count_space UNIV" by(simp add: nn_integral_count_space_indicator ennreal_indicator[symmetric] SUP_mult_right_ennreal nonempty) also have "… = (SUP i∈Y. ∫⇧^{+}x. ?f i x ∂count_space UNIV)" proof(rule nn_integral_monotone_convergence_SUP_nat) show "Complete_Partial_Order.chain (≤) (?f ` Y)" by(rule chain_imageI[OF chain, unfolded image_image])(auto intro!: le_funI split: split_indicator dest: le_funD) qed fact also have "… = (SUP i∈Y. ∫⇧^{+}x. f i (from_nat_into B x) ∂count_space (to_nat_on B ` B))" by(simp add: nn_integral_count_space_indicator) also have "… = (SUP i∈Y. ∫⇧^{+}x. f i (from_nat_into B (to_nat_on B x)) ∂count_space B)" by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1) also have "… = ?rhs" by(intro arg_cong2[where f = "λA f. Sup (f ` A)"] ext nn_integral_cong_AE)(simp_all add: AE_count_space countable) finally show ?thesis . qed end