Theory HOL-Analysis.Embed_Measure

(*  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.
›
definitiontag 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. XA  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]
     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" "{xspace ?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: "{xspace ?M. ¬P x} = f ` {xspace M. ¬P (f x)}"
    by (auto simp: inj space_embed_measure)
  from A_props(3) have "{xspace 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" "{xspace M. ¬P (f x)}  A"
    by (force elim: AE_E)
  hence "f`A  sets ?M" "emeasure ?M (f`A) = 0" "{xspace ?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 iY. f i x) count_space B) = (SUP iY. (+ 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 iY. 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 iY. 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 iY. ?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 iY. + 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 iY. + 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 iY. + 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