Theory Differential_Privacy.Source_and_Sink_Algebras
theory Source_and_Sink_Algebras
imports
"HOL-Analysis.Sigma_Algebra"
"HOL-Analysis.Measure_Space"
begin
section ‹Meausrable Spaces form a Topological Concrete Category›
text ‹ This entry is based on the fact that the category Meas of measurable spaces and measurable functions forms a topological concrete category (see also, [Brümmer, Topology Appl. 1983], [Adamek, Herrlich and Strecker,1990]), where (i) for any family of functions from a set X to measurable spaces Y(i), the coarsest ‹σ›-algebra over X retracted from the ones Y(i) (initial lift) exists and (ii) for any family of functions from measurable spaces X(i) to Y, the finest ‹σ›-algebra over Y pushed out from the one of X(i) (called final lift) exists. All limits and colimits are given by initial and final lifts respectively. Due to the type system of Isabelle/HOL, the type of family in the construction of initial and final lifts are restricted. ›
subsection ‹Initial lift: the coarsest ‹σ›-algebra retracted from a family of functions ›
definition initial_source :: "'a set ⇒ (('a ⇒ 'b) × 'b measure) set ⇒ 'a measure" where
"initial_source X F = sigma X {f -` A ∩ X | A f M. (f,M) ∈ F ∧ A ∈ sets M}"
text ‹ Roughly speaking, @{term F} is a structured source @{term"{(f,M) | f M. (f,M) ∈ F}"} having the common domain @{term X}. @{term"initial_source X F"} is the initial lift with respect to the source @{term"{(f,M) | f M. (f,M) ∈ F}"}›
text ‹ It is an extension of @{term vimage_algebra} that accepts a family of functions. ›
lemma vimage_algebra_to_initial_source:
shows "vimage_algebra X f M = initial_source X {(f, M)}"
unfolding vimage_algebra_def initial_source_def by auto
lemma space_initial_source [simp]:
shows "space (initial_source X F) = X"
unfolding initial_source_def by (rule space_measure_of) auto
lemma sets_initial_source:
shows "sets (initial_source X F) = sigma_sets X {f -` A ∩ X | A f M. (f,M) ∈ F ∧ A ∈ sets M}"
unfolding initial_source_def
by (rule sets_measure_of) auto
lemma sets_initial_source_mono:
assumes "∀ (f, M) ∈ F. ∀ A ∈ sets M. f -` A ∩ X ∈ (sigma_sets X {g -` A ∩ X | A g N. (g,N) ∈ G ∧ A ∈ sets N})"
shows "sets (initial_source X F) ⊆ sets (initial_source X G)"
proof-
have "{f -` A ∩ X | A f M. (f,M) ∈ F ∧ A ∈ sets M} ⊆ (sigma_sets X {g -` A ∩ X | A g N. (g,N) ∈ G ∧ A ∈ sets N})"
using assms by auto
hence "sigma_sets X {f -` A ∩ X | A f M. (f,M) ∈ F ∧ A ∈ sets M} ⊆ sigma_sets X {g -` A ∩ X | A g N. (g,N) ∈ G ∧ A ∈ sets N}"
by (auto simp: sigma_sets_mono sigma_sets_subseteq sigma_sets_sigma_sets_eq)
thus ?thesis
by (auto simp: sets_initial_source)
qed
lemma sets_initial_source_cong:
assumes "∀ (f, M) ∈ F. ∀ A ∈ sets M. f -` A ∩ X ∈ (sigma_sets X {g -` A ∩ X | A g N. (g,N) ∈ G ∧ A ∈ sets N})"
and "∀ (g, N) ∈ G. ∀ B ∈ sets N. g -` B ∩ X ∈ (sigma_sets X {f -` A ∩ X | A f M. (f,M) ∈ F ∧ A ∈ sets M})"
shows "sets (initial_source X F) = sets (initial_source X G)"
proof
show "sets (initial_source X F) ⊆ sets (initial_source X G)"
by (auto simp: sets_initial_source_mono[where X ="X", OF assms(1)])
show "sets (initial_source X G) ⊆ sets (initial_source X F)"
by (auto simp: sets_initial_source_mono[where X ="X", OF assms(2)])
qed
lemma initial_source_cong:
assumes "X = Y"
and "∀ (f, M) ∈ F. ∀ A ∈ sets M. f -` A ∩ X ∈ (sigma_sets X {g -` A ∩ X | A g N. (g,N) ∈ G ∧ A ∈ sets N})"
and "∀ (g, N) ∈ G. ∀ B ∈ sets N. g -` B ∩ X ∈ (sigma_sets X {f -` A ∩ X | A f M. (f,M) ∈ F ∧ A ∈ sets M})"
shows "(initial_source X F) = (initial_source Y G)"
proof(rule measure_eqI)
show "sets (initial_source X F) = sets (initial_source Y G)"
using sets_initial_source_cong assms by auto
fix A assume "A ∈ sets (initial_source X F)"
show "emeasure (initial_source X F) A = emeasure (initial_source Y G) A"
unfolding initial_source_def by (auto simp: emeasure_sigma)
qed
proposition in_initial_source:
shows "(f,M) ∈ F ⟹ A ∈ sets M ⟹ f -` A ∩ X ∈ sets (initial_source X F)"
by (auto simp: initial_source_def)
text‹ Axiom of initial lift I: it makes the family measurable ›
proposition measurable_initial_source1[measurable(raw)]:
shows "(f,M) ∈ F ⟹ f ∈ X → space M ⟹ f ∈ measurable (initial_source X F) M"
unfolding measurable_def by (auto intro: in_initial_source)
text‹ Axiom of initial lift II: factorization ›
proposition measurable_initial_source2:
assumes "g ∈ space N → X"
and "∀(f,M) ∈ F. f ∈ X → space M"
and "∀(f,M) ∈ F. (λx. f (g x)) ∈ measurable N M"
shows "g ∈ measurable N (initial_source X F)"
unfolding initial_source_def
proof (rule measurableI)
fix x assume xinN: "x ∈ space N"
show "g x ∈ space (sigma X {B. ∃A f M. B = f -` A ∩ X ∧ (f, M) ∈ F ∧ A ∈ sets M})"
using assms(1) xinN space_measure_of_conv by fastforce
next fix B assume "B ∈ sets (sigma X {C. ∃A f M. C = f -` A ∩ X ∧ (f, M) ∈ F ∧ A ∈ sets M})"
hence "B ∈ sigma_sets X {C. ∃A f M. C = f -` A ∩ X ∧ (f, M) ∈ F ∧ A ∈ sets M}"
by (metis sets_initial_source initial_source_def)
thus "g -` B ∩ space N ∈ sets N"
proof(induction B rule: sigma_sets.induct)
case (Basic a)
then obtain A f M where"a = f -` A ∩ X ∧ (f, M) ∈ F ∧ A ∈ sets M"
by auto
hence prop1: "a = f -` A ∩ X" "f ∈ X → space M" "(λx. f (g x)) ∈ measurable N M" "A ∈ sets M"
using assms by auto
hence "g -` a ∩ space N = (λx. f (g x)) -` A ∩ space N"
using assms(1) by auto
also have "... ∈ sets N"
using prop1 by (auto simp: measurable_sets)
finally show ?case .
next
case Empty
thus ?case by auto
next
case (Compl a)
have "g -` (X - a) ∩ space N = (g -` X ∩ space N) - (g -` a ∩ space N)"
by (auto simp: Diff_Int_distrib inf_commute vimage_Diff)
also have "... = (space N) - (g -` a ∩ space N)"
using assms(1) by auto
also have "... ∈ sets N"
by (auto simp: Compl.IH sets.compl_sets)
finally show ?case .
next
case (Union a)
have "g -` ⋃ (range a) ∩ space N =⋃ (range (λ i. ((g -` a i) ∩ space N)))"
by auto
also have "... ∈ sets N"
using Union.IH by blast
finally show ?case .
qed
qed
text‹ The ‹σ›-algebra of a initial lift is the coarsest one that makes the family measurable. ›
lemma sets_image_in_sets_family:
assumes N: "space N = X"
and f: "∀(f, M)∈F. f ∈ N →⇩M M"
shows "sets (initial_source X F) ⊆ sets N"
unfolding sets_initial_source N[symmetric]
proof
fix A assume A: "A ∈ sigma_sets (space N) {f -` A ∩ (space N) | A f M. (f,M) ∈ F ∧ A ∈ sets M}"
{
fix A f M assume a0: "(f,M) ∈ F ∧ A ∈ sets M"
hence "f ∈ measurable N M"using f by auto
hence "f -` A ∩ (space N) ∈ sets N"using a0
by (auto simp: measurable_sets)
}
hence "{f -` A ∩ (space N) | A f M. (f,M) ∈ F ∧ A ∈ sets M} ⊆ (sets N)"
by auto
with A have "A ∈ sigma_sets (space N) (sets N)"
by (meson in_mono sigma_sets_subseteq)
also have "... = (sets N)"
by (auto simp: sets.sigma_sets_eq)
finally show "A ∈ (sets N)".
qed
proposition initial_source_coarsest:
assumes "∀(f, M)∈F. f ∈ X → space M"
shows "sets (initial_source X F) = Inf{ sets N | N. space N = X ∧ (∀(f, M)∈F. f ∈ N →⇩M M) } "
proof(subst Inf_eqI)
show "⋀i. i ∈ { sets N | N. space N = X ∧ (∀(f, M)∈F. f ∈ N →⇩M M) } ⟹ sets (initial_source X F) ⊆ i "
proof-
fix i assume " i ∈ { sets N | N. space N = X ∧ (∀(f, M)∈F. f ∈ N →⇩M M) }"
then obtain N where i: "i = sets N" and N: "space N = X" and f: " ∀(f, M)∈F. f ∈ N →⇩M M"
by auto
show "sets (initial_source X F) ⊆ i"
by(auto simp: i sets_image_in_sets_family[OF N f])
qed
have "⋀ f M. (f, M)∈F ⟹ f ∈ initial_source X F →⇩M M"
using assms measurable_initial_source1 by blast
hence "sets (initial_source X F) ∈ {sets N |N. space N = X ∧ (∀(f, M)∈F. f ∈ N →⇩M M)}"
by(auto intro!: CollectI exI[of _ "(initial_source X F)" ])
thus "⋀y. (⋀i. i ∈ {sets N |N. space N = X ∧ (∀(f, M)∈F. f ∈ N →⇩M M)} ⟹ y ⊆ i) ⟹ y ⊆ sets (initial_source X F)" by auto
qed(auto)
text‹ An initial lift of a bundle of initial lifts is flatten to an initial lift. ›
lemma initial_source_initial_source_eq:
assumes "∀ i ∈ I. G i ∈ Z → (Y i)"
and "∀ i ∈ I. ∀ j ∈ J i. F i j ∈ Y i → space (M i j)"
shows "initial_source Z {((G i), (initial_source (Y i) {((F i j),(M i j)) | j. j ∈ (J i)})) | i. i ∈ I} = initial_source Z {(((F i j) o (G i)),(M i j)) | i j. i ∈ I ∧ j ∈ (J i)}"
proof (rule measure_eqI)
show "⋀A. A ∈ sets (initial_source Z {(G i, initial_source (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I}) ⟹ emeasure (initial_source Z {(G i, initial_source (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I}) A = emeasure (initial_source Z {(F i j ∘ G i, M i j) |i j. i ∈ I ∧ j ∈ J i}) A"
by (auto simp: emeasure_sigma initial_source_def)
show "sets (initial_source Z {(G i, initial_source (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I}) =
sets (initial_source Z {(F i j ∘ G i, M i j) |i j. i ∈ I ∧ j ∈ J i})"
proof
show "sets (initial_source Z {(G i, initial_source (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I}) ⊆ sets (initial_source Z {(F i j ∘ G i, M i j) |i j. i ∈ I ∧ j ∈ J i})"
proof(rule sets_image_in_sets_family)
show "space (initial_source Z {(F i j ∘ G i, M i j) |i j. i ∈ I ∧ j ∈ J i}) = Z"
by auto
{
fix i assume i: "i ∈ I"
hence "G i ∈ initial_source Z {(F i j ∘ G i, M i j) |i j. i ∈ I ∧ j ∈ J i} →⇩M initial_source (Y i) {(F i j, M i j) |j. j ∈ J i}"
proof(intro measurable_initial_source2)
show "G i ∈ space (initial_source Z {(F i j ∘ G i, M i j) |i j. i ∈ I ∧ j ∈ J i}) → Y i"
using i assms(1) by auto
show "∀(f, M)∈{(F i j, M i j) |j. j ∈ J i}. f ∈ Y i → space M"
using assms(2) i by auto
show "∀(f, N)∈{(F i j, M i j) |j. j ∈ J i}. (λx. f (G i x)) ∈ initial_source Z {(F i j ∘ G i, M i j) |i j. i ∈ I ∧ j ∈ J i} →⇩M N"
proof
{
fix j assume j: "j ∈ J i"
hence "(λx. F i j(G i x)) ∈ initial_source Z {(F i j ∘ G i, M i j) |i j. i ∈ I ∧ j ∈ J i} →⇩M M i j"
proof(intro measurable_initial_source1)
have "(F i j ∘ G i, M i j) ∈ {(F i j ∘ G i, M i j) |i j. i ∈ I ∧ j ∈ J i}"
using i j by blast
thus "(λx. F i j (G i x), M i j) ∈ {(F i j ∘ G i, M i j) |i j. i ∈ I ∧ j ∈ J i}"
by(auto simp: comp_def)
show "(λx. F i j (G i x)) ∈ Z → space (M i j)"
using assms by (auto simp: Pi_iff i j)
qed
}
thus "⋀x. x ∈ {(F i j, M i j) |j. j ∈ J i} ⟹ case x of (f, N) ⇒ (λx. f (G i x)) ∈ initial_source Z {(F i j ∘ G i, M i j) |i j. i ∈ I ∧ j ∈ J i} →⇩M N"
by auto
qed
qed
}
thus "∀(f, N)∈{(G i, initial_source (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I}. f ∈ initial_source Z {(F i j ∘ G i, M i j) |i j. i ∈ I ∧ j ∈ J i} →⇩M N"
by force
qed
show "sets (initial_source Z {(F i j ∘ G i, M i j) |i j. i ∈ I ∧ j ∈ J i}) ⊆ sets (initial_source Z {(G i, initial_source (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I})"
proof(rule sets_image_in_sets_family)
show "space (initial_source Z {(G i, initial_source (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I}) = Z"
by auto
{
fix i j assume ij: "i ∈ I ∧ j ∈ J i"
have measFij: "(F i j) ∈ initial_source (Y i) {(F i j, M i j) |j. j ∈ J i} →⇩M M i j"
proof(intro measurable_initial_source1)
show "(F i j, M i j) ∈ {(F i j, M i j) |j. j ∈ J i}"
using ij by auto
show "F i j ∈ Y i → space (M i j)"
using ij assms(2) by auto
qed
have measGi: "G i ∈ initial_source Z {(G i, initial_source (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I} →⇩M initial_source (Y i) {(F i j, M i j) |j. j ∈ J i}"
proof(intro measurable_initial_source1)
show "(G i, initial_source (Y i) {(F i j, M i j) |j. j ∈ J i}) ∈ {(G i, initial_source (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I}"
using ij by auto
show "G i ∈ Z → space (initial_source (Y i) {(F i j, M i j) |j. j ∈ J i})"
using ij assms(1) by auto
qed
from measFij measGi
have "F i j ∘ G i ∈ initial_source Z {(G i, initial_source (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I} →⇩M M i j"
by(auto simp: measurable_comp)
}
thus "∀(f, N)∈{(F i j ∘ G i, M i j) |i j. i ∈ I ∧ j ∈ J i}. f ∈ initial_source Z {(G i, initial_source (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I} →⇩M N"
by blast
qed
qed
qed
subsection ‹Final lift: the finest ‹σ›-algebra pushed out from a family of functions›
definition final_sink :: "'b set ⇒ (('a ⇒ 'b) × 'a measure) set ⇒ 'b measure" where
"final_sink Y G = sigma Y {A | A. A ∈ Pow Y ∧ (∀ (g,N) ∈ G. (g -` A ∩ (space N) ∈ sets N))}"
text ‹ Roughly speaking, @{term G} is a structured sink @{term"{(g,N) | g N. (g,N) ∈ G}"} having the common codomain @{term Y}. @{term"final_sink Y G"} is the final lift with respect to the sink @{term"{(g,N) | g N. (g,N) ∈ G}"}.›
lemma space_final_sink [simp]:
shows "space (final_sink Y G) = Y"
unfolding final_sink_def by (auto simp: space_measure_of_conv)
lemma sets_final_sink:
shows "sets (final_sink Y G) = sigma_sets Y {A | A. A ∈ Pow Y ∧ (∀ (g,N) ∈ G. (g -` A ∩ (space N)∈ sets N))}"
unfolding final_sink_def by (auto simp: subset_eq)
lemma sets_final_sink2:
assumes g: "∀(g,N) ∈ G . g ∈ space N → Y"
shows "sigma_sets Y {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)} = {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)}"
proof-
have "sigma_algebra Y {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)}"
proof
show inclfam: "{A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)} ⊆ Pow Y"
by auto
show empty: "{} ∈ {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)}"
by auto
{
fix g N assume "(g, N)∈G"
hence "g ∈ space N → Y"using g
by auto
hence "g -` Y ∩ space N = space N"
by auto
hence "g -` Y ∩ space N ∈ sets N"
by auto
}
thus "Y ∈ {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)}"
by auto
fix A B assume ABgN: "A ∈ {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)}"
"B ∈ {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)}"
hence AB: "A ∈ Pow Y" "B ∈ Pow Y" "⋀g N .(g, N)∈G ⟹ g -` A ∩ space N ∈ sets N ∧ g -` B ∩ space N ∈ sets N"
by auto
{
fix g N assume G: "(g, N)∈G"
from AB G have IntinN: "g -` (A ∩ B) ∩ space N ∈ sets N"
by (metis Int_assoc imageI sets_restrict_space sets_restrict_space_iff vimage_Int)
from AB G have UnioninN: "g -` (A ∪ B) ∩ space N ∈ sets N"
by (auto simp: boolean_algebra.conj_disj_distrib2 sets.Un)
from AB G have MinusinN: "g -` (A - B) ∩ space N ∈ sets N"
by (auto simp: Diff_Int_distrib2 sets.Diff vimage_Diff)
note IntinN UnioninN MinusinN
} note ABbinary = this
show "A ∩ B ∈ {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)}"
using AB(1,2) ABbinary(1) by auto
show "A ∪ B ∈ {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)}"
using AB(1,2) ABbinary(2) by auto
have "A - B ∈ {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)}"
using AB(1,2) ABbinary(3) by auto
hence "{A - B,{}}⊆ {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)} ∧ finite {A - B,{}} ∧ disjoint {A - B,{}} ∧ A - B = ⋃ {A - B,{}}"
by (auto simp: inclfam empty pairwise_insert)
thus "∃C ⊆ {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)}. finite C ∧ disjoint C ∧ A - B = ⋃ C"
by(intro exI)
next fix W :: "nat ⇒ _" assume W: "range W ⊆ {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)}"
{
fix g N assume G: "(g, N)∈G"
have Wi: "∀ i. W i ∈ Pow Y ∧ W i ∈ {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)}"
using W by blast
hence UWPow: "(⋃ (range W)) ∈ Pow Y"by auto
from Wi have Wimeas: "∀ i. W i ∈ Pow Y ∧ g -` (W i) ∩ space N ∈ sets N"
using G by blast
have "g -` (⋃ (range W)) ∩ space N = ⋃(range (λ i. g -` (W i) ∩ space N))"
by auto
hence "g -` (⋃ (range W)) ∩ space N = ⋃(range (λ i. g -` (W i) ∩ space N))"
by auto
also have "... ∈ sets N"
using Wimeas by blast
finally have UWg: "g -` (⋃ (range W)) ∩ space N ∈ sets N".
note * = UWPow UWg
} note WiUnion = this
thus "⋃ (range W) ∈ {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)}"
using Collect_mono_iff Pow_def W by auto
qed
thus "sigma_sets Y {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)} = {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)}"
by (auto simp: sigma_algebra.sigma_sets_eq)
qed
lemma sets_final_sink':
assumes g: "∀(g,N) ∈ G . g ∈ space N → Y"
shows "sets (final_sink Y G) = {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)}"
using sets_final_sink sets_final_sink2[OF assms] by auto
lemma set_final_sink_mono:
assumes "⋀A. A ∈ Pow Y ⟹ (∀ (f, M) ∈ F. (f -` A ∩ (space M)∈ sets M)) ⟹ A ∈ sigma_sets Y {A | A. A ∈ Pow Y ∧ (∀ (g,N) ∈ G. (g -` A ∩ (space N)∈ sets N))}"
shows "sets (final_sink Y F) ⊆ sets (final_sink Y G)"
proof-
have "{A | A. A ∈ Pow Y ∧ (∀ (f,M) ∈ F. (f -` A ∩ (space M)∈ sets M))} ⊆ sigma_sets Y {A | A. A ∈ Pow Y ∧ (∀ (g,N) ∈ G. (g -` A ∩ (space N)∈ sets N))}"
using assms by auto
hence "sigma_sets Y{A | A. A ∈ Pow Y ∧ (∀ (f,M) ∈ F. (f -` A ∩ (space M)∈ sets M))} ⊆ sigma_sets Y {A | A. A ∈ Pow Y ∧ (∀ (g,N) ∈ G. (g -` A ∩ (space N)∈ sets N))}"
by (meson sigma_sets_mono)
thus "sets (final_sink Y F) ⊆ sets (final_sink Y G)"
unfolding final_sink_def
by (metis sets_final_sink final_sink_def)
qed
lemma set_final_sink_cong:
assumes "⋀A. A ∈ Pow Y ⟹ (∀ (g, N) ∈ G. (g -` A ∩ (space N)∈ sets N))⟹ A ∈ sigma_sets Y{A | A. A ∈ Pow Y ∧ (∀ (f,M) ∈ F. (f -` A ∩ (space M)∈ sets M))}"
and "⋀A. A ∈ Pow Y ⟹ (∀ (f, M) ∈ F. (f -` A ∩ (space M)∈ sets M)) ⟹ A ∈ sigma_sets Y {A | A. A ∈ Pow Y ∧ (∀ (g,N) ∈ G. (g -` A ∩ (space N)∈ sets N))}"
shows "sets (final_sink Y G) = sets (final_sink Y F)"
proof
show "sets (final_sink Y G) ⊆ sets (final_sink Y F)"
using set_final_sink_mono assms(1) by auto
show "sets (final_sink Y F) ⊆ sets (final_sink Y G)"
using set_final_sink_mono assms(2) by auto
qed
lemma final_sink_cong:
assumes "X = Y"
and "⋀A. A ∈ Pow Y ⟹ (∀ (g, N) ∈ G. (g -` A ∩ (space N)∈ sets N))⟹ A ∈ sigma_sets Y{A | A. A ∈ Pow Y ∧ (∀ (f,M) ∈ F. (f -` A ∩ (space M)∈ sets M))}"
and "⋀A. A ∈ Pow Y ⟹ (∀ (f, M) ∈ F. (f -` A ∩ (space M)∈ sets M)) ⟹ A ∈ sigma_sets Y {A | A. A ∈ Pow Y ∧ (∀ (g,N) ∈ G. (g -` A ∩ (space N)∈ sets N))}"
shows "(final_sink Y G) = (final_sink X F)"
proof(rule measure_eqI)
show "sets (final_sink Y G) = sets (final_sink X F)"
unfolding assms(1) by(subst set_final_sink_cong[OF assms(2,3)],auto)
fix A assume "A ∈ sets (final_sink Y G)"
show "emeasure (final_sink Y G) A = emeasure (final_sink X F) A"
unfolding final_sink_def
by (auto simp: emeasure_sigma)
qed
lemma in_final_sink:
shows "∀(g,N) ∈ G . g ∈ space N → Y ⟹ (g,N) ∈ G ⟹ A ∈ sets (final_sink Y G) ⟹ ((g -` A ∩ (space N))∈ sets N)"
by (metis (mono_tags, lifting) case_prodD mem_Collect_eq sets_final_sink sets_final_sink2)
text ‹ Axiom of final lift I: it makes the family measurable ›
lemma measurable_final_sink1[measurable(raw)]:
shows "∀(g,N) ∈ G . g ∈ space N → Y ⟹ (g,N) ∈ G ⟹ g ∈ N →⇩M (final_sink Y G)"
unfolding measurable_def by (auto intro: in_final_sink)
text ‹ Axiom of final lift II: factorization ›
lemma measurable_final_sink2:
assumes "f ∈ Y → space M"
and "∀(g,N) ∈ G . g ∈ space N → Y"
and "∀(g,N) ∈ G . (λx. f (g x)) ∈ N →⇩M M"
shows "f ∈ (final_sink Y G) →⇩M M"
unfolding final_sink_def
proof (rule measurableI)
have Ysp: "space (sigma Y {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)}) = Y"
by (auto simp: space_measure_of_conv)
show "⋀x. x ∈ space (sigma Y {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)}) ⟹ f x ∈ space M"
using assms Ysp by auto
fix A assume A: "A ∈ sets M"
{
fix g N assume gN: "(g,N) ∈ G"
hence *: "g ∈ space N → Y" "(λx. f (g x)) ∈ N →⇩M M"
using assms(2,3) by auto
hence eq1: "g -` Y ∩ space N = space N"
by auto
from * A have "g -`(f -` A ∩ Y) = (λx. f (g x))-` A ∩g -`Y"
by auto
with eq1 have "g -`(f -` A ∩ Y) ∩ space N = (λx. f (g x))-` A ∩ space N"
by (auto simp: inf_assoc)
}note ** = this
hence "f -` A ∩ Y ∈ {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)}"
using A assms(3) measurable_sets by fastforce
also have "... ⊆ sets (sigma Y {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)})"
by auto
finally have eq2: "f -` A ∩ Y ∈ sets (sigma Y {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)})".
have eq3: "f -` A ∩ space (sigma Y {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)}) = f -` A ∩ Y"
using Ysp by auto
from eq2 eq3 show "f -` A ∩ space (sigma Y {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)}) ∈ sets (sigma Y {A |A. A ∈ Pow Y ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)})"
by auto
qed
text‹ The ‹σ›-algebra of a final lift is finest one that it makes the family measurable. ›
lemma sets_vimage_in_set_family:
assumes M: "space M = Y"
and g: "∀(g,N) ∈ G . g ∈ N →⇩M M"
shows "sets M ⊆ sets (final_sink Y G)"
unfolding sets_final_sink M[symmetric]
proof
fix B assume "B ∈ sets M"
with g M have "B ∈ Pow (space M) ∧ (∀(g, N)∈G. g -` B ∩ space N ∈ sets N)"
by (metis (no_types, lifting) Pow_iff case_prodD case_prodI2 measurable_sets sets.sets_into_space)
thus "B ∈ sigma_sets (space M) {A |A. A ∈ Pow (space M) ∧ (∀(g, N)∈G. g -` A ∩ space N ∈ sets N)}"
by auto
qed
proposition final_sink_finest:
assumes "∀(g, N)∈G. g ∈ space N → Y"
shows "sets (final_sink Y G) = Sup{ sets M | M. space M = Y ∧ (∀(g, N)∈G. g ∈ N →⇩M M ) } "
proof(subst Sup_eqI)
show " ⋀y. y ∈ {sets M |M. space M = Y ∧ (∀(g, N)∈G. g ∈ N →⇩M M)} ⟹ y ⊆ sets (final_sink Y G)"
proof-
fix y assume " y ∈ {sets M |M. space M = Y ∧ (∀(g, N)∈G. g ∈ N →⇩M M)}"
then obtain M where y: "y = sets M" and M: "space M = Y" and g: "∀(g, N)∈G. g ∈ N →⇩M M"
by auto
show "y ⊆ sets (final_sink Y G)"
by(auto simp: y sets_vimage_in_set_family[OF M g])
qed
have "∀(g, N)∈G. g ∈ N →⇩M (final_sink Y G)"
using measurable_final_sink1 assms by blast
hence "(sets (final_sink Y G)) ∈ {sets M |M. space M = Y ∧ (∀(g, N)∈G. g ∈ N →⇩M M)}"
by(intro CollectI exI[of _ "(final_sink Y G)"],auto)
thus "⋀y. (⋀z. z ∈ {sets M |M. space M = Y ∧ (∀(g, N)∈G. g ∈ N →⇩M M)} ⟹ z ⊆ y) ⟹ sets (final_sink Y G) ⊆ y"
by auto
qed(auto)
text‹ A final lift of a bundle of final lifts is flatten to a final lift. ›
lemma final_sink_final_sink_eq:
assumes "∀ i ∈ I. G i ∈ (Y i) → Z"
and "∀ i ∈ I. ∀ j ∈ J i. F i j ∈ space (M i j) → (Y i)"
shows "final_sink Z {((G i), (final_sink (Y i) {((F i j),(M i j)) | j. j ∈ (J i)})) | i. i ∈ I} = final_sink Z {((G i) o (F i j), (M i j)) | i j. i ∈ I ∧ j ∈ (J i)}"
proof (rule measure_eqI)
show "⋀A. A ∈ sets (final_sink Z {(G i, final_sink (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I}) ⟹ emeasure (final_sink Z {(G i, final_sink (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I}) A = emeasure (final_sink Z {(G i ∘ F i j, M i j) |i j. i ∈ I ∧ j ∈ J i}) A"
unfolding final_sink_def by (auto simp: emeasure_sigma)
show "sets (final_sink Z {(G i, final_sink (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I}) = sets (final_sink Z {(G i ∘ F i j, M i j) |i j. i ∈ I ∧ j ∈ J i})"
proof
show "sets (final_sink Z {(G i, final_sink (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I}) ⊆ sets (final_sink Z {(G i ∘ F i j, M i j) |i j. i ∈ I ∧ j ∈ J i})"
proof(rule sets_vimage_in_set_family)
show "space (final_sink Z {(G i, final_sink (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I}) = Z"
by auto
{
fix i j assume i: "i ∈ I" and j: "j ∈ J i"
hence measFij: "F i j ∈ M i j →⇩M final_sink (Y i) {(F i j, M i j) |j. j ∈ J i}"
proof(intro measurable_final_sink1)
show "∀(g, N)∈{(F i j, M i j) |j. j ∈ J i}. g ∈ space N → Y i"
using assms(2) i by blast
show "(F i j, M i j) ∈ {(F i j, M i j) |j. j ∈ J i}"
using j by auto
qed
from i j have measGi: "G i ∈ final_sink (Y i) {(F i j, M i j) |j. j ∈ J i} →⇩M final_sink Z {(G i, final_sink (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I}"
proof(intro measurable_final_sink1)
show "∀(g, N)∈{(G i, final_sink (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I}. g ∈ space N → Z"
proof
show "⋀x. x ∈ {(G i, final_sink (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I} ⟹ case x of (g, N) ⇒ g ∈ space N → Z"
using assms(1) by fastforce
qed
show "(G i, final_sink (Y i) {(F i j, M i j) |j. j ∈ J i}) ∈ {(G i, final_sink (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I}"
using i by auto
qed
from measFij measGi
have "G i ∘ F i j ∈ M i j →⇩M final_sink Z {(G i, final_sink (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I}"
by (auto simp: measurable_comp)
}
thus "∀(g, N)∈{(G i ∘ F i j, M i j) |i j. i ∈ I ∧ j ∈ J i}. g ∈ N →⇩M final_sink Z {(G i, final_sink (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I}"
by blast
qed
show "sets (final_sink Z {(G i ∘ F i j, M i j) |i j. i ∈ I ∧ j ∈ J i}) ⊆ sets (final_sink Z {(G i, final_sink (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I})"
proof(rule sets_vimage_in_set_family)
show "space (final_sink Z {(G i ∘ F i j, M i j) |i j. i ∈ I ∧ j ∈ J i}) = Z"
by auto
{
fix i assume i: "i ∈ I"
have "G i ∈ final_sink (Y i) {(F i j, M i j) |j. j ∈ J i} →⇩M final_sink Z {(G i ∘ F i j, M i j) |i j. i ∈ I ∧ j ∈ J i}"
proof(rule measurable_final_sink2)
show "G i ∈ Y i → space (final_sink Z {(G i ∘ F i j, M i j) |i j. i ∈ I ∧ j ∈ J i})"
using i assms(1) by auto
show "∀(g, N)∈{(F i j, M i j) |j. j ∈ J i}. g ∈ space N → Y i"
using assms(2) i by blast
show "∀(g, N)∈{(F i j, M i j) |j. j ∈ J i}. (λx. G i (g x)) ∈ N →⇩M final_sink Z {(G i ∘ F i j, M i j) |i j. i ∈ I ∧ j ∈ J i}"
proof(clarify)
fix j assume j: "j ∈ J i"
thus "(λx. G i (F i j x)) ∈ M i j →⇩M final_sink Z {(G i ∘ F i j, M i j) |i j. i ∈ I ∧ j ∈ J i}"
proof(intro measurable_final_sink1)
show "∀(g, N)∈{(G i ∘ F i j, M i j) |i j. i ∈ I ∧ j ∈ J i}. g ∈ space N → Z"
using assms by fastforce
show "(λx. G i (F i j x), M i j) ∈ {(G i ∘ F i j, M i j) |i j. i ∈ I ∧ j ∈ J i}"
using i j comp_def[THEN sym] by blast
qed
qed
qed
}
thus "∀(g, N)∈{(G i, final_sink (Y i) {(F i j, M i j) |j. j ∈ J i}) |i. i ∈ I}. g ∈ N →⇩M final_sink Z {(G i ∘ F i j, M i j) |i j. i ∈ I ∧ j ∈ J i}"
by blast
qed
qed
qed
end