# HG changeset patch # User wenzelm # Date 1466514643 -7200 # Node ID 94c6e3ed0afb151a54dc5a7473226d88f38217a5 # Parent bd37a72a940ada891eff07b3d07805886c6f1567# Parent ae9330fdbc16fe443840244c0a5f0f467551fb31 merged diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Archimedean_Field.thy --- a/src/HOL/Archimedean_Field.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Archimedean_Field.thy Tue Jun 21 15:10:43 2016 +0200 @@ -8,6 +8,63 @@ imports Main begin +lemma cInf_abs_ge: + fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set" + assumes "S \ {}" and bdd: "\x. x\S \ \x\ \ a" + shows "\Inf S\ \ a" +proof - + have "Sup (uminus ` S) = - (Inf S)" + proof (rule antisym) + show "- (Inf S) \ Sup(uminus ` S)" + apply (subst minus_le_iff) + apply (rule cInf_greatest [OF \S \ {}\]) + apply (subst minus_le_iff) + apply (rule cSup_upper, force) + using bdd apply (force simp add: abs_le_iff bdd_above_def) + done + next + show "Sup (uminus ` S) \ - Inf S" + apply (rule cSup_least) + using \S \ {}\ apply (force simp add: ) + apply clarsimp + apply (rule cInf_lower) + apply assumption + using bdd apply (simp add: bdd_below_def) + apply (rule_tac x="-a" in exI) + apply force + done + qed + with cSup_abs_le [of "uminus ` S"] assms show ?thesis by fastforce +qed + +lemma cSup_asclose: + fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set" + assumes S: "S \ {}" + and b: "\x\S. \x - l\ \ e" + shows "\Sup S - l\ \ e" +proof - + have th: "\(x::'a) l e. \x - l\ \ e \ l - e \ x \ x \ l + e" + by arith + have "bdd_above S" + using b by (auto intro!: bdd_aboveI[of _ "l + e"]) + with S b show ?thesis + unfolding th by (auto intro!: cSup_upper2 cSup_least) +qed + +lemma cInf_asclose: + fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set" + assumes S: "S \ {}" + and b: "\x\S. \x - l\ \ e" + shows "\Inf S - l\ \ e" +proof - + have th: "\(x::'a) l e. \x - l\ \ e \ l - e \ x \ x \ l + e" + by arith + have "bdd_below S" + using b by (auto intro!: bdd_belowI[of _ "l - e"]) + with S b show ?thesis + unfolding th by (auto intro!: cInf_lower2 cInf_greatest) +qed + subsection \Class of Archimedean fields\ text \Archimedean fields have no infinite elements.\ @@ -329,10 +386,10 @@ also have "\ = (of_int (k div l) + of_int (k mod l) / of_int l) * of_int l" using False by (simp only: of_int_add) (simp add: field_simps) finally have "(of_int k / of_int l :: 'a) = \ / of_int l" - by simp + by simp then have "(of_int k / of_int l :: 'a) = of_int (k div l) + of_int (k mod l) / of_int l" using False by (simp only:) (simp add: field_simps) - then have "\of_int k / of_int l :: 'a\ = \of_int (k div l) + of_int (k mod l) / of_int l :: 'a\" + then have "\of_int k / of_int l :: 'a\ = \of_int (k div l) + of_int (k mod l) / of_int l :: 'a\" by simp then have "\of_int k / of_int l :: 'a\ = \of_int (k mod l) / of_int l + of_int (k div l) :: 'a\" by (simp add: ac_simps) @@ -355,10 +412,10 @@ also have "\ = (of_nat (m div n) + of_nat (m mod n) / of_nat n) * of_nat n" using False by (simp only: of_nat_add) (simp add: field_simps of_nat_mult) finally have "(of_nat m / of_nat n :: 'a) = \ / of_nat n" - by simp + by simp then have "(of_nat m / of_nat n :: 'a) = of_nat (m div n) + of_nat (m mod n) / of_nat n" using False by (simp only:) simp - then have "\of_nat m / of_nat n :: 'a\ = \of_nat (m div n) + of_nat (m mod n) / of_nat n :: 'a\" + then have "\of_nat m / of_nat n :: 'a\ = \of_nat (m div n) + of_nat (m mod n) / of_nat n :: 'a\" by simp then have "\of_nat m / of_nat n :: 'a\ = \of_nat (m mod n) / of_nat n + of_nat (m div n) :: 'a\" by (simp add: ac_simps) @@ -376,7 +433,7 @@ where "\x\ = - \- x\" lemma ceiling_correct: "of_int \x\ - 1 < x \ x \ of_int \x\" - unfolding ceiling_def using floor_correct [of "- x"] by (simp add: le_minus_iff) + unfolding ceiling_def using floor_correct [of "- x"] by (simp add: le_minus_iff) lemma ceiling_unique: "\of_int z - 1 < x; x \ of_int z\ \ \x\ = z" unfolding ceiling_def using floor_unique [of "- z" "- x"] by simp @@ -512,7 +569,7 @@ lemma ceiling_diff_floor_le_1: "\x\ - \x\ \ 1" proof - - have "of_int \x\ - 1 < x" + have "of_int \x\ - 1 < x" using ceiling_correct[of x] by simp also have "x < of_int \x\ + 1" using floor_correct[of x] by simp_all @@ -552,7 +609,7 @@ lemma frac_of_int [simp]: "frac (of_int z) = 0" by (simp add: frac_def) -lemma floor_add: "\x + y\ = (if frac x + frac y < 1 then \x\ + \y\ else (\x\ + \y\) + 1)" +lemma floor_add: "\x + y\ = (if frac x + frac y < 1 then \x\ + \y\ else (\x\ + \y\) + 1)" proof - {assume "x + y < 1 + (of_int \x\ + of_int \y\)" then have "\x + y\ = \x\ + \y\" @@ -563,14 +620,14 @@ then have "\x + y\ = 1 + (\x\ + \y\)" apply (simp add: floor_unique_iff) apply (auto simp add: algebra_simps) - by linarith + by linarith } ultimately show ?thesis by (auto simp add: frac_def algebra_simps) qed lemma frac_add: "frac (x + y) = (if frac x + frac y < 1 then frac x + frac y - else (frac x + frac y) - 1)" + else (frac x + frac y) - 1)" by (simp add: frac_def floor_add) lemma frac_unique_iff: @@ -582,7 +639,7 @@ lemma frac_eq: "(frac x) = x \ 0 \ x \ x < 1" by (simp add: frac_unique_iff) - + lemma frac_neg: fixes x :: "'a::floor_ceiling" shows "frac (-x) = (if x \ \ then 0 else 1 - frac x)" @@ -643,8 +700,8 @@ unfolding round_def by (intro floor_mono) simp lemma ceiling_ge_round: "\x\ \ round x" unfolding round_altdef by simp - -lemma round_diff_minimal: + +lemma round_diff_minimal: fixes z :: "'a :: floor_ceiling" shows "\z - of_int (round z)\ \ \z - of_int m\" proof (cases "of_int m \ z") diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Conditionally_Complete_Lattices.thy --- a/src/HOL/Conditionally_Complete_Lattices.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Conditionally_Complete_Lattices.thy Tue Jun 21 15:10:43 2016 +0200 @@ -7,7 +7,7 @@ section \Conditionally-complete Lattices\ theory Conditionally_Complete_Lattices -imports Main +imports Finite_Set Lattices_Big Set_Interval begin lemma (in linorder) Sup_fin_eq_Max: "finite X \ X \ {} \ Sup_fin X = Max X" @@ -107,7 +107,7 @@ lemma bdd_below_image_mono: "mono f \ bdd_below A \ bdd_below (f`A)" by (auto simp: bdd_below_def mono_def) - + lemma bdd_above_image_antimono: "antimono f \ bdd_below A \ bdd_above (f`A)" by (auto simp: bdd_above_def bdd_below_def antimono_def) @@ -394,7 +394,7 @@ class conditionally_complete_linorder = conditionally_complete_lattice + linorder begin -lemma less_cSup_iff : (*REAL_SUP_LE in HOL4*) +lemma less_cSup_iff: "X \ {} \ bdd_above X \ y < Sup X \ (\x\X. y < x)" by (rule iffI) (metis cSup_least not_less, metis cSup_upper less_le_trans) @@ -429,7 +429,7 @@ (metis \a < b\ \\ P b\ linear less_le) next show "Sup {d. \c. a \ c \ c < d \ P c} \ b" - apply (rule cSup_least) + apply (rule cSup_least) apply auto apply (metis less_le_not_le) apply (metis \a \~ P b\ linear less_le) @@ -440,7 +440,7 @@ show "P x" apply (rule less_cSupE [OF lt], auto) apply (metis less_le_not_le) - apply (metis x) + apply (metis x) done next fix d @@ -512,7 +512,7 @@ unfolding Inf_nat_def ex_in_conv[symmetric] by (rule LeastI2_ex) } { assume "x \ X" "bdd_above X" then show "x \ Sup X" by (simp add: Sup_nat_def bdd_above_nat) } - { assume "X \ {}" "\y. y \ X \ y \ x" + { assume "X \ {}" "\y. y \ X \ y \ x" moreover then have "bdd_above X" by (auto simp: bdd_above_def) ultimately show "Sup X \ x" @@ -593,7 +593,7 @@ define lower upper where "lower = {x. \s\S. s \ x}" and "upper = {x. \s\S. x \ s}" with ivl have "S = lower \ upper" by auto - moreover + moreover have "\a. upper = UNIV \ upper = {} \ upper = {.. a} \ upper = {..< a}" proof cases assume *: "bdd_above S \ S \ {}" @@ -644,7 +644,7 @@ using a bdd apply (auto simp: cINF_lower) apply (metis eq cSUP_upper) -done +done lemma cSUP_UNION: fixes f :: "_ \ 'b::conditionally_complete_lattice" @@ -686,67 +686,10 @@ by (rule order_antisym) qed -lemma cSup_abs_le: +lemma cSup_abs_le: fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set" shows "S \ {} \ (\x. x\S \ \x\ \ a) \ \Sup S\ \ a" apply (auto simp add: abs_le_iff intro: cSup_least) by (metis bdd_aboveI cSup_upper neg_le_iff_le order_trans) -lemma cInf_abs_ge: - fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set" - assumes "S \ {}" and bdd: "\x. x\S \ \x\ \ a" - shows "\Inf S\ \ a" -proof - - have "Sup (uminus ` S) = - (Inf S)" - proof (rule antisym) - show "- (Inf S) \ Sup(uminus ` S)" - apply (subst minus_le_iff) - apply (rule cInf_greatest [OF \S \ {}\]) - apply (subst minus_le_iff) - apply (rule cSup_upper, force) - using bdd apply (force simp add: abs_le_iff bdd_above_def) - done - next - show "Sup (uminus ` S) \ - Inf S" - apply (rule cSup_least) - using \S \ {}\ apply (force simp add: ) - apply clarsimp - apply (rule cInf_lower) - apply assumption - using bdd apply (simp add: bdd_below_def) - apply (rule_tac x="-a" in exI) - apply force - done - qed - with cSup_abs_le [of "uminus ` S"] assms show ?thesis by fastforce -qed - -lemma cSup_asclose: - fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set" - assumes S: "S \ {}" - and b: "\x\S. \x - l\ \ e" - shows "\Sup S - l\ \ e" -proof - - have th: "\(x::'a) l e. \x - l\ \ e \ l - e \ x \ x \ l + e" - by arith - have "bdd_above S" - using b by (auto intro!: bdd_aboveI[of _ "l + e"]) - with S b show ?thesis - unfolding th by (auto intro!: cSup_upper2 cSup_least) -qed - -lemma cInf_asclose: - fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set" - assumes S: "S \ {}" - and b: "\x\S. \x - l\ \ e" - shows "\Inf S - l\ \ e" -proof - - have th: "\(x::'a) l e. \x - l\ \ e \ l - e \ x \ x \ l + e" - by arith - have "bdd_below S" - using b by (auto intro!: bdd_belowI[of _ "l - e"]) - with S b show ?thesis - unfolding th by (auto intro!: cInf_lower2 cInf_greatest) -qed - end diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Library/FSet.thy --- a/src/HOL/Library/FSet.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Library/FSet.thy Tue Jun 21 15:10:43 2016 +0200 @@ -7,7 +7,7 @@ section \Type of finite sets defined as a subtype of sets\ theory FSet -imports Conditionally_Complete_Lattices +imports Main begin subsection \Definition of the type\ @@ -31,18 +31,18 @@ interpretation lifting_syntax . -lift_definition bot_fset :: "'a fset" is "{}" parametric empty_transfer by simp +lift_definition bot_fset :: "'a fset" is "{}" parametric empty_transfer by simp -lift_definition less_eq_fset :: "'a fset \ 'a fset \ bool" is subset_eq parametric subset_transfer +lift_definition less_eq_fset :: "'a fset \ 'a fset \ bool" is subset_eq parametric subset_transfer . definition less_fset :: "'a fset \ 'a fset \ bool" where "xs < ys \ xs \ ys \ xs \ (ys::'a fset)" lemma less_fset_transfer[transfer_rule]: - assumes [transfer_rule]: "bi_unique A" + assumes [transfer_rule]: "bi_unique A" shows "((pcr_fset A) ===> (pcr_fset A) ===> op =) op \ op <" unfolding less_fset_def[abs_def] psubset_eq[abs_def] by transfer_prover - + lift_definition sup_fset :: "'a fset \ 'a fset \ 'a fset" is union parametric union_transfer by simp @@ -69,7 +69,7 @@ begin definition "HOL.equal A B \ A |\| B \ B |\| A" instance by intro_classes (auto simp add: equal_fset_def) -end +end instantiation fset :: (type) conditionally_complete_lattice begin @@ -78,18 +78,18 @@ lemma right_total_Inf_fset_transfer: assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A" - shows "(rel_set (rel_set A) ===> rel_set A) - (\S. if finite (\S \ Collect (Domainp A)) then \S \ Collect (Domainp A) else {}) + shows "(rel_set (rel_set A) ===> rel_set A) + (\S. if finite (\S \ Collect (Domainp A)) then \S \ Collect (Domainp A) else {}) (\S. if finite (Inf S) then Inf S else {})" by transfer_prover lemma Inf_fset_transfer: assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A" - shows "(rel_set (rel_set A) ===> rel_set A) (\A. if finite (Inf A) then Inf A else {}) + shows "(rel_set (rel_set A) ===> rel_set A) (\A. if finite (Inf A) then Inf A else {}) (\A. if finite (Inf A) then Inf A else {})" by transfer_prover -lift_definition Inf_fset :: "'a fset set \ 'a fset" is "\A. if finite (Inf A) then Inf A else {}" +lift_definition Inf_fset :: "'a fset set \ 'a fset" is "\A. if finite (Inf A) then Inf A else {}" parametric right_total_Inf_fset_transfer Inf_fset_transfer by simp lemma Sup_fset_transfer: @@ -107,11 +107,11 @@ by auto instance -proof +proof fix x z :: "'a fset" fix X :: "'a fset set" { - assume "x \ X" "bdd_below X" + assume "x \ X" "bdd_below X" then show "Inf X |\| x" by transfer auto next assume "X \ {}" "(\x. x \ X \ z |\| x)" @@ -129,7 +129,7 @@ qed end -instantiation fset :: (finite) complete_lattice +instantiation fset :: (finite) complete_lattice begin lift_definition top_fset :: "'a fset" is UNIV parametric right_total_UNIV_transfer UNIV_transfer @@ -143,7 +143,7 @@ instantiation fset :: (finite) complete_boolean_algebra begin -lift_definition uminus_fset :: "'a fset \ 'a fset" is uminus +lift_definition uminus_fset :: "'a fset \ 'a fset" is uminus parametric right_total_Compl_transfer Compl_transfer by simp instance @@ -169,7 +169,7 @@ "{|x, xs|}" == "CONST finsert x {|xs|}" "{|x|}" == "CONST finsert x {||}" -lift_definition fmember :: "'a \ 'a fset \ bool" (infix "|\|" 50) is Set.member +lift_definition fmember :: "'a \ 'a fset \ bool" (infix "|\|" 50) is Set.member parametric member_transfer . abbreviation notin_fset :: "'a \ 'a fset \ bool" (infix "|\|" 50) where "x |\| S \ \ (x |\| S)" @@ -179,20 +179,20 @@ interpretation lifting_syntax . -lift_definition ffilter :: "('a \ bool) \ 'a fset \ 'a fset" is Set.filter +lift_definition ffilter :: "('a \ bool) \ 'a fset \ 'a fset" is Set.filter parametric Lifting_Set.filter_transfer unfolding Set.filter_def by simp -lift_definition fPow :: "'a fset \ 'a fset fset" is Pow parametric Pow_transfer +lift_definition fPow :: "'a fset \ 'a fset fset" is Pow parametric Pow_transfer by (simp add: finite_subset) lift_definition fcard :: "'a fset \ nat" is card parametric card_transfer . -lift_definition fimage :: "('a \ 'b) \ 'a fset \ 'b fset" (infixr "|`|" 90) is image +lift_definition fimage :: "('a \ 'b) \ 'a fset \ 'b fset" (infixr "|`|" 90) is image parametric image_transfer by simp lift_definition fthe_elem :: "'a fset \ 'a" is the_elem . -lift_definition fbind :: "'a fset \ ('a \ 'b fset) \ 'b fset" is Set.bind parametric bind_transfer +lift_definition fbind :: "'a fset \ ('a \ 'b fset) \ 'b fset" is Set.bind parametric bind_transfer by (simp add: Set.bind_def) lift_definition ffUnion :: "'a fset fset \ 'a fset" is Union parametric Union_transfer by simp @@ -464,7 +464,7 @@ lemmas fset_simps[simp] = bot_fset.rep_eq finsert.rep_eq -lemma finite_fset [simp]: +lemma finite_fset [simp]: shows "finite (fset S)" by transfer simp @@ -485,16 +485,16 @@ subsubsection \\filter_fset\\ -lemma subset_ffilter: +lemma subset_ffilter: "ffilter P A |\| ffilter Q A = (\ x. x |\| A \ P x \ Q x)" by transfer auto -lemma eq_ffilter: +lemma eq_ffilter: "(ffilter P A = ffilter Q A) = (\x. x |\| A \ P x = Q x)" by transfer auto lemma pfsubset_ffilter: - "(\x. x |\| A \ P x \ Q x) \ (x |\| A & \ P x & Q x) \ + "(\x. x |\| A \ P x \ Q x) \ (x |\| A & \ P x & Q x) \ ffilter P A |\| ffilter Q A" unfolding less_fset_def by (auto simp add: subset_ffilter eq_ffilter) @@ -520,9 +520,9 @@ subsubsection \bounded quantification\ lemma bex_simps [simp, no_atp]: - "\A P Q. fBex A (\x. P x \ Q) = (fBex A P \ Q)" + "\A P Q. fBex A (\x. P x \ Q) = (fBex A P \ Q)" "\A P Q. fBex A (\x. P \ Q x) = (P \ fBex A Q)" - "\P. fBex {||} P = False" + "\P. fBex {||} P = False" "\a B P. fBex (finsert a B) P = (P a \ fBex B P)" "\A P f. fBex (f |`| A) P = fBex A (\x. P (f x))" "\A P. (\ fBex A P) = fBall A (\x. \ P x)" @@ -601,7 +601,7 @@ lemma pfsubset_fcard_mono: "A |\| B \ fcard A < fcard B" by transfer (rule psubset_card_mono) -lemma fcard_funion_finter: +lemma fcard_funion_finter: "fcard A + fcard B = fcard (A |\| B) + fcard (A |\| B)" by transfer (rule card_Un_Int) @@ -656,7 +656,7 @@ assumes "x |\| A" shows "ffold f z A = f x (ffold f z (A |-| {|x|}))" using assms by (transfer fixing: f) (rule fold_rec) - + lemma ffold_finsert_fremove: "ffold f z (finsert x A) = f x (ffold f z (A |-| {|x|}))" by (transfer fixing: f) (rule fold_insert_remove) @@ -680,9 +680,9 @@ lemma ffold_finsert_idem: "ffold f z (finsert x A) = f x (ffold f z A)" by (transfer fixing: f) (rule fold_insert_idem) - + declare ffold_finsert [simp del] ffold_finsert_idem [simp] - + lemma ffold_finsert_idem2: "ffold f z (finsert x A) = ffold f (f x z) A" by (transfer fixing: f) (rule fold_insert_idem2) @@ -692,7 +692,7 @@ subsection \Choice in fsets\ -lemma fset_choice: +lemma fset_choice: assumes "\x. x |\| A \ (\y. P x y)" shows "\f. \x. x |\| A \ P x (f x)" using assms by transfer metis @@ -701,7 +701,7 @@ subsection \Induction and Cases rules for fsets\ lemma fset_exhaust [case_names empty insert, cases type: fset]: - assumes fempty_case: "S = {||} \ P" + assumes fempty_case: "S = {||} \ P" and finsert_case: "\x S'. S = finsert x S' \ P" shows "P" using assms by transfer blast @@ -739,9 +739,9 @@ case (insert x S) have h: "P S" by fact have "x |\| S" by fact - then have "Suc (fcard S) = fcard (finsert x S)" + then have "Suc (fcard S) = fcard (finsert x S)" by transfer auto - then show "P (finsert x S)" + then show "P (finsert x S)" using h card_fset_Suc_case by simp qed @@ -771,11 +771,11 @@ lift_definition rel_fset :: "('a \ 'b \ bool) \ 'a fset \ 'b fset \ bool" is rel_set parametric rel_set_transfer . -lemma rel_fset_alt_def: "rel_fset R = (\A B. (\x.\y. x|\|A \ y|\|B \ R x y) +lemma rel_fset_alt_def: "rel_fset R = (\A B. (\x.\y. x|\|A \ y|\|B \ R x y) \ (\y. \x. y|\|B \ x|\|A \ R x y))" apply (rule ext)+ apply transfer' -apply (subst rel_set_def[unfolded fun_eq_iff]) +apply (subst rel_set_def[unfolded fun_eq_iff]) by blast lemma finite_rel_set: @@ -787,12 +787,12 @@ apply atomize_elim apply (subst bchoice_iff[symmetric]) using R_S[unfolded rel_set_def OO_def] by blast - + obtain g where g: "\z\Z. S (g z) z \ (\x\X. R x (g z))" apply atomize_elim apply (subst bchoice_iff[symmetric]) using R_S[unfolded rel_set_def OO_def] by blast - + let ?Y = "f ` X \ g ` Z" have "finite ?Y" by (simp add: fin) moreover have "rel_set R X ?Y" @@ -960,7 +960,7 @@ bnf "'a fset" map: fimage - sets: fset + sets: fset bd: natLeq wits: "{||}" rel: rel_fset @@ -974,7 +974,7 @@ apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq) apply (fastforce simp: rel_fset_alt) apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff rel_fset_alt - rel_fset_aux[unfolded OO_Grp_alt]) + rel_fset_aux[unfolded OO_Grp_alt]) apply transfer apply simp done @@ -1009,7 +1009,7 @@ lemma fset_size_o_map: "inj f \ size_fset g \ fimage f = size_fset (g \ f)" apply (subst fun_eq_iff) including fset.lifting by transfer (auto intro: setsum.reindex_cong subset_inj_on) - + setup \ BNF_LFP_Size.register_size_global @{type_name fset} @{const_name size_fset} @{thm size_fset_overloaded_def} @{thms size_fset_simps size_fset_overloaded_simps} @@ -1023,8 +1023,8 @@ (* Set vs. sum relators: *) -lemma rel_set_rel_sum[simp]: -"rel_set (rel_sum \ \) A1 A2 \ +lemma rel_set_rel_sum[simp]: +"rel_set (rel_sum \ \) A1 A2 \ rel_set \ (Inl -` A1) (Inl -` A2) \ rel_set \ (Inr -` A1) (Inr -` A2)" (is "?L \ ?Rl \ ?Rr") proof safe diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Main.thy --- a/src/HOL/Main.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Main.thy Tue Jun 21 15:10:43 2016 +0200 @@ -1,7 +1,7 @@ section \Main HOL\ theory Main -imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint Filter +imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices begin text \ diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Jun 21 15:10:43 2016 +0200 @@ -1437,7 +1437,7 @@ lemma closed_unit_cube: "closed unit_cube" unfolding unit_cube_def Collect_ball_eq Collect_conj_eq - by (rule closed_INT, auto intro!: closed_Collect_le) + by (rule closed_INT, auto intro!: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id) lemma compact_unit_cube: "compact unit_cube" (is "compact ?C") unfolding compact_eq_seq_compact_metric @@ -1903,7 +1903,7 @@ proof (rule interiorI) let ?I = "(\i\Basis. {x::'a. 0 < x \ i} \ {x. x \ i < 1})" show "open ?I" - by (intro open_INT finite_Basis ballI open_Int, auto intro: open_Collect_less) + by (intro open_INT finite_Basis ballI open_Int, auto intro: open_Collect_less simp: continuous_on_inner continuous_on_const continuous_on_id) show "\Basis /\<^sub>R 2 \ ?I" by simp show "?I \ unit_cube" diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Jun 21 15:10:43 2016 +0200 @@ -486,7 +486,7 @@ where "v v* m == (\ j. setsum (\i. ((m$i)$j) * (v$i)) (UNIV :: 'm set)) :: 'a^'n" definition "(mat::'a::zero => 'a ^'n^'n) k = (\ i j. if i = j then k else 0)" -definition transpose where +definition transpose where "(transpose::'a^'n^'m \ 'a^'m^'n) A = (\ i j. ((A$j)$i))" definition "(row::'m => 'a ^'n^'m \ 'a ^'n) i A = (\ j. ((A$i)$j))" definition "(column::'n =>'a^'n^'m =>'a^'m) j A = (\ i. ((A$i)$j))" @@ -935,14 +935,18 @@ using Basis_le_infnorm[of "axis i 1" x] by (simp add: Basis_vec_def axis_eq_axis inner_axis) -lemma continuous_component: "continuous F f \ continuous F (\x. f x $ i)" +lemma continuous_component[continuous_intros]: "continuous F f \ continuous F (\x. f x $ i)" unfolding continuous_def by (rule tendsto_vec_nth) -lemma continuous_on_component: "continuous_on s f \ continuous_on s (\x. f x $ i)" +lemma continuous_on_component[continuous_intros]: "continuous_on s f \ continuous_on s (\x. f x $ i)" unfolding continuous_on_def by (fast intro: tendsto_vec_nth) +lemma continuous_on_vec_lambda[continuous_intros]: + "(\i. continuous_on S (f i)) \ continuous_on S (\x. \ i. f i x)" + unfolding continuous_on_def by (auto intro: tendsto_vec_lambda) + lemma closed_positive_orthant: "closed {x::real^'n. \i. 0 \x$i}" - by (simp add: Collect_all_eq closed_INT closed_Collect_le) + by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) lemma bounded_component_cart: "bounded s \ bounded ((\x. x $ i) ` s)" unfolding bounded_def @@ -1091,12 +1095,12 @@ lemma closed_interval_left_cart: fixes b :: "real^'n" shows "closed {x::real^'n. \i. x$i \ b$i}" - by (simp add: Collect_all_eq closed_INT closed_Collect_le) + by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) lemma closed_interval_right_cart: fixes a::"real^'n" shows "closed {x::real^'n. \i. a$i \ x$i}" - by (simp add: Collect_all_eq closed_INT closed_Collect_le) + by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) lemma is_interval_cart: "is_interval (s::(real^'n) set) \ @@ -1104,16 +1108,16 @@ by (simp add: is_interval_def Ball_def Basis_vec_def inner_axis imp_ex) lemma closed_halfspace_component_le_cart: "closed {x::real^'n. x$i \ a}" - by (simp add: closed_Collect_le) + by (simp add: closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) lemma closed_halfspace_component_ge_cart: "closed {x::real^'n. x$i \ a}" - by (simp add: closed_Collect_le) + by (simp add: closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) lemma open_halfspace_component_lt_cart: "open {x::real^'n. x$i < a}" - by (simp add: open_Collect_less) + by (simp add: open_Collect_less continuous_on_const continuous_on_id continuous_on_component) lemma open_halfspace_component_gt_cart: "open {x::real^'n. x$i > a}" - by (simp add: open_Collect_less) + by (simp add: open_Collect_less continuous_on_const continuous_on_id continuous_on_component) lemma Lim_component_le_cart: fixes f :: "'a \ real^'n" @@ -1149,7 +1153,7 @@ proof - { fix i::'n have "closed {x::'a ^ 'n. P i \ x$i = 0}" - by (cases "P i") (simp_all add: closed_Collect_eq) } + by (cases "P i") (simp_all add: closed_Collect_eq continuous_on_const continuous_on_id continuous_on_component) } thus ?thesis unfolding Collect_all_eq by (simp add: closed_INT) qed @@ -1201,7 +1205,7 @@ shows "(\ i. f (axis i 1)) = (\i\Basis. f i *\<^sub>R i)" unfolding euclidean_eq_iff[where 'a="real^'n"] by simp (simp add: Basis_vec_def inner_axis) - + lemma const_vector_cart:"((\ i. d)::real^'n) = (\i\Basis. d *\<^sub>R i)" by (rule vector_cart) @@ -1221,7 +1225,7 @@ using assms unfolding convex_def by auto lemma convex_positive_orthant_cart: "convex {x::real^'n. (\i. 0 \ x$i)}" - by (rule convex_box_cart) (simp add: atLeast_def[symmetric] convex_real_interval) + by (rule convex_box_cart) (simp add: atLeast_def[symmetric]) lemma unit_interval_convex_hull_cart: "cbox (0::real^'n) 1 = convex hull {x. \i. (x$i = 0) \ (x$i = 1)}" diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Tue Jun 21 15:10:43 2016 +0200 @@ -209,8 +209,8 @@ and closed_halfspace_Im_ge: "closed {z. Im(z) \ b}" and closed_halfspace_Im_le: "closed {z. Im(z) \ b}" and closed_halfspace_Im_eq: "closed {z. Im(z) = b}" - by (intro open_Collect_less closed_Collect_le closed_Collect_eq isCont_Re - isCont_Im continuous_ident continuous_const)+ + by (intro open_Collect_less closed_Collect_le closed_Collect_eq continuous_on_Re + continuous_on_Im continuous_on_id continuous_on_const)+ lemma closed_complex_Reals: "closed (\ :: complex set)" proof - diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Jun 21 15:10:43 2016 +0200 @@ -10557,16 +10557,16 @@ next case False define f where "f \ \x. setdist {x} T - setdist {x} S" - have contf: "\x. isCont f x" - unfolding f_def by (intro continuous_intros continuous_at_setdist) + have contf: "continuous_on UNIV f" + unfolding f_def by (intro continuous_intros continuous_on_setdist) show ?thesis proof (rule_tac U = "{x. f x > 0}" and V = "{x. f x < 0}" in that) show "{x. 0 < f x} \ {x. f x < 0} = {}" by auto show "open {x. 0 < f x}" - by (simp add: open_Collect_less contf) + by (simp add: open_Collect_less contf continuous_on_const) show "open {x. f x < 0}" - by (simp add: open_Collect_less contf) + by (simp add: open_Collect_less contf continuous_on_const) show "S \ {x. 0 < f x}" apply (clarsimp simp add: f_def setdist_sing_in_set) using assms diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Jun 21 15:10:43 2016 +0200 @@ -7732,51 +7732,6 @@ using assms unfolding closed_def vimage_Compl [symmetric] by (rule isCont_open_vimage) -lemma open_Collect_less: - fixes f g :: "'a::t2_space \ real" - assumes f: "\x. isCont f x" - and g: "\x. isCont g x" - shows "open {x. f x < g x}" -proof - - have "open ((\x. g x - f x) -` {0<..})" - using isCont_diff [OF g f] open_real_greaterThan - by (rule isCont_open_vimage) - also have "((\x. g x - f x) -` {0<..}) = {x. f x < g x}" - by auto - finally show ?thesis . -qed - -lemma closed_Collect_le: - fixes f g :: "'a::t2_space \ real" - assumes f: "\x. isCont f x" - and g: "\x. isCont g x" - shows "closed {x. f x \ g x}" -proof - - have "closed ((\x. g x - f x) -` {0..})" - using isCont_diff [OF g f] closed_real_atLeast - by (rule isCont_closed_vimage) - also have "((\x. g x - f x) -` {0..}) = {x. f x \ g x}" - by auto - finally show ?thesis . -qed - -lemma closed_Collect_eq: - fixes f g :: "'a::t2_space \ 'b::t2_space" - assumes f: "\x. isCont f x" - and g: "\x. isCont g x" - shows "closed {x. f x = g x}" -proof - - have "open {(x::'b, y::'b). x \ y}" - unfolding open_prod_def by (auto dest!: hausdorff) - then have "closed {(x::'b, y::'b). x = y}" - unfolding closed_def split_def Collect_neg_eq . - with isCont_Pair [OF f g] - have "closed ((\x. (f x, g x)) -` {(x, y). x = y})" - by (rule isCont_closed_vimage) - also have "\ = {x. f x = g x}" by auto - finally show ?thesis . -qed - lemma continuous_on_closed_Collect_le: fixes f g :: "'a::t2_space \ real" assumes f: "continuous_on s f" and g: "continuous_on s g" and s: "closed s" @@ -7794,29 +7749,29 @@ unfolding continuous_at by (intro tendsto_intros) lemma closed_halfspace_le: "closed {x. inner a x \ b}" - by (simp add: closed_Collect_le) + by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id) lemma closed_halfspace_ge: "closed {x. inner a x \ b}" - by (simp add: closed_Collect_le) + by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id) lemma closed_hyperplane: "closed {x. inner a x = b}" - by (simp add: closed_Collect_eq) + by (simp add: closed_Collect_eq continuous_on_inner continuous_on_const continuous_on_id) lemma closed_halfspace_component_le: "closed {x::'a::euclidean_space. x\i \ a}" - by (simp add: closed_Collect_le) + by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id) lemma closed_halfspace_component_ge: "closed {x::'a::euclidean_space. x\i \ a}" - by (simp add: closed_Collect_le) + by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id) lemma closed_interval_left: fixes b :: "'a::euclidean_space" shows "closed {x::'a. \i\Basis. x\i \ b\i}" - by (simp add: Collect_ball_eq closed_INT closed_Collect_le) + by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id) lemma closed_interval_right: fixes a :: "'a::euclidean_space" shows "closed {x::'a. \i\Basis. a\i \ x\i}" - by (simp add: Collect_ball_eq closed_INT closed_Collect_le) + by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id) lemma continuous_le_on_closure: fixes a::real @@ -7840,16 +7795,16 @@ text \Openness of halfspaces.\ lemma open_halfspace_lt: "open {x. inner a x < b}" - by (simp add: open_Collect_less) + by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id) lemma open_halfspace_gt: "open {x. inner a x > b}" - by (simp add: open_Collect_less) + by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id) lemma open_halfspace_component_lt: "open {x::'a::euclidean_space. x\i < a}" - by (simp add: open_Collect_less) + by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id) lemma open_halfspace_component_gt: "open {x::'a::euclidean_space. x\i > a}" - by (simp add: open_Collect_less) + by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id) text \This gives a simple derivation of limit component bounds.\ @@ -8347,7 +8302,7 @@ shows "closed {x. \i\Basis. a \ i \ x \ i}" "closed {x. \i\Basis. x \ i \ a \ i}" unfolding eucl_le_eq_halfspaces - by (simp_all add: closed_INT closed_Collect_le) + by (simp_all add: closed_INT closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id) lemma image_affinity_cbox: fixes m::real fixes a b c :: "'a::euclidean_space" @@ -9024,7 +8979,7 @@ proof - let ?D = "{i\Basis. P i}" have "closed (\i\?D. {x::'a. x\i = 0})" - by (simp add: closed_INT closed_Collect_eq) + by (simp add: closed_INT closed_Collect_eq continuous_on_inner continuous_on_const continuous_on_id) also have "(\i\?D. {x::'a. x\i = 0}) = ?A" by auto finally show "closed ?A" . diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Probability/Binary_Product_Measure.thy --- a/src/HOL/Probability/Binary_Product_Measure.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Probability/Binary_Product_Measure.thy Tue Jun 21 15:10:43 2016 +0200 @@ -37,12 +37,6 @@ unfolding pair_measure_def using pair_measure_closed[of A B] by (rule sets_measure_of) -lemma sets_pair_in_sets: - assumes N: "space A \ space B = space N" - assumes "\a b. a \ sets A \ b \ sets B \ a \ b \ sets N" - shows "sets (A \\<^sub>M B) \ sets N" - using assms by (auto intro!: sets.sigma_sets_subset simp: sets_pair_measure N) - lemma sets_pair_measure_cong[measurable_cong, cong]: "sets M1 = sets M1' \ sets M2 = sets M2' \ sets (M1 \\<^sub>M M2) = sets (M1' \\<^sub>M M2')" unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq) @@ -122,23 +116,45 @@ and measurable_snd'': "(\x. f (snd x)) \ measurable (P \\<^sub>M M) N" by simp_all +lemma sets_pair_in_sets: + assumes "\a b. a \ sets A \ b \ sets B \ a \ b \ sets N" + shows "sets (A \\<^sub>M B) \ sets N" + unfolding sets_pair_measure + by (intro sets.sigma_sets_subset') (auto intro!: assms) + lemma sets_pair_eq_sets_fst_snd: - "sets (A \\<^sub>M B) = sets (Sup_sigma {vimage_algebra (space A \ space B) fst A, vimage_algebra (space A \ space B) snd B})" - (is "?P = sets (Sup_sigma {?fst, ?snd})") + "sets (A \\<^sub>M B) = sets (Sup {vimage_algebra (space A \ space B) fst A, vimage_algebra (space A \ space B) snd B})" + (is "?P = sets (Sup {?fst, ?snd})") proof - { fix a b assume ab: "a \ sets A" "b \ sets B" then have "a \ b = (fst -` a \ (space A \ space B)) \ (snd -` b \ (space A \ space B))" by (auto dest: sets.sets_into_space) - also have "\ \ sets (Sup_sigma {?fst, ?snd})" - using ab by (auto intro: in_Sup_sigma in_vimage_algebra) - finally have "a \ b \ sets (Sup_sigma {?fst, ?snd})" . } + also have "\ \ sets (Sup {?fst, ?snd})" + apply (rule sets.Int) + apply (rule in_sets_Sup) + apply auto [] + apply (rule insertI1) + apply (auto intro: ab in_vimage_algebra) [] + apply (rule in_sets_Sup) + apply auto [] + apply (rule insertI2) + apply (auto intro: ab in_vimage_algebra) + done + finally have "a \ b \ sets (Sup {?fst, ?snd})" . } moreover have "sets ?fst \ sets (A \\<^sub>M B)" by (rule sets_image_in_sets) (auto simp: space_pair_measure[symmetric]) moreover have "sets ?snd \ sets (A \\<^sub>M B)" by (rule sets_image_in_sets) (auto simp: space_pair_measure) ultimately show ?thesis - by (intro antisym[of "sets A" for A] sets_Sup_in_sets sets_pair_in_sets ) - (auto simp add: space_Sup_sigma space_pair_measure) + apply (intro antisym[of "sets A" for A] sets_Sup_in_sets sets_pair_in_sets) + apply simp + apply simp + apply simp + apply (elim disjE) + apply (simp add: space_pair_measure) + apply (simp add: space_pair_measure) + apply (auto simp add: space_pair_measure) + done qed lemma measurable_pair_iff: @@ -597,11 +613,10 @@ have [simp]: "snd \ X \ Y \ Y" "fst \ X \ Y \ X" by auto let ?XY = "{{fst -` a \ X \ Y | a. a \ A}, {snd -` b \ X \ Y | b. b \ B}}" - have "sets ?P = - sets (\\<^sub>\ xy\?XY. sigma (X \ Y) xy)" + have "sets ?P = sets (SUP xy:?XY. sigma (X \ Y) xy)" by (simp add: vimage_algebra_sigma sets_pair_eq_sets_fst_snd A B) also have "\ = sets (sigma (X \ Y) (\?XY))" - by (intro Sup_sigma_sigma arg_cong[where f=sets]) auto + by (intro Sup_sigma arg_cong[where f=sets]) auto also have "\ = sets ?S" proof (intro arg_cong[where f=sets] sigma_eqI sigma_sets_eqI) show "\?XY \ Pow (X \ Y)" "{a \ b |a b. a \ A \ b \ B} \ Pow (X \ Y)" diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Probability/Borel_Space.thy --- a/src/HOL/Probability/Borel_Space.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Probability/Borel_Space.thy Tue Jun 21 15:10:43 2016 +0200 @@ -15,26 +15,6 @@ "(\i. {x\space M. P x i} \ sets M) \ {x\space M. eventually (P x) sequentially} \ sets M" unfolding eventually_sequentially by simp -lemma open_Collect_less: - fixes f g :: "'i::topological_space \ 'a :: {dense_linorder, linorder_topology}" - assumes "continuous_on UNIV f" - assumes "continuous_on UNIV g" - shows "open {x. f x < g x}" -proof - - have "open (\y. {x \ UNIV. f x \ {..< y}} \ {x \ UNIV. g x \ {y <..}})" (is "open ?X") - by (intro open_UN ballI open_Int continuous_open_preimage assms) auto - also have "?X = {x. f x < g x}" - by (auto intro: dense) - finally show ?thesis . -qed - -lemma closed_Collect_le: - fixes f g :: "'i::topological_space \ 'a :: {dense_linorder, linorder_topology}" - assumes f: "continuous_on UNIV f" - assumes g: "continuous_on UNIV g" - shows "closed {x. f x \ g x}" - using open_Collect_less[OF g f] unfolding not_less[symmetric] Collect_neg_eq open_closed . - lemma topological_basis_trivial: "topological_basis {A. open A}" by (auto simp: topological_basis_def) @@ -794,7 +774,7 @@ by (rule borel_measurableI_less) (auto simp: not_le[symmetric]) lemma borel_measurable_less[measurable]: - fixes f :: "'a \ 'b::{second_countable_topology, dense_linorder, linorder_topology}" + fixes f :: "'a \ 'b::{second_countable_topology, linorder_topology}" assumes "f \ borel_measurable M" assumes "g \ borel_measurable M" shows "{w \ space M. f w < g w} \ sets M" @@ -808,7 +788,7 @@ qed lemma - fixes f :: "'a \ 'b::{second_countable_topology, dense_linorder, linorder_topology}" + fixes f :: "'a \ 'b::{second_countable_topology, linorder_topology}" assumes f[measurable]: "f \ borel_measurable M" assumes g[measurable]: "g \ borel_measurable M" shows borel_measurable_le[measurable]: "{w \ space M. f w \ g w} \ sets M" @@ -947,19 +927,19 @@ unfolding liminf_SUP_INF limsup_INF_SUP using assms by auto lemma measurable_convergent[measurable (raw)]: - fixes f :: "nat \ 'a \ 'b::{complete_linorder, second_countable_topology, dense_linorder, linorder_topology}" + fixes f :: "nat \ 'a \ 'b::{complete_linorder, second_countable_topology, linorder_topology}" assumes [measurable]: "\i. f i \ borel_measurable M" shows "Measurable.pred M (\x. convergent (\i. f i x))" unfolding convergent_ereal by measurable lemma sets_Collect_convergent[measurable]: - fixes f :: "nat \ 'a \ 'b::{complete_linorder, second_countable_topology, dense_linorder, linorder_topology}" + fixes f :: "nat \ 'a \ 'b::{complete_linorder, second_countable_topology, linorder_topology}" assumes f[measurable]: "\i. f i \ borel_measurable M" shows "{x\space M. convergent (\i. f i x)} \ sets M" by measurable lemma borel_measurable_lim[measurable (raw)]: - fixes f :: "nat \ 'a \ 'b::{complete_linorder, second_countable_topology, dense_linorder, linorder_topology}" + fixes f :: "nat \ 'a \ 'b::{complete_linorder, second_countable_topology, linorder_topology}" assumes [measurable]: "\i. f i \ borel_measurable M" shows "(\x. lim (\i. f i x)) \ borel_measurable M" proof - @@ -970,7 +950,7 @@ qed lemma borel_measurable_LIMSEQ_order: - fixes u :: "nat \ 'a \ 'b::{complete_linorder, second_countable_topology, dense_linorder, linorder_topology}" + fixes u :: "nat \ 'a \ 'b::{complete_linorder, second_countable_topology, linorder_topology}" assumes u': "\x. x \ space M \ (\i. u i x) \ u' x" and u: "\i. u i \ borel_measurable M" shows "u' \ borel_measurable M" @@ -999,7 +979,7 @@ qed simp lemma borel_measurable_suminf_order[measurable (raw)]: - fixes f :: "nat \ 'a \ 'b::{complete_linorder, second_countable_topology, dense_linorder, linorder_topology, topological_comm_monoid_add}" + fixes f :: "nat \ 'a \ 'b::{complete_linorder, second_countable_topology, linorder_topology, topological_comm_monoid_add}" assumes f[measurable]: "\i. f i \ borel_measurable M" shows "(\x. suminf (\i. f i x)) \ borel_measurable M" unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Probability/Central_Limit_Theorem.thy --- a/src/HOL/Probability/Central_Limit_Theorem.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Probability/Central_Limit_Theorem.thy Tue Jun 21 15:10:43 2016 +0200 @@ -1,5 +1,5 @@ -(* Theory: Central_Limit_Theorem.thy - Authors: Jeremy Avigad, Luke Serafin +(* Title: HOL/Probability/Central_Limit_Theorem.thy + Authors: Jeremy Avigad (CMU), Luke Serafin (CMU) *) section \The Central Limit Theorem\ @@ -73,20 +73,20 @@ using \_pos by (simp add: power_divide) also have "t^2 / n / 2 = (t^2 / 2) / n" by simp - finally have **: "norm (\ n t - (1 + (-(t^2) / 2) / n)) \ + finally have **: "norm (\ n t - (1 + (-(t^2) / 2) / n)) \ ?t\<^sup>2 / 6 * (LINT x|\. min (6 * x\<^sup>2) (\?t\ * \x\ ^ 3))" by simp - have "norm (\ n t - (complex_of_real (1 + (-(t^2) / 2) / n))^n) \ + have "norm (\ n t - (complex_of_real (1 + (-(t^2) / 2) / n))^n) \ n * norm (\ n t - (complex_of_real (1 + (-(t^2) / 2) / n)))" using n by (auto intro!: norm_power_diff \.cmod_char_le_1 abs_leI simp del: of_real_diff simp: of_real_diff[symmetric] divide_le_eq \_eq \_def) also have "\ \ n * (?t\<^sup>2 / 6 * (LINT x|\. min (6 * x\<^sup>2) (\?t\ * \x\ ^ 3)))" by (rule mult_left_mono [OF **], simp) - also have "\ = (t\<^sup>2 / (6 * \\<^sup>2) * (LINT x|\. min (6 * x\<^sup>2) (\?t\ * \x\ ^ 3)))" + also have "\ = (t\<^sup>2 / (6 * \\<^sup>2) * (LINT x|\. min (6 * x\<^sup>2) (\?t\ * \x\ ^ 3)))" using \_pos by (simp add: field_simps min_absorb2) - finally show "norm (\ n t - (1 + (-(t^2) / 2) / n)^n) \ - (t\<^sup>2 / (6 * \\<^sup>2) * (LINT x|\. min (6 * x\<^sup>2) (\?t\ * \x\ ^ 3)))" + finally show "norm (\ n t - (1 + (-(t^2) / 2) / n)^n) \ + (t\<^sup>2 / (6 * \\<^sup>2) * (LINT x|\. min (6 * x\<^sup>2) (\?t\ * \x\ ^ 3)))" by simp qed @@ -95,7 +95,7 @@ fix t let ?t = "\n. t / sqrt (\\<^sup>2 * n)" have "\x. (\n. min (6 * x\<^sup>2) (\t\ * \x\ ^ 3 / \sqrt (\\<^sup>2 * real n)\)) \ 0" - using \_pos + using \_pos by (auto simp: real_sqrt_mult min_absorb2 intro!: tendsto_min[THEN tendsto_eq_rhs] sqrt_at_top[THEN filterlim_compose] filterlim_tendsto_pos_mult_at_top filterlim_at_top_imp_at_infinity diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Probability/Characteristic_Functions.thy --- a/src/HOL/Probability/Characteristic_Functions.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Probability/Characteristic_Functions.thy Tue Jun 21 15:10:43 2016 +0200 @@ -1,6 +1,5 @@ -(* - Theory: Characteristic_Functions.thy - Authors: Jeremy Avigad, Luke Serafin +(* Title: Characteristic_Functions.thy + Authors: Jeremy Avigad (CMU), Luke Serafin (CMU), Johannes Hölzl (TUM) *) section \Characteristic Functions\ @@ -29,7 +28,7 @@ qed qed -lemma limseq_even_odd: +lemma limseq_even_odd: assumes "(\n. f (2 * n)) \ (l :: 'a :: topological_space)" and "(\n. f (2 * n + 1)) \ l" shows "f \ l" @@ -63,7 +62,7 @@ lemma (in real_distribution) char_zero: "char M 0 = 1" unfolding char_def by (simp del: space_eq_univ add: prob_space) -lemma (in prob_space) integrable_iexp: +lemma (in prob_space) integrable_iexp: assumes f: "f \ borel_measurable M" "\x. Im (f x) = 0" shows "integrable M (\x. exp (ii * (f x)))" proof (intro integrable_const_bound [of _ 1]) @@ -96,7 +95,7 @@ subsection \Independence\ -(* the automation can probably be improved *) +(* the automation can probably be improved *) lemma (in prob_space) char_distr_sum: fixes X1 X2 :: "'a \ real" and t :: real assumes "indep_var borel X1 borel X2" @@ -145,13 +144,13 @@ let ?F = "\s. complex_of_real(-((x - s) ^ (Suc n) / (Suc n))) * iexp s" have "x^(Suc n) / (Suc n) = (CLBINT s=0..x. (f s n * iexp s + (ii * iexp s) * -(f s (Suc n) / (Suc n))))" (is "?LHS = ?RHS") proof - - have "?RHS = (CLBINT s=0..x. (f s n * iexp s + (ii * iexp s) * + have "?RHS = (CLBINT s=0..x. (f s n * iexp s + (ii * iexp s) * complex_of_real(-((x - s) ^ (Suc n) / (Suc n)))))" by (cases "0 \ x") (auto intro!: simp: f_def[abs_def]) also have "... = ?F x - ?F 0" unfolding zero_ereal_def using 1 by (intro interval_integral_FTC_finite) - (auto simp: f_def add_nonneg_eq_0_iff complex_eq_iff + (auto simp: f_def add_nonneg_eq_0_iff complex_eq_iff intro!: continuous_at_imp_continuous_on continuous_intros) finally show ?thesis by auto @@ -184,7 +183,7 @@ lemma iexp_eq2: fixes x :: real - defines "f s m \ complex_of_real ((x - s) ^ m)" + defines "f s m \ complex_of_real ((x - s) ^ m)" shows "iexp x = (\k\Suc n. (ii*x)^k/fact k) + ii^Suc n/fact n * (CLBINT s=0..x. f s n*(iexp s - 1))" proof - have isCont_f: "isCont (\s. f s n) x" for n x @@ -224,7 +223,7 @@ intro!: interval_integral_cong) then show ?thesis by simp next - assume "\ (0 \ x \ even n)" + assume "\ (0 \ x \ even n)" then have "(LBINT s=0..x. \(x - s)^n\) = LBINT s=0..x. -((x - s)^n)" by (auto simp add: zero_ereal_def power_abs min_absorb1 max_absorb2 ereal_min[symmetric] ereal_max[symmetric] power_minus_odd[symmetric] @@ -307,11 +306,11 @@ proof - have integ_iexp: "integrable M (\x. iexp (t * x))" by (intro integrable_const_bound) auto - + define c where [abs_def]: "c k x = (ii * t)^k / fact k * complex_of_real (x^k)" for k x have integ_c: "\k. k \ n \ integrable M (\x. c k x)" unfolding c_def by (intro integrable_mult_right integrable_of_real integrable_moments) - + have "k \ n \ expectation (c k) = (\*t) ^ k * (expectation (\x. x ^ k)) / fact k" for k unfolding c_def integral_mult_right_zero integral_complex_of_real by simp then have "norm (char M t - ?t1) = norm (char M t - (CLINT x | M. (\k \ n. c k x)))" @@ -342,7 +341,7 @@ proof - have integ_iexp: "integrable M (\x. iexp (t * x))" by (intro integrable_const_bound) auto - + define c where [abs_def]: "c k x = (ii * t)^k / fact k * complex_of_real (x^k)" for k x have integ_c: "\k. k \ n \ integrable M (\x. c k x)" unfolding c_def by (intro integrable_mult_right integrable_of_real integrable_moments) @@ -355,7 +354,7 @@ apply (simp_all add: field_simps abs_mult del: fact_Suc) apply (simp_all add: field_simps) done - + have "k \ n \ expectation (c k) = (\*t) ^ k * (expectation (\x. x ^ k)) / fact k" for k unfolding c_def integral_mult_right_zero integral_complex_of_real by simp then have "norm (char M t - ?t1) = norm (char M t - (CLINT x | M. (\k \ n. c k x)))" @@ -399,9 +398,9 @@ proof - note real_distribution.char_approx2 [of M 2 t, simplified] have [simp]: "prob UNIV = 1" by (metis prob_space space_eq_univ) - from integral_2 have [simp]: "expectation (\x. x * x) = \2" + from integral_2 have [simp]: "expectation (\x. x * x) = \2" by (simp add: integral_1 numeral_eq_Suc) - have 1: "k \ 2 \ integrable M (\x. x^k)" for k + have 1: "k \ 2 \ integrable M (\x. x^k)" for k using assms by (auto simp: eval_nat_numeral le_Suc_eq) note char_approx1 note 2 = char_approx1 [of 2 t, OF 1, simplified] @@ -417,7 +416,7 @@ qed text \ - This is a more familiar textbook formulation in terms of random variables, but + This is a more familiar textbook formulation in terms of random variables, but we will use the previous version for the CLT. \ diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Probability/Distribution_Functions.thy --- a/src/HOL/Probability/Distribution_Functions.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Probability/Distribution_Functions.thy Tue Jun 21 15:10:43 2016 +0200 @@ -1,6 +1,5 @@ -(* - Title : Distribution_Functions.thy - Authors : Jeremy Avigad and Luke Serafin +(* Title: Distribution_Functions.thy + Authors: Jeremy Avigad (CMU) and Luke Serafin (CMU) *) section \Distribution Functions\ diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Probability/Embed_Measure.thy --- a/src/HOL/Probability/Embed_Measure.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Probability/Embed_Measure.thy Tue Jun 21 15:10:43 2016 +0200 @@ -241,20 +241,25 @@ 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] SUP_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 vimage_algebra_Sup_sigma) + 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 image_insert) + apply simp 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_sigma] arg_cong2[where f=insert] vimage_algebra_cong) + 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) @@ -270,6 +275,19 @@ 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") diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Probability/Finite_Product_Measure.thy --- a/src/HOL/Probability/Finite_Product_Measure.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Probability/Finite_Product_Measure.thy Tue Jun 21 15:10:43 2016 +0200 @@ -389,8 +389,12 @@ qed lemma sets_PiM_eq_proj: - "I \ {} \ sets (PiM I M) = sets (\\<^sub>\ i\I. vimage_algebra (\\<^sub>E i\I. space (M i)) (\x. x i) (M i))" - apply (simp add: sets_PiM_single sets_Sup_sigma) + "I \ {} \ sets (PiM I M) = sets (SUP i:I. vimage_algebra (\\<^sub>E i\I. space (M i)) (\x. x i) (M i))" + apply (simp add: sets_PiM_single) + apply (subst sets_Sup_eq[where X="\\<^sub>E i\I. space (M i)"]) + apply auto [] + apply auto [] + apply simp apply (subst SUP_cong[OF refl]) apply (rule sets_vimage_algebra2) apply auto [] @@ -418,10 +422,10 @@ let ?F = "\i. {(\x. x i) -` A \ Pi\<^sub>E I \ |A. A \ E i}" assume "I \ {}" then have "sets (Pi\<^sub>M I (\i. sigma (\ i) (E i))) = - sets (\\<^sub>\ i\I. vimage_algebra (\\<^sub>E i\I. \ i) (\x. x i) (sigma (\ i) (E i)))" + sets (SUP i:I. vimage_algebra (\\<^sub>E i\I. \ i) (\x. x i) (sigma (\ i) (E i)))" by (subst sets_PiM_eq_proj) (auto simp: space_measure_of_conv) - also have "\ = sets (\\<^sub>\ i\I. sigma (Pi\<^sub>E I \) (?F i))" - using E by (intro SUP_sigma_cong arg_cong[where f=sets] vimage_algebra_sigma) auto + also have "\ = sets (SUP i:I. sigma (Pi\<^sub>E I \) (?F i))" + using E by (intro sets_SUP_cong arg_cong[where f=sets] vimage_algebra_sigma) auto also have "\ = sets (sigma (Pi\<^sub>E I \) (\i\I. ?F i))" using \I \ {}\ by (intro arg_cong[where f=sets] SUP_sigma_sigma) auto also have "\ = sets (sigma (Pi\<^sub>E I \) P)" diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Probability/Giry_Monad.thy --- a/src/HOL/Probability/Giry_Monad.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Probability/Giry_Monad.thy Tue Jun 21 15:10:43 2016 +0200 @@ -162,17 +162,17 @@ definition subprob_algebra :: "'a measure \ 'a measure measure" where "subprob_algebra K = - (\\<^sub>\ A\sets K. vimage_algebra {M. subprob_space M \ sets M = sets K} (\M. emeasure M A) borel)" + (SUP A : sets K. vimage_algebra {M. subprob_space M \ sets M = sets K} (\M. emeasure M A) borel)" lemma space_subprob_algebra: "space (subprob_algebra A) = {M. subprob_space M \ sets M = sets A}" - by (auto simp add: subprob_algebra_def space_Sup_sigma) + by (auto simp add: subprob_algebra_def space_Sup_eq_UN) lemma subprob_algebra_cong: "sets M = sets N \ subprob_algebra M = subprob_algebra N" by (simp add: subprob_algebra_def) lemma measurable_emeasure_subprob_algebra[measurable]: "a \ sets A \ (\M. emeasure M a) \ borel_measurable (subprob_algebra A)" - by (auto intro!: measurable_Sup_sigma1 measurable_vimage_algebra1 simp: subprob_algebra_def) + by (auto intro!: measurable_Sup1 measurable_vimage_algebra1 simp: subprob_algebra_def) lemma measurable_measure_subprob_algebra[measurable]: "a \ sets A \ (\M. measure M a) \ borel_measurable (subprob_algebra A)" @@ -227,7 +227,7 @@ (\a. a \ space M \ sets (K a) = sets N) \ (\A. A \ sets N \ (\a. emeasure (K a) A) \ borel_measurable M) \ K \ measurable M (subprob_algebra N)" - by (auto intro!: measurable_Sup_sigma2 measurable_vimage_algebra2 simp: subprob_algebra_def) + by (auto intro!: measurable_Sup2 measurable_vimage_algebra2 simp: subprob_algebra_def) lemma measurable_submarkov: "K \ measurable M (subprob_algebra M) \ @@ -1504,55 +1504,6 @@ finally show ?thesis . qed -section \Measures form a $\omega$-chain complete partial order\ - -definition SUP_measure :: "(nat \ 'a measure) \ 'a measure" where - "SUP_measure M = measure_of (\i. space (M i)) (\i. sets (M i)) (\A. SUP i. emeasure (M i) A)" - -lemma - assumes const: "\i j. sets (M i) = sets (M j)" - shows space_SUP_measure: "space (SUP_measure M) = space (M i)" (is ?sp) - and sets_SUP_measure: "sets (SUP_measure M) = sets (M i)" (is ?st) -proof - - have "(\i. sets (M i)) = sets (M i)" - using const by auto - moreover have "(\i. space (M i)) = space (M i)" - using const[THEN sets_eq_imp_space_eq] by auto - moreover have "\i. sets (M i) \ Pow (space (M i))" - by (auto dest: sets.sets_into_space) - ultimately show ?sp ?st - by (simp_all add: SUP_measure_def) -qed - -lemma emeasure_SUP_measure: - assumes const: "\i j. sets (M i) = sets (M j)" - and mono: "mono (\i. emeasure (M i))" - shows "emeasure (SUP_measure M) A = (SUP i. emeasure (M i) A)" -proof cases - assume "A \ sets (SUP_measure M)" - show ?thesis - proof (rule emeasure_measure_of[OF SUP_measure_def]) - show "countably_additive (sets (SUP_measure M)) (\A. SUP i. emeasure (M i) A)" - proof (rule countably_additiveI) - fix A :: "nat \ 'a set" assume "range A \ sets (SUP_measure M)" - then have "\i j. A i \ sets (M j)" - using sets_SUP_measure[of M, OF const] by simp - moreover assume "disjoint_family A" - ultimately show "(\i. SUP ia. emeasure (M ia) (A i)) = (SUP i. emeasure (M i) (\i. A i))" - using suminf_SUP_eq - using mono by (subst ennreal_suminf_SUP_eq) (auto simp: mono_def le_fun_def intro!: SUP_cong suminf_emeasure) - qed - show "positive (sets (SUP_measure M)) (\A. SUP i. emeasure (M i) A)" - by (auto simp: positive_def intro: SUP_upper2) - show "(\i. sets (M i)) \ Pow (\i. space (M i))" - using sets.sets_into_space by auto - qed fact -next - assume "A \ sets (SUP_measure M)" - with sets_SUP_measure[of M, OF const] show ?thesis - by (simp add: emeasure_notin_sets) -qed - lemma bind_return'': "sets M = sets N \ M \ return N = M" by (cases "space M = {}") (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return' diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Probability/Helly_Selection.thy --- a/src/HOL/Probability/Helly_Selection.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Probability/Helly_Selection.thy Tue Jun 21 15:10:43 2016 +0200 @@ -1,6 +1,6 @@ -(* - Theory: Helly_Selection.thy - Authors: Jeremy Avigad, Luke Serafin +(* Title: HOL/Probability/Helly_Selection.thy + Authors: Jeremy Avigad (CMU), Luke Serafin (CMU) + Authors: Johannes Hölzl, TU München *) section \Helly's selection theorem\ @@ -36,7 +36,7 @@ fix n :: nat and s :: "nat \ nat" assume s: "subseq s" have "bounded {-M..M}" using bounded_closed_interval by auto - moreover have "\k. f (s k) (r n) \ {-M..M}" + moreover have "\k. f (s k) (r n) \ {-M..M}" using bdd by (simp add: abs_le_iff minus_le_iff) ultimately have "\l s'. subseq s' \ ((\k. f (s k) (r n)) \ s') \ l" using compact_Icc compact_imp_seq_compact seq_compactE by metis diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Probability/Interval_Integral.thy --- a/src/HOL/Probability/Interval_Integral.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Probability/Interval_Integral.thy Tue Jun 21 15:10:43 2016 +0200 @@ -1,5 +1,5 @@ (* Title: HOL/Probability/Interval_Integral.thy - Author: Jeremy Avigad, Johannes Hölzl, Luke Serafin + Author: Jeremy Avigad (CMU), Johannes Hölzl (TUM), Luke Serafin (CMU) Lebesgue integral over an interval (with endpoints possibly +-\) *) @@ -15,7 +15,7 @@ lemma has_vector_derivative_weaken: fixes x D and f g s t assumes f: "(f has_vector_derivative D) (at x within t)" - and "x \ s" "s \ t" + and "x \ s" "s \ t" and "\x. x \ s \ f x = g x" shows "(g has_vector_derivative D) (at x within s)" proof - @@ -51,7 +51,7 @@ lemma borel_einterval[measurable]: "einterval a b \ sets borel" unfolding einterval_def by measurable -(* +(* Approximating a (possibly infinite) interval *) @@ -61,7 +61,7 @@ lemma ereal_incseq_approx: fixes a b :: ereal assumes "a < b" - obtains X :: "nat \ real" where + obtains X :: "nat \ real" where "incseq X" "\i. a < X i" "\i. X i < b" "X \ b" proof (cases b) case PInf @@ -104,7 +104,7 @@ lemma ereal_decseq_approx: fixes a b :: ereal assumes "a < b" - obtains X :: "nat \ real" where + obtains X :: "nat \ real" where "decseq X" "\i. a < X i" "\i. X i < b" "X \ a" proof - have "-b < -a" using \a < b\ by simp @@ -120,7 +120,7 @@ lemma einterval_Icc_approximation: fixes a b :: ereal assumes "a < b" - obtains u l :: "nat \ real" where + obtains u l :: "nat \ real" where "einterval a b = (\i. {l i .. u i})" "incseq u" "decseq l" "\i. l i < u i" "\i. a < l i" "\i. u i < b" "l \ a" "u \ b" @@ -134,7 +134,7 @@ fix x assume "a < ereal x" "ereal x < b" have "eventually (\i. ereal (l i) < ereal x) sequentially" using l(4) \a < ereal x\ by (rule order_tendstoD) - moreover + moreover have "eventually (\i. ereal x < ereal (u i)) sequentially" using u(4) \ereal x< b\ by (rule order_tendstoD) ultimately have "eventually (\i. l i < x \ x < u i) sequentially" @@ -142,7 +142,7 @@ then show "\i. l i \ x \ x \ u i" by (auto intro: less_imp_le simp: eventually_sequentially) next - fix x i assume "l i \ x" "x \ u i" + fix x i assume "l i \ x" "x \ u i" with \a < ereal (l i)\ \ereal (u i) < b\ show "a < ereal x" "ereal x < b" by (auto simp del: ereal_less_eq(3) simp add: ereal_less_eq(3)[symmetric]) @@ -151,7 +151,7 @@ by (intro that) fact+ qed -(* TODO: in this definition, it would be more natural if einterval a b included a and b when +(* TODO: in this definition, it would be more natural if einterval a b included a and b when they are real. *) definition interval_lebesgue_integral :: "real measure \ ereal \ ereal \ (real \ 'a) \ 'a::{banach, second_countable_topology}" where "interval_lebesgue_integral M a b f = @@ -203,23 +203,23 @@ by (simp add: *) qed -lemma interval_lebesgue_integral_add [intro, simp]: - fixes M a b f +lemma interval_lebesgue_integral_add [intro, simp]: + fixes M a b f assumes "interval_lebesgue_integrable M a b f" "interval_lebesgue_integrable M a b g" - shows "interval_lebesgue_integrable M a b (\x. f x + g x)" and - "interval_lebesgue_integral M a b (\x. f x + g x) = + shows "interval_lebesgue_integrable M a b (\x. f x + g x)" and + "interval_lebesgue_integral M a b (\x. f x + g x) = interval_lebesgue_integral M a b f + interval_lebesgue_integral M a b g" -using assms by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def +using assms by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def field_simps) -lemma interval_lebesgue_integral_diff [intro, simp]: - fixes M a b f +lemma interval_lebesgue_integral_diff [intro, simp]: + fixes M a b f assumes "interval_lebesgue_integrable M a b f" "interval_lebesgue_integrable M a b g" - shows "interval_lebesgue_integrable M a b (\x. f x - g x)" and - "interval_lebesgue_integral M a b (\x. f x - g x) = + shows "interval_lebesgue_integrable M a b (\x. f x - g x)" and + "interval_lebesgue_integral M a b (\x. f x - g x) = interval_lebesgue_integral M a b f - interval_lebesgue_integral M a b g" -using assms by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def +using assms by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def field_simps) lemma interval_lebesgue_integrable_mult_right [intro, simp]: @@ -268,13 +268,13 @@ unfolding interval_lebesgue_integral_def by (auto simp add: interval_lebesgue_integral_def set_integral_complex_of_real) -lemma interval_lebesgue_integral_le_eq: +lemma interval_lebesgue_integral_le_eq: fixes a b f assumes "a \ b" shows "interval_lebesgue_integral M a b f = (LINT x : einterval a b | M. f x)" using assms by (auto simp add: interval_lebesgue_integral_def) -lemma interval_lebesgue_integral_gt_eq: +lemma interval_lebesgue_integral_gt_eq: fixes a b f assumes "a > b" shows "interval_lebesgue_integral M a b f = -(LINT x : einterval b a | M. f x)" @@ -318,13 +318,13 @@ lemma interval_lebesgue_integral_0_infty: "interval_lebesgue_integrable M 0 \ f \ set_integrable M {0<..} f" "interval_lebesgue_integral M 0 \ f = (LINT x:{0<..}|M. f x)" - unfolding zero_ereal_def + unfolding zero_ereal_def by (auto simp: interval_lebesgue_integral_le_eq interval_lebesgue_integrable_def) lemma interval_integral_to_infinity_eq: "(LINT x=ereal a..\ | M. f x) = (LINT x : {a<..} | M. f x)" unfolding interval_lebesgue_integral_def by auto -lemma interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a \ f) = +lemma interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a \ f) = (set_integrable M {a<..} f)" unfolding interval_lebesgue_integrable_def by auto @@ -334,14 +334,14 @@ lemma interval_integral_zero [simp]: fixes a b :: ereal - shows"LBINT x=a..b. 0 = 0" -unfolding interval_lebesgue_integral_def einterval_eq + shows"LBINT x=a..b. 0 = 0" +unfolding interval_lebesgue_integral_def einterval_eq by simp lemma interval_integral_const [intro, simp]: fixes a b c :: real - shows "interval_lebesgue_integrable lborel a b (\x. c)" and "LBINT x=a..b. c = c * (b - a)" -unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq + shows "interval_lebesgue_integrable lborel a b (\x. c)" and "LBINT x=a..b. c = c * (b - a)" +unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq by (auto simp add: less_imp_le field_simps measure_def) lemma interval_integral_cong_AE: @@ -359,7 +359,7 @@ qed lemma interval_integral_cong: - assumes "\x. x \ einterval (min a b) (max a b) \ f x = g x" + assumes "\x. x \ einterval (min a b) (max a b) \ f x = g x" shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g" using assms proof (induct a b rule: linorder_wlog) @@ -434,9 +434,9 @@ apply (auto simp: eq anti_eq einterval_iff split: split_indicator) done -lemma interval_integral_sum: +lemma interval_integral_sum: fixes a b c :: ereal - assumes integrable: "interval_lebesgue_integrable lborel (min a (min b c)) (max a (max b c)) f" + assumes integrable: "interval_lebesgue_integrable lborel (min a (min b c)) (max a (max b c)) f" shows "(LBINT x=a..b. f x) + (LBINT x=b..c. f x) = (LBINT x=a..c. f x)" proof - let ?I = "\a b. LBINT x=a..b. f x" @@ -487,16 +487,16 @@ using assms unfolding interval_lebesgue_integrable_def apply simp by (rule set_integrable_subset, rule borel_integrable_atLeastAtMost' [of a b], auto) -lemma interval_integral_eq_integral: +lemma interval_integral_eq_integral: fixes f :: "real \ 'a::euclidean_space" shows "a \ b \ set_integrable lborel {a..b} f \ LBINT x=a..b. f x = integral {a..b} f" by (subst interval_integral_Icc, simp) (rule set_borel_integral_eq_integral) -lemma interval_integral_eq_integral': +lemma interval_integral_eq_integral': fixes f :: "real \ 'a::euclidean_space" shows "a \ b \ set_integrable lborel (einterval a b) f \ LBINT x=a..b. f x = integral (einterval a b) f" by (subst interval_lebesgue_integral_le_eq, simp) (rule set_borel_integral_eq_integral) - + (* General limit approximation arguments *) @@ -513,7 +513,7 @@ assumes f_nonneg: "AE x in lborel. a < ereal x \ ereal x < b \ 0 \ f x" assumes f_measurable: "set_borel_measurable lborel (einterval a b) f" assumes lbint_lim: "(\i. LBINT x=l i.. u i. f x) \ C" - shows + shows "set_integrable lborel (einterval a b) f" "(LBINT x=a..b. f x) = C" proof - @@ -551,7 +551,7 @@ also have "... = C" by (rule integral_monotone_convergence [OF 1 2 3 4 5]) finally show "(LBINT x=a..b. f x) = C" . - show "set_integrable lborel (einterval a b) f" + show "set_integrable lborel (einterval a b) f" by (rule integrable_monotone_convergence[OF 1 2 3 4 5]) qed @@ -578,7 +578,7 @@ show "AE x in lborel. (\i. indicator {l i..u i} x *\<^sub>R f x) \ indicator (einterval a b) x *\<^sub>R f x" proof (intro AE_I2 tendsto_intros Lim_eventually) fix x - { fix i assume "l i \ x" "x \ u i" + { fix i assume "l i \ x" "x \ u i" with \incseq u\[THEN incseqD, of i] \decseq l\[THEN decseqD, of i] have "eventually (\i. l i \ x \ x \ u i) sequentially" by (auto simp: eventually_sequentially decseq_def incseq_def intro: order_trans) } @@ -592,7 +592,7 @@ qed (* - A slightly stronger version of integral_FTC_atLeastAtMost and related facts, + A slightly stronger version of integral_FTC_atLeastAtMost and related facts, with continuous_on instead of isCont TODO: make the older versions corollaries of these (using continuous_at_imp_continuous_on, etc.) @@ -615,8 +615,8 @@ lemma interval_integral_FTC_finite: fixes f F :: "real \ 'a::euclidean_space" and a b :: real assumes f: "continuous_on {min a b..max a b} f" - assumes F: "\x. min a b \ x \ x \ max a b \ (F has_vector_derivative (f x)) (at x within - {min a b..max a b})" + assumes F: "\x. min a b \ x \ x \ max a b \ (F has_vector_derivative (f x)) (at x within + {min a b..max a b})" shows "(LBINT x=a..b. f x) = F b - F a" apply (case_tac "a \ b") apply (subst interval_integral_Icc, simp) @@ -632,13 +632,13 @@ lemma interval_integral_FTC_nonneg: fixes f F :: "real \ real" and a b :: ereal assumes "a < b" - assumes F: "\x. a < ereal x \ ereal x < b \ DERIV F x :> f x" - assumes f: "\x. a < ereal x \ ereal x < b \ isCont f x" + assumes F: "\x. a < ereal x \ ereal x < b \ DERIV F x :> f x" + assumes f: "\x. a < ereal x \ ereal x < b \ isCont f x" assumes f_nonneg: "AE x in lborel. a < ereal x \ ereal x < b \ 0 \ f x" assumes A: "((F \ real_of_ereal) \ A) (at_right a)" assumes B: "((F \ real_of_ereal) \ B) (at_left b)" shows - "set_integrable lborel (einterval a b) f" + "set_integrable lborel (einterval a b) f" "(LBINT x=a..b. f x) = B - A" proof - from einterval_Icc_approximation[OF \a < b\] guess u l . note approx = this @@ -660,7 +660,7 @@ (auto simp del: ereal_less_eq simp add: ereal_less_eq(3)[symmetric]) qed have 2: "set_borel_measurable lborel (einterval a b) f" - by (auto simp del: real_scaleR_def intro!: set_borel_measurable_continuous + by (auto simp del: real_scaleR_def intro!: set_borel_measurable_continuous simp: continuous_on_eq_continuous_at einterval_iff f) have 3: "(\i. LBINT x=l i..u i. f x) \ B - A" apply (subst FTCi) @@ -672,15 +672,15 @@ by (elim allE[of _ "\i. ereal (l i)"], auto) show "(LBINT x=a..b. f x) = B - A" by (rule interval_integral_Icc_approx_nonneg [OF \a < b\ approx 1 f_nonneg 2 3]) - show "set_integrable lborel (einterval a b) f" + show "set_integrable lborel (einterval a b) f" by (rule interval_integral_Icc_approx_nonneg [OF \a < b\ approx 1 f_nonneg 2 3]) qed lemma interval_integral_FTC_integrable: fixes f F :: "real \ 'a::euclidean_space" and a b :: ereal assumes "a < b" - assumes F: "\x. a < ereal x \ ereal x < b \ (F has_vector_derivative f x) (at x)" - assumes f: "\x. a < ereal x \ ereal x < b \ isCont f x" + assumes F: "\x. a < ereal x \ ereal x < b \ (F has_vector_derivative f x) (at x)" + assumes f: "\x. a < ereal x \ ereal x < b \ isCont f x" assumes f_integrable: "set_integrable lborel (einterval a b) f" assumes A: "((F \ real_of_ereal) \ A) (at_right a)" assumes B: "((F \ real_of_ereal) \ B) (at_left b)" @@ -709,7 +709,7 @@ by (elim LIMSEQ_unique) qed -(* +(* The second Fundamental Theorem of Calculus and existence of antiderivatives on an einterval. *) @@ -746,12 +746,12 @@ qed (insert assms, auto) qed -lemma einterval_antiderivative: +lemma einterval_antiderivative: fixes a b :: ereal and f :: "real \ 'a::euclidean_space" assumes "a < b" and contf: "\x :: real. a < x \ x < b \ isCont f x" shows "\F. \x :: real. a < x \ x < b \ (F has_vector_derivative f x) (at x)" proof - - from einterval_nonempty [OF \a < b\] obtain c :: real where [simp]: "a < c" "c < b" + from einterval_nonempty [OF \a < b\] obtain c :: real where [simp]: "a < c" "c < b" by (auto simp add: einterval_def) let ?F = "(\u. LBINT y=c..u. f y)" show ?thesis @@ -759,10 +759,10 @@ fix x :: real assume [simp]: "a < x" "x < b" have 1: "a < min c x" by simp - from einterval_nonempty [OF 1] obtain d :: real where [simp]: "a < d" "d < c" "d < x" + from einterval_nonempty [OF 1] obtain d :: real where [simp]: "a < d" "d < c" "d < x" by (auto simp add: einterval_def) have 2: "max c x < b" by simp - from einterval_nonempty [OF 2] obtain e :: real where [simp]: "c < e" "x < e" "e < b" + from einterval_nonempty [OF 2] obtain e :: real where [simp]: "c < e" "x < e" "e < b" by (auto simp add: einterval_def) show "(?F has_vector_derivative f x) (at x)" (* TODO: factor out the next three lines to has_field_derivative_within_open *) @@ -785,7 +785,7 @@ Once again, three versions: first, for finite intervals, and then two versions for arbitrary intervals. *) - + lemma interval_integral_substitution_finite: fixes a b :: real and f :: "real \ 'a::euclidean_space" assumes "a \ b" @@ -798,7 +798,7 @@ using derivg unfolding has_field_derivative_iff_has_vector_derivative . then have contg [simp]: "continuous_on {a..b} g" by (rule continuous_on_vector_derivative) auto - have 1: "\u. min (g a) (g b) \ u \ u \ max (g a) (g b) \ + have 1: "\u. min (g a) (g b) \ u \ u \ max (g a) (g b) \ \x\{a..b}. u = g x" apply (case_tac "g a \ g b") apply (auto simp add: min_def max_def less_imp_le) @@ -814,7 +814,7 @@ apply (rule continuous_on_subset [OF contf]) using g_im by auto then guess F .. - then have derivF: "\x. a \ x \ x \ b \ + then have derivF: "\x. a \ x \ x \ b \ (F has_vector_derivative (f (g x))) (at (g x) within (g ` {a..b}))" by auto have contf2: "continuous_on {min (g a) (g b)..max (g a) (g b)} f" apply (rule continuous_on_subset [OF contf]) @@ -842,7 +842,7 @@ lemma interval_integral_substitution_integrable: fixes f :: "real \ 'a::euclidean_space" and a b u v :: ereal - assumes "a < b" + assumes "a < b" and deriv_g: "\x. a < ereal x \ ereal x < b \ DERIV g x :> g' x" and contf: "\x. a < ereal x \ ereal x < b \ isCont f (g x)" and contg': "\x. a < ereal x \ ereal x < b \ isCont g' x" @@ -859,10 +859,10 @@ by (rule order_less_le_trans, rule approx, force) have [simp]: "\x i. x \ u i \ ereal x < b" by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx) - have [simp]: "\i. l i < b" - apply (rule order_less_trans) prefer 2 + have [simp]: "\i. l i < b" + apply (rule order_less_trans) prefer 2 by (rule approx, auto, rule approx) - have [simp]: "\i. a < u i" + have [simp]: "\i. a < u i" by (rule order_less_trans, rule approx, auto, rule approx) have [simp]: "\i j. i \ j \ l j \ l i" by (rule decseqD, rule approx) have [simp]: "\i j. i \ j \ u i \ u j" by (rule incseqD, rule approx) @@ -875,7 +875,7 @@ apply (rule less_imp_le, erule order_less_le_trans, auto) by (rule less_imp_le, rule le_less_trans, subst ereal_less_eq(3), assumption, auto) have "A \ B" and un: "einterval A B = (\i. {g(l i)<..i. g (l i)) \ A" using A apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def) by (drule_tac x = "\i. ereal (l i)" in spec, auto) @@ -891,7 +891,7 @@ apply (rule order_trans [OF _ B3 [of 0]]) by auto { fix x :: real - assume "A < x" and "x < B" + assume "A < x" and "x < B" then have "eventually (\i. ereal (g (l i)) < x \ x < ereal (g (u i))) sequentially" apply (intro eventually_conj order_tendstoD) by (rule A2, assumption, rule B2, assumption) @@ -903,7 +903,7 @@ apply (erule (1) AB) apply (rule order_le_less_trans, rule A3, simp) apply (rule order_less_le_trans) prefer 2 - by (rule B3, simp) + by (rule B3, simp) qed (* finally, the main argument *) { @@ -942,7 +942,7 @@ lemma interval_integral_substitution_nonneg: fixes f g g':: "real \ real" and a b u v :: ereal - assumes "a < b" + assumes "a < b" and deriv_g: "\x. a < ereal x \ ereal x < b \ DERIV g x :> g' x" and contf: "\x. a < ereal x \ ereal x < b \ isCont f (g x)" and contg': "\x. a < ereal x \ ereal x < b \ isCont g' x" @@ -951,7 +951,7 @@ and A: "((ereal \ g \ real_of_ereal) \ A) (at_right a)" and B: "((ereal \ g \ real_of_ereal) \ B) (at_left b)" and integrable_fg: "set_integrable lborel (einterval a b) (\x. f (g x) * g' x)" - shows + shows "set_integrable lborel (einterval A B) f" "(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))" proof - @@ -961,10 +961,10 @@ by (rule order_less_le_trans, rule approx, force) have [simp]: "\x i. x \ u i \ ereal x < b" by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx) - have [simp]: "\i. l i < b" - apply (rule order_less_trans) prefer 2 + have [simp]: "\i. l i < b" + apply (rule order_less_trans) prefer 2 by (rule approx, auto, rule approx) - have [simp]: "\i. a < u i" + have [simp]: "\i. a < u i" by (rule order_less_trans, rule approx, auto, rule approx) have [simp]: "\i j. i \ j \ l j \ l i" by (rule decseqD, rule approx) have [simp]: "\i j. i \ j \ u i \ u j" by (rule incseqD, rule approx) @@ -977,7 +977,7 @@ apply (rule less_imp_le, erule order_less_le_trans, auto) by (rule less_imp_le, rule le_less_trans, subst ereal_less_eq(3), assumption, auto) have "A \ B" and un: "einterval A B = (\i. {g(l i)<..i. g (l i)) \ A" using A apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def) by (drule_tac x = "\i. ereal (l i)" in spec, auto) @@ -993,7 +993,7 @@ apply (rule order_trans [OF _ B3 [of 0]]) by auto { fix x :: real - assume "A < x" and "x < B" + assume "A < x" and "x < B" then have "eventually (\i. ereal (g (l i)) < x \ x < ereal (g (u i))) sequentially" apply (intro eventually_conj order_tendstoD) by (rule A2, assumption, rule B2, assumption) @@ -1005,7 +1005,7 @@ apply (erule (1) AB) apply (rule order_le_less_trans, rule A3, simp) apply (rule order_less_le_trans) prefer 2 - by (rule B3, simp) + by (rule B3, simp) qed (* finally, the main argument *) { @@ -1031,7 +1031,7 @@ apply (rule g_nondec, auto) by (erule order_less_le_trans, rule g_nondec, auto) have img: "\x i. g (l i) \ x \ x \ g (u i) \ \c \ l i. c \ u i \ x = g c" - apply (frule (1) IVT' [of g], auto) + apply (frule (1) IVT' [of g], auto) apply (rule continuous_at_imp_continuous_on, auto) by (rule DERIV_isCont, rule deriv_g, auto) have nonneg_f2: "\x i. g (l i) \ x \ x \ g (u i) \ 0 \ f x" @@ -1076,11 +1076,11 @@ translations "CLBINT x:A. f" == "CONST complex_set_lebesgue_integral CONST lborel A (\x. f)" -abbreviation complex_interval_lebesgue_integral :: +abbreviation complex_interval_lebesgue_integral :: "real measure \ ereal \ ereal \ (real \ complex) \ complex" where "complex_interval_lebesgue_integral M a b f \ interval_lebesgue_integral M a b f" -abbreviation complex_interval_lebesgue_integrable :: +abbreviation complex_interval_lebesgue_integrable :: "real measure \ ereal \ ereal \ (real \ complex) \ bool" where "complex_interval_lebesgue_integrable M a b f \ interval_lebesgue_integrable M a b f" @@ -1099,14 +1099,14 @@ by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def) lemma interval_integral_norm2: - "interval_lebesgue_integrable lborel a b f \ + "interval_lebesgue_integrable lborel a b f \ norm (LBINT t=a..b. f t) \ \LBINT t=a..b. norm (f t)\" proof (induct a b rule: linorder_wlog) case (sym a b) then show ?case by (simp add: interval_integral_endpoints_reverse[of a b] interval_integrable_endpoints_reverse[of a b]) next - case (le a b) - then have "\LBINT t=a..b. norm (f t)\ = LBINT t=a..b. norm (f t)" + case (le a b) + then have "\LBINT t=a..b. norm (f t)\ = LBINT t=a..b. norm (f t)" using integrable_norm[of lborel "\x. indicator (einterval a b) x *\<^sub>R f x"] by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def intro!: integral_nonneg_AE abs_of_nonneg) diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Probability/Levy.thy --- a/src/HOL/Probability/Levy.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Probability/Levy.thy Tue Jun 21 15:10:43 2016 +0200 @@ -1,5 +1,5 @@ -(* Theory: Levy.thy - Author: Jeremy Avigad +(* Title: HOL/Probability/Levy.thy + Authors: Jeremy Avigad (CMU) *) section \The Levy inversion theorem, and the Levy continuity theorem.\ diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Probability/Measurable.thy --- a/src/HOL/Probability/Measurable.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Probability/Measurable.thy Tue Jun 21 15:10:43 2016 +0200 @@ -266,7 +266,7 @@ unfolding finite_nat_set_iff_bounded by (simp add: Ball_def) lemma measurable_Least[measurable]: - assumes [measurable]: "(\i::nat. (\x. P i x) \ measurable M (count_space UNIV))"q + assumes [measurable]: "(\i::nat. (\x. P i x) \ measurable M (count_space UNIV))" shows "(\x. LEAST i. P i x) \ measurable M (count_space UNIV)" unfolding measurable_def by (safe intro!: sets_Least) simp_all diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Probability/Measure_Space.thy --- a/src/HOL/Probability/Measure_Space.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Probability/Measure_Space.thy Tue Jun 21 15:10:43 2016 +0200 @@ -26,7 +26,7 @@ proof (rule SUP_eqI) fix y :: ennreal assume "\n. n \ UNIV \ (if i < n then f i else 0) \ y" from this[of "Suc i"] show "f i \ y" by auto - qed (insert assms, simp add: zero_le) + qed (insert assms, simp) ultimately show ?thesis using assms by (subst suminf_eq_SUP) (auto simp: indicator_def) qed @@ -325,7 +325,7 @@ by (auto simp: UN_disjointed_eq disjoint_family_disjointed) moreover have "(\n. (\i (\i. f (disjointed A i))" using f(1)[unfolded positive_def] dA - by (auto intro!: summable_LIMSEQ summableI) + by (auto intro!: summable_LIMSEQ) from LIMSEQ_Suc[OF this] have "(\n. (\i\n. f (disjointed A i))) \ (\i. f (disjointed A i))" unfolding lessThan_Suc_atMost . @@ -1395,7 +1395,7 @@ qed (auto dest: sets.sets_into_space) lemma measure_nonneg[simp]: "0 \ measure M A" - unfolding measure_def by (auto simp: enn2real_nonneg) + unfolding measure_def by auto lemma zero_less_measure_iff: "0 < measure M A \ measure M A \ 0" using measure_nonneg[of M A] by (auto simp add: le_less) @@ -1418,13 +1418,13 @@ by (cases "A \ M") (auto simp: measure_notin_sets emeasure_notin_sets) lemma enn2real_plus:"a < top \ b < top \ enn2real (a + b) = enn2real a + enn2real b" - by (simp add: enn2real_def plus_ennreal.rep_eq real_of_ereal_add enn2ereal_nonneg less_top + by (simp add: enn2real_def plus_ennreal.rep_eq real_of_ereal_add less_top del: real_of_ereal_enn2ereal) lemma measure_Union: "emeasure M A \ \ \ emeasure M B \ \ \ A \ sets M \ B \ sets M \ A \ B = {} \ measure M (A \ B) = measure M A + measure M B" - by (simp add: measure_def enn2ereal_nonneg plus_emeasure[symmetric] enn2real_plus less_top) + by (simp add: measure_def plus_emeasure[symmetric] enn2real_plus less_top) lemma disjoint_family_on_insert: "i \ I \ disjoint_family_on A (insert i I) \ A i \ (\i\I. A i) = {} \ disjoint_family_on A I" @@ -1462,8 +1462,7 @@ then have "emeasure M (A i) = ennreal ((measure M (A i)))" using finite by (intro emeasure_eq_ennreal_measure) (auto simp: top_unique) } ultimately show ?thesis using finite - by (subst (asm) (2) emeasure_eq_ennreal_measure) - (simp_all add: measure_nonneg) + by (subst (asm) (2) emeasure_eq_ennreal_measure) simp_all qed lemma measure_subadditive: @@ -1494,7 +1493,7 @@ show ?thesis using emeasure_subadditive_finite[OF A] fin unfolding emeasure_eq_ennreal_measure[OF *] - by (simp_all add: setsum_ennreal measure_nonneg setsum_nonneg emeasure_eq_ennreal_measure) + by (simp_all add: setsum_nonneg emeasure_eq_ennreal_measure) qed lemma measure_subadditive_countably: @@ -2161,185 +2160,1124 @@ lemma scale_null_measure [simp]: "scale_measure r (null_measure M) = null_measure M" by (rule measure_eqI) simp_all -subsection \Measures form a chain-complete partial order\ + +subsection \Complete lattice structure on measures\ + +lemma (in finite_measure) finite_measure_Diff': + "A \ sets M \ B \ sets M \ measure M (A - B) = measure M A - measure M (A \ B)" + using finite_measure_Diff[of A "A \ B"] by (auto simp: Diff_Int) + +lemma (in finite_measure) finite_measure_Union': + "A \ sets M \ B \ sets M \ measure M (A \ B) = measure M A + measure M (B - A)" + using finite_measure_Union[of A "B - A"] by auto + +lemma finite_unsigned_Hahn_decomposition: + assumes "finite_measure M" "finite_measure N" and [simp]: "sets N = sets M" + shows "\Y\sets M. (\X\sets M. X \ Y \ N X \ M X) \ (\X\sets M. X \ Y = {} \ M X \ N X)" +proof - + interpret M: finite_measure M by fact + interpret N: finite_measure N by fact + + define d where "d X = measure M X - measure N X" for X + + have [intro]: "bdd_above (d`sets M)" + using sets.sets_into_space[of _ M] + by (intro bdd_aboveI[where M="measure M (space M)"]) + (auto simp: d_def field_simps subset_eq intro!: add_increasing M.finite_measure_mono) + + define \ where "\ = (SUP X:sets M. d X)" + have le_\[intro]: "X \ sets M \ d X \ \" for X + by (auto simp: \_def intro!: cSUP_upper) + + have "\f. \n. f n \ sets M \ d (f n) > \ - 1 / 2^n" + proof (intro choice_iff[THEN iffD1] allI) + fix n + have "\X\sets M. \ - 1 / 2^n < d X" + unfolding \_def by (intro less_cSUP_iff[THEN iffD1]) auto + then show "\y. y \ sets M \ \ - 1 / 2 ^ n < d y" + by auto + qed + then obtain E where [measurable]: "E n \ sets M" and E: "d (E n) > \ - 1 / 2^n" for n + by auto + + define F where "F m n = (if m \ n then \i\{m..n}. E i else space M)" for m n + + have [measurable]: "m \ n \ F m n \ sets M" for m n + by (auto simp: F_def) + + have 1: "\ - 2 / 2 ^ m + 1 / 2 ^ n \ d (F m n)" if "m \ n" for m n + using that + proof (induct rule: dec_induct) + case base with E[of m] show ?case + by (simp add: F_def field_simps) + next + case (step i) + have F_Suc: "F m (Suc i) = F m i \ E (Suc i)" + using \m \ i\ by (auto simp: F_def le_Suc_eq) + + have "\ + (\ - 2 / 2^m + 1 / 2 ^ Suc i) \ (\ - 1 / 2^Suc i) + (\ - 2 / 2^m + 1 / 2^i)" + by (simp add: field_simps) + also have "\ \ d (E (Suc i)) + d (F m i)" + using E[of "Suc i"] by (intro add_mono step) auto + also have "\ = d (E (Suc i)) + d (F m i - E (Suc i)) + d (F m (Suc i))" + using \m \ i\ by (simp add: d_def field_simps F_Suc M.finite_measure_Diff' N.finite_measure_Diff') + also have "\ = d (E (Suc i) \ F m i) + d (F m (Suc i))" + using \m \ i\ by (simp add: d_def field_simps M.finite_measure_Union' N.finite_measure_Union') + also have "\ \ \ + d (F m (Suc i))" + using \m \ i\ by auto + finally show ?case + by auto + qed + + define F' where "F' m = (\i\{m..}. E i)" for m + have F'_eq: "F' m = (\i. F m (i + m))" for m + by (fastforce simp: le_iff_add[of m] F'_def F_def) + + have [measurable]: "F' m \ sets M" for m + by (auto simp: F'_def) + + have \_le: "\ - 0 \ d (\m. F' m)" + proof (rule LIMSEQ_le) + show "(\n. \ - 2 / 2 ^ n) \ \ - 0" + by (intro tendsto_intros LIMSEQ_divide_realpow_zero) auto + have "incseq F'" + by (auto simp: incseq_def F'_def) + then show "(\m. d (F' m)) \ d (\m. F' m)" + unfolding d_def + by (intro tendsto_diff M.finite_Lim_measure_incseq N.finite_Lim_measure_incseq) auto + + have "\ - 2 / 2 ^ m + 0 \ d (F' m)" for m + proof (rule LIMSEQ_le) + have *: "decseq (\n. F m (n + m))" + by (auto simp: decseq_def F_def) + show "(\n. d (F m n)) \ d (F' m)" + unfolding d_def F'_eq + by (rule LIMSEQ_offset[where k=m]) + (auto intro!: tendsto_diff M.finite_Lim_measure_decseq N.finite_Lim_measure_decseq *) + show "(\n. \ - 2 / 2 ^ m + 1 / 2 ^ n) \ \ - 2 / 2 ^ m + 0" + by (intro tendsto_add LIMSEQ_divide_realpow_zero tendsto_const) auto + show "\N. \n\N. \ - 2 / 2 ^ m + 1 / 2 ^ n \ d (F m n)" + using 1[of m] by (intro exI[of _ m]) auto + qed + then show "\N. \n\N. \ - 2 / 2 ^ n \ d (F' n)" + by auto + qed + + show ?thesis + proof (safe intro!: bexI[of _ "\m. F' m"]) + fix X assume [measurable]: "X \ sets M" and X: "X \ (\m. F' m)" + have "d (\m. F' m) - d X = d ((\m. F' m) - X)" + using X by (auto simp: d_def M.finite_measure_Diff N.finite_measure_Diff) + also have "\ \ \" + by auto + finally have "0 \ d X" + using \_le by auto + then show "emeasure N X \ emeasure M X" + by (auto simp: d_def M.emeasure_eq_measure N.emeasure_eq_measure) + next + fix X assume [measurable]: "X \ sets M" and X: "X \ (\m. F' m) = {}" + then have "d (\m. F' m) + d X = d (X \ (\m. F' m))" + by (auto simp: d_def M.finite_measure_Union N.finite_measure_Union) + also have "\ \ \" + by auto + finally have "d X \ 0" + using \_le by auto + then show "emeasure M X \ emeasure N X" + by (auto simp: d_def M.emeasure_eq_measure N.emeasure_eq_measure) + qed auto +qed + +lemma unsigned_Hahn_decomposition: + assumes [simp]: "sets N = sets M" and [measurable]: "A \ sets M" + and [simp]: "emeasure M A \ top" "emeasure N A \ top" + shows "\Y\sets M. Y \ A \ (\X\sets M. X \ Y \ N X \ M X) \ (\X\sets M. X \ A \ X \ Y = {} \ M X \ N X)" +proof - + have "\Y\sets (restrict_space M A). + (\X\sets (restrict_space M A). X \ Y \ (restrict_space N A) X \ (restrict_space M A) X) \ + (\X\sets (restrict_space M A). X \ Y = {} \ (restrict_space M A) X \ (restrict_space N A) X)" + proof (rule finite_unsigned_Hahn_decomposition) + show "finite_measure (restrict_space M A)" "finite_measure (restrict_space N A)" + by (auto simp: space_restrict_space emeasure_restrict_space less_top intro!: finite_measureI) + qed (simp add: sets_restrict_space) + then guess Y .. + then show ?thesis + apply (intro bexI[of _ Y] conjI ballI conjI) + apply (simp_all add: sets_restrict_space emeasure_restrict_space) + apply safe + subgoal for X Z + by (erule ballE[of _ _ X]) (auto simp add: Int_absorb1) + subgoal for X Z + by (erule ballE[of _ _ X]) (auto simp add: Int_absorb1 ac_simps) + apply auto + done +qed + +text \ + Define a lexicographical order on @{type measure}, in the order space, sets and measure. The parts + of the lexicographical order are point-wise ordered. +\ instantiation measure :: (type) order_bot begin -definition bot_measure :: "'a measure" where - "bot_measure = sigma {} {{}}" - -lemma space_bot[simp]: "space bot = {}" - unfolding bot_measure_def by (rule space_measure_of) auto - -lemma sets_bot[simp]: "sets bot = {{}}" - unfolding bot_measure_def by (subst sets_measure_of) auto - -lemma emeasure_bot[simp]: "emeasure bot = (\x. 0)" - unfolding bot_measure_def by (rule emeasure_sigma) - inductive less_eq_measure :: "'a measure \ 'a measure \ bool" where - "sets N = sets M \ (\A. A \ sets M \ emeasure M A \ emeasure N A) \ less_eq_measure M N" -| "less_eq_measure bot N" + "space M \ space N \ less_eq_measure M N" +| "space M = space N \ sets M \ sets N \ less_eq_measure M N" +| "space M = space N \ sets M = sets N \ emeasure M \ emeasure N \ less_eq_measure M N" + +lemma le_measure_iff: + "M \ N \ (if space M = space N then + if sets M = sets N then emeasure M \ emeasure N else sets M \ sets N else space M \ space N)" + by (auto elim: less_eq_measure.cases intro: less_eq_measure.intros) definition less_measure :: "'a measure \ 'a measure \ bool" where "less_measure M N \ (M \ N \ \ N \ M)" -instance -proof (standard, goal_cases) - case 1 then show ?case - unfolding less_measure_def .. -next - case (2 M) then show ?case - by (intro less_eq_measure.intros) auto -next - case (3 M N L) then show ?case - apply (safe elim!: less_eq_measure.cases) - apply (simp_all add: less_eq_measure.intros) - apply (rule less_eq_measure.intros) - apply simp - apply (blast intro: order_trans) [] - unfolding less_eq_measure.simps - apply (rule disjI2) - apply simp - apply (rule measure_eqI) - apply (auto intro!: antisym) - done -next - case (4 M N) then show ?case - apply (safe elim!: less_eq_measure.cases intro!: measure_eqI) - apply simp - apply simp - apply (blast intro: antisym) - apply (simp) - apply simp - done -qed (rule less_eq_measure.intros) -end - -lemma le_emeasureD: "M \ N \ emeasure M A \ emeasure N A" - by (cases "A \ sets M") (auto elim!: less_eq_measure.cases simp: emeasure_notin_sets) - -lemma le_sets: "N \ M \ sets N \ sets M" - unfolding less_eq_measure.simps by auto - -instantiation measure :: (type) ccpo -begin - -definition Sup_measure :: "'a measure set \ 'a measure" where - "Sup_measure A = measure_of (SUP a:A. space a) (SUP a:A. sets a) (SUP a:A. emeasure a)" +definition bot_measure :: "'a measure" where + "bot_measure = sigma {} {}" lemma - assumes A: "Complete_Partial_Order.chain op \ A" and a: "a \ bot" "a \ A" - shows space_Sup: "space (Sup A) = space a" - and sets_Sup: "sets (Sup A) = sets a" + shows space_bot[simp]: "space bot = {}" + and sets_bot[simp]: "sets bot = {{}}" + and emeasure_bot[simp]: "emeasure bot X = 0" + by (auto simp: bot_measure_def sigma_sets_empty_eq emeasure_sigma) + +instance +proof standard + show "bot \ a" for a :: "'a measure" + by (simp add: le_measure_iff bot_measure_def sigma_sets_empty_eq emeasure_sigma le_fun_def) +qed (auto simp: le_measure_iff less_measure_def split: if_split_asm intro: measure_eqI) + +end + +lemma le_measure: "sets M = sets N \ M \ N \ (\A\sets M. emeasure M A \ emeasure N A)" + apply (auto simp: le_measure_iff le_fun_def dest: sets_eq_imp_space_eq) + subgoal for X + by (cases "X \ sets M") (auto simp: emeasure_notin_sets) + done + +definition sup_measure' :: "'a measure \ 'a measure \ 'a measure" +where + "sup_measure' A B = measure_of (space A) (sets A) (\X. SUP Y:sets A. emeasure A (X \ Y) + emeasure B (X \ - Y))" + +lemma assumes [simp]: "sets B = sets A" + shows space_sup_measure'[simp]: "space (sup_measure' A B) = space A" + and sets_sup_measure'[simp]: "sets (sup_measure' A B) = sets A" + using sets_eq_imp_space_eq[OF assms] by (simp_all add: sup_measure'_def) + +lemma emeasure_sup_measure': + assumes sets_eq[simp]: "sets B = sets A" and [simp, intro]: "X \ sets A" + shows "emeasure (sup_measure' A B) X = (SUP Y:sets A. emeasure A (X \ Y) + emeasure B (X \ - Y))" + (is "_ = ?S X") proof - - have sets: "(SUP a:A. sets a) = sets a" - proof (intro antisym SUP_least) - fix a' show "a' \ A \ sets a' \ sets a" - using a chainD[OF A, of a a'] by (auto elim!: less_eq_measure.cases) - qed (insert \a\A\, auto) - have space: "(SUP a:A. space a) = space a" - proof (intro antisym SUP_least) - fix a' show "a' \ A \ space a' \ space a" - using a chainD[OF A, of a a'] by (intro sets_le_imp_space_le) (auto elim!: less_eq_measure.cases) - qed (insert \a\A\, auto) - show "space (Sup A) = space a" - unfolding Sup_measure_def sets space sets.space_measure_of_eq .. - show "sets (Sup A) = sets a" - unfolding Sup_measure_def sets space sets.sets_measure_of_eq .. + note sets_eq_imp_space_eq[OF sets_eq, simp] + show ?thesis + using sup_measure'_def + proof (rule emeasure_measure_of) + let ?d = "\X Y. emeasure A (X \ Y) + emeasure B (X \ - Y)" + show "countably_additive (sets (sup_measure' A B)) (\X. SUP Y : sets A. emeasure A (X \ Y) + emeasure B (X \ - Y))" + proof (rule countably_additiveI, goal_cases) + case (1 X) + then have [measurable]: "\i. X i \ sets A" and "disjoint_family X" + by auto + have "(\i. ?S (X i)) = (SUP Y:sets A. \i. ?d (X i) Y)" + proof (rule ennreal_suminf_SUP_eq_directed) + fix J :: "nat set" and a b assume "finite J" and [measurable]: "a \ sets A" "b \ sets A" + have "\c\sets A. c \ X i \ (\a\sets A. ?d (X i) a \ ?d (X i) c)" for i + proof cases + assume "emeasure A (X i) = top \ emeasure B (X i) = top" + then show ?thesis + proof + assume "emeasure A (X i) = top" then show ?thesis + by (intro bexI[of _ "X i"]) auto + next + assume "emeasure B (X i) = top" then show ?thesis + by (intro bexI[of _ "{}"]) auto + qed + next + assume finite: "\ (emeasure A (X i) = top \ emeasure B (X i) = top)" + then have "\Y\sets A. Y \ X i \ (\C\sets A. C \ Y \ B C \ A C) \ (\C\sets A. C \ X i \ C \ Y = {} \ A C \ B C)" + using unsigned_Hahn_decomposition[of B A "X i"] by simp + then obtain Y where [measurable]: "Y \ sets A" and [simp]: "Y \ X i" + and B_le_A: "\C. C \ sets A \ C \ Y \ B C \ A C" + and A_le_B: "\C. C \ sets A \ C \ X i \ C \ Y = {} \ A C \ B C" + by auto + + show ?thesis + proof (intro bexI[of _ Y] ballI conjI) + fix a assume [measurable]: "a \ sets A" + have *: "(X i \ a \ Y \ (X i \ a - Y)) = X i \ a" "(X i - a) \ Y \ (X i - a - Y) = X i \ - a" + for a Y by auto + then have "?d (X i) a = + (A (X i \ a \ Y) + A (X i \ a \ - Y)) + (B (X i \ - a \ Y) + B (X i \ - a \ - Y))" + by (subst (1 2) plus_emeasure) (auto simp: Diff_eq[symmetric]) + also have "\ \ (A (X i \ a \ Y) + B (X i \ a \ - Y)) + (A (X i \ - a \ Y) + B (X i \ - a \ - Y))" + by (intro add_mono order_refl B_le_A A_le_B) (auto simp: Diff_eq[symmetric]) + also have "\ \ (A (X i \ Y \ a) + A (X i \ Y \ - a)) + (B (X i \ - Y \ a) + B (X i \ - Y \ - a))" + by (simp add: ac_simps) + also have "\ \ A (X i \ Y) + B (X i \ - Y)" + by (subst (1 2) plus_emeasure) (auto simp: Diff_eq[symmetric] *) + finally show "?d (X i) a \ ?d (X i) Y" . + qed auto + qed + then obtain C where [measurable]: "C i \ sets A" and "C i \ X i" + and C: "\a. a \ sets A \ ?d (X i) a \ ?d (X i) (C i)" for i + by metis + have *: "X i \ (\i. C i) = X i \ C i" for i + proof safe + fix x j assume "x \ X i" "x \ C j" + moreover have "i = j \ X i \ X j = {}" + using \disjoint_family X\ by (auto simp: disjoint_family_on_def) + ultimately show "x \ C i" + using \C i \ X i\ \C j \ X j\ by auto + qed auto + have **: "X i \ - (\i. C i) = X i \ - C i" for i + proof safe + fix x j assume "x \ X i" "x \ C i" "x \ C j" + moreover have "i = j \ X i \ X j = {}" + using \disjoint_family X\ by (auto simp: disjoint_family_on_def) + ultimately show False + using \C i \ X i\ \C j \ X j\ by auto + qed auto + show "\c\sets A. \i\J. ?d (X i) a \ ?d (X i) c \ ?d (X i) b \ ?d (X i) c" + apply (intro bexI[of _ "\i. C i"]) + unfolding * ** + apply (intro C ballI conjI) + apply auto + done + qed + also have "\ = ?S (\i. X i)" + unfolding UN_extend_simps(4) + by (auto simp add: suminf_add[symmetric] Diff_eq[symmetric] simp del: UN_simps + intro!: SUP_cong arg_cong2[where f="op +"] suminf_emeasure + disjoint_family_on_bisimulation[OF \disjoint_family X\]) + finally show "(\i. ?S (X i)) = ?S (\i. X i)" . + qed + qed (auto dest: sets.sets_into_space simp: positive_def intro!: SUP_const) qed -lemma emeasure_Sup: - assumes A: "Complete_Partial_Order.chain op \ A" "A \ {}" - assumes "X \ sets (Sup A)" - shows "emeasure (Sup A) X = (SUP a:A. emeasure a) X" -proof (rule emeasure_measure_of[OF Sup_measure_def]) - show "countably_additive (sets (Sup A)) (SUP a:A. emeasure a)" - unfolding countably_additive_def - proof safe - fix F :: "nat \ 'a set" assume F: "range F \ sets (Sup A)" "disjoint_family F" - show "(\i. (SUP a:A. emeasure a) (F i)) = SUPREMUM A emeasure (UNION UNIV F)" - unfolding SUP_apply +lemma le_emeasure_sup_measure'1: + assumes "sets B = sets A" "X \ sets A" shows "emeasure A X \ emeasure (sup_measure' A B) X" + by (subst emeasure_sup_measure'[OF assms]) (auto intro!: SUP_upper2[of "X"] assms) + +lemma le_emeasure_sup_measure'2: + assumes "sets B = sets A" "X \ sets A" shows "emeasure B X \ emeasure (sup_measure' A B) X" + by (subst emeasure_sup_measure'[OF assms]) (auto intro!: SUP_upper2[of "{}"] assms) + +lemma emeasure_sup_measure'_le2: + assumes [simp]: "sets B = sets C" "sets A = sets C" and [measurable]: "X \ sets C" + assumes A: "\Y. Y \ X \ Y \ sets A \ emeasure A Y \ emeasure C Y" + assumes B: "\Y. Y \ X \ Y \ sets A \ emeasure B Y \ emeasure C Y" + shows "emeasure (sup_measure' A B) X \ emeasure C X" +proof (subst emeasure_sup_measure') + show "(SUP Y:sets A. emeasure A (X \ Y) + emeasure B (X \ - Y)) \ emeasure C X" + unfolding \sets A = sets C\ + proof (intro SUP_least) + fix Y assume [measurable]: "Y \ sets C" + have [simp]: "X \ Y \ (X - Y) = X" + by auto + have "emeasure A (X \ Y) + emeasure B (X \ - Y) \ emeasure C (X \ Y) + emeasure C (X \ - Y)" + by (intro add_mono A B) (auto simp: Diff_eq[symmetric]) + also have "\ = emeasure C X" + by (subst plus_emeasure) (auto simp: Diff_eq[symmetric]) + finally show "emeasure A (X \ Y) + emeasure B (X \ - Y) \ emeasure C X" . + qed +qed simp_all + +definition sup_lexord :: "'a \ 'a \ ('a \ 'b::order) \ 'a \ 'a \ 'a" +where + "sup_lexord A B k s c = + (if k A = k B then c else if \ k A \ k B \ \ k B \ k A then s else if k B \ k A then A else B)" + +lemma sup_lexord: + "(k A < k B \ P B) \ (k B < k A \ P A) \ (k A = k B \ P c) \ + (\ k B \ k A \ \ k A \ k B \ P s) \ P (sup_lexord A B k s c)" + by (auto simp: sup_lexord_def) + +lemmas le_sup_lexord = sup_lexord[where P="\a. c \ a" for c] + +lemma sup_lexord1: "k A = k B \ sup_lexord A B k s c = c" + by (simp add: sup_lexord_def) + +lemma sup_lexord_commute: "sup_lexord A B k s c = sup_lexord B A k s c" + by (auto simp: sup_lexord_def) + +lemma sigma_sets_le_sets_iff: "(sigma_sets (space x) \ \ sets x) = (\ \ sets x)" + using sets.sigma_sets_subset[of \ x] by auto + +lemma sigma_le_iff: "\ \ Pow \ \ sigma \ \ \ x \ (\ \ space x \ (space x = \ \ \ \ sets x))" + by (cases "\ = space x") + (simp_all add: eq_commute[of _ "sets x"] le_measure_iff emeasure_sigma le_fun_def + sigma_sets_superset_generator sigma_sets_le_sets_iff) + +instantiation measure :: (type) semilattice_sup +begin + +definition sup_measure :: "'a measure \ 'a measure \ 'a measure" +where + "sup_measure A B = + sup_lexord A B space (sigma (space A \ space B) {}) + (sup_lexord A B sets (sigma (space A) (sets A \ sets B)) (sup_measure' A B))" + +instance +proof + fix x y z :: "'a measure" + show "x \ sup x y" + unfolding sup_measure_def + proof (intro le_sup_lexord) + assume "space x = space y" + then have *: "sets x \ sets y \ Pow (space x)" + using sets.space_closed by auto + assume "\ sets y \ sets x" "\ sets x \ sets y" + then have "sets x \ sets x \ sets y" + by auto + also have "\ \ sigma (space x) (sets x \ sets y)" + by (subst sets_measure_of[OF *]) (rule sigma_sets_superset_generator) + finally show "x \ sigma (space x) (sets x \ sets y)" + by (simp add: space_measure_of[OF *] less_eq_measure.intros(2)) + next + assume "\ space y \ space x" "\ space x \ space y" + then show "x \ sigma (space x \ space y) {}" + by (intro less_eq_measure.intros) auto + next + assume "sets x = sets y" then show "x \ sup_measure' x y" + by (simp add: le_measure le_emeasure_sup_measure'1) + qed (auto intro: less_eq_measure.intros) + show "y \ sup x y" + unfolding sup_measure_def + proof (intro le_sup_lexord) + assume **: "space x = space y" + then have *: "sets x \ sets y \ Pow (space y)" + using sets.space_closed by auto + assume "\ sets y \ sets x" "\ sets x \ sets y" + then have "sets y \ sets x \ sets y" + by auto + also have "\ \ sigma (space y) (sets x \ sets y)" + by (subst sets_measure_of[OF *]) (rule sigma_sets_superset_generator) + finally show "y \ sigma (space x) (sets x \ sets y)" + by (simp add: ** space_measure_of[OF *] less_eq_measure.intros(2)) + next + assume "\ space y \ space x" "\ space x \ space y" + then show "y \ sigma (space x \ space y) {}" + by (intro less_eq_measure.intros) auto + next + assume "sets x = sets y" then show "y \ sup_measure' x y" + by (simp add: le_measure le_emeasure_sup_measure'2) + qed (auto intro: less_eq_measure.intros) + show "x \ y \ z \ y \ sup x z \ y" + unfolding sup_measure_def + proof (intro sup_lexord[where P="\x. x \ y"]) + assume "x \ y" "z \ y" and [simp]: "space x = space z" "sets x = sets z" + from \x \ y\ show "sup_measure' x z \ y" + proof cases + case 1 then show ?thesis + by (intro less_eq_measure.intros(1)) simp + next + case 2 then show ?thesis + by (intro less_eq_measure.intros(2)) simp_all + next + case 3 with \z \ y\ \x \ y\ show ?thesis + by (auto simp add: le_measure intro!: emeasure_sup_measure'_le2) + qed + next + assume **: "x \ y" "z \ y" "space x = space z" "\ sets z \ sets x" "\ sets x \ sets z" + then have *: "sets x \ sets z \ Pow (space x)" + using sets.space_closed by auto + show "sigma (space x) (sets x \ sets z) \ y" + unfolding sigma_le_iff[OF *] using ** by (auto simp: le_measure_iff split: if_split_asm) + next + assume "x \ y" "z \ y" "\ space z \ space x" "\ space x \ space z" + then have "space x \ space y" "space z \ space y" + by (auto simp: le_measure_iff split: if_split_asm) + then show "sigma (space x \ space z) {} \ y" + by (simp add: sigma_le_iff) + qed +qed + +end + +lemma space_empty_eq_bot: "space a = {} \ a = bot" + using space_empty[of a] by (auto intro!: measure_eqI) + +interpretation sup_measure: comm_monoid_set sup "bot :: 'a measure" + proof qed (auto intro!: antisym) + +lemma sup_measure_F_mono': + "finite J \ finite I \ sup_measure.F id I \ sup_measure.F id (I \ J)" +proof (induction J rule: finite_induct) + case empty then show ?case + by simp +next + case (insert i J) + show ?case + proof cases + assume "i \ I" with insert show ?thesis + by (auto simp: insert_absorb) + next + assume "i \ I" + have "sup_measure.F id I \ sup_measure.F id (I \ J)" + by (intro insert) + also have "\ \ sup_measure.F id (insert i (I \ J))" + using insert \i \ I\ by (subst sup_measure.insert) auto + finally show ?thesis + by auto + qed +qed + +lemma sup_measure_F_mono: "finite I \ J \ I \ sup_measure.F id J \ sup_measure.F id I" + using sup_measure_F_mono'[of I J] by (auto simp: finite_subset Un_absorb1) + +lemma sets_eq_iff_bounded: "A \ B \ B \ C \ sets A = sets C \ sets B = sets A" + by (auto dest: sets_eq_imp_space_eq simp add: le_measure_iff split: if_split_asm) + +lemma sets_sup: "sets A = sets M \ sets B = sets M \ sets (sup A B) = sets M" + by (auto simp add: sup_measure_def sup_lexord_def dest: sets_eq_imp_space_eq) + +lemma sets_sup_measure_F: + "finite I \ I \ {} \ (\i. i \ I \ sets i = sets M) \ sets (sup_measure.F id I) = sets M" + by (induction I rule: finite_ne_induct) (simp_all add: sets_sup) + +lemma le_measureD1: "A \ B \ space A \ space B" + by (auto simp: le_measure_iff split: if_split_asm) + +lemma le_measureD2: "A \ B \ space A = space B \ sets A \ sets B" + by (auto simp: le_measure_iff split: if_split_asm) + +lemma le_measureD3: "A \ B \ sets A = sets B \ emeasure A X \ emeasure B X" + by (auto simp: le_measure_iff le_fun_def dest: sets_eq_imp_space_eq split: if_split_asm) + +definition Sup_measure' :: "'a measure set \ 'a measure" +where + "Sup_measure' M = measure_of (\a\M. space a) (\a\M. sets a) + (\X. (SUP P:{P. finite P \ P \ M }. sup_measure.F id P X))" + +lemma UN_space_closed: "UNION S sets \ Pow (UNION S space)" + using sets.space_closed by auto + +lemma space_Sup_measure'2: "space (Sup_measure' M) = (\m\M. space m)" + unfolding Sup_measure'_def by (intro space_measure_of[OF UN_space_closed]) + +lemma sets_Sup_measure'2: "sets (Sup_measure' M) = sigma_sets (\m\M. space m) (\m\M. sets m)" + unfolding Sup_measure'_def by (intro sets_measure_of[OF UN_space_closed]) + +lemma sets_Sup_measure': + assumes sets_eq[simp]: "\m. m \ M \ sets m = sets A" and "M \ {}" + shows "sets (Sup_measure' M) = sets A" + using sets_eq[THEN sets_eq_imp_space_eq, simp] \M \ {}\ by (simp add: Sup_measure'_def) + +lemma space_Sup_measure': + assumes sets_eq[simp]: "\m. m \ M \ sets m = sets A" and "M \ {}" + shows "space (Sup_measure' M) = space A" + using sets_eq[THEN sets_eq_imp_space_eq, simp] \M \ {}\ + by (simp add: Sup_measure'_def ) + +lemma emeasure_Sup_measure': + assumes sets_eq[simp]: "\m. m \ M \ sets m = sets A" and "X \ sets A" "M \ {}" + shows "emeasure (Sup_measure' M) X = (SUP P:{P. finite P \ P \ M}. sup_measure.F id P X)" + (is "_ = ?S X") + using Sup_measure'_def +proof (rule emeasure_measure_of) + note sets_eq[THEN sets_eq_imp_space_eq, simp] + have *: "sets (Sup_measure' M) = sets A" "space (Sup_measure' M) = space A" + using \M \ {}\ by (simp_all add: Sup_measure'_def) + let ?\ = "sup_measure.F id" + show "countably_additive (sets (Sup_measure' M)) ?S" + proof (rule countably_additiveI, goal_cases) + case (1 F) + then have **: "range F \ sets A" + by (auto simp: *) + show "(\i. ?S (F i)) = ?S (\i. F i)" proof (subst ennreal_suminf_SUP_eq_directed) - fix N i j assume "i \ A" "j \ A" - with A(1) - show "\k\A. \n\N. emeasure i (F n) \ emeasure k (F n) \ emeasure j (F n) \ emeasure k (F n)" - by (blast elim: chainE dest: le_emeasureD) + fix i j and N :: "nat set" assume ij: "i \ {P. finite P \ P \ M}" "j \ {P. finite P \ P \ M}" + have "(i \ {} \ sets (?\ i) = sets A) \ (j \ {} \ sets (?\ j) = sets A) \ + (i \ {} \ j \ {} \ sets (?\ (i \ j)) = sets A)" + using ij by (intro impI sets_sup_measure_F conjI) auto + then have "?\ j (F n) \ ?\ (i \ j) (F n) \ ?\ i (F n) \ ?\ (i \ j) (F n)" for n + using ij + by (cases "i = {}"; cases "j = {}") + (auto intro!: le_measureD3 sup_measure_F_mono simp: sets_sup_measure_F + simp del: id_apply) + with ij show "\k\{P. finite P \ P \ M}. \n\N. ?\ i (F n) \ ?\ k (F n) \ ?\ j (F n) \ ?\ k (F n)" + by (safe intro!: bexI[of _ "i \ j"]) auto next - show "(SUP n:A. \i. emeasure n (F i)) = (SUP y:A. emeasure y (UNION UNIV F))" + show "(SUP P : {P. finite P \ P \ M}. \n. ?\ P (F n)) = (SUP P : {P. finite P \ P \ M}. ?\ P (UNION UNIV F))" proof (intro SUP_cong refl) - fix a assume "a \ A" then show "(\i. emeasure a (F i)) = emeasure a (UNION UNIV F)" - using sets_Sup[OF A(1), of a] F by (cases "a = bot") (auto simp: suminf_emeasure) + fix i assume i: "i \ {P. finite P \ P \ M}" + show "(\n. ?\ i (F n)) = ?\ i (UNION UNIV F)" + proof cases + assume "i \ {}" with i ** show ?thesis + apply (intro suminf_emeasure \disjoint_family F\) + apply (subst sets_sup_measure_F[OF _ _ sets_eq]) + apply auto + done + qed simp qed qed qed -qed (insert \A \ {}\ \X \ sets (Sup A)\, auto simp: positive_def dest: sets.sets_into_space intro: SUP_upper2) + show "positive (sets (Sup_measure' M)) ?S" + by (auto simp: positive_def bot_ennreal[symmetric]) + show "X \ sets (Sup_measure' M)" + using assms * by auto +qed (rule UN_space_closed) + +definition Sup_lexord :: "('a \ 'b::complete_lattice) \ ('a set \ 'a) \ ('a set \ 'a) \ 'a set \ 'a" +where + "Sup_lexord k c s A = (let U = (SUP a:A. k a) in if \a\A. k a = U then c {a\A. k a = U} else s A)" + +lemma Sup_lexord: + "(\a S. a \ A \ k a = (SUP a:A. k a) \ S = {a'\A. k a' = k a} \ P (c S)) \ ((\a. a \ A \ k a \ (SUP a:A. k a)) \ P (s A)) \ + P (Sup_lexord k c s A)" + by (auto simp: Sup_lexord_def Let_def) + +lemma Sup_lexord1: + assumes A: "A \ {}" "(\a. a \ A \ k a = (\a\A. k a))" "P (c A)" + shows "P (Sup_lexord k c s A)" + unfolding Sup_lexord_def Let_def +proof (clarsimp, safe) + show "\a\A. k a \ (\x\A. k x) \ P (s A)" + by (metis assms(1,2) ex_in_conv) +next + fix a assume "a \ A" "k a = (\x\A. k x)" + then have "{a \ A. k a = (\x\A. k x)} = {a \ A. k a = k a}" + by (metis A(2)[symmetric]) + then show "P (c {a \ A. k a = (\x\A. k x)})" + by (simp add: A(3)) +qed + +instantiation measure :: (type) complete_lattice +begin + +definition Sup_measure :: "'a measure set \ 'a measure" +where + "Sup_measure = Sup_lexord space (Sup_lexord sets Sup_measure' + (\U. sigma (\u\U. space u) (\u\U. sets u))) (\U. sigma (\u\U. space u) {})" + +definition Inf_measure :: "'a measure set \ 'a measure" +where + "Inf_measure A = Sup {x. \a\A. x \ a}" + +definition inf_measure :: "'a measure \ 'a measure \ 'a measure" +where + "inf_measure a b = Inf {a, b}" + +definition top_measure :: "'a measure" +where + "top_measure = Inf {}" instance proof - fix A and x :: "'a measure" assume A: "Complete_Partial_Order.chain op \ A" and x: "x \ A" - show "x \ Sup A" - proof cases - assume "x \ bot" - show ?thesis - proof - show "sets (Sup A) = sets x" - using A \x \ bot\ x by (rule sets_Sup) - with x show "\a. a \ sets x \ emeasure x a \ emeasure (Sup A) a" - by (subst emeasure_Sup[OF A]) (auto intro: SUP_upper) + note UN_space_closed [simp] + show upper: "x \ Sup A" if x: "x \ A" for x :: "'a measure" and A + unfolding Sup_measure_def + proof (intro Sup_lexord[where P="\y. x \ y"]) + assume "\a. a \ A \ space a \ (\a\A. space a)" + from this[OF \x \ A\] \x \ A\ show "x \ sigma (\a\A. space a) {}" + by (intro less_eq_measure.intros) auto + next + fix a S assume "a \ A" and a: "space a = (\a\A. space a)" and S: "S = {a' \ A. space a' = space a}" + and neq: "\aa. aa \ S \ sets aa \ (\a\S. sets a)" + have sp_a: "space a = (UNION S space)" + using \a\A\ by (auto simp: S) + show "x \ sigma (UNION S space) (UNION S sets)" + proof cases + assume [simp]: "space x = space a" + have "sets x \ (\a\S. sets a)" + using \x\A\ neq[of x] by (auto simp: S) + also have "\ \ sigma_sets (\x\S. space x) (\x\S. sets x)" + by (rule sigma_sets_superset_generator) + finally show ?thesis + by (intro less_eq_measure.intros(2)) (simp_all add: sp_a) + next + assume "space x \ space a" + moreover have "space x \ space a" + unfolding a using \x\A\ by auto + ultimately show ?thesis + by (intro less_eq_measure.intros) (simp add: less_le sp_a) qed - qed simp -next - fix A and x :: "'a measure" assume A: "Complete_Partial_Order.chain op \ A" and x: "\z. z \ A \ z \ x" - consider "A = {}" | "A = {bot}" | x where "x\A" "x \ bot" - by blast - then show "Sup A \ x" - proof cases - assume "A = {}" - moreover have "Sup ({}::'a measure set) = bot" - by (auto simp add: Sup_measure_def sigma_sets_empty_eq intro!: measure_eqI) - ultimately show ?thesis - by simp next - assume "A = {bot}" - moreover have "Sup ({bot}::'a measure set) = bot" - by (auto simp add: Sup_measure_def sigma_sets_empty_eq intro!: measure_eqI) - ultimately show ?thesis - by simp + fix a b S S' assume "a \ A" and a: "space a = (\a\A. space a)" and S: "S = {a' \ A. space a' = space a}" + and "b \ S" and b: "sets b = (\a\S. sets a)" and S': "S' = {a' \ S. sets a' = sets b}" + then have "S' \ {}" "space b = space a" + by auto + have sets_eq: "\x. x \ S' \ sets x = sets b" + by (auto simp: S') + note sets_eq[THEN sets_eq_imp_space_eq, simp] + have *: "sets (Sup_measure' S') = sets b" "space (Sup_measure' S') = space b" + using \S' \ {}\ by (simp_all add: Sup_measure'_def sets_eq) + show "x \ Sup_measure' S'" + proof cases + assume "x \ S" + with \b \ S\ have "space x = space b" + by (simp add: S) + show ?thesis + proof cases + assume "x \ S'" + show "x \ Sup_measure' S'" + proof (intro le_measure[THEN iffD2] ballI) + show "sets x = sets (Sup_measure' S')" + using \x\S'\ * by (simp add: S') + fix X assume "X \ sets x" + show "emeasure x X \ emeasure (Sup_measure' S') X" + proof (subst emeasure_Sup_measure'[OF _ \X \ sets x\]) + show "emeasure x X \ (SUP P : {P. finite P \ P \ S'}. emeasure (sup_measure.F id P) X)" + using \x\S'\ by (intro SUP_upper2[where i="{x}"]) auto + qed (insert \x\S'\ S', auto) + qed + next + assume "x \ S'" + then have "sets x \ sets b" + using \x\S\ by (auto simp: S') + moreover have "sets x \ sets b" + using \x\S\ unfolding b by auto + ultimately show ?thesis + using * \x \ S\ + by (intro less_eq_measure.intros(2)) + (simp_all add: * \space x = space b\ less_le) + qed + next + assume "x \ S" + with \x\A\ \x \ S\ \space b = space a\ show ?thesis + by (intro less_eq_measure.intros) + (simp_all add: * less_le a SUP_upper S) + qed + qed + show least: "Sup A \ x" if x: "\z. z \ A \ z \ x" for x :: "'a measure" and A + unfolding Sup_measure_def + proof (intro Sup_lexord[where P="\y. y \ x"]) + assume "\a. a \ A \ space a \ (\a\A. space a)" + show "sigma (UNION A space) {} \ x" + using x[THEN le_measureD1] by (subst sigma_le_iff) auto next - fix a assume "a \ A" "a \ bot" - then have "a \ x" "x \ bot" "a \ bot" - using x[OF \a \ A\] by (auto simp: bot_unique) - then have "sets x = sets a" - by (auto elim: less_eq_measure.cases) - - show "Sup A \ x" - proof (rule less_eq_measure.intros) - show "sets x = sets (Sup A)" - by (subst sets_Sup[OF A \a \ bot\ \a \ A\]) fact + fix a S assume "a \ A" "space a = (\a\A. space a)" and S: "S = {a' \ A. space a' = space a}" + "\a. a \ S \ sets a \ (\a\S. sets a)" + have "UNION S space \ space x" + using S le_measureD1[OF x] by auto + moreover + have "UNION S space = space a" + using \a\A\ S by auto + then have "space x = UNION S space \ UNION S sets \ sets x" + using \a \ A\ le_measureD2[OF x] by (auto simp: S) + ultimately show "sigma (UNION S space) (UNION S sets) \ x" + by (subst sigma_le_iff) simp_all + next + fix a b S S' assume "a \ A" and a: "space a = (\a\A. space a)" and S: "S = {a' \ A. space a' = space a}" + and "b \ S" and b: "sets b = (\a\S. sets a)" and S': "S' = {a' \ S. sets a' = sets b}" + then have "S' \ {}" "space b = space a" + by auto + have sets_eq: "\x. x \ S' \ sets x = sets b" + by (auto simp: S') + note sets_eq[THEN sets_eq_imp_space_eq, simp] + have *: "sets (Sup_measure' S') = sets b" "space (Sup_measure' S') = space b" + using \S' \ {}\ by (simp_all add: Sup_measure'_def sets_eq) + show "Sup_measure' S' \ x" + proof cases + assume "space x = space a" + show ?thesis + proof cases + assume **: "sets x = sets b" + show ?thesis + proof (intro le_measure[THEN iffD2] ballI) + show ***: "sets (Sup_measure' S') = sets x" + by (simp add: * **) + fix X assume "X \ sets (Sup_measure' S')" + show "emeasure (Sup_measure' S') X \ emeasure x X" + unfolding *** + proof (subst emeasure_Sup_measure'[OF _ \X \ sets (Sup_measure' S')\]) + show "(SUP P : {P. finite P \ P \ S'}. emeasure (sup_measure.F id P) X) \ emeasure x X" + proof (safe intro!: SUP_least) + fix P assume P: "finite P" "P \ S'" + show "emeasure (sup_measure.F id P) X \ emeasure x X" + proof cases + assume "P = {}" then show ?thesis + by auto + next + assume "P \ {}" + from P have "finite P" "P \ A" + unfolding S' S by (simp_all add: subset_eq) + then have "sup_measure.F id P \ x" + by (induction P) (auto simp: x) + moreover have "sets (sup_measure.F id P) = sets x" + using \finite P\ \P \ {}\ \P \ S'\ \sets x = sets b\ + by (intro sets_sup_measure_F) (auto simp: S') + ultimately show "emeasure (sup_measure.F id P) X \ emeasure x X" + by (rule le_measureD3) + qed + qed + show "m \ S' \ sets m = sets (Sup_measure' S')" for m + unfolding * by (simp add: S') + qed fact + qed + next + assume "sets x \ sets b" + moreover have "sets b \ sets x" + unfolding b S using x[THEN le_measureD2] \space x = space a\ by auto + ultimately show "Sup_measure' S' \ x" + using \space x = space a\ \b \ S\ + by (intro less_eq_measure.intros(2)) (simp_all add: * S) + qed next - fix X assume "X \ sets (Sup A)" - then have "emeasure (Sup A) X \ (SUP a:A. emeasure a X)" - using \a\A\ by (subst emeasure_Sup[OF A _]) auto - also have "\ \ emeasure x X" - by (intro SUP_least le_emeasureD x) - finally show "emeasure (Sup A) X \ emeasure x X" . + assume "space x \ space a" + then have "space a < space x" + using le_measureD1[OF x[OF \a\A\]] by auto + then show "Sup_measure' S' \ x" + by (intro less_eq_measure.intros) (simp add: * \space b = space a\) qed qed + show "Sup {} = (bot::'a measure)" "Inf {} = (top::'a measure)" + by (auto intro!: antisym least simp: top_measure_def) + show lower: "x \ A \ Inf A \ x" for x :: "'a measure" and A + unfolding Inf_measure_def by (intro least) auto + show greatest: "(\z. z \ A \ x \ z) \ x \ Inf A" for x :: "'a measure" and A + unfolding Inf_measure_def by (intro upper) auto + show "inf x y \ x" "inf x y \ y" "x \ y \ x \ z \ x \ inf y z" for x y z :: "'a measure" + by (auto simp: inf_measure_def intro!: lower greatest) qed + end -lemma - assumes A: "Complete_Partial_Order.chain op \ (f ` A)" and a: "a \ A" "f a \ bot" - shows space_SUP: "space (SUP M:A. f M) = space (f a)" - and sets_SUP: "sets (SUP M:A. f M) = sets (f a)" -by(rule space_Sup[OF A a(2) imageI[OF a(1)]] sets_Sup[OF A a(2) imageI[OF a(1)]])+ +lemma sets_SUP: + assumes "\x. x \ I \ sets (M x) = sets N" + shows "I \ {} \ sets (SUP i:I. M i) = sets N" + unfolding Sup_measure_def + using assms assms[THEN sets_eq_imp_space_eq] + sets_Sup_measure'[where A=N and M="M`I"] + by (intro Sup_lexord1[where P="\x. sets x = sets N"]) auto lemma emeasure_SUP: - assumes A: "Complete_Partial_Order.chain op \ (f ` A)" "A \ {}" - assumes "X \ sets (SUP M:A. f M)" - shows "emeasure (SUP M:A. f M) X = (SUP M:A. emeasure (f M)) X" -using \X \ _\ by(subst emeasure_Sup[OF A(1)]; simp add: A) + assumes sets: "\i. i \ I \ sets (M i) = sets N" "X \ sets N" "I \ {}" + shows "emeasure (SUP i:I. M i) X = (SUP J:{J. J \ {} \ finite J \ J \ I}. emeasure (SUP i:J. M i) X)" +proof - + have eq: "finite J \ sup_measure.F id J = (SUP i:J. i)" for J :: "'b measure set" + by (induction J rule: finite_induct) auto + have 1: "J \ {} \ J \ I \ sets (SUP x:J. M x) = sets N" for J + by (intro sets_SUP sets) (auto ) + + from \I \ {}\ obtain i where "i\I" by auto + have "Sup_measure' (M`I) X = (SUP P:{P. finite P \ P \ M`I}. sup_measure.F id P X)" + using sets by (intro emeasure_Sup_measure') auto + also have "Sup_measure' (M`I) = (SUP i:I. M i)" + unfolding Sup_measure_def using \I \ {}\ sets sets(1)[THEN sets_eq_imp_space_eq] + by (intro Sup_lexord1[where P="\x. _ = x"]) auto + also have "(SUP P:{P. finite P \ P \ M`I}. sup_measure.F id P X) = + (SUP J:{J. J \ {} \ finite J \ J \ I}. (SUP i:J. M i) X)" + proof (intro SUP_eq) + fix J assume "J \ {P. finite P \ P \ M`I}" + then obtain J' where J': "J' \ I" "finite J'" and J: "J = M`J'" and "finite J" + using finite_subset_image[of J M I] by auto + show "\j\{J. J \ {} \ finite J \ J \ I}. sup_measure.F id J X \ (SUP i:j. M i) X" + proof cases + assume "J' = {}" with \i \ I\ show ?thesis + by (auto simp add: J) + next + assume "J' \ {}" with J J' show ?thesis + by (intro bexI[of _ "J'"]) (auto simp add: eq simp del: id_apply) + qed + next + fix J assume J: "J \ {P. P \ {} \ finite P \ P \ I}" + show "\J'\{J. finite J \ J \ M`I}. (SUP i:J. M i) X \ sup_measure.F id J' X" + using J by (intro bexI[of _ "M`J"]) (auto simp add: eq simp del: id_apply) + qed + finally show ?thesis . +qed + +lemma emeasure_SUP_chain: + assumes sets: "\i. i \ A \ sets (M i) = sets N" "X \ sets N" + assumes ch: "Complete_Partial_Order.chain op \ (M ` A)" and "A \ {}" + shows "emeasure (SUP i:A. M i) X = (SUP i:A. emeasure (M i) X)" +proof (subst emeasure_SUP[OF sets \A \ {}\]) + show "(SUP J:{J. J \ {} \ finite J \ J \ A}. emeasure (SUPREMUM J M) X) = (SUP i:A. emeasure (M i) X)" + proof (rule SUP_eq) + fix J assume "J \ {J. J \ {} \ finite J \ J \ A}" + then have J: "Complete_Partial_Order.chain op \ (M ` J)" "finite J" "J \ {}" and "J \ A" + using ch[THEN chain_subset, of "M`J"] by auto + with in_chain_finite[OF J(1)] obtain j where "j \ J" "(SUP j:J. M j) = M j" + by auto + with \J \ A\ show "\j\A. emeasure (SUPREMUM J M) X \ emeasure (M j) X" + by auto + next + fix j assume "j\A" then show "\i\{J. J \ {} \ finite J \ J \ A}. emeasure (M j) X \ emeasure (SUPREMUM i M) X" + by (intro bexI[of _ "{j}"]) auto + qed +qed + +subsubsection \Supremum of a set of $\sigma$-algebras\ + +lemma space_Sup_eq_UN: "space (Sup M) = (\x\M. space x)" + unfolding Sup_measure_def + apply (intro Sup_lexord[where P="\x. space x = _"]) + apply (subst space_Sup_measure'2) + apply auto [] + apply (subst space_measure_of[OF UN_space_closed]) + apply auto + done + +lemma sets_Sup_eq: + assumes *: "\m. m \ M \ space m = X" and "M \ {}" + shows "sets (Sup M) = sigma_sets X (\x\M. sets x)" + unfolding Sup_measure_def + apply (rule Sup_lexord1) + apply fact + apply (simp add: assms) + apply (rule Sup_lexord) + subgoal premises that for a S + unfolding that(3) that(2)[symmetric] + using that(1) + apply (subst sets_Sup_measure'2) + apply (intro arg_cong2[where f=sigma_sets]) + apply (auto simp: *) + done + apply (subst sets_measure_of[OF UN_space_closed]) + apply (simp add: assms) + done + +lemma in_sets_Sup: "(\m. m \ M \ space m = X) \ m \ M \ A \ sets m \ A \ sets (Sup M)" + by (subst sets_Sup_eq[where X=X]) auto + +lemma Sup_lexord_rel: + assumes "\i. i \ I \ k (A i) = k (B i)" + "R (c (A ` {a \ I. k (B a) = (SUP x:I. k (B x))})) (c (B ` {a \ I. k (B a) = (SUP x:I. k (B x))}))" + "R (s (A`I)) (s (B`I))" + shows "R (Sup_lexord k c s (A`I)) (Sup_lexord k c s (B`I))" +proof - + have "A ` {a \ I. k (B a) = (SUP x:I. k (B x))} = {a \ A ` I. k a = (SUP x:I. k (B x))}" + using assms(1) by auto + moreover have "B ` {a \ I. k (B a) = (SUP x:I. k (B x))} = {a \ B ` I. k a = (SUP x:I. k (B x))}" + by auto + ultimately show ?thesis + using assms by (auto simp: Sup_lexord_def Let_def) +qed + +lemma sets_SUP_cong: + assumes eq: "\i. i \ I \ sets (M i) = sets (N i)" shows "sets (SUP i:I. M i) = sets (SUP i:I. N i)" + unfolding Sup_measure_def + using eq eq[THEN sets_eq_imp_space_eq] + apply (intro Sup_lexord_rel[where R="\x y. sets x = sets y"]) + apply simp + apply simp + apply (simp add: sets_Sup_measure'2) + apply (intro arg_cong2[where f="\x y. sets (sigma x y)"]) + apply auto + done + +lemma sets_Sup_in_sets: + assumes "M \ {}" + assumes "\m. m \ M \ space m = space N" + assumes "\m. m \ M \ sets m \ sets N" + shows "sets (Sup M) \ sets N" +proof - + have *: "UNION M space = space N" + using assms by auto + show ?thesis + unfolding * using assms by (subst sets_Sup_eq[of M "space N"]) (auto intro!: sets.sigma_sets_subset) +qed + +lemma measurable_Sup1: + assumes m: "m \ M" and f: "f \ measurable m N" + and const_space: "\m n. m \ M \ n \ M \ space m = space n" + shows "f \ measurable (Sup M) N" +proof - + have "space (Sup M) = space m" + using m by (auto simp add: space_Sup_eq_UN dest: const_space) + then show ?thesis + using m f unfolding measurable_def by (auto intro: in_sets_Sup[OF const_space]) +qed + +lemma measurable_Sup2: + assumes M: "M \ {}" + assumes f: "\m. m \ M \ f \ measurable N m" + and const_space: "\m n. m \ M \ n \ M \ space m = space n" + shows "f \ measurable N (Sup M)" +proof - + from M obtain m where "m \ M" by auto + have space_eq: "\n. n \ M \ space n = space m" + by (intro const_space \m \ M\) + have "f \ measurable N (sigma (\m\M. space m) (\m\M. sets m))" + proof (rule measurable_measure_of) + show "f \ space N \ UNION M space" + using measurable_space[OF f] M by auto + qed (auto intro: measurable_sets f dest: sets.sets_into_space) + also have "measurable N (sigma (\m\M. space m) (\m\M. sets m)) = measurable N (Sup M)" + apply (intro measurable_cong_sets refl) + apply (subst sets_Sup_eq[OF space_eq M]) + apply simp + apply (subst sets_measure_of[OF UN_space_closed]) + apply (simp add: space_eq M) + done + finally show ?thesis . +qed + +lemma sets_Sup_sigma: + assumes [simp]: "M \ {}" and M: "\m. m \ M \ m \ Pow \" + shows "sets (SUP m:M. sigma \ m) = sets (sigma \ (\M))" +proof - + { fix a m assume "a \ sigma_sets \ m" "m \ M" + then have "a \ sigma_sets \ (\M)" + by induction (auto intro: sigma_sets.intros) } + then show "sets (SUP m:M. sigma \ m) = sets (sigma \ (\M))" + apply (subst sets_Sup_eq[where X="\"]) + apply (auto simp add: M) [] + apply auto [] + apply (simp add: space_measure_of_conv M Union_least) + apply (rule sigma_sets_eqI) + apply auto + done +qed + +lemma Sup_sigma: + assumes [simp]: "M \ {}" and M: "\m. m \ M \ m \ Pow \" + shows "(SUP m:M. sigma \ m) = (sigma \ (\M))" +proof (intro antisym SUP_least) + have *: "\M \ Pow \" + using M by auto + show "sigma \ (\M) \ (SUP m:M. sigma \ m)" + proof (intro less_eq_measure.intros(3)) + show "space (sigma \ (\M)) = space (SUP m:M. sigma \ m)" + "sets (sigma \ (\M)) = sets (SUP m:M. sigma \ m)" + using sets_Sup_sigma[OF assms] sets_Sup_sigma[OF assms, THEN sets_eq_imp_space_eq] + by auto + qed (simp add: emeasure_sigma le_fun_def) + fix m assume "m \ M" then show "sigma \ m \ sigma \ (\M)" + by (subst sigma_le_iff) (auto simp add: M *) +qed + +lemma SUP_sigma_sigma: + "M \ {} \ (\m. m \ M \ f m \ Pow \) \ (SUP m:M. sigma \ (f m)) = sigma \ (\m\M. f m)" + using Sup_sigma[of "f`M" \] by auto + +lemma sets_vimage_Sup_eq: + assumes *: "M \ {}" "f \ X \ Y" "\m. m \ M \ space m = Y" + shows "sets (vimage_algebra X f (Sup M)) = sets (SUP m : M. vimage_algebra X f m)" + (is "?IS = ?SI") +proof + show "?IS \ ?SI" + apply (intro sets_image_in_sets measurable_Sup2) + apply (simp add: space_Sup_eq_UN *) + apply (simp add: *) + apply (intro measurable_Sup1) + apply (rule imageI) + apply assumption + apply (rule measurable_vimage_algebra1) + apply (auto simp: *) + done + show "?SI \ ?IS" + apply (intro sets_Sup_in_sets) + apply (auto simp: *) [] + apply (auto simp: *) [] + apply (elim imageE) + apply simp + apply (rule sets_image_in_sets) + apply simp + apply (simp add: measurable_def) + apply (simp add: * space_Sup_eq_UN sets_vimage_algebra2) + apply (auto intro: in_sets_Sup[OF *(3)]) + done +qed + +lemma restrict_space_eq_vimage_algebra': + "sets (restrict_space M \) = sets (vimage_algebra (\ \ space M) (\x. x) M)" +proof - + have *: "{A \ (\ \ space M) |A. A \ sets M} = {A \ \ |A. A \ sets M}" + using sets.sets_into_space[of _ M] by blast + + show ?thesis + unfolding restrict_space_def + by (subst sets_measure_of) + (auto simp add: image_subset_iff sets_vimage_algebra * dest: sets.sets_into_space intro!: arg_cong2[where f=sigma_sets]) +qed + +lemma sigma_le_sets: + assumes [simp]: "A \ Pow X" shows "sets (sigma X A) \ sets N \ X \ sets N \ A \ sets N" +proof + have "X \ sigma_sets X A" "A \ sigma_sets X A" + by (auto intro: sigma_sets_top) + moreover assume "sets (sigma X A) \ sets N" + ultimately show "X \ sets N \ A \ sets N" + by auto +next + assume *: "X \ sets N \ A \ sets N" + { fix Y assume "Y \ sigma_sets X A" from this * have "Y \ sets N" + by induction auto } + then show "sets (sigma X A) \ sets N" + by auto +qed + +lemma measurable_iff_sets: + "f \ measurable M N \ (f \ space M \ space N \ sets (vimage_algebra (space M) f N) \ sets M)" +proof - + have *: "{f -` A \ space M |A. A \ sets N} \ Pow (space M)" + by auto + show ?thesis + unfolding measurable_def + by (auto simp add: vimage_algebra_def sigma_le_sets[OF *]) +qed + +lemma sets_vimage_algebra_space: "X \ sets (vimage_algebra X f M)" + using sets.top[of "vimage_algebra X f M"] by simp + +lemma measurable_mono: + assumes N: "sets N' \ sets N" "space N = space N'" + assumes M: "sets M \ sets M'" "space M = space M'" + shows "measurable M N \ measurable M' N'" + unfolding measurable_def +proof safe + fix f A assume "f \ space M \ space N" "A \ sets N'" + moreover assume "\y\sets N. f -` y \ space M \ sets M" note this[THEN bspec, of A] + ultimately show "f -` A \ space M' \ sets M'" + using assms by auto +qed (insert N M, auto) + +lemma measurable_Sup_measurable: + assumes f: "f \ space N \ A" + shows "f \ measurable N (Sup {M. space M = A \ f \ measurable N M})" +proof (rule measurable_Sup2) + show "{M. space M = A \ f \ measurable N M} \ {}" + using f unfolding ex_in_conv[symmetric] + by (intro exI[of _ "sigma A {}"]) (auto intro!: measurable_measure_of) +qed auto + +lemma (in sigma_algebra) sigma_sets_subset': + assumes a: "a \ M" "\' \ M" + shows "sigma_sets \' a \ M" +proof + show "x \ M" if x: "x \ sigma_sets \' a" for x + using x by (induct rule: sigma_sets.induct) (insert a, auto) +qed + +lemma in_sets_SUP: "i \ I \ (\i. i \ I \ space (M i) = Y) \ X \ sets (M i) \ X \ sets (SUP i:I. M i)" + by (intro in_sets_Sup[where X=Y]) auto + +lemma measurable_SUP1: + "i \ I \ f \ measurable (M i) N \ (\m n. m \ I \ n \ I \ space (M m) = space (M n)) \ + f \ measurable (SUP i:I. M i) N" + by (auto intro: measurable_Sup1) + +lemma sets_image_in_sets': + assumes X: "X \ sets N" + assumes f: "\A. A \ sets M \ f -` A \ X \ sets N" + shows "sets (vimage_algebra X f M) \ sets N" + unfolding sets_vimage_algebra + by (rule sets.sigma_sets_subset') (auto intro!: measurable_sets X f) + +lemma mono_vimage_algebra: + "sets M \ sets N \ sets (vimage_algebra X f M) \ sets (vimage_algebra X f N)" + using sets.top[of "sigma X {f -` A \ X |A. A \ sets N}"] + unfolding vimage_algebra_def + apply (subst (asm) space_measure_of) + apply auto [] + apply (subst sigma_le_sets) + apply auto + done + +lemma mono_restrict_space: "sets M \ sets N \ sets (restrict_space M X) \ sets (restrict_space N X)" + unfolding sets_restrict_space by (rule image_mono) + +lemma sets_eq_bot: "sets M = {{}} \ M = bot" + apply safe + apply (intro measure_eqI) + apply auto + done + +lemma sets_eq_bot2: "{{}} = sets M \ M = bot" + using sets_eq_bot[of M] by blast end diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Tue Jun 21 15:10:43 2016 +0200 @@ -1525,6 +1525,18 @@ subsection \Integral under concrete measures\ +lemma nn_integral_mono_measure: + assumes "sets M = sets N" "M \ N" shows "nn_integral M f \ nn_integral N f" + unfolding nn_integral_def +proof (intro SUP_subset_mono) + note \sets M = sets N\[simp] \sets M = sets N\[THEN sets_eq_imp_space_eq, simp] + show "{g. simple_function M g \ g \ f} \ {g. simple_function N g \ g \ f}" + by (simp add: simple_function_def) + show "integral\<^sup>S M x \ integral\<^sup>S N x" for x + using le_measureD3[OF \M \ N\] + by (auto simp add: simple_integral_def intro!: setsum_mono mult_mono) +qed + lemma nn_integral_empty: assumes "space M = {}" shows "nn_integral M f = 0" @@ -1534,6 +1546,9 @@ thus ?thesis by simp qed +lemma nn_integral_bot[simp]: "nn_integral bot f = 0" + by (simp add: nn_integral_empty) + subsubsection \Distributions\ lemma nn_integral_distr: diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Probability/Radon_Nikodym.thy --- a/src/HOL/Probability/Radon_Nikodym.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Probability/Radon_Nikodym.thy Tue Jun 21 15:10:43 2016 +0200 @@ -8,8 +8,9 @@ imports Bochner_Integration begin -definition "diff_measure M N = - measure_of (space M) (sets M) (\A. emeasure M A - emeasure N A)" +definition diff_measure :: "'a measure \ 'a measure \ 'a measure" +where + "diff_measure M N = measure_of (space M) (sets M) (\A. emeasure M A - emeasure N A)" lemma shows space_diff_measure[simp]: "space (diff_measure M N) = space M" @@ -36,7 +37,7 @@ (\i. emeasure M (A i)) - (\i. emeasure N (A i))" using fin pos[of "A _"] by (intro ennreal_suminf_minus) - (auto simp: sets_eq finite_measure.emeasure_eq_measure suminf_emeasure measure_nonneg) + (auto simp: sets_eq finite_measure.emeasure_eq_measure suminf_emeasure) then show "(\i. emeasure M (A i) - emeasure N (A i)) = emeasure M (\i. A i) - emeasure N (\i. A i) " by (simp add: suminf) @@ -53,6 +54,8 @@ disjoint: "disjoint_family A" using sigma_finite_disjoint by blast let ?B = "\i. 2^Suc i * emeasure M (A i)" + have [measurable]: "\i. A i \ sets M" + using range by fastforce+ have "\i. \x. 0 < x \ x < inverse (?B i)" proof fix i show "\x. 0 < x \ x < inverse (?B i)" @@ -65,9 +68,7 @@ let ?h = "\x. \i. n i * indicator (A i) x" show ?thesis proof (safe intro!: bexI[of _ ?h] del: notI) - have "\i. A i \ sets M" - using range by fastforce+ - then have "integral\<^sup>N M ?h = (\i. n i * emeasure M (A i))" using pos + have "integral\<^sup>N M ?h = (\i. n i * emeasure M (A i))" using pos by (simp add: nn_integral_suminf nn_integral_cmult_indicator) also have "\ \ (\i. ennreal ((1/2)^Suc i))" proof (intro suminf_le allI) @@ -81,10 +82,8 @@ del: power_Suc) also have "\ \ inverse (ennreal 2) ^ Suc N" using measure[of N] - apply (cases "emeasure M (A N)" rule: ennreal_cases) - apply (cases "emeasure M (A N) = 0") - apply (auto simp: inverse_ennreal ennreal_mult[symmetric] divide_ennreal_def simp del: power_Suc) - done + by (cases "emeasure M (A N)"; cases "emeasure M (A N) = 0") + (auto simp: inverse_ennreal ennreal_mult[symmetric] divide_ennreal_def simp del: power_Suc) also have "\ = ennreal (inverse 2 ^ Suc N)" by (subst ennreal_power[symmetric], simp) (simp add: inverse_ennreal) finally show "n N * emeasure M (A N) \ ennreal ((1/2)^Suc N)" @@ -92,11 +91,8 @@ qed auto also have "\ < top" unfolding less_top[symmetric] - apply (rule ennreal_suminf_neq_top) - apply (subst summable_Suc_iff) - apply (subst summable_geometric) - apply auto - done + by (rule ennreal_suminf_neq_top) + (auto simp: summable_geometric summable_Suc_iff simp del: power_Suc) finally show "integral\<^sup>N M ?h \ \" by (auto simp: top_unique) next @@ -125,6 +121,10 @@ "(\x. \ x \ A ; f x \ 0 \ \ g x \ 0) \ absolutely_continuous (point_measure A f) (point_measure A g)" unfolding absolutely_continuous_def by (force simp: null_sets_point_measure_iff) +lemma absolutely_continuousD: + "absolutely_continuous M N \ A \ sets M \ emeasure M A = 0 \ emeasure N A = 0" + by (auto simp: absolutely_continuous_def null_sets_def) + lemma absolutely_continuous_AE: assumes sets_eq: "sets M' = sets M" and "absolutely_continuous M M'" "AE x in M. P x" @@ -142,175 +142,25 @@ subsection "Existence of the Radon-Nikodym derivative" -lemma (in finite_measure) Radon_Nikodym_aux_epsilon: - fixes e :: real assumes "0 < e" - assumes "finite_measure N" and sets_eq: "sets N = sets M" - shows "\A\sets M. measure M (space M) - measure N (space M) \ measure M A - measure N A \ - (\B\sets M. B \ A \ - e < measure M B - measure N B)" -proof - - interpret M': finite_measure N by fact - let ?d = "\A. measure M A - measure N A" - let ?A = "\A. if (\B\sets M. B \ space M - A \ -e < ?d B) - then {} - else (SOME B. B \ sets M \ B \ space M - A \ ?d B \ -e)" - define A where "A n = ((\B. B \ ?A B) ^^ n) {}" for n - have A_simps[simp]: - "A 0 = {}" - "\n. A (Suc n) = (A n \ ?A (A n))" unfolding A_def by simp_all - { fix A assume "A \ sets M" - have "?A A \ sets M" - by (auto intro!: someI2[of _ _ "\A. A \ sets M"] simp: not_less) } - note A'_in_sets = this - { fix n have "A n \ sets M" - proof (induct n) - case (Suc n) thus "A (Suc n) \ sets M" - using A'_in_sets[of "A n"] by (auto split: if_split_asm) - qed (simp add: A_def) } - note A_in_sets = this - hence "range A \ sets M" by auto - { fix n B - assume Ex: "\B. B \ sets M \ B \ space M - A n \ ?d B \ -e" - hence False: "\ (\B\sets M. B \ space M - A n \ -e < ?d B)" by (auto simp: not_less) - have "?d (A (Suc n)) \ ?d (A n) - e" unfolding A_simps if_not_P[OF False] - proof (rule someI2_ex[OF Ex]) - fix B assume "B \ sets M \ B \ space M - A n \ ?d B \ - e" - hence "A n \ B = {}" "B \ sets M" and dB: "?d B \ -e" by auto - hence "?d (A n \ B) = ?d (A n) + ?d B" - using \A n \ sets M\ finite_measure_Union M'.finite_measure_Union by (simp add: sets_eq) - also have "\ \ ?d (A n) - e" using dB by simp - finally show "?d (A n \ B) \ ?d (A n) - e" . - qed } - note dA_epsilon = this - { fix n have "?d (A (Suc n)) \ ?d (A n)" - proof (cases "\B. B\sets M \ B \ space M - A n \ ?d B \ - e") - case True from dA_epsilon[OF this] show ?thesis using \0 < e\ by simp - next - case False - hence "\B\sets M. B \ space M - A n \ -e < ?d B" by (auto simp: not_le) - thus ?thesis by simp - qed } - note dA_mono = this - show ?thesis - proof (cases "\n. \B\sets M. B \ space M - A n \ -e < ?d B") - case True then obtain n where B: "\B. \ B \ sets M; B \ space M - A n\ \ -e < ?d B" by blast - show ?thesis - proof (safe intro!: bexI[of _ "space M - A n"]) - fix B assume "B \ sets M" "B \ space M - A n" - from B[OF this] show "-e < ?d B" . - next - show "space M - A n \ sets M" by (rule sets.compl_sets) fact - next - show "?d (space M) \ ?d (space M - A n)" - proof (induct n) - fix n assume "?d (space M) \ ?d (space M - A n)" - also have "\ \ ?d (space M - A (Suc n))" - using A_in_sets sets.sets_into_space dA_mono[of n] finite_measure_compl M'.finite_measure_compl - by (simp del: A_simps add: sets_eq sets_eq_imp_space_eq[OF sets_eq]) - finally show "?d (space M) \ ?d (space M - A (Suc n))" . - qed simp - qed - next - case False hence B: "\n. \B. B\sets M \ B \ space M - A n \ ?d B \ - e" - by (auto simp add: not_less) - { fix n have "?d (A n) \ - real n * e" - proof (induct n) - case (Suc n) with dA_epsilon[of n, OF B] show ?case by (simp del: A_simps add: of_nat_Suc field_simps) - next - case 0 with measure_empty show ?case by (simp add: zero_ennreal_def) - qed } note dA_less = this - have decseq: "decseq (\n. ?d (A n))" unfolding decseq_eq_incseq - proof (rule incseq_SucI) - fix n show "- ?d (A n) \ - ?d (A (Suc n))" using dA_mono[of n] by auto - qed - have A: "incseq A" by (auto intro!: incseq_SucI) - from finite_Lim_measure_incseq[OF _ A] \range A \ sets M\ - M'.finite_Lim_measure_incseq[OF _ A] - have convergent: "(\i. ?d (A i)) \ ?d (\i. A i)" - by (auto intro!: tendsto_diff simp: sets_eq) - obtain n :: nat where "- ?d (\i. A i) / e < real n" using reals_Archimedean2 by auto - moreover from order_trans[OF decseq_le[OF decseq convergent] dA_less] - have "real n \ - ?d (\i. A i) / e" using \0 by (simp add: field_simps) - ultimately show ?thesis by auto - qed -qed - -lemma (in finite_measure) Radon_Nikodym_aux: - assumes "finite_measure N" and sets_eq: "sets N = sets M" - shows "\A\sets M. measure M (space M) - measure N (space M) \ - measure M A - measure N A \ - (\B\sets M. B \ A \ 0 \ measure M B - measure N B)" +lemma (in finite_measure) Radon_Nikodym_finite_measure: + assumes "finite_measure N" and sets_eq[simp]: "sets N = sets M" + assumes "absolutely_continuous M N" + shows "\f \ borel_measurable M. density M f = N" proof - interpret N: finite_measure N by fact - let ?d = "\A. measure M A - measure N A" - let ?P = "\A n. if n = 0 then A = space M else (\C\sets M. C \ A \ - 1 / real (Suc n) < ?d C)" - let ?Q = "\A B. A \ B \ ?d B \ ?d A" - - have "\A. \n. (A n \ sets M \ ?P (A n) n) \ ?Q (A (Suc n)) (A n)" - proof (rule dependent_nat_choice) - show "\A. A \ sets M \ ?P A 0" - by auto - next - fix A n assume "A \ sets M \ ?P A n" - then have A: "A \ sets M" by auto - then have "finite_measure (density M (indicator A))" "0 < 1 / real (Suc (Suc n))" - "finite_measure (density N (indicator A))" "sets (density N (indicator A)) = sets (density M (indicator A))" - by (auto simp: finite_measure_restricted N.finite_measure_restricted sets_eq) - from finite_measure.Radon_Nikodym_aux_epsilon[OF this] guess X .. note X = this - with A have "A \ X \ sets M \ ?P (A \ X) (Suc n) \ ?Q (A \ X) A" - by (simp add: measure_restricted sets_eq sets.Int) (metis inf_absorb2) - then show "\B. (B \ sets M \ ?P B (Suc n)) \ ?Q B A" - by blast - qed - then obtain A where A: "\n. A n \ sets M" "\n. ?P (A n) n" "\n. ?Q (A (Suc n)) (A n)" - by metis - then have mono_dA: "mono (\i. ?d (A i))" and A_0[simp]: "A 0 = space M" - by (auto simp add: mono_iff_le_Suc) - show ?thesis - proof (safe intro!: bexI[of _ "\i. A i"]) - show "(\i. A i) \ sets M" using \\n. A n \ sets M\ by auto - have "decseq A" using A by (auto intro!: decseq_SucI) - from A(1) finite_Lim_measure_decseq[OF _ this] N.finite_Lim_measure_decseq[OF _ this] - have "(\i. ?d (A i)) \ ?d (\i. A i)" by (auto intro!: tendsto_diff simp: sets_eq) - thus "?d (space M) \ ?d (\i. A i)" using mono_dA[THEN monoD, of 0 _] - by (rule_tac LIMSEQ_le_const) auto - next - fix B assume B: "B \ sets M" "B \ (\i. A i)" - show "0 \ ?d B" - proof (rule ccontr) - assume "\ 0 \ ?d B" - hence "0 < - ?d B" by auto - from reals_Archimedean[OF this] - obtain n where *: "?d B < - 1 / real (Suc n)" - by (auto simp: field_simps) - also have "\ \ - 1 / real (Suc (Suc n))" - by (auto simp: field_simps) - finally show False - using * A(2)[of "Suc n"] B by (auto elim!: ballE[of _ _ B]) - qed - qed -qed - -lemma (in finite_measure) Radon_Nikodym_finite_measure: - assumes "finite_measure N" and sets_eq: "sets N = sets M" - assumes "absolutely_continuous M N" - shows "\f \ borel_measurable M. (\x. 0 \ f x) \ density M f = N" -proof - - interpret N: finite_measure N by fact - define G where "G = - {g \ borel_measurable M. (\x. 0 \ g x) \ (\A\sets M. (\\<^sup>+x. g x * indicator A x \M) \ N A)}" - { fix f have "f \ G \ f \ borel_measurable M" by (auto simp: G_def) } + define G where "G = {g \ borel_measurable M. \A\sets M. (\\<^sup>+x. g x * indicator A x \M) \ N A}" + have [measurable_dest]: "f \ G \ f \ borel_measurable M" + and G_D: "\A. f \ G \ A \ sets M \ (\\<^sup>+x. f x * indicator A x \M) \ N A" for f + by (auto simp: G_def) note this[measurable_dest] have "(\x. 0) \ G" unfolding G_def by auto hence "G \ {}" by auto - { fix f g assume f: "f \ G" and g: "g \ G" + { fix f g assume f[measurable]: "f \ G" and g[measurable]: "g \ G" have "(\x. max (g x) (f x)) \ G" (is "?max \ G") unfolding G_def proof safe - show "?max \ borel_measurable M" using f g unfolding G_def by auto let ?A = "{x \ space M. f x \ g x}" have "?A \ sets M" using f g unfolding G_def by auto - fix A assume "A \ sets M" - hence sets: "?A \ A \ sets M" "(space M - ?A) \ A \ sets M" using \?A \ sets M\ by auto - hence sets': "?A \ A \ sets N" "(space M - ?A) \ A \ sets N" by (auto simp: sets_eq) + fix A assume [measurable]: "A \ sets M" have union: "((?A \ A) \ ((space M - ?A) \ A)) = A" using sets.sets_into_space[OF \A \ sets M\] by auto have "\x. x \ space M \ max (g x) (f x) * indicator A x = @@ -319,24 +169,19 @@ hence "(\\<^sup>+x. max (g x) (f x) * indicator A x \M) = (\\<^sup>+x. g x * indicator (?A \ A) x \M) + (\\<^sup>+x. f x * indicator ((space M - ?A) \ A) x \M)" - using f g sets unfolding G_def by (auto cong: nn_integral_cong intro!: nn_integral_add) also have "\ \ N (?A \ A) + N ((space M - ?A) \ A)" - using f g sets unfolding G_def by (auto intro!: add_mono) + using f g unfolding G_def by (auto intro!: add_mono) also have "\ = N A" - using plus_emeasure[OF sets'] union by auto + using union by (subst plus_emeasure) auto finally show "(\\<^sup>+x. max (g x) (f x) * indicator A x \M) \ N A" . - next - fix x show "0 \ max (g x) (f x)" using f g by (auto simp: G_def split: split_max) - qed } + qed auto } note max_in_G = this { fix f assume "incseq f" and f: "\i. f i \ G" then have [measurable]: "\i. f i \ borel_measurable M" by (auto simp: G_def) have "(\x. SUP i. f i x) \ G" unfolding G_def proof safe show "(\x. SUP i. f i x) \ borel_measurable M" by measurable - { fix x show "0 \ (SUP i. f i x)" - using f by (auto simp: G_def intro: SUP_upper2) } next fix A assume "A \ sets M" have "(\\<^sup>+x. (SUP i. f i x) * indicator A x \M) = @@ -347,7 +192,7 @@ by (intro nn_integral_monotone_convergence_SUP) (auto simp: G_def incseq_Suc_iff le_fun_def split: split_indicator) finally show "(\\<^sup>+x. (SUP i. f i x) * indicator A x \M) \ N A" - using f \A \ sets M\ by (auto intro!: SUP_least simp: G_def) + using f \A \ sets M\ by (auto intro!: SUP_least simp: G_D) qed } note SUP_in_G = this let ?y = "SUP g : G. integral\<^sup>N M g" @@ -381,11 +226,12 @@ note g_in_G = this have "incseq ?g" using gs_not_empty by (auto intro!: incseq_SucI le_funI simp add: atMost_Suc) + from SUP_in_G[OF this g_in_G] have [measurable]: "f \ G" unfolding f_def . - then have [simp, intro]: "f \ borel_measurable M" unfolding G_def by auto + then have [measurable]: "f \ borel_measurable M" unfolding G_def by auto + have "integral\<^sup>N M f = (SUP i. integral\<^sup>N M (?g i))" unfolding f_def - using g_in_G \incseq ?g\ - by (auto intro!: nn_integral_monotone_convergence_SUP simp: G_def) + using g_in_G \incseq ?g\ by (auto intro!: nn_integral_monotone_convergence_SUP simp: G_def) also have "\ = ?y" proof (rule antisym) show "(SUP i. integral\<^sup>N M (?g i)) \ ?y" @@ -394,148 +240,95 @@ by (auto intro!: SUP_mono nn_integral_mono Max_ge) qed finally have int_f_eq_y: "integral\<^sup>N M f = ?y" . - have "\x. 0 \ f x" - unfolding f_def using \\i. gs i \ G\ - by (auto intro!: SUP_upper2 Max_ge_iff[THEN iffD2] simp: G_def) - let ?t = "\A. N A - (\\<^sup>+x. ?F A x \M)" - let ?M = "diff_measure N (density M f)" - have f_le_N: "\A. A \ sets M \ (\\<^sup>+x. ?F A x \M) \ N A" - using \f \ G\ unfolding G_def by auto - have emeasure_M: "\A. A \ sets M \ emeasure ?M A = ?t A" - proof (subst emeasure_diff_measure) - from f_le_N[of "space M"] show "finite_measure N" "finite_measure (density M f)" - by (auto intro!: finite_measureI simp: emeasure_density top_unique cong: nn_integral_cong) - next - fix B assume "B \ sets N" with f_le_N[of B] show "emeasure (density M f) B \ emeasure N B" - by (auto simp: sets_eq emeasure_density cong: nn_integral_cong) - qed (auto simp: sets_eq emeasure_density) - from emeasure_M[of "space M"] N.finite_emeasure_space - interpret M': finite_measure ?M - by (auto intro!: finite_measureI simp: sets_eq_imp_space_eq[OF sets_eq] N.emeasure_eq_measure ) - have ac: "absolutely_continuous M ?M" unfolding absolutely_continuous_def - proof - fix A assume A_M: "A \ null_sets M" - with \absolutely_continuous M N\ have A_N: "A \ null_sets N" - unfolding absolutely_continuous_def by auto - moreover from A_M A_N have "(\\<^sup>+ x. ?F A x \M) \ N A" using \f \ G\ by (auto simp: G_def) - ultimately have "N A - (\\<^sup>+ x. ?F A x \M) = 0" - by (auto intro!: antisym) - then show "A \ null_sets ?M" - using A_M by (simp add: emeasure_M null_sets_def sets_eq) - qed - have upper_bound: "\A\sets M. ?M A \ 0" + have upper_bound: "\A\sets M. N A \ density M f A" proof (rule ccontr) assume "\ ?thesis" - then obtain A where A: "A \ sets M" and pos: "0 < ?M A" + then obtain A where A[measurable]: "A \ sets M" and f_less_N: "density M f A < N A" + by (auto simp: not_le) + then have pos_A: "0 < M A" + using \absolutely_continuous M N\[THEN absolutely_continuousD, OF A] by (auto simp: zero_less_iff_neq_zero) - note pos - also have "?M A \ ?M (space M)" - using emeasure_space[of ?M A] by (simp add: sets_eq[THEN sets_eq_imp_space_eq]) - finally have pos_t: "0 < ?M (space M)" by simp - moreover - from pos_t have "emeasure M (space M) \ 0" - using ac unfolding absolutely_continuous_def by (auto simp: null_sets_def) - then have pos_M: "0 < emeasure M (space M)" - by (simp add: zero_less_iff_neq_zero) - moreover - have "(\\<^sup>+x. f x * indicator (space M) x \M) \ N (space M)" - using \f \ G\ unfolding G_def by auto - hence "(\\<^sup>+x. f x * indicator (space M) x \M) \ \" - using M'.finite_emeasure_space by (auto simp: top_unique) + + define b where "b = (N A - density M f A) / M A / 2" + with f_less_N pos_A have "0 < b" "b \ top" + by (auto intro!: diff_gr0_ennreal simp: zero_less_iff_neq_zero diff_eq_0_iff_ennreal ennreal_divide_eq_top_iff) + + let ?f = "\x. f x + b" + have "nn_integral M f \ top" + using `f \ G`[THEN G_D, of "space M"] by (auto simp: top_unique cong: nn_integral_cong) + with \b \ top\ interpret Mf: finite_measure "density M ?f" + by (intro finite_measureI) + (auto simp: field_simps mult_indicator_subset ennreal_mult_eq_top_iff + emeasure_density nn_integral_cmult_indicator nn_integral_add + cong: nn_integral_cong) + + from unsigned_Hahn_decomposition[of "density M ?f" N A] + obtain Y where [measurable]: "Y \ sets M" and [simp]: "Y \ A" + and Y1: "\C. C \ sets M \ C \ Y \ density M ?f C \ N C" + and Y2: "\C. C \ sets M \ C \ A \ C \ Y = {} \ N C \ density M ?f C" + by auto + + let ?f' = "\x. f x + b * indicator Y x" + have "M Y \ 0" + proof + assume "M Y = 0" + then have "N Y = 0" + using \absolutely_continuous M N\[THEN absolutely_continuousD, of Y] by auto + then have "N A = N (A - Y)" + by (subst emeasure_Diff) auto + also have "\ \ density M ?f (A - Y)" + by (rule Y2) auto + also have "\ \ density M ?f A - density M ?f Y" + by (subst emeasure_Diff) auto + also have "\ \ density M ?f A - 0" + by (intro ennreal_minus_mono) auto + also have "density M ?f A = b * M A + density M f A" + by (simp add: emeasure_density field_simps mult_indicator_subset nn_integral_add nn_integral_cmult_indicator) + also have "\ < N A" + using f_less_N pos_A + by (cases "density M f A"; cases "M A"; cases "N A") + (auto simp: b_def ennreal_less_iff ennreal_minus divide_ennreal ennreal_numeral[symmetric] + ennreal_plus[symmetric] ennreal_mult[symmetric] field_simps + simp del: ennreal_numeral ennreal_plus) + finally show False + by simp + qed + then have "nn_integral M f < nn_integral M ?f'" + using \0 < b\ \nn_integral M f \ top\ + by (simp add: nn_integral_add nn_integral_cmult_indicator ennreal_zero_less_mult_iff zero_less_iff_neq_zero) moreover - define b where "b = ?M (space M) / emeasure M (space M) / 2" - ultimately have b: "b \ 0 \ 0 \ b \ b \ \" - by (auto simp: ennreal_divide_eq_top_iff) - then have b: "b \ 0" "0 \ b" "0 < b" "b \ \" - by (auto simp: less_le) - let ?Mb = "density M (\_. b)" - have Mb: "finite_measure ?Mb" "sets ?Mb = sets ?M" - using b by (auto simp: emeasure_density_const sets_eq ennreal_mult_eq_top_iff intro!: finite_measureI) - from M'.Radon_Nikodym_aux[OF this] guess A0 .. - then have "A0 \ sets M" - and space_le_A0: "measure ?M (space M) - enn2real b * measure M (space M) \ measure ?M A0 - enn2real b * measure M A0" - and *: "\B. B \ sets M \ B \ A0 \ 0 \ measure ?M B - enn2real b * measure M B" - using b by (simp_all add: measure_density_const sets_eq_imp_space_eq[OF sets_eq] sets_eq) - { fix B assume B: "B \ sets M" "B \ A0" - with *[OF this] have "b * emeasure M B \ ?M B" - using b unfolding M'.emeasure_eq_measure emeasure_eq_measure - by (cases b rule: ennreal_cases) (auto simp: ennreal_mult[symmetric] measure_nonneg) } - note bM_le_t = this - let ?f0 = "\x. f x + b * indicator A0 x" - { fix A assume A: "A \ sets M" - hence "A \ A0 \ sets M" using \A0 \ sets M\ by auto - have "(\\<^sup>+x. ?f0 x * indicator A x \M) = - (\\<^sup>+x. f x * indicator A x + b * indicator (A \ A0) x \M)" - by (auto intro!: nn_integral_cong split: split_indicator) - hence "(\\<^sup>+x. ?f0 x * indicator A x \M) = - (\\<^sup>+x. f x * indicator A x \M) + b * emeasure M (A \ A0)" - using \A0 \ sets M\ \A \ A0 \ sets M\ A b \f \ G\ - by (simp add: nn_integral_add nn_integral_cmult_indicator G_def) } - note f0_eq = this - { fix A assume A: "A \ sets M" - hence "A \ A0 \ sets M" using \A0 \ sets M\ by auto - have f_le_v: "(\\<^sup>+x. ?F A x \M) \ N A" using \f \ G\ A unfolding G_def by auto - note f0_eq[OF A] - also have "(\\<^sup>+x. ?F A x \M) + b * emeasure M (A \ A0) \ (\\<^sup>+x. ?F A x \M) + ?M (A \ A0)" - using bM_le_t[OF \A \ A0 \ sets M\] \A \ sets M\ \A0 \ sets M\ - by (auto intro!: add_left_mono) - also have "\ \ (\\<^sup>+x. f x * indicator A x \M) + ?M A" - using emeasure_mono[of "A \ A0" A ?M] \A \ sets M\ \A0 \ sets M\ - by (auto intro!: add_left_mono simp: sets_eq) - also have "\ \ N A" - unfolding emeasure_M[OF \A \ sets M\] - using f_le_v N.emeasure_eq_measure[of A] - by (cases "\\<^sup>+x. ?F A x \M" "N A" rule: ennreal2_cases) - (auto simp: top_unique measure_nonneg ennreal_minus ennreal_plus[symmetric] simp del: ennreal_plus) - finally have "(\\<^sup>+x. ?f0 x * indicator A x \M) \ N A" . } - hence "?f0 \ G" using \A0 \ sets M\ b \f \ G\ by (auto simp: G_def) - have int_f_finite: "integral\<^sup>N M f \ \" - by (metis top_unique infinity_ennreal_def int_f_eq_y y_le N.emeasure_finite) - have pos: "0 < measure ?M (space M) - enn2real b * measure M (space M)" - using pos_t pos_M - by (simp add: M'.emeasure_eq_measure emeasure_eq_measure b_def divide_ennreal ennreal_divide_numeral) - also have "\ \ measure ?M A0 - enn2real b * measure M A0" - by (rule space_le_A0) - finally have "enn2real b * measure M A0 < measure ?M A0" - by simp - with b have "?M A0 \ 0" - by (cases b rule: ennreal_cases) - (auto simp: M'.emeasure_eq_measure measure_nonneg mult_less_0_iff not_le[symmetric]) - then have "emeasure M A0 \ 0" - using ac \A0 \ sets M\ by (auto simp: absolutely_continuous_def null_sets_def) - then have "0 < emeasure M A0" - by (auto simp: zero_less_iff_neq_zero) - hence "0 < b * emeasure M A0" - using b by (auto simp: ennreal_zero_less_mult_iff) - with int_f_finite have "?y < integral\<^sup>N M f + b * emeasure M A0" - unfolding int_f_eq_y by auto - also have "\ = integral\<^sup>N M ?f0" - using f0_eq[OF sets.top] \A0 \ sets M\ sets.sets_into_space by (simp cong: nn_integral_cong) - finally have "?y < integral\<^sup>N M ?f0" - by simp - moreover have "integral\<^sup>N M ?f0 \ ?y" - using \?f0 \ G\ by (auto intro!: SUP_upper) - ultimately show False by auto + have "?f' \ G" + unfolding G_def + proof safe + fix X assume [measurable]: "X \ sets M" + have "(\\<^sup>+ x. ?f' x * indicator X x \M) = density M f (X - Y) + density M ?f (X \ Y)" + by (auto simp add: emeasure_density nn_integral_add[symmetric] split: split_indicator intro!: nn_integral_cong) + also have "\ \ N (X - Y) + N (X \ Y)" + using G_D[OF \f \ G\] by (intro add_mono Y1) (auto simp: emeasure_density) + also have "\ = N X" + by (subst plus_emeasure) (auto intro!: arg_cong2[where f=emeasure]) + finally show "(\\<^sup>+ x. ?f' x * indicator X x \M) \ N X" . + qed simp + then have "nn_integral M ?f' \ ?y" + by (rule SUP_upper) + ultimately show False + by (simp add: int_f_eq_y) qed show ?thesis - proof (intro bexI[of _ f] measure_eqI conjI) - show "sets (density M f) = sets N" - by (simp add: sets_eq) - fix A assume A: "A\sets (density M f)" - then show "emeasure (density M f) A = emeasure N A" - using \f \ G\ A upper_bound[THEN bspec, of A] N.emeasure_eq_measure[of A] - by (cases "integral\<^sup>N M (?F A)") - (auto intro!: antisym simp: emeasure_density G_def emeasure_M ennreal_minus_eq_0 top_unique - simp del: measure_nonneg) + proof (intro bexI[of _ f] measure_eqI conjI antisym) + fix A assume "A \ sets (density M f)" then show "emeasure (density M f) A \ emeasure N A" + by (auto simp: emeasure_density intro!: G_D[OF \f \ G\]) + next + fix A assume A: "A \ sets (density M f)" then show "emeasure N A \ emeasure (density M f) A" + using upper_bound by auto qed auto qed lemma (in finite_measure) split_space_into_finite_sets_and_rest: - assumes ac: "absolutely_continuous M N" and sets_eq: "sets N = sets M" - shows "\A0\sets M. \B::nat\'a set. disjoint_family B \ range B \ sets M \ A0 = space M - (\i. B i) \ - (\A\sets M. A \ A0 \ (emeasure M A = 0 \ N A = 0) \ (emeasure M A > 0 \ N A = \)) \ - (\i. N (B i) \ \)" + assumes ac: "absolutely_continuous M N" and sets_eq[simp]: "sets N = sets M" + shows "\B::nat\'a set. disjoint_family B \ range B \ sets M \ (\i. N (B i) \ \) \ + (\A\sets M. A \ (\i. B i) = {} \ (emeasure M A = 0 \ N A = 0) \ (emeasure M A > 0 \ N A = \))" proof - let ?Q = "{Q\sets M. N Q \ \}" let ?a = "SUP Q:?Q. emeasure M Q" @@ -559,13 +352,13 @@ show "range ?O \ sets M" using Q' by auto show "incseq ?O" by (fastforce intro!: incseq_SucI) qed - have Q'_sets: "\i. Q' i \ sets M" using Q' by auto + have Q'_sets[measurable]: "\i. Q' i \ sets M" using Q' by auto have O_sets: "\i. ?O i \ sets M" using Q' by auto then have O_in_G: "\i. ?O i \ ?Q" proof (safe del: notI) fix i have "Q' ` {..i} \ sets M" using Q' by auto then have "N (?O i) \ (\i\i. N (Q' i))" - by (simp add: sets_eq emeasure_subadditive_finite) + by (simp add: emeasure_subadditive_finite) also have "\ < \" using Q' by (simp add: less_top) finally show "N (?O i) \ \" by simp qed auto @@ -585,17 +378,18 @@ qed let ?O_0 = "(\i. ?O i)" have "?O_0 \ sets M" using Q' by auto - define Q where "Q i = (case i of 0 \ Q' 0 | Suc n \ ?O (Suc n) - ?O n)" for i - { fix i have "Q i \ sets M" unfolding Q_def using Q'[of 0] by (cases i) (auto intro: O_sets) } + have "disjointed Q' i \ sets M" for i + using sets.range_disjointed_sets[of Q' M] using Q'_sets by (auto simp: subset_eq) note Q_sets = this show ?thesis proof (intro bexI exI conjI ballI impI allI) - show "disjoint_family Q" - by (fastforce simp: disjoint_family_on_def Q_def - split: nat.split_asm) - show "range Q \ sets M" - using Q_sets by auto - { fix A assume A: "A \ sets M" "A \ space M - ?O_0" + show "disjoint_family (disjointed Q')" + by (rule disjoint_family_disjointed) + show "range (disjointed Q') \ sets M" + using Q'_sets by (intro sets.range_disjointed_sets) auto + { fix A assume A: "A \ sets M" "A \ (\i. disjointed Q' i) = {}" + then have A1: "A \ (\i. Q' i) = {}" + unfolding UN_disjointed_eq by auto show "emeasure M A = 0 \ N A = 0 \ 0 < emeasure M A \ N A = \" proof (rule disjCI, simp) assume *: "emeasure M A = 0 \ N A \ top" @@ -609,7 +403,7 @@ case False with * have "N A \ \" by auto with A have "emeasure M ?O_0 + emeasure M A = emeasure M (?O_0 \ A)" - using Q' by (auto intro!: plus_emeasure sets.countable_UN) + using Q' A1 by (auto intro!: plus_emeasure simp: set_eq_iff) also have "\ = (SUP i. emeasure M (?O i \ A))" proof (rule SUP_emeasure_incseq[of "\i. ?O i \ A", symmetric, simplified]) show "range (\i. ?O i \ A) \ sets M" @@ -621,7 +415,7 @@ proof (safe del: notI) show "?O i \ A \ sets M" using O_sets A by auto from O_in_G[of i] have "N (?O i \ A) \ N (?O i) + N A" - using emeasure_subadditive[of "?O i" N A] A O_sets by (auto simp: sets_eq) + using emeasure_subadditive[of "?O i" N A] A O_sets by auto with O_in_G[of i] show "N (?O i \ A) \ \" using \N A \ \\ by (auto simp: top_unique) qed @@ -632,46 +426,26 @@ with \emeasure M A \ 0\ show ?thesis by auto qed qed } - { fix i show "N (Q i) \ \" - proof (cases i) - case 0 then show ?thesis - unfolding Q_def using Q'[of 0] by simp - next - case (Suc n) - with \?O n \ ?Q\ \?O (Suc n) \ ?Q\ emeasure_Diff[OF _ _ _ O_mono, of N n] - show ?thesis - by (auto simp: sets_eq Q_def) - qed } - show "space M - ?O_0 \ sets M" using Q'_sets by auto - { fix j have "(\i\j. ?O i) = (\i\j. Q i)" - proof (induct j) - case 0 then show ?case by (simp add: Q_def) - next - case (Suc j) - have eq: "\j. (\i\j. ?O i) = (\i\j. Q' i)" by fastforce - have "{..j} \ {..Suc j} = {..Suc j}" by auto - then have "(\i\Suc j. Q' i) = (\i\j. Q' i) \ Q (Suc j)" - by (simp add: UN_Un[symmetric] Q_def del: UN_Un) - then show ?case using Suc by (auto simp add: eq atMost_Suc) - qed } - then have "(\j. (\i\j. ?O i)) = (\j. (\i\j. Q i))" by simp - then show "space M - ?O_0 = space M - (\i. Q i)" by fastforce + { fix i + have "N (disjointed Q' i) \ N (Q' i)" + by (auto intro!: emeasure_mono simp: disjointed_def) + then show "N (disjointed Q' i) \ \" + using Q'(2)[of i] by (auto simp: top_unique) } qed qed lemma (in finite_measure) Radon_Nikodym_finite_measure_infinite: assumes "absolutely_continuous M N" and sets_eq: "sets N = sets M" - shows "\f\borel_measurable M. (\x. 0 \ f x) \ density M f = N" + shows "\f\borel_measurable M. density M f = N" proof - from split_space_into_finite_sets_and_rest[OF assms] - obtain Q0 and Q :: "nat \ 'a set" + obtain Q :: "nat \ 'a set" where Q: "disjoint_family Q" "range Q \ sets M" - and Q0: "Q0 \ sets M" "Q0 = space M - (\i. Q i)" - and in_Q0: "\A. A \ sets M \ A \ Q0 \ emeasure M A = 0 \ N A = 0 \ 0 < emeasure M A \ N A = \" + and in_Q0: "\A. A \ sets M \ A \ (\i. Q i) = {} \ emeasure M A = 0 \ N A = 0 \ 0 < emeasure M A \ N A = \" and Q_fin: "\i. N (Q i) \ \" by force from Q have Q_sets: "\i. Q i \ sets M" by auto let ?N = "\i. density N (indicator (Q i))" and ?M = "\i. density M (indicator (Q i))" - have "\i. \f\borel_measurable (?M i). (\x. 0 \ f x) \ density (?M i) f = ?N i" + have "\i. \f\borel_measurable (?M i). density (?M i) f = ?N i" proof (intro allI finite_measure.Radon_Nikodym_finite_measure) fix i from Q show "finite_measure (?M i)" @@ -700,12 +474,11 @@ using A Q by (simp add: f_density emeasure_restricted subset_eq sets_eq) finally have "emeasure N (Q i \ A) = (\\<^sup>+x. f i x * indicator (Q i \ A) x \M)" .. } note integral_eq = this - let ?f = "\x. (\i. f i x * indicator (Q i) x) + \ * indicator Q0 x" + let ?f = "\x. (\i. f i x * indicator (Q i) x) + \ * indicator (space M - (\i. Q i)) x" show ?thesis proof (safe intro!: bexI[of _ ?f]) - show "?f \ borel_measurable M" using Q0 borel Q_sets + show "?f \ borel_measurable M" using borel Q_sets by (auto intro!: measurable_If) - show "\x. 0 \ ?f x" using borel by (auto intro!: suminf_0_le simp: indicator_def) show "density M ?f = N" proof (rule measure_eqI) fix A assume "A \ sets (density M ?f)" @@ -713,31 +486,31 @@ have Qi: "\i. Q i \ sets M" using Q by auto have [intro,simp]: "\i. (\x. f i x * indicator (Q i \ A) x) \ borel_measurable M" "\i. AE x in M. 0 \ f i x * indicator (Q i \ A) x" - using borel Qi Q0(1) \A \ sets M\ by auto - have "(\\<^sup>+x. ?f x * indicator A x \M) = (\\<^sup>+x. (\i. f i x * indicator (Q i \ A) x) + \ * indicator (Q0 \ A) x \M)" + using borel Qi \A \ sets M\ by auto + have "(\\<^sup>+x. ?f x * indicator A x \M) = (\\<^sup>+x. (\i. f i x * indicator (Q i \ A) x) + \ * indicator ((space M - (\i. Q i)) \ A) x \M)" using borel by (intro nn_integral_cong) (auto simp: indicator_def) - also have "\ = (\\<^sup>+x. (\i. f i x * indicator (Q i \ A) x) \M) + \ * emeasure M (Q0 \ A)" - using borel Qi Q0(1) \A \ sets M\ + also have "\ = (\\<^sup>+x. (\i. f i x * indicator (Q i \ A) x) \M) + \ * emeasure M ((space M - (\i. Q i)) \ A)" + using borel Qi \A \ sets M\ by (subst nn_integral_add) (auto simp add: nn_integral_cmult_indicator sets.Int intro!: suminf_0_le) - also have "\ = (\i. N (Q i \ A)) + \ * emeasure M (Q0 \ A)" + also have "\ = (\i. N (Q i \ A)) + \ * emeasure M ((space M - (\i. Q i)) \ A)" by (subst integral_eq[OF \A \ sets M\], subst nn_integral_suminf) auto - finally have "(\\<^sup>+x. ?f x * indicator A x \M) = (\i. N (Q i \ A)) + \ * emeasure M (Q0 \ A)" . + finally have "(\\<^sup>+x. ?f x * indicator A x \M) = (\i. N (Q i \ A)) + \ * emeasure M ((space M - (\i. Q i)) \ A)" . moreover have "(\i. N (Q i \ A)) = N ((\i. Q i) \ A)" using Q Q_sets \A \ sets M\ by (subst suminf_emeasure) (auto simp: disjoint_family_on_def sets_eq) - moreover have "\ * emeasure M (Q0 \ A) = N (Q0 \ A)" - proof - - have "Q0 \ A \ sets M" using Q0(1) \A \ sets M\ by blast - from in_Q0[OF this] show ?thesis by (auto simp: ennreal_top_mult) - qed - moreover have "Q0 \ A \ sets M" "((\i. Q i) \ A) \ sets M" - using Q_sets \A \ sets M\ Q0(1) by auto - moreover have "((\i. Q i) \ A) \ (Q0 \ A) = A" "((\i. Q i) \ A) \ (Q0 \ A) = {}" - using \A \ sets M\ sets.sets_into_space Q0 by auto + moreover + have "(space M - (\x. Q x)) \ A \ (\x. Q x) = {}" + by auto + then have "\ * emeasure M ((space M - (\i. Q i)) \ A) = N ((space M - (\i. Q i)) \ A)" + using in_Q0[of "(space M - (\i. Q i)) \ A"] \A \ sets M\ Q by (auto simp: ennreal_top_mult) + moreover have "(space M - (\i. Q i)) \ A \ sets M" "((\i. Q i) \ A) \ sets M" + using Q_sets \A \ sets M\ by auto + moreover have "((\i. Q i) \ A) \ ((space M - (\i. Q i)) \ A) = A" "((\i. Q i) \ A) \ ((space M - (\i. Q i)) \ A) = {}" + using \A \ sets M\ sets.sets_into_space by auto ultimately have "N A = (\\<^sup>+x. ?f x * indicator A x \M)" - using plus_emeasure[of "(\i. Q i) \ A" N "Q0 \ A"] by (simp add: sets_eq) - with \A \ sets M\ borel Q Q0(1) show "emeasure (density M ?f) A = N A" + using plus_emeasure[of "(\i. Q i) \ A" N "(space M - (\i. Q i)) \ A"] by (simp add: sets_eq) + with \A \ sets M\ borel Q show "emeasure (density M ?f) A = N A" by (auto simp: subset_eq emeasure_density) qed (simp add: sets_eq) qed @@ -745,7 +518,7 @@ lemma (in sigma_finite_measure) Radon_Nikodym: assumes ac: "absolutely_continuous M N" assumes sets_eq: "sets N = sets M" - shows "\f \ borel_measurable M. (\x. 0 \ f x) \ density M f = N" + shows "\f \ borel_measurable M. density M f = N" proof - from Ex_finite_integrable_function obtain h where finite: "integral\<^sup>N M h \ \" and @@ -770,7 +543,7 @@ by (auto simp: absolutely_continuous_def) qed (auto simp add: sets_eq) from T.Radon_Nikodym_finite_measure_infinite[OF this] - obtain f where f_borel: "f \ borel_measurable M" "\x. 0 \ f x" "density ?MT f = N" by auto + obtain f where f_borel: "f \ borel_measurable M" "density ?MT f = N" by auto with nn borel show ?thesis by (auto intro!: bexI[of _ "\x. h x * f x"] simp: density_density_eq) qed @@ -834,15 +607,14 @@ have ac: "absolutely_continuous M (density M f)" "sets (density M f) = sets M" using borel by (auto intro!: absolutely_continuousI_density) from split_space_into_finite_sets_and_rest[OF this] - obtain Q0 and Q :: "nat \ 'a set" + obtain Q :: "nat \ 'a set" where Q: "disjoint_family Q" "range Q \ sets M" - and Q0: "Q0 \ sets M" "Q0 = space M - (\i. Q i)" - and in_Q0: "\A. A \ sets M \ A \ Q0 \ emeasure M A = 0 \ ?D f A = 0 \ 0 < emeasure M A \ ?D f A = \" + and in_Q0: "\A. A \ sets M \ A \ (\i. Q i) = {} \ emeasure M A = 0 \ ?D f A = 0 \ 0 < emeasure M A \ ?D f A = \" and Q_fin: "\i. ?D f (Q i) \ \" by force - with borel pos have in_Q0: "\A. A \ sets M \ A \ Q0 \ emeasure M A = 0 \ ?N A = 0 \ 0 < emeasure M A \ ?N A = \" + with borel pos have in_Q0: "\A. A \ sets M \ A \ (\i. Q i) = {} \ emeasure M A = 0 \ ?N A = 0 \ 0 < emeasure M A \ ?N A = \" and Q_fin: "\i. ?N (Q i) \ \" by (auto simp: emeasure_density subset_eq) - from Q have Q_sets: "\i. Q i \ sets M" by auto + from Q have Q_sets[measurable]: "\i. Q i \ sets M" by auto let ?D = "{x\space M. f x \ f' x}" have "?D \ sets M" using borel by auto have *: "\i x A. \y::ennreal. y * indicator (Q i) x * indicator A x = y * indicator (Q i \ A) x" @@ -850,15 +622,15 @@ have "\i. AE x in M. ?f (Q i) x = ?f' (Q i) x" using borel Q_fin Q pos by (intro finite_density_unique[THEN iffD1] allI) (auto intro!: f measure_eqI simp: emeasure_density * subset_eq) - moreover have "AE x in M. ?f Q0 x = ?f' Q0 x" + moreover have "AE x in M. ?f (space M - (\i. Q i)) x = ?f' (space M - (\i. Q i)) x" proof (rule AE_I') { fix f :: "'a \ ennreal" assume borel: "f \ borel_measurable M" and eq: "\A. A \ sets M \ ?N A = (\\<^sup>+x. f x * indicator A x \M)" - let ?A = "\i. Q0 \ {x \ space M. f x < (i::nat)}" + let ?A = "\i. (space M - (\i. Q i)) \ {x \ space M. f x < (i::nat)}" have "(\i. ?A i) \ null_sets M" proof (rule null_sets_UN) fix i ::nat have "?A i \ sets M" - using borel Q0(1) by auto + using borel by auto have "?N (?A i) \ (\\<^sup>+x. (i::ennreal) * indicator (?A i) x \M)" unfolding eq[OF \?A i \ sets M\] by (auto intro!: nn_integral_mono simp: indicator_def) @@ -868,21 +640,21 @@ finally have "?N (?A i) \ \" by simp then show "?A i \ null_sets M" using in_Q0[OF \?A i \ sets M\] \?A i \ sets M\ by auto qed - also have "(\i. ?A i) = Q0 \ {x\space M. f x \ \}" + also have "(\i. ?A i) = (space M - (\i. Q i)) \ {x\space M. f x \ \}" by (auto simp: ennreal_Ex_less_of_nat less_top[symmetric]) - finally have "Q0 \ {x\space M. f x \ \} \ null_sets M" by simp } + finally have "(space M - (\i. Q i)) \ {x\space M. f x \ \} \ null_sets M" by simp } from this[OF borel(1) refl] this[OF borel(2) f] - have "Q0 \ {x\space M. f x \ \} \ null_sets M" "Q0 \ {x\space M. f' x \ \} \ null_sets M" by simp_all - then show "(Q0 \ {x\space M. f x \ \}) \ (Q0 \ {x\space M. f' x \ \}) \ null_sets M" by (rule null_sets.Un) - show "{x \ space M. ?f Q0 x \ ?f' Q0 x} \ - (Q0 \ {x\space M. f x \ \}) \ (Q0 \ {x\space M. f' x \ \})" by (auto simp: indicator_def) + have "(space M - (\i. Q i)) \ {x\space M. f x \ \} \ null_sets M" "(space M - (\i. Q i)) \ {x\space M. f' x \ \} \ null_sets M" by simp_all + then show "((space M - (\i. Q i)) \ {x\space M. f x \ \}) \ ((space M - (\i. Q i)) \ {x\space M. f' x \ \}) \ null_sets M" by (rule null_sets.Un) + show "{x \ space M. ?f (space M - (\i. Q i)) x \ ?f' (space M - (\i. Q i)) x} \ + ((space M - (\i. Q i)) \ {x\space M. f x \ \}) \ ((space M - (\i. Q i)) \ {x\space M. f' x \ \})" by (auto simp: indicator_def) qed - moreover have "AE x in M. (?f Q0 x = ?f' Q0 x) \ (\i. ?f (Q i) x = ?f' (Q i) x) \ + moreover have "AE x in M. (?f (space M - (\i. Q i)) x = ?f' (space M - (\i. Q i)) x) \ (\i. ?f (Q i) x = ?f' (Q i) x) \ ?f (space M) x = ?f' (space M) x" - by (auto simp: indicator_def Q0) + by (auto simp: indicator_def) ultimately have "AE x in M. ?f (space M) x = ?f' (space M) x" unfolding AE_all_countable[symmetric] - by eventually_elim (auto intro!: AE_I2 split: if_split_asm simp: indicator_def) + by eventually_elim (auto split: if_split_asm simp: indicator_def) then show "AE x in M. f x = f' x" by auto qed diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Probability/SPMF.thy --- a/src/HOL/Probability/SPMF.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Probability/SPMF.thy Tue Jun 21 15:10:43 2016 +0200 @@ -302,7 +302,7 @@ finally show ?thesis . qed -lemma integral_measure_spmf: +lemma integral_measure_spmf: assumes "integrable (measure_spmf p) f" shows "(\ x. f x \measure_spmf p) = \ x. spmf p x * f x \count_space UNIV" proof - @@ -340,7 +340,7 @@ proof(rule neq_top_trans) show "(SUP i. ennreal (spmf (Y i) x)) \ 1" by(rule SUP_least)(simp add: pmf_le_1) qed simp - + lemma SUP_emeasure_spmf_neq_top: "(SUP p:Y. emeasure (measure_spmf p) A) \ \" proof(rule neq_top_trans) show "(SUP p:Y. emeasure (measure_spmf p) A) \ 1" @@ -453,7 +453,7 @@ lemma set_map_spmf [simp]: "set_spmf (map_spmf f p) = f ` set_spmf p" by(simp add: set_spmf_def image_bind bind_image o_def Option.option.set_map) - + lemma map_spmf_cong: "\ p = q; \x. x \ set_spmf q \ f x = g x \ \ map_spmf f p = map_spmf g q" @@ -576,7 +576,7 @@ by(simp add: sets_bind[where N="count_space UNIV"] space_measure_spmf) next fix A :: "'a set" - have "emeasure ?lhs A = \\<^sup>+ x. emeasure (measure_spmf (f x)) A \measure_pmf p" + have "emeasure ?lhs A = \\<^sup>+ x. emeasure (measure_spmf (f x)) A \measure_pmf p" by(simp add: measure_spmf_def emeasure_distr space_restrict_space emeasure_restrict_space bind_spmf_def) also have "\ = emeasure ?rhs A" by(simp add: emeasure_bind[where N="count_space UNIV"] space_measure_spmf space_subprob_algebra) @@ -591,13 +591,13 @@ next fix A :: "'a set" let ?A = "the -` A \ range Some" - have "emeasure ?lhs A = \\<^sup>+ x. emeasure (measure_pmf (case x of None \ return_pmf None | Some x \ f x)) ?A \measure_pmf p" + have "emeasure ?lhs A = \\<^sup>+ x. emeasure (measure_pmf (case x of None \ return_pmf None | Some x \ f x)) ?A \measure_pmf p" by(simp add: measure_spmf_def emeasure_distr space_restrict_space emeasure_restrict_space bind_spmf_def) also have "\ = \\<^sup>+ x. emeasure (measure_pmf (f (the x))) ?A * indicator (range Some) x \measure_pmf p" by(rule nn_integral_cong)(auto split: option.split simp add: indicator_def) also have "\ = \\<^sup>+ x. emeasure (measure_spmf (f x)) A \measure_spmf p" by(simp add: measure_spmf_def nn_integral_distr nn_integral_restrict_space emeasure_distr space_restrict_space emeasure_restrict_space) - also have "\ = emeasure ?rhs A" + also have "\ = emeasure ?rhs A" by(simp add: emeasure_bind[where N="count_space UNIV"] space_measure_spmf space_subprob_algebra) finally show "emeasure ?lhs A = emeasure ?rhs A" . qed @@ -663,7 +663,7 @@ lemma rel_spmf_mono: "\rel_spmf A f g; \x y. A x y \ B x y \ \ rel_spmf B f g" -apply(erule rel_pmf_mono) +apply(erule rel_pmf_mono) using option.rel_mono[of A B] by(simp add: le_fun_def) lemma rel_spmf_mono_strong: @@ -684,7 +684,7 @@ lemma rel_spmfE [elim?, consumes 1, case_names rel_spmf]: assumes "rel_spmf P p q" - obtains pq where + obtains pq where "\x y. (x, y) \ set_spmf pq \ P x y" "p = map_spmf fst pq" "q = map_spmf snd pq" @@ -847,7 +847,7 @@ lemma weight_spmf_nonneg: "weight_spmf p \ 0" by(fact measure_nonneg) -lemma (in finite_measure) integrable_weight_spmf [simp]: +lemma (in finite_measure) integrable_weight_spmf [simp]: "(\x. weight_spmf (f x)) \ borel_measurable M \ integrable M (\x. weight_spmf (f x))" by(rule integrable_const_bound[where B=1])(simp_all add: weight_spmf_nonneg weight_spmf_le_1) @@ -1068,7 +1068,7 @@ and refl: "\x. x \ set_spmf p \ R x x" shows "ord_spmf R p q" proof(rule rel_pmf.intros) - define pq where "pq = embed_pmf + define pq where "pq = embed_pmf (\(x, y). case x of Some x' \ (case y of Some y' \ if x' = y' then spmf p x' else 0 | None \ 0) | None \ (case y of None \ pmf q None | Some y' \ spmf q y' - spmf p y'))" (is "_ = embed_pmf ?f") @@ -1077,8 +1077,8 @@ have integral: "(\\<^sup>+ xy. ?f xy \count_space UNIV) = 1" (is "nn_integral ?M _ = _") proof - have "(\\<^sup>+ xy. ?f xy \count_space UNIV) = - \\<^sup>+ xy. ennreal (?f xy) * indicator {(None, None)} xy + - ennreal (?f xy) * indicator (range (\x. (None, Some x))) xy + + \\<^sup>+ xy. ennreal (?f xy) * indicator {(None, None)} xy + + ennreal (?f xy) * indicator (range (\x. (None, Some x))) xy + ennreal (?f xy) * indicator (range (\x. (Some x, Some x))) xy \?M" by(rule nn_integral_cong)(auto split: split_indicator option.splits if_split_asm) also have "\ = (\\<^sup>+ xy. ?f xy * indicator {(None, None)} xy \?M) + @@ -1132,8 +1132,8 @@ then show ?thesis using Some by simp next case None - have "(\\<^sup>+ y. pmf pq (None, y) \count_space UNIV) = - (\\<^sup>+ y. ennreal (pmf pq (None, Some (the y))) * indicator (range Some) y + + have "(\\<^sup>+ y. pmf pq (None, y) \count_space UNIV) = + (\\<^sup>+ y. ennreal (pmf pq (None, Some (the y))) * indicator (range Some) y + ennreal (pmf pq (None, None)) * indicator {None} y \count_space UNIV)" by(rule nn_integral_cong)(auto split: split_indicator) also have "\ = (\\<^sup>+ y. ennreal (pmf pq (None, Some (the y))) \count_space (range Some)) + pmf pq (None, None)" @@ -1170,8 +1170,8 @@ then show ?thesis using None by simp next case (Some y) - have "(\\<^sup>+ x. pmf pq (x, Some y) \count_space UNIV) = - (\\<^sup>+ x. ennreal (pmf pq (x, Some y)) * indicator (range Some) x + + have "(\\<^sup>+ x. pmf pq (x, Some y) \count_space UNIV) = + (\\<^sup>+ x. ennreal (pmf pq (x, Some y)) * indicator (range Some) x + ennreal (pmf pq (None, Some y)) * indicator {None} x \count_space UNIV)" by(rule nn_integral_cong)(auto split: split_indicator) also have "\ = (\\<^sup>+ x. ennreal (pmf pq (x, Some y)) * indicator (range Some) x \count_space UNIV) + pmf pq (None, Some y)" @@ -1215,8 +1215,7 @@ by(auto intro!: nn_integral_mono split: split_indicator dest: ord_spmf_eq_leD simp add: nn_integral_measure_spmf nn_integral_indicator[symmetric]) lemma ord_spmf_eqD_measure_spmf: "ord_spmf op = p q \ measure_spmf p \ measure_spmf q" -by(rule less_eq_measure.intros)(simp_all add: ord_spmf_eqD_emeasure) - + by (subst le_measure) (auto simp: ord_spmf_eqD_emeasure) subsection \CCPO structure for the flat ccpo @{term "ord_option op ="}\ @@ -1224,7 +1223,7 @@ definition lub_spmf :: "'a spmf" where "lub_spmf = embed_spmf (\x. enn2real (SUP p : Y. ennreal (spmf p x)))" - \ \We go through @{typ ennreal} to have a sensible definition even if @{term Y} is empty.\ + \ \We go through @{typ ennreal} to have a sensible definition even if @{term Y} is empty.\ lemma lub_spmf_empty [simp]: "SPMF.lub_spmf {} = return_pmf None" by(simp add: SPMF.lub_spmf_def bot_ereal_def) @@ -1259,18 +1258,18 @@ proof(rule spmf_eqI) fix i from le have le': "\x. spmf p x \ spmf q x" by(rule ord_spmf_eq_leD) - have "(\\<^sup>+ x. ennreal (spmf q x) - spmf p x \count_space UNIV) = + have "(\\<^sup>+ x. ennreal (spmf q x) - spmf p x \count_space UNIV) = (\\<^sup>+ x. spmf q x \count_space UNIV) - (\\<^sup>+ x. spmf p x \count_space UNIV)" by(subst nn_integral_diff)(simp_all add: AE_count_space le' nn_integral_spmf_neq_top) also have "\ = (1 - pmf q None) - (1 - pmf p None)" unfolding pmf_None_eq_weight_spmf by(simp add: weight_spmf_eq_nn_integral_spmf[symmetric] ennreal_minus) also have "\ = 0" using None by simp - finally have "\x. spmf q x \ spmf p x" + finally have "\x. spmf q x \ spmf p x" by(simp add: nn_integral_0_iff_AE AE_count_space ennreal_minus ennreal_eq_0_iff) with le' show "spmf p i = spmf q i" by(rule antisym) qed -lemma ord_spmf_eqD_pmf_None: +lemma ord_spmf_eqD_pmf_None: assumes "ord_spmf op = x y" shows "pmf x None \ pmf y None" using assms @@ -1283,7 +1282,7 @@ Chains on @{typ "'a spmf"} maintain countable support. Thanks to Johannes Hölzl for the proof idea. \ -lemma spmf_chain_countable: "countable (\p\Y. set_spmf p)" +lemma spmf_chain_countable: "countable (\p\Y. set_spmf p)" proof(cases "Y = {}") case Y: False show ?thesis @@ -1295,13 +1294,13 @@ next case False define N :: "'a option pmf \ real" where "N p = pmf p None" for p - + have N_less_imp_le_spmf: "\ x \ Y; y \ Y; N y < N x \ \ ord_spmf op = x y" for x y using chainD[OF chain, of x y] ord_spmf_eqD_pmf_None[of x y] ord_spmf_eqD_pmf_None[of y x] by (auto simp: N_def) have N_eq_imp_eq: "\ x \ Y; y \ Y; N y = N x \ \ x = y" for x y using chainD[OF chain, of x y] by(auto simp add: N_def dest: ord_spmf_eq_pmf_None_eq) - + have NC: "N ` Y \ {}" "bdd_below (N ` Y)" using \Y \ {}\ by(auto intro!: bdd_belowI[of _ 0] simp: N_def) have NC_less: "Inf (N ` Y) < N x" if "x \ Y" for x unfolding cInf_less_iff[OF NC] @@ -1314,12 +1313,12 @@ by cases(auto dest: N_less_imp_le_spmf N_eq_imp_eq intro: ord_spmf_reflI) } with False \x \ Y\ show False by blast qed - + from NC have "Inf (N ` Y) \ closure (N ` Y)" by (intro closure_contains_Inf) then obtain X' where "\n. X' n \ N ` Y" and X': "X' \ Inf (N ` Y)" unfolding closure_sequential by auto then obtain X where X: "\n. X n \ Y" and "X' = (\n. N (X n))" unfolding image_iff Bex_def by metis - + with X' have seq: "(\n. N (X n)) \ Inf (N ` Y)" by simp have "(\x \ Y. set_spmf x) \ (\n. set_spmf (X n))" proof(rule UN_least) @@ -1343,7 +1342,7 @@ let ?B = "\p\Y. set_spmf p" have countable: "countable ?B" by(rule spmf_chain_countable) - have "(\\<^sup>+ x. (SUP p:Y. ennreal (spmf p x)) \count_space UNIV) = + have "(\\<^sup>+ x. (SUP p:Y. ennreal (spmf p x)) \count_space UNIV) = (\\<^sup>+ x. (SUP p:Y. ennreal (spmf p x) * indicator ?B x) \count_space UNIV)" by(intro nn_integral_cong SUP_cong)(auto split: split_indicator simp add: spmf_eq_0_set_spmf) also have "\ = (\\<^sup>+ x. (SUP p:Y. ennreal (spmf p x)) \count_space ?B)" @@ -1481,8 +1480,10 @@ from assms obtain p where p: "p \ Y" by auto from chain have chain': "Complete_Partial_Order.chain op \ (measure_spmf ` Y)" by(rule chain_imageI)(rule ord_spmf_eqD_measure_spmf) - show "sets ?lhs = sets ?rhs" and "emeasure ?lhs A = emeasure ?rhs A" for A - using chain' Y p by(simp_all add: sets_SUP emeasure_SUP emeasure_lub_spmf) + show "sets ?lhs = sets ?rhs" + using Y by (subst sets_SUP) auto + show "emeasure ?lhs A = emeasure ?rhs A" for A + using chain' Y p by (subst emeasure_SUP_chain) (auto simp: emeasure_lub_spmf) qed end @@ -1552,11 +1553,11 @@ ultimately show "ord_spmf op = (bind_spmf (B f) (\y. C y f)) (bind_spmf (B g) (\y'. C y' g))" by(rule bind_spmf_mono') qed - + lemma monotone_bind_spmf1: "monotone (ord_spmf op =) (ord_spmf op =) (\y. bind_spmf y g)" by(rule monotoneI)(simp add: bind_spmf_mono' ord_spmf_reflI) -lemma monotone_bind_spmf2: +lemma monotone_bind_spmf2: assumes g: "\x. monotone ord (ord_spmf op =) (\y. g y x)" shows "monotone ord (ord_spmf op =) (\y. bind_spmf p (g y))" by(rule monotoneI)(auto intro: bind_spmf_mono' monotoneD[OF g] ord_spmf_reflI) @@ -1611,7 +1612,7 @@ using chain by(rule chain_imageI)(auto simp add: le_fun_def dest: ord_spmf_eq_leD monotoneD[OF g] intro!: mult_left_mono) have chain''': "Complete_Partial_Order.chain (ord_spmf op =) ((\p. bind_spmf x (\y. g y p)) ` Y)" using chain by(rule chain_imageI)(rule monotone_bind_spmf2[OF g, THEN monotoneD]) - + have "ennreal (spmf ?lhs i) = \\<^sup>+ y. (SUP p:Y. ennreal (spmf x y * spmf (g y p) i)) \count_space (set_spmf x)" by(simp add: ennreal_spmf_bind ennreal_spmf_lub_spmf[OF chain'] Y nn_integral_measure_spmf' SUP_mult_left_ennreal ennreal_mult) also have "\ = (SUP p:Y. \\<^sup>+ y. ennreal (spmf x y * spmf (g y p) i) \count_space (set_spmf x))" @@ -1707,7 +1708,7 @@ locale rel_spmf_characterisation = assumes rel_pmf_measureI: - "\(R :: 'a option \ 'b option \ bool) p q. + "\(R :: 'a option \ 'b option \ bool) p q. (\A. measure (measure_pmf p) A \ measure (measure_pmf q) {y. \x\A. R x y}) \ rel_pmf R p q" \ \This assumption is shown to hold in general in the AFP entry \MFMC_Countable\.\ @@ -1911,7 +1912,7 @@ subsection \Subprobability distributions of sets\ definition spmf_of_set :: "'a set \ 'a spmf" -where +where "spmf_of_set A = (if finite A \ A \ {} then spmf_of_pmf (pmf_of_set A) else return_pmf None)" lemma spmf_of_set: "spmf (spmf_of_set A) x = indicator A x / card A" @@ -1933,7 +1934,7 @@ "inj_on f A \ map_spmf f (spmf_of_set A) = spmf_of_set (f ` A)" by(auto simp add: spmf_of_set_def map_pmf_of_set_inj dest: finite_imageD) -lemma spmf_of_pmf_pmf_of_set [simp]: +lemma spmf_of_pmf_pmf_of_set [simp]: "\ finite A; A \ {} \ \ spmf_of_pmf (pmf_of_set A) = spmf_of_set A" by(simp add: spmf_of_set_def) @@ -2001,7 +2002,7 @@ lemma rel_pmf_of_set_bij: assumes f: "bij_betw f A B" and A: "A \ {}" "finite A" - and B: "B \ {}" "finite B" + and B: "B \ {}" "finite B" and R: "\x. x \ A \ R x (f x)" shows "rel_pmf R (pmf_of_set A) (pmf_of_set B)" proof(rule pmf.rel_mono_strong) @@ -2056,7 +2057,7 @@ by(auto intro: arg_cong[where f=card]) also have "\ = (if i then card (B \ A) / card B else (card B - card (B \ A)) / card B)" by(auto simp add: card_Diff_subset_Int assms) - also have "\ = ennreal (spmf ?rhs i)" + also have "\ = ennreal (spmf ?rhs i)" by(simp add: assms card_gt_0_iff field_simps card_mono Int_commute of_nat_diff) finally show "spmf ?lhs i = spmf ?rhs i" by simp qed @@ -2233,7 +2234,7 @@ apply(auto simp add: max_def min_def ennreal_mult[symmetric] not_le ennreal_lt_0) done -lemma measure_spmf_scale_spmf': +lemma measure_spmf_scale_spmf': "r \ 1 \ measure_spmf (scale_spmf r p) = scale_measure r (measure_spmf p)" unfolding measure_spmf_scale_spmf apply(cases "weight_spmf p > 0") @@ -2250,7 +2251,7 @@ lemma scale_spmf_0 [simp]: "scale_spmf 0 p = return_pmf None" by(rule spmf_eqI)(simp add: spmf_scale_spmf min_def max_def weight_spmf_le_0) -lemma bind_scale_spmf: +lemma bind_scale_spmf: assumes r: "r \ 1" shows "bind_spmf (scale_spmf r p) f = bind_spmf p (\x. scale_spmf r (f x))" (is "?lhs = ?rhs") @@ -2262,7 +2263,7 @@ thus "spmf ?lhs x = spmf ?rhs x" by simp qed -lemma scale_bind_spmf: +lemma scale_bind_spmf: assumes "r \ 1" shows "scale_spmf r (bind_spmf p f) = bind_spmf p (\x. scale_spmf r (f x))" (is "?lhs = ?rhs") @@ -2298,7 +2299,7 @@ lemma set_scale_spmf' [simp]: "0 < r \ set_spmf (scale_spmf r p) = set_spmf p" by(simp add: set_scale_spmf) -lemma rel_spmf_scaleI: +lemma rel_spmf_scaleI: assumes "r > 0 \ rel_spmf A p q" shows "rel_spmf A (scale_spmf r p) (scale_spmf r q)" proof(cases "r > 0") @@ -2319,7 +2320,7 @@ thus ?thesis by(auto simp add: min_def max_def ennreal_mult[symmetric] split: if_split_asm) qed -lemma weight_scale_spmf' [simp]: +lemma weight_scale_spmf' [simp]: "\ 0 \ r; r \ 1 \ \ weight_spmf (scale_spmf r p) = r * weight_spmf p" by(simp add: weight_scale_spmf max_def min_def)(metis antisym_conv mult_left_le order_trans weight_spmf_le_1) @@ -2327,7 +2328,7 @@ "pmf (scale_spmf k p) None = 1 - min 1 (max 0 k * (1 - pmf p None))" unfolding pmf_None_eq_weight_spmf by(simp add: weight_scale_spmf) -lemma scale_scale_spmf: +lemma scale_scale_spmf: "scale_spmf r (scale_spmf r' p) = scale_spmf (r * max 0 (min (inverse (weight_spmf p)) r')) p" (is "?lhs = ?rhs") proof(rule spmf_eqI) @@ -2432,7 +2433,7 @@ lemma set_pair_spmf [simp]: "set_spmf (pair_spmf p q) = set_spmf p \ set_spmf q" by(auto 4 3 simp add: pair_spmf_def set_spmf_bind_pmf bind_UNION in_set_spmf intro: rev_bexI split: option.splits) - + lemma spmf_pair [simp]: "spmf (pair_spmf p q) (x, y) = spmf p x * spmf q y" (is "?lhs = ?rhs") proof - have "ennreal ?lhs = \\<^sup>+ a. \\<^sup>+ b. indicator {(x, y)} (a, b) \measure_spmf q \measure_spmf p" @@ -2483,8 +2484,8 @@ by(simp add: pair_spmf_return_spmf1) lemma rel_pair_spmf_prod: - "rel_spmf (rel_prod A B) (pair_spmf p q) (pair_spmf p' q') \ - rel_spmf A (scale_spmf (weight_spmf q) p) (scale_spmf (weight_spmf q') p') \ + "rel_spmf (rel_prod A B) (pair_spmf p q) (pair_spmf p' q') \ + rel_spmf A (scale_spmf (weight_spmf q) p) (scale_spmf (weight_spmf q') p') \ rel_spmf B (scale_spmf (weight_spmf p) q) (scale_spmf (weight_spmf p') q')" (is "?lhs \ ?rhs" is "_ \ ?A \ ?B" is "_ \ rel_spmf _ ?p ?p' \ rel_spmf _ ?q ?q'") proof(intro iffI conjI) @@ -2506,7 +2507,7 @@ moreover have "(weight_spmf p * weight_spmf q) * (weight_spmf p * weight_spmf q) \ (1 * 1) * (1 * 1)" by(intro mult_mono)(simp_all add: weight_spmf_nonneg weight_spmf_le_1) ultimately have "(weight_spmf p * weight_spmf q) * (weight_spmf p * weight_spmf q) = 1" by simp - hence *: "weight_spmf p * weight_spmf q = 1" + hence *: "weight_spmf p * weight_spmf q = 1" by(metis antisym_conv less_le mult_less_cancel_left1 weight_pair_spmf weight_spmf_le_1 weight_spmf_nonneg) hence "weight_spmf p = 1" by(metis antisym_conv mult_left_le weight_spmf_le_1 weight_spmf_nonneg) moreover with * have "weight_spmf q = 1" by simp @@ -2526,7 +2527,7 @@ have [simp]: "snd \ ?f = map_prod snd snd" by(simp add: fun_eq_iff) from \?rhs\ have eq: "weight_spmf p * weight_spmf q = weight_spmf p' * weight_spmf q'" by(auto dest!: rel_spmf_weightD simp add: weight_spmf_le_1 weight_spmf_nonneg) - + have "map_spmf snd ?pq = scale_spmf ?r (pair_spmf ?p' ?q')" by(simp add: pair_map_spmf[symmetric] p' q' map_scale_spmf spmf.map_comp) also have "\ = pair_spmf p' q'" using full[of p' q'] eq @@ -2546,24 +2547,24 @@ let ?f = "(\((x, y), (x', y')). (x, x'))" let ?pq = "map_spmf ?f pq" have [simp]: "fst \ ?f = fst \ fst" by(simp add: split_def o_def) - show "map_spmf fst ?pq = scale_spmf (weight_spmf q) p" using pq + show "map_spmf fst ?pq = scale_spmf (weight_spmf q) p" using pq by(simp add: spmf.map_comp)(simp add: spmf.map_comp[symmetric]) have [simp]: "snd \ ?f = fst \ snd" by(simp add: split_def o_def) - show "map_spmf snd ?pq = scale_spmf (weight_spmf q') p'" using pq' + show "map_spmf snd ?pq = scale_spmf (weight_spmf q') p'" using pq' by(simp add: spmf.map_comp)(simp add: spmf.map_comp[symmetric]) qed(auto dest: * ) - + show ?B proof let ?f = "(\((x, y), (x', y')). (y, y'))" let ?pq = "map_spmf ?f pq" have [simp]: "fst \ ?f = snd \ fst" by(simp add: split_def o_def) - show "map_spmf fst ?pq = scale_spmf (weight_spmf p) q" using pq + show "map_spmf fst ?pq = scale_spmf (weight_spmf p) q" using pq by(simp add: spmf.map_comp)(simp add: spmf.map_comp[symmetric]) have [simp]: "snd \ ?f = snd \ snd" by(simp add: split_def o_def) - show "map_spmf snd ?pq = scale_spmf (weight_spmf p') q'" using pq' + show "map_spmf snd ?pq = scale_spmf (weight_spmf p') q'" using pq' by(simp add: spmf.map_comp)(simp add: spmf.map_comp[symmetric]) qed(auto dest: * ) qed @@ -2650,7 +2651,7 @@ lemma rel_spmf_try_spmf: "\ rel_spmf R p p'; \ lossless_spmf p' \ rel_spmf R q q' \ \ rel_spmf R (TRY p ELSE q) (TRY p' ELSE q')" -unfolding try_spmf_def +unfolding try_spmf_def apply(rule rel_pmf_bindI[where R="\x y. rel_option R x y \ x \ set_pmf p \ y \ set_pmf p'"]) apply(erule pmf.rel_mono_strong; simp) apply(auto split: option.split simp add: lossless_iff_set_pmf_None) diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Probability/Set_Integral.thy --- a/src/HOL/Probability/Set_Integral.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Probability/Set_Integral.thy Tue Jun 21 15:10:43 2016 +0200 @@ -1,5 +1,5 @@ (* Title: HOL/Probability/Set_Integral.thy - Author: Jeremy Avigad, Johannes Hölzl, Luke Serafin + Author: Jeremy Avigad (CMU), Johannes Hölzl (TUM), Luke Serafin (CMU) Notation and useful facts for working with integrals over a set. diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Probability/Sigma_Algebra.thy --- a/src/HOL/Probability/Sigma_Algebra.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Probability/Sigma_Algebra.thy Tue Jun 21 15:10:43 2016 +0200 @@ -2002,86 +2002,6 @@ using emeasure_extend_measure[OF M _ _ ms(2,3), of "(i,j)"] eq ms(1) \I i j\ by (auto simp: subset_eq) -subsubsection \Supremum of a set of $\sigma$-algebras\ - -definition "Sup_sigma M = sigma (\x\M. space x) (\x\M. sets x)" - -syntax - "_SUP_sigma" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\\<^sub>\ _\_./ _)" [0, 0, 10] 10) - -translations - "\\<^sub>\ x\A. B" == "CONST Sup_sigma ((\x. B) ` A)" - -lemma space_Sup_sigma: "space (Sup_sigma M) = (\x\M. space x)" - unfolding Sup_sigma_def by (rule space_measure_of) (auto dest: sets.sets_into_space) - -lemma sets_Sup_sigma: "sets (Sup_sigma M) = sigma_sets (\x\M. space x) (\x\M. sets x)" - unfolding Sup_sigma_def by (rule sets_measure_of) (auto dest: sets.sets_into_space) - -lemma in_Sup_sigma: "m \ M \ A \ sets m \ A \ sets (Sup_sigma M)" - unfolding sets_Sup_sigma by auto - -lemma SUP_sigma_cong: - assumes *: "\i. i \ I \ sets (M i) = sets (N i)" shows "sets (\\<^sub>\ i\I. M i) = sets (\\<^sub>\ i\I. N i)" - using * sets_eq_imp_space_eq[OF *] by (simp add: Sup_sigma_def) - -lemma sets_Sup_in_sets: - assumes "M \ {}" - assumes "\m. m \ M \ space m = space N" - assumes "\m. m \ M \ sets m \ sets N" - shows "sets (Sup_sigma M) \ sets N" -proof - - have *: "UNION M space = space N" - using assms by auto - show ?thesis - unfolding sets_Sup_sigma * using assms by (auto intro!: sets.sigma_sets_subset) -qed - -lemma measurable_Sup_sigma1: - assumes m: "m \ M" and f: "f \ measurable m N" - and const_space: "\m n. m \ M \ n \ M \ space m = space n" - shows "f \ measurable (Sup_sigma M) N" -proof - - have "space (Sup_sigma M) = space m" - using m by (auto simp add: space_Sup_sigma dest: const_space) - then show ?thesis - using m f unfolding measurable_def by (auto intro: in_Sup_sigma) -qed - -lemma measurable_Sup_sigma2: - assumes M: "M \ {}" - assumes f: "\m. m \ M \ f \ measurable N m" - shows "f \ measurable N (Sup_sigma M)" - unfolding Sup_sigma_def -proof (rule measurable_measure_of) - show "f \ space N \ UNION M space" - using measurable_space[OF f] M by auto -qed (auto intro: measurable_sets f dest: sets.sets_into_space) - -lemma Sup_sigma_sigma: - assumes [simp]: "M \ {}" and M: "\m. m \ M \ m \ Pow \" - shows "(\\<^sub>\ m\M. sigma \ m) = sigma \ (\M)" -proof (rule measure_eqI) - { fix a m assume "a \ sigma_sets \ m" "m \ M" - then have "a \ sigma_sets \ (\M)" - by induction (auto intro: sigma_sets.intros) } - then show "sets (\\<^sub>\ m\M. sigma \ m) = sets (sigma \ (\M))" - apply (simp add: sets_Sup_sigma space_measure_of_conv M Union_least) - apply (rule sigma_sets_eqI) - apply auto - done -qed (simp add: Sup_sigma_def emeasure_sigma) - -lemma SUP_sigma_sigma: - assumes M: "M \ {}" "\m. m \ M \ f m \ Pow \" - shows "(\\<^sub>\ m\M. sigma \ (f m)) = sigma \ (\m\M. f m)" -proof - - have "Sup_sigma (sigma \ ` f ` M) = sigma \ (\(f ` M))" - using M by (intro Sup_sigma_sigma) auto - then show ?thesis - by (simp add: image_image) -qed - subsection \The smallest $\sigma$-algebra regarding a function\ definition @@ -2157,31 +2077,6 @@ by (simp add: sets_vimage_algebra2 ex_simps[symmetric] vimage_comp comp_def del: ex_simps) qed (simp add: vimage_algebra_def emeasure_sigma) -lemma sets_vimage_Sup_eq: - assumes *: "M \ {}" "\m. m \ M \ f \ X \ space m" - shows "sets (vimage_algebra X f (Sup_sigma M)) = sets (\\<^sub>\ m \ M. vimage_algebra X f m)" - (is "?IS = ?SI") -proof - show "?IS \ ?SI" - by (intro sets_image_in_sets measurable_Sup_sigma2 measurable_Sup_sigma1) - (auto simp: space_Sup_sigma measurable_vimage_algebra1 *) - { fix m assume "m \ M" - moreover then have "f \ X \ space (Sup_sigma M)" "f \ X \ space m" - using * by (auto simp: space_Sup_sigma) - ultimately have "f \ measurable (vimage_algebra X f (Sup_sigma M)) m" - by (auto simp add: measurable_def sets_vimage_algebra2 intro: in_Sup_sigma) } - then show "?SI \ ?IS" - by (auto intro!: sets_image_in_sets sets_Sup_in_sets del: subsetI simp: *) -qed - -lemma vimage_algebra_Sup_sigma: - assumes [simp]: "MM \ {}" and "\M. M \ MM \ f \ X \ space M" - shows "vimage_algebra X f (Sup_sigma MM) = Sup_sigma (vimage_algebra X f ` MM)" -proof (rule measure_eqI) - show "sets (vimage_algebra X f (Sup_sigma MM)) = sets (Sup_sigma (vimage_algebra X f ` MM))" - using assms by (rule sets_vimage_Sup_eq) -qed (simp add: vimage_algebra_def Sup_sigma_def emeasure_sigma) - subsubsection \Restricted Space Sigma Algebra\ definition restrict_space where diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Probability/Sinc_Integral.thy --- a/src/HOL/Probability/Sinc_Integral.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Probability/Sinc_Integral.thy Tue Jun 21 15:10:43 2016 +0200 @@ -1,6 +1,6 @@ -(* - Theory: Sinc_Integral.thy - Authors: Jeremy Avigad, Luke Serafin, Johannes Hölzl +(* Title: HOL/Probability/Sinc_Integral.thy + Authors: Jeremy Avigad (CMU), Luke Serafin (CMU) + Authors: Johannes Hölzl, TU München *) section \Integral of sinc\ diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Probability/Stream_Space.thy --- a/src/HOL/Probability/Stream_Space.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Probability/Stream_Space.thy Tue Jun 21 15:10:43 2016 +0200 @@ -94,16 +94,16 @@ shows "(\x. f x ## g x) \ measurable N (stream_space M)" by (rule measurable_stream_space2) (simp add: Stream_snth) -lemma measurable_smap[measurable]: +lemma measurable_smap[measurable]: assumes X[measurable]: "X \ measurable N M" shows "smap X \ measurable (stream_space N) (stream_space M)" by (rule measurable_stream_space2) simp -lemma measurable_stake[measurable]: +lemma measurable_stake[measurable]: "stake i \ measurable (stream_space (count_space UNIV)) (count_space (UNIV :: 'a::countable list set))" by (induct i) auto -lemma measurable_shift[measurable]: +lemma measurable_shift[measurable]: assumes f: "f \ measurable N (stream_space M)" assumes [measurable]: "g \ measurable N (stream_space M)" shows "(\x. stake n (f x) @- g x) \ measurable N (stream_space M)" @@ -168,7 +168,7 @@ lemma (in prob_space) nn_integral_stream_space: assumes [measurable]: "f \ borel_measurable (stream_space M)" shows "(\\<^sup>+X. f X \stream_space M) = (\\<^sup>+x. (\\<^sup>+X. f (x ## X) \stream_space M) \M)" -proof - +proof - interpret S: sequence_space M .. interpret P: pair_sigma_finite M "\\<^sub>M i::nat\UNIV. M" .. @@ -230,7 +230,7 @@ apply (simp add: AE_iff_nn_integral[symmetric]) done qed - + lemma (in prob_space) AE_stream_all: assumes [measurable]: "Measurable.pred M P" and P: "AE x in M. P x" shows "AE x in stream_space M. stream_all P x" @@ -271,14 +271,14 @@ assumes sets: "\i. (\x. x !! i) \ measurable N M" shows "sets (stream_space M) \ sets N" unfolding stream_space_def sets_distr - by (auto intro!: sets_image_in_sets measurable_Sup_sigma2 measurable_vimage_algebra2 del: subsetI equalityI + by (auto intro!: sets_image_in_sets measurable_Sup2 measurable_vimage_algebra2 del: subsetI equalityI simp add: sets_PiM_eq_proj snth_in space sets cong: measurable_cong_sets) lemma sets_stream_space_eq: "sets (stream_space M) = - sets (\\<^sub>\ i\UNIV. vimage_algebra (streams (space M)) (\s. s !! i) M)" + sets (SUP i:UNIV. vimage_algebra (streams (space M)) (\s. s !! i) M)" by (auto intro!: sets_stream_space_in_sets sets_Sup_in_sets sets_image_in_sets - measurable_Sup_sigma1 snth_in measurable_vimage_algebra1 del: subsetI - simp: space_Sup_sigma space_stream_space) + measurable_Sup1 snth_in measurable_vimage_algebra1 del: subsetI + simp: space_Sup_eq_UN space_stream_space) lemma sets_restrict_stream_space: assumes S[measurable]: "S \ sets M" @@ -288,17 +288,17 @@ apply (simp add: space_stream_space streams_mono2) apply (subst vimage_algebra_cong[OF refl refl sets_stream_space_eq]) apply (subst sets_stream_space_eq) - apply (subst sets_vimage_Sup_eq) + apply (subst sets_vimage_Sup_eq[where Y="streams (space M)"]) apply simp + apply auto [] apply (auto intro: streams_mono) [] + apply auto [] apply (simp add: image_image space_restrict_space) - apply (intro SUP_sigma_cong) apply (simp add: vimage_algebra_cong[OF refl refl restrict_space_eq_vimage_algebra]) apply (subst (1 2) vimage_algebra_vimage_algebra_eq) - apply (auto simp: streams_mono snth_in) + apply (auto simp: streams_mono snth_in ) done - primrec sstart :: "'a set \ 'a list \ 'a stream set" where "sstart S [] = streams S" | [simp del]: "sstart S (x # xs) = op ## x ` sstart S xs" diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Probability/Weak_Convergence.thy --- a/src/HOL/Probability/Weak_Convergence.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Probability/Weak_Convergence.thy Tue Jun 21 15:10:43 2016 +0200 @@ -1,6 +1,5 @@ -(* - Theory: Weak_Convergence.thy - Authors: Jeremy Avigad, Luke Serafin +(* Title: HOL/Probability/Weak_Convergence.thy + Authors: Jeremy Avigad (CMU), Johannes Hölzl (TUM) *) section \Weak Convergence of Functions and Distributions\ diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Real.thy --- a/src/HOL/Real.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Real.thy Tue Jun 21 15:10:43 2016 +0200 @@ -10,7 +10,7 @@ section \Development of the Reals using Cauchy Sequences\ theory Real -imports Rat Conditionally_Complete_Lattices +imports Rat begin text \ @@ -961,7 +961,6 @@ qed end - subsection \Hiding implementation details\ hide_const (open) vanishes cauchy positive Real diff -r ae9330fdbc16 -r 94c6e3ed0afb src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Tue Jun 21 14:42:47 2016 +0200 +++ b/src/HOL/Topological_Spaces.thy Tue Jun 21 15:10:43 2016 +0200 @@ -6,7 +6,7 @@ section \Topological Spaces\ theory Topological_Spaces -imports Main Conditionally_Complete_Lattices +imports Main begin named_theorems continuous_intros "structural introduction rules for continuity" @@ -1802,6 +1802,58 @@ "continuous (at (x::'a::linorder_topology)) f = (continuous (at_left x) f \ continuous (at_right x) f)" by (simp add: continuous_within filterlim_at_split) +(* The following open/closed Collect lemmas are ported from Sébastien Gouëzel's Ergodic_Theory *) +lemma open_Collect_neq: + fixes f g :: "'a :: topological_space \ 'b::t2_space" + assumes f: "continuous_on UNIV f" and g: "continuous_on UNIV g" + shows "open {x. f x \ g x}" +proof (rule openI) + fix t assume "t \ {x. f x \ g x}" + then obtain U V where *: "open U" "open V" "f t \ U" "g t \ V" "U \ V = {}" + by (auto simp add: separation_t2) + with open_vimage[OF \open U\ f] open_vimage[OF \open V\ g] + show "\T. open T \ t \ T \ T \ {x. f x \ g x}" + by (intro exI[of _ "f -` U \ g -` V"]) auto +qed + +lemma closed_Collect_eq: + fixes f g :: "'a :: topological_space \ 'b::t2_space" + assumes f: "continuous_on UNIV f" and g: "continuous_on UNIV g" + shows "closed {x. f x = g x}" + using open_Collect_neq[OF f g] by (simp add: closed_def Collect_neg_eq) + +lemma open_Collect_less: + fixes f g :: "'a :: topological_space \ 'b::linorder_topology" + assumes f: "continuous_on UNIV f" and g: "continuous_on UNIV g" + shows "open {x. f x < g x}" +proof (rule openI) + fix t assume t: "t \ {x. f x < g x}" + show "\T. open T \ t \ T \ T \ {x. f x < g x}" + proof (cases) + assume "\z. f t < z \ z < g t" + then obtain z where z: "f t < z \ z < g t" by blast + then show ?thesis + using open_vimage[OF _ f, of "{..< z}"] open_vimage[OF _ g, of "{z <..}"] + by (intro exI[of _ "f -` {.. g -` {z<..}"]) auto + next + assume "\(\z. f t < z \ z < g t)" + then have *: "{g t ..} = {f t <..}" "{..< g t} = {.. f t}" + using t by (auto intro: leI) + show ?thesis + using open_vimage[OF _ f, of "{..< g t}"] open_vimage[OF _ g, of "{f t <..}"] t + apply (intro exI[of _ "f -` {..< g t} \ g -` {f t<..}"]) + apply (simp add: open_Int) + apply (auto simp add: *) + done + qed +qed + +lemma closed_Collect_le: + fixes f g :: "'a :: topological_space \ 'b::linorder_topology" + assumes f: "continuous_on UNIV f" and g: "continuous_on UNIV g" + shows "closed {x. f x \ g x}" + using open_Collect_less[OF g f] by (simp add: closed_def Collect_neg_eq[symmetric] not_le) + subsubsection \Open-cover compactness\ context topological_space diff -r ae9330fdbc16 -r 94c6e3ed0afb src/Pure/Tools/ci_profile.scala --- a/src/Pure/Tools/ci_profile.scala Tue Jun 21 14:42:47 2016 +0200 +++ b/src/Pure/Tools/ci_profile.scala Tue Jun 21 15:10:43 2016 +0200 @@ -7,6 +7,9 @@ package isabelle +import java.util.{Properties => JProperties} + + abstract class CI_Profile extends Isabelle_Tool.Body { @@ -39,10 +42,22 @@ } } + private def load_properties(): JProperties = + { + val props = new JProperties() + val file = Path.explode(Isabelle_System.getenv_strict("ISABELLE_CI_PROPERTIES")).file + if (file.exists()) + props.load(new java.io.FileReader(file)) + props + } + override final def apply(args: List[String]): Unit = { List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS").foreach(print_variable) + val props = load_properties() + System.getProperties().putAll(props) + val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME")) println(s"Build for Isabelle id ${hg_id(isabelle_home)}")