src/HOL/Analysis/Embed_Measure.thy
 changeset 69180 922833cc6839 parent 67399 eab6ce8368fa child 69260 0a9688695a1b
```     1.1 --- a/src/HOL/Analysis/Embed_Measure.thy	Mon Oct 22 12:22:18 2018 +0200
1.2 +++ b/src/HOL/Analysis/Embed_Measure.thy	Mon Oct 22 19:03:47 2018 +0200
1.3 @@ -6,13 +6,23 @@
1.4      measure on the left part of the sum type 'a + 'b)
1.5  *)
1.6
1.7 -section \<open>Embed Measure Spaces with a Function\<close>
1.8 +section \<open>Embedding Measure Spaces with a Function\<close>
1.9
1.10  theory Embed_Measure
1.11  imports Binary_Product_Measure
1.12  begin
1.13
1.14 -definition embed_measure :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
1.15 +text \<open>
1.16 +  Given a measure space on some carrier set \<open>\<Omega>\<close> and a function \<open>f\<close>, we can define a push-forward
1.17 +  measure on the carrier set \$f(\Omega)\$ whose \<open>\<sigma>\<close>-algebra is the one generated by mapping \<open>f\<close> over
1.18 +  the original sigma algebra.
1.19 +
1.20 +  This is useful e.\,g.\ when \<open>f\<close> is injective, i.\,e.\ it is some kind of ``tagging'' function.
1.21 +  For instance, suppose we have some algebraaic datatype of values with various constructors,
1.22 +  including a constructor \<open>RealVal\<close> for real numbers. Then \<open>embed_measure\<close> allows us to lift a
1.23 +  measure on real numbers to the appropriate subset of that algebraic datatype.
1.24 +\<close>
1.25 +definition%important embed_measure :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
1.26    "embed_measure M f = measure_of (f ` space M) {f ` A |A. A \<in> sets M}
1.27                             (\<lambda>A. emeasure M (f -` A \<inter> space M))"
1.28
```