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