Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/Analysis/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 20 kB

Quelle Embed_Measure.thy Sprache: Isabelle

(*  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 \<open>Embedding Measure Spaces with a Function\<close>

theory Embed_Measure
imports Binary_Product_Measure
begin

text \<open>
  Given a measure space on some carrier set \<open>\<Omega>\<close> and a function \<open>f\<close>, we can define a push-forward
  measure on the carrier set \<open>f(\<Omega>)\<close> whose \<open>\<sigma>\<close>-algebra is the one generated by mapping \<open>f\<close> over
  the original sigma algebra.

  This is useful e.\,g.\ when \<open>f\<close> 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 \<open>RealVal\<close> for real numbers. Then \<open>embed_measure\<close> allows us to lift a
  measure on real numbers to the appropriate subset of that algebraic datatype.
\<close>
definition\<^marker>\<open>tag important\<close> embed_measure :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
  "embed_measure M f = measure_of (f ` space M) {f ` A |A. A \ sets M}
                           (\<lambda>A. emeasure M (f -` A \<inter> 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 \<in> sets M}
                       (\<lambda>A. emeasure M (f -` A \<inter> 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 (\<lambda>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 (\<lambda>x. g (f x))"
  by(erule nn_integral_embed_measure'[OF inj_on_subset]) 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 \<circ> 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 inj_on_subset, 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 \<open>X \<in> sets A\<close> and \<open>sets A = sets B\<close> 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 \\<^sub>M embed_measure N g = embed_measure (M \\<^sub>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 \\<^sub>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 \\<^sub>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 \\<^sub>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 \<Otimes>\<^sub>M N) (map_prod f g)) (A \<times> 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 = \\<^sup>+ x. g x * indicator X x \embed_measure M f"
    by (subst emeasure_density) simp_all
  also from X have "... = \\<^sup>+ x. g (f x) * indicator X (f x) \M"
    by (subst embed_measure_eq_distr[OF inj], subst nn_integral_distr) auto
  also have "... = \\<^sup>+ 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 \<open>y \<in> B\<close> show "x \<in> 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 "(\\<^sup>+ x. (SUP i\Y. f i x) \count_space B) = (SUP i\Y. (\\<^sup>+ 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 = \\<^sup>+ 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 "\ = \\<^sup>+ 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 "\ = \\<^sup>+ 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. \\<^sup>+ 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. \\<^sup>+ 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. \\<^sup>+ 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

quality100%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.