# HG changeset patch # User Angeliki KoutsoukouArgyraki # Date 1547467159 0 # Node ID 3417a8f154ebc69f9a370c8203cdf9e6c5f963d9 # Parent e61b0b819d288bb01c7df55fad9935dd715cc6b4 updated tagging first 5 diff -r e61b0b819d28 -r 3417a8f154eb src/HOL/Analysis/Arcwise_Connected.thy --- a/src/HOL/Analysis/Arcwise_Connected.thy Sun Jan 13 20:25:41 2019 +0100 +++ b/src/HOL/Analysis/Arcwise_Connected.thy Mon Jan 14 11:59:19 2019 +0000 @@ -10,12 +10,12 @@ subsection%important \The Brouwer reduction theorem\ -theorem%important Brouwer_reduction_theorem_gen: +theorem Brouwer_reduction_theorem_gen: fixes S :: "'a::euclidean_space set" assumes "closed S" "\ S" and \: "\F. \\n. closed(F n); \n. \(F n); \n. F(Suc n) \ F n\ \ \(\range F)" obtains T where "T \ S" "closed T" "\ T" "\U. \U \ S; closed U; \ U\ \ \ (U \ T)" -proof%unimportant - +proof - obtain B :: "nat \ 'a set" where "inj B" "\n. open(B n)" and open_cov: "\S. open S \ \K. S = \(B ` K)" by (metis Setcompr_eq_image that univ_second_countable_sequence) @@ -78,13 +78,13 @@ qed qed -corollary%important Brouwer_reduction_theorem: +corollary Brouwer_reduction_theorem: fixes S :: "'a::euclidean_space set" assumes "compact S" "\ S" "S \ {}" and \: "\F. \\n. compact(F n); \n. F n \ {}; \n. \(F n); \n. F(Suc n) \ F n\ \ \(\range F)" obtains T where "T \ S" "compact T" "T \ {}" "\ T" "\U. \U \ S; closed U; U \ {}; \ U\ \ \ (U \ T)" -proof%unimportant (rule Brouwer_reduction_theorem_gen [of S "\T. T \ {} \ T \ S \ \ T"]) +proof (rule Brouwer_reduction_theorem_gen [of S "\T. T \ {} \ T \ S \ \ T"]) fix F assume cloF: "\n. closed (F n)" and F: "\n. F n \ {} \ F n \ S \ \ (F n)" and Fsub: "\n. F (Suc n) \ F n" @@ -106,14 +106,14 @@ qed (meson assms compact_imp_closed seq_compact_closed_subset seq_compact_eq_compact)+ -subsection%important\Arcwise Connections\(*FIX ME this subsection is empty(?) *) +subsection%unimportant\Arcwise Connections\(*FIX ME this subsection is empty(?) *) subsection%important\Density of points with dyadic rational coordinates\ -proposition%important closure_dyadic_rationals: +proposition closure_dyadic_rationals: "closure (\k. \f \ Basis \ \. { \i :: 'a :: euclidean_space \ Basis. (f i / 2^k) *\<^sub>R i }) = UNIV" -proof%unimportant - +proof - have "x \ closure (\k. \f \ Basis \ \. {\i \ Basis. (f i / 2^k) *\<^sub>R i})" for x::'a proof (clarsimp simp: closure_approachable) fix e::real @@ -151,9 +151,9 @@ then show ?thesis by auto qed -corollary%important closure_rational_coordinates: +corollary closure_rational_coordinates: "closure (\f \ Basis \ \. { \i :: 'a :: euclidean_space \ Basis. f i *\<^sub>R i }) = UNIV" -proof%unimportant - +proof - have *: "(\k. \f \ Basis \ \. { \i::'a \ Basis. (f i / 2^k) *\<^sub>R i }) \ (\f \ Basis \ \. { \i \ Basis. f i *\<^sub>R i })" proof clarsimp @@ -167,7 +167,7 @@ using closure_dyadic_rationals closure_mono [OF *] by blast qed -lemma%unimportant closure_dyadic_rationals_in_convex_set: +lemma closure_dyadic_rationals_in_convex_set: "\convex S; interior S \ {}\ \ closure(S \ (\k. \f \ Basis \ \. @@ -175,7 +175,7 @@ closure S" by (simp add: closure_dyadic_rationals closure_convex_Int_superset) -lemma%unimportant closure_rationals_in_convex_set: +lemma closure_rationals_in_convex_set: "\convex S; interior S \ {}\ \ closure(S \ (\f \ Basis \ \. { \i :: 'a :: euclidean_space \ Basis. f i *\<^sub>R i })) = closure S" @@ -186,11 +186,11 @@ path connection is equivalent to arcwise connection for distinct points. The proof is based on Whyburn's "Topological Analysis".\ -lemma%important closure_dyadic_rationals_in_convex_set_pos_1: +lemma closure_dyadic_rationals_in_convex_set_pos_1: fixes S :: "real set" assumes "convex S" and intnz: "interior S \ {}" and pos: "\x. x \ S \ 0 \ x" shows "closure(S \ (\k m. {of_nat m / 2^k})) = closure S" -proof%unimportant - +proof - have "\m. f 1/2^k = real m / 2^k" if "(f 1) / 2^k \ S" "f 1 \ \" for k and f :: "real \ real" using that by (force simp: Ints_def zero_le_divide_iff power_le_zero_eq dest: pos zero_le_imp_eq_int) then have "S \ (\k m. {real m / 2^k}) = S \ @@ -201,13 +201,13 @@ qed -definition%important dyadics :: "'a::field_char_0 set" where "dyadics \ \k m. {of_nat m / 2^k}" +definition%unimportant dyadics :: "'a::field_char_0 set" where "dyadics \ \k m. {of_nat m / 2^k}" -lemma%unimportant real_in_dyadics [simp]: "real m \ dyadics" +lemma real_in_dyadics [simp]: "real m \ dyadics" apply (simp add: dyadics_def) by (metis divide_numeral_1 numeral_One power_0) -lemma%unimportant nat_neq_4k1: "of_nat m \ (4 * of_nat k + 1) / (2 * 2^n :: 'a::field_char_0)" +lemma nat_neq_4k1: "of_nat m \ (4 * of_nat k + 1) / (2 * 2^n :: 'a::field_char_0)" proof assume "of_nat m = (4 * of_nat k + 1) / (2 * 2^n :: 'a)" then have "of_nat (m * (2 * 2^n)) = (of_nat (Suc (4 * k)) :: 'a)" @@ -220,8 +220,8 @@ by simp qed -lemma%important nat_neq_4k3: "of_nat m \ (4 * of_nat k + 3) / (2 * 2^n :: 'a::field_char_0)" -proof%unimportant +lemma nat_neq_4k3: "of_nat m \ (4 * of_nat k + 3) / (2 * 2^n :: 'a::field_char_0)" +proof assume "of_nat m = (4 * of_nat k + 3) / (2 * 2^n :: 'a)" then have "of_nat (m * (2 * 2^n)) = (of_nat (4 * k + 3) :: 'a)" by (simp add: divide_simps) @@ -233,10 +233,10 @@ by simp qed -lemma%important iff_4k: +lemma iff_4k: assumes "r = real k" "odd k" shows "(4 * real m + r) / (2 * 2^n) = (4 * real m' + r) / (2 * 2 ^ n') \ m=m' \ n=n'" -proof%unimportant - +proof - { assume "(4 * real m + r) / (2 * 2^n) = (4 * real m' + r) / (2 * 2 ^ n')" then have "real ((4 * m + k) * (2 * 2 ^ n')) = real ((4 * m' + k) * (2 * 2^n))" using assms by (auto simp: field_simps) @@ -253,8 +253,8 @@ then show ?thesis by blast qed -lemma%important neq_4k1_k43: "(4 * real m + 1) / (2 * 2^n) \ (4 * real m' + 3) / (2 * 2 ^ n')" -proof%unimportant +lemma neq_4k1_k43: "(4 * real m + 1) / (2 * 2^n) \ (4 * real m' + 3) / (2 * 2 ^ n')" +proof assume "(4 * real m + 1) / (2 * 2^n) = (4 * real m' + 3) / (2 * 2 ^ n')" then have "real (Suc (4 * m) * (2 * 2 ^ n')) = real ((4 * m' + 3) * (2 * 2^n))" by (auto simp: field_simps) @@ -270,11 +270,11 @@ using even_Suc by presburger qed -lemma%important dyadic_413_cases: +lemma dyadic_413_cases: obtains "(of_nat m::'a::field_char_0) / 2^k \ Nats" | m' k' where "k' < k" "(of_nat m:: 'a) / 2^k = of_nat (4*m' + 1) / 2^Suc k'" | m' k' where "k' < k" "(of_nat m:: 'a) / 2^k = of_nat (4*m' + 3) / 2^Suc k'" -proof%unimportant (cases "m>0") +proof (cases "m>0") case False then have "m=0" by simp with that show ?thesis by auto @@ -323,11 +323,11 @@ qed -lemma%important dyadics_iff: +lemma dyadics_iff: "(dyadics :: 'a::field_char_0 set) = Nats \ (\k m. {of_nat (4*m + 1) / 2^Suc k}) \ (\k m. {of_nat (4*m + 3) / 2^Suc k})" (is "_ = ?rhs") -proof%unimportant +proof show "dyadics \ ?rhs" unfolding dyadics_def apply clarify @@ -344,7 +344,7 @@ qed -function (domintros) dyad_rec :: "[nat \ 'a, 'a\'a, 'a\'a, real] \ 'a" where +function%unimportant (domintros) dyad_rec :: "[nat \ 'a, 'a\'a, 'a\'a, real] \ 'a" where "dyad_rec b l r (real m) = b m" | "dyad_rec b l r ((4 * real m + 1) / 2 ^ (Suc n)) = l (dyad_rec b l r ((2*m + 1) / 2^n))" | "dyad_rec b l r ((4 * real m + 3) / 2 ^ (Suc n)) = r (dyad_rec b l r ((2*m + 1) / 2^n))" @@ -354,14 +354,14 @@ apply (fastforce simp add: dyadics_iff Nats_def field_simps)+ done -lemma%unimportant dyadics_levels: "dyadics = (\K. \k m. {of_nat m / 2^k})" +lemma dyadics_levels: "dyadics = (\K. \k m. {of_nat m / 2^k})" unfolding dyadics_def by auto -lemma%important dyad_rec_level_termination: +lemma dyad_rec_level_termination: assumes "k < K" shows "dyad_rec_dom(b, l, r, real m / 2^k)" using assms -proof%unimportant (induction K arbitrary: k m) +proof (induction K arbitrary: k m) case 0 then show ?case by auto next @@ -426,22 +426,22 @@ qed -lemma%unimportant dyad_rec_termination: "x \ dyadics \ dyad_rec_dom(b,l,r,x)" +lemma dyad_rec_termination: "x \ dyadics \ dyad_rec_dom(b,l,r,x)" by (auto simp: dyadics_levels intro: dyad_rec_level_termination) -lemma%unimportant dyad_rec_of_nat [simp]: "dyad_rec b l r (real m) = b m" +lemma dyad_rec_of_nat [simp]: "dyad_rec b l r (real m) = b m" by (simp add: dyad_rec.psimps dyad_rec_termination) -lemma%unimportant dyad_rec_41 [simp]: "dyad_rec b l r ((4 * real m + 1) / 2 ^ (Suc n)) = l (dyad_rec b l r ((2*m + 1) / 2^n))" +lemma dyad_rec_41 [simp]: "dyad_rec b l r ((4 * real m + 1) / 2 ^ (Suc n)) = l (dyad_rec b l r ((2*m + 1) / 2^n))" apply (rule dyad_rec.psimps) by (metis dyad_rec_level_termination lessI add.commute of_nat_Suc of_nat_mult of_nat_numeral) -lemma%unimportant dyad_rec_43 [simp]: "dyad_rec b l r ((4 * real m + 3) / 2 ^ (Suc n)) = r (dyad_rec b l r ((2*m + 1) / 2^n))" +lemma dyad_rec_43 [simp]: "dyad_rec b l r ((4 * real m + 3) / 2 ^ (Suc n)) = r (dyad_rec b l r ((2*m + 1) / 2^n))" apply (rule dyad_rec.psimps) by (metis dyad_rec_level_termination lessI of_nat_add of_nat_mult of_nat_numeral) -lemma%unimportant dyad_rec_41_times2: +lemma dyad_rec_41_times2: assumes "n > 0" shows "dyad_rec b l r (2 * ((4 * real m + 1) / 2^Suc n)) = l (dyad_rec b l r (2 * (2 * real m + 1) / 2^n))" proof - @@ -460,10 +460,10 @@ finally show ?thesis . qed -lemma%important dyad_rec_43_times2: +lemma dyad_rec_43_times2: assumes "n > 0" shows "dyad_rec b l r (2 * ((4 * real m + 3) / 2^Suc n)) = r (dyad_rec b l r (2 * (2 * real m + 1) / 2^n))" -proof%unimportant - +proof - obtain n' where n': "n = Suc n'" using assms not0_implies_Suc by blast have "dyad_rec b l r (2 * ((4 * real m + 3) / 2^Suc n)) = dyad_rec b l r ((2 * (4 * real m + 3)) / (2 * 2^n))" @@ -479,22 +479,22 @@ finally show ?thesis . qed -definition%important dyad_rec2 +definition%unimportant dyad_rec2 where "dyad_rec2 u v lc rc x = dyad_rec (\z. (u,v)) (\(a,b). (a, lc a b (midpoint a b))) (\(a,b). (rc a b (midpoint a b), b)) (2*x)" -abbreviation leftrec where "leftrec u v lc rc x \ fst (dyad_rec2 u v lc rc x)" -abbreviation rightrec where "rightrec u v lc rc x \ snd (dyad_rec2 u v lc rc x)" +abbreviation%unimportant leftrec where "leftrec u v lc rc x \ fst (dyad_rec2 u v lc rc x)" +abbreviation%unimportant rightrec where "rightrec u v lc rc x \ snd (dyad_rec2 u v lc rc x)" -lemma%unimportant leftrec_base: "leftrec u v lc rc (real m / 2) = u" +lemma leftrec_base: "leftrec u v lc rc (real m / 2) = u" by (simp add: dyad_rec2_def) -lemma%unimportant leftrec_41: "n > 0 \ leftrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) = leftrec u v lc rc ((2 * real m + 1) / 2^n)" +lemma leftrec_41: "n > 0 \ leftrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) = leftrec u v lc rc ((2 * real m + 1) / 2^n)" apply (simp only: dyad_rec2_def dyad_rec_41_times2) apply (simp add: case_prod_beta) done -lemma%unimportant leftrec_43: "n > 0 \ +lemma leftrec_43: "n > 0 \ leftrec u v lc rc ((4 * real m + 3) / 2 ^ (Suc n)) = rc (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)) (midpoint (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)))" @@ -502,10 +502,10 @@ apply (simp add: case_prod_beta) done -lemma%unimportant rightrec_base: "rightrec u v lc rc (real m / 2) = v" +lemma rightrec_base: "rightrec u v lc rc (real m / 2) = v" by (simp add: dyad_rec2_def) -lemma%unimportant rightrec_41: "n > 0 \ +lemma rightrec_41: "n > 0 \ rightrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) = lc (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)) (midpoint (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)))" @@ -513,24 +513,24 @@ apply (simp add: case_prod_beta) done -lemma%unimportant rightrec_43: "n > 0 \ rightrec u v lc rc ((4 * real m + 3) / 2 ^ (Suc n)) = rightrec u v lc rc ((2 * real m + 1) / 2^n)" +lemma rightrec_43: "n > 0 \ rightrec u v lc rc ((4 * real m + 3) / 2 ^ (Suc n)) = rightrec u v lc rc ((2 * real m + 1) / 2^n)" apply (simp only: dyad_rec2_def dyad_rec_43_times2) apply (simp add: case_prod_beta) done -lemma%unimportant dyadics_in_open_unit_interval: +lemma dyadics_in_open_unit_interval: "{0<..<1} \ (\k m. {real m / 2^k}) = (\k. \m \ {0<..<2^k}. {real m / 2^k})" by (auto simp: divide_simps) -theorem%important homeomorphic_monotone_image_interval: +theorem homeomorphic_monotone_image_interval: fixes f :: "real \ 'a::{real_normed_vector,complete_space}" assumes cont_f: "continuous_on {0..1} f" and conn: "\y. connected ({0..1} \ f -` {y})" and f_1not0: "f 1 \ f 0" shows "(f ` {0..1}) homeomorphic {0..1::real}" -proof%unimportant - +proof - have "\c d. a \ c \ c \ m \ m \ d \ d \ b \ (\x \ {c..d}. f x = f m) \ (\x \ {a.. f m)) \ @@ -1663,11 +1663,11 @@ qed -theorem%important path_contains_arc: +theorem path_contains_arc: fixes p :: "real \ 'a::{complete_space,real_normed_vector}" assumes "path p" and a: "pathstart p = a" and b: "pathfinish p = b" and "a \ b" obtains q where "arc q" "path_image q \ path_image p" "pathstart q = a" "pathfinish q = b" -proof%unimportant - +proof - have ucont_p: "uniformly_continuous_on {0..1} p" using \path p\ unfolding path_def by (metis compact_Icc compact_uniformly_continuous) @@ -1960,12 +1960,12 @@ qed -corollary%important path_connected_arcwise: +corollary path_connected_arcwise: fixes S :: "'a::{complete_space,real_normed_vector} set" shows "path_connected S \ (\x \ S. \y \ S. x \ y \ (\g. arc g \ path_image g \ S \ pathstart g = x \ pathfinish g = y))" (is "?lhs = ?rhs") -proof%unimportant (intro iffI impI ballI) +proof (intro iffI impI ballI) fix x y assume "path_connected S" "x \ S" "y \ S" "x \ y" then obtain p where p: "path p" "path_image p \ S" "pathstart p = x" "pathfinish p = y" @@ -1991,23 +1991,23 @@ qed -corollary%important arc_connected_trans: +corollary arc_connected_trans: fixes g :: "real \ 'a::{complete_space,real_normed_vector}" assumes "arc g" "arc h" "pathfinish g = pathstart h" "pathstart g \ pathfinish h" obtains i where "arc i" "path_image i \ path_image g \ path_image h" "pathstart i = pathstart g" "pathfinish i = pathfinish h" - by%unimportant (metis (no_types, hide_lams) arc_imp_path assms path_contains_arc path_image_join path_join pathfinish_join pathstart_join) + by (metis (no_types, hide_lams) arc_imp_path assms path_contains_arc path_image_join path_join pathfinish_join pathstart_join) subsection%important\Accessibility of frontier points\ -lemma%important dense_accessible_frontier_points: +lemma dense_accessible_frontier_points: fixes S :: "'a::{complete_space,real_normed_vector} set" assumes "open S" and opeSV: "openin (subtopology euclidean (frontier S)) V" and "V \ {}" obtains g where "arc g" "g ` {0..<1} \ S" "pathstart g \ S" "pathfinish g \ V" -proof%unimportant - +proof - obtain z where "z \ V" using \V \ {}\ by auto then obtain r where "r > 0" and r: "ball z r \ frontier S \ V" @@ -2098,12 +2098,12 @@ qed -lemma%important dense_accessible_frontier_points_connected: +lemma dense_accessible_frontier_points_connected: fixes S :: "'a::{complete_space,real_normed_vector} set" assumes "open S" "connected S" "x \ S" "V \ {}" and ope: "openin (subtopology euclidean (frontier S)) V" obtains g where "arc g" "g ` {0..<1} \ S" "pathstart g = x" "pathfinish g \ V" -proof%unimportant - +proof - have "V \ frontier S" using ope openin_imp_subset by blast with \open S\ \x \ S\ have "x \ V" @@ -2133,14 +2133,14 @@ using h \pathfinish g \ V\ by auto qed -lemma%important dense_access_fp_aux: +lemma dense_access_fp_aux: fixes S :: "'a::{complete_space,real_normed_vector} set" assumes S: "open S" "connected S" and opeSU: "openin (subtopology euclidean (frontier S)) U" and opeSV: "openin (subtopology euclidean (frontier S)) V" and "V \ {}" "\ U \ V" obtains g where "arc g" "pathstart g \ U" "pathfinish g \ V" "g ` {0<..<1} \ S" -proof%unimportant - +proof - have "S \ {}" using opeSV \V \ {}\ by (metis frontier_empty openin_subtopology_empty) then obtain x where "x \ S" by auto @@ -2180,14 +2180,14 @@ qed qed -lemma%important dense_accessible_frontier_point_pairs: +lemma dense_accessible_frontier_point_pairs: fixes S :: "'a::{complete_space,real_normed_vector} set" assumes S: "open S" "connected S" and opeSU: "openin (subtopology euclidean (frontier S)) U" and opeSV: "openin (subtopology euclidean (frontier S)) V" and "U \ {}" "V \ {}" "U \ V" obtains g where "arc g" "pathstart g \ U" "pathfinish g \ V" "g ` {0<..<1} \ S" -proof%unimportant - +proof - consider "\ U \ V" | "\ V \ U" using \U \ V\ by blast then show ?thesis diff -r e61b0b819d28 -r 3417a8f154eb src/HOL/Analysis/Binary_Product_Measure.thy --- a/src/HOL/Analysis/Binary_Product_Measure.thy Sun Jan 13 20:25:41 2019 +0100 +++ b/src/HOL/Analysis/Binary_Product_Measure.thy Mon Jan 14 11:59:19 2019 +0000 @@ -8,10 +8,10 @@ imports Nonnegative_Lebesgue_Integration begin -lemma%unimportant Pair_vimage_times[simp]: "Pair x -` (A \ B) = (if x \ A then B else {})" +lemma Pair_vimage_times[simp]: "Pair x -` (A \ B) = (if x \ A then B else {})" by auto -lemma%unimportant rev_Pair_vimage_times[simp]: "(\x. (x, y)) -` (A \ B) = (if y \ B then A else {})" +lemma rev_Pair_vimage_times[simp]: "(\x. (x, y)) -` (A \ B) = (if y \ B then A else {})" by auto subsection%important "Binary products" @@ -21,48 +21,48 @@ {a \ b | a b. a \ sets A \ b \ sets B} (\X. \\<^sup>+x. (\\<^sup>+y. indicator X (x,y) \B) \A)" -lemma%important pair_measure_closed: "{a \ b | a b. a \ sets A \ b \ sets B} \ Pow (space A \ space B)" - using%unimportant sets.space_closed[of A] sets.space_closed[of B] by auto +lemma pair_measure_closed: "{a \ b | a b. a \ sets A \ b \ sets B} \ Pow (space A \ space B)" + using sets.space_closed[of A] sets.space_closed[of B] by auto -lemma%important space_pair_measure: +lemma space_pair_measure: "space (A \\<^sub>M B) = space A \ space B" unfolding pair_measure_def using pair_measure_closed[of A B] - by%unimportant (rule space_measure_of) + by (rule space_measure_of) -lemma%unimportant SIGMA_Collect_eq: "(SIGMA x:space M. {y\space N. P x y}) = {x\space (M \\<^sub>M N). P (fst x) (snd x)}" +lemma SIGMA_Collect_eq: "(SIGMA x:space M. {y\space N. P x y}) = {x\space (M \\<^sub>M N). P (fst x) (snd x)}" by (auto simp: space_pair_measure) -lemma%unimportant sets_pair_measure: +lemma sets_pair_measure: "sets (A \\<^sub>M B) = sigma_sets (space A \ space B) {a \ b | a b. a \ sets A \ b \ sets B}" unfolding pair_measure_def using pair_measure_closed[of A B] by (rule sets_measure_of) -lemma%unimportant sets_pair_measure_cong[measurable_cong, cong]: +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) -lemma%unimportant pair_measureI[intro, simp, measurable]: +lemma pair_measureI[intro, simp, measurable]: "x \ sets A \ y \ sets B \ x \ y \ sets (A \\<^sub>M B)" by (auto simp: sets_pair_measure) -lemma%unimportant sets_Pair: "{x} \ sets M1 \ {y} \ sets M2 \ {(x, y)} \ sets (M1 \\<^sub>M M2)" +lemma sets_Pair: "{x} \ sets M1 \ {y} \ sets M2 \ {(x, y)} \ sets (M1 \\<^sub>M M2)" using pair_measureI[of "{x}" M1 "{y}" M2] by simp -lemma%unimportant measurable_pair_measureI: +lemma measurable_pair_measureI: assumes 1: "f \ space M \ space M1 \ space M2" assumes 2: "\A B. A \ sets M1 \ B \ sets M2 \ f -` (A \ B) \ space M \ sets M" shows "f \ measurable M (M1 \\<^sub>M M2)" unfolding pair_measure_def using 1 2 by (intro measurable_measure_of) (auto dest: sets.sets_into_space) -lemma%unimportant measurable_split_replace[measurable (raw)]: +lemma measurable_split_replace[measurable (raw)]: "(\x. f x (fst (g x)) (snd (g x))) \ measurable M N \ (\x. case_prod (f x) (g x)) \ measurable M N" unfolding split_beta' . -lemma%important measurable_Pair[measurable (raw)]: +lemma measurable_Pair[measurable (raw)]: assumes f: "f \ measurable M M1" and g: "g \ measurable M M2" shows "(\x. (f x, g x)) \ measurable M (M1 \\<^sub>M M2)" -proof%unimportant (rule measurable_pair_measureI) +proof (rule measurable_pair_measureI) show "(\x. (f x, g x)) \ space M \ space M1 \ space M2" using f g by (auto simp: measurable_def) fix A B assume *: "A \ sets M1" "B \ sets M2" @@ -73,59 +73,59 @@ finally show "(\x. (f x, g x)) -` (A \ B) \ space M \ sets M" . qed -lemma%unimportant measurable_fst[intro!, simp, measurable]: "fst \ measurable (M1 \\<^sub>M M2) M1" +lemma measurable_fst[intro!, simp, measurable]: "fst \ measurable (M1 \\<^sub>M M2) M1" by (auto simp: fst_vimage_eq_Times space_pair_measure sets.sets_into_space times_Int_times measurable_def) -lemma%unimportant measurable_snd[intro!, simp, measurable]: "snd \ measurable (M1 \\<^sub>M M2) M2" +lemma measurable_snd[intro!, simp, measurable]: "snd \ measurable (M1 \\<^sub>M M2) M2" by (auto simp: snd_vimage_eq_Times space_pair_measure sets.sets_into_space times_Int_times measurable_def) -lemma%unimportant measurable_Pair_compose_split[measurable_dest]: +lemma measurable_Pair_compose_split[measurable_dest]: assumes f: "case_prod f \ measurable (M1 \\<^sub>M M2) N" assumes g: "g \ measurable M M1" and h: "h \ measurable M M2" shows "(\x. f (g x) (h x)) \ measurable M N" using measurable_compose[OF measurable_Pair f, OF g h] by simp -lemma%unimportant measurable_Pair1_compose[measurable_dest]: +lemma measurable_Pair1_compose[measurable_dest]: assumes f: "(\x. (f x, g x)) \ measurable M (M1 \\<^sub>M M2)" assumes [measurable]: "h \ measurable N M" shows "(\x. f (h x)) \ measurable N M1" using measurable_compose[OF f measurable_fst] by simp -lemma%unimportant measurable_Pair2_compose[measurable_dest]: +lemma measurable_Pair2_compose[measurable_dest]: assumes f: "(\x. (f x, g x)) \ measurable M (M1 \\<^sub>M M2)" assumes [measurable]: "h \ measurable N M" shows "(\x. g (h x)) \ measurable N M2" using measurable_compose[OF f measurable_snd] by simp -lemma%unimportant measurable_pair: +lemma measurable_pair: assumes "(fst \ f) \ measurable M M1" "(snd \ f) \ measurable M M2" shows "f \ measurable M (M1 \\<^sub>M M2)" using measurable_Pair[OF assms] by simp -lemma%unimportant (*FIX ME needs a name *) +lemma (*FIX ME needs a name *) assumes f[measurable]: "f \ measurable M (N \\<^sub>M P)" shows measurable_fst': "(\x. fst (f x)) \ measurable M N" and measurable_snd': "(\x. snd (f x)) \ measurable M P" by simp_all -lemma%unimportant (*FIX ME needs a name *) +lemma (*FIX ME needs a name *) assumes f[measurable]: "f \ measurable M N" shows measurable_fst'': "(\x. f (fst x)) \ measurable (M \\<^sub>M P) N" and measurable_snd'': "(\x. f (snd x)) \ measurable (P \\<^sub>M M) N" by simp_all -lemma%unimportant sets_pair_in_sets: +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%important sets_pair_eq_sets_fst_snd: +lemma sets_pair_eq_sets_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%unimportant - +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) @@ -157,29 +157,29 @@ done qed -lemma%unimportant measurable_pair_iff: +lemma measurable_pair_iff: "f \ measurable M (M1 \\<^sub>M M2) \ (fst \ f) \ measurable M M1 \ (snd \ f) \ measurable M M2" by (auto intro: measurable_pair[of f M M1 M2]) -lemma%unimportant measurable_split_conv: +lemma measurable_split_conv: "(\(x, y). f x y) \ measurable A B \ (\x. f (fst x) (snd x)) \ measurable A B" by (intro arg_cong2[where f="(\)"]) auto -lemma%unimportant measurable_pair_swap': "(\(x,y). (y, x)) \ measurable (M1 \\<^sub>M M2) (M2 \\<^sub>M M1)" +lemma measurable_pair_swap': "(\(x,y). (y, x)) \ measurable (M1 \\<^sub>M M2) (M2 \\<^sub>M M1)" by (auto intro!: measurable_Pair simp: measurable_split_conv) -lemma%unimportant measurable_pair_swap: +lemma measurable_pair_swap: assumes f: "f \ measurable (M1 \\<^sub>M M2) M" shows "(\(x,y). f (y, x)) \ measurable (M2 \\<^sub>M M1) M" using measurable_comp[OF measurable_Pair f] by (auto simp: measurable_split_conv comp_def) -lemma%unimportant measurable_pair_swap_iff: +lemma measurable_pair_swap_iff: "f \ measurable (M2 \\<^sub>M M1) M \ (\(x,y). f (y,x)) \ measurable (M1 \\<^sub>M M2) M" by (auto dest: measurable_pair_swap) -lemma%unimportant measurable_Pair1': "x \ space M1 \ Pair x \ measurable M2 (M1 \\<^sub>M M2)" +lemma measurable_Pair1': "x \ space M1 \ Pair x \ measurable M2 (M1 \\<^sub>M M2)" by simp -lemma%unimportant sets_Pair1[measurable (raw)]: +lemma sets_Pair1[measurable (raw)]: assumes A: "A \ sets (M1 \\<^sub>M M2)" shows "Pair x -` A \ sets M2" proof - have "Pair x -` A = (if x \ space M1 then Pair x -` A \ space M2 else {})" @@ -189,10 +189,10 @@ finally show ?thesis . qed -lemma%unimportant measurable_Pair2': "y \ space M2 \ (\x. (x, y)) \ measurable M1 (M1 \\<^sub>M M2)" +lemma measurable_Pair2': "y \ space M2 \ (\x. (x, y)) \ measurable M1 (M1 \\<^sub>M M2)" by (auto intro!: measurable_Pair) -lemma%unimportant sets_Pair2: assumes A: "A \ sets (M1 \\<^sub>M M2)" shows "(\x. (x, y)) -` A \ sets M1" +lemma sets_Pair2: assumes A: "A \ sets (M1 \\<^sub>M M2)" shows "(\x. (x, y)) -` A \ sets M1" proof - have "(\x. (x, y)) -` A = (if y \ space M2 then (\x. (x, y)) -` A \ space M1 else {})" using A[THEN sets.sets_into_space] by (auto simp: space_pair_measure) @@ -201,23 +201,23 @@ finally show ?thesis . qed -lemma%unimportant measurable_Pair2: +lemma measurable_Pair2: assumes f: "f \ measurable (M1 \\<^sub>M M2) M" and x: "x \ space M1" shows "(\y. f (x, y)) \ measurable M2 M" using measurable_comp[OF measurable_Pair1' f, OF x] by (simp add: comp_def) -lemma%unimportant measurable_Pair1: +lemma measurable_Pair1: assumes f: "f \ measurable (M1 \\<^sub>M M2) M" and y: "y \ space M2" shows "(\x. f (x, y)) \ measurable M1 M" using measurable_comp[OF measurable_Pair2' f, OF y] by (simp add: comp_def) -lemma%unimportant Int_stable_pair_measure_generator: "Int_stable {a \ b | a b. a \ sets A \ b \ sets B}" +lemma Int_stable_pair_measure_generator: "Int_stable {a \ b | a b. a \ sets A \ b \ sets B}" unfolding Int_stable_def by safe (auto simp add: times_Int_times) -lemma%unimportant (in finite_measure) finite_measure_cut_measurable: +lemma (in finite_measure) finite_measure_cut_measurable: assumes [measurable]: "Q \ sets (N \\<^sub>M M)" shows "(\x. emeasure M (Pair x -` Q)) \ borel_measurable N" (is "?s Q \ _") @@ -239,7 +239,7 @@ unfolding sets_pair_measure[symmetric] by simp qed (auto simp add: if_distrib Int_def[symmetric] intro!: measurable_If) -lemma%unimportant (in sigma_finite_measure) measurable_emeasure_Pair: +lemma (in sigma_finite_measure) measurable_emeasure_Pair: assumes Q: "Q \ sets (N \\<^sub>M M)" shows "(\x. emeasure M (Pair x -` Q)) \ borel_measurable N" (is "?s Q \ _") proof - from sigma_finite_disjoint guess F . note F = this @@ -279,7 +279,7 @@ by auto qed -lemma%unimportant (in sigma_finite_measure) measurable_emeasure[measurable (raw)]: +lemma (in sigma_finite_measure) measurable_emeasure[measurable (raw)]: assumes space: "\x. x \ space N \ A x \ space M" assumes A: "{x\space (N \\<^sub>M M). snd x \ A (fst x)} \ sets (N \\<^sub>M M)" shows "(\x. emeasure M (A x)) \ borel_measurable N" @@ -290,7 +290,7 @@ by (auto cong: measurable_cong) qed -lemma%unimportant (in sigma_finite_measure) emeasure_pair_measure: +lemma (in sigma_finite_measure) emeasure_pair_measure: assumes "X \ sets (N \\<^sub>M M)" shows "emeasure (N \\<^sub>M M) X = (\\<^sup>+ x. \\<^sup>+ y. indicator X (x, y) \M \N)" (is "_ = ?\ X") proof (rule emeasure_measure_of[OF pair_measure_def]) @@ -314,7 +314,7 @@ using sets.space_closed[of N] sets.space_closed[of M] by auto qed fact -lemma%unimportant (in sigma_finite_measure) emeasure_pair_measure_alt: +lemma (in sigma_finite_measure) emeasure_pair_measure_alt: assumes X: "X \ sets (N \\<^sub>M M)" shows "emeasure (N \\<^sub>M M) X = (\\<^sup>+x. emeasure M (Pair x -` X) \N)" proof - @@ -324,10 +324,10 @@ using X by (auto intro!: nn_integral_cong simp: emeasure_pair_measure sets_Pair1) qed -lemma%important (in sigma_finite_measure) emeasure_pair_measure_Times: +proposition (in sigma_finite_measure) emeasure_pair_measure_Times: assumes A: "A \ sets N" and B: "B \ sets M" shows "emeasure (N \\<^sub>M M) (A \ B) = emeasure N A * emeasure M B" -proof%unimportant - +proof - have "emeasure (N \\<^sub>M M) (A \ B) = (\\<^sup>+x. emeasure M B * indicator A x \N)" using A B by (auto intro!: nn_integral_cong simp: emeasure_pair_measure_alt) also have "\ = emeasure M B * emeasure N A" @@ -338,16 +338,16 @@ subsection%important \Binary products of \\\-finite emeasure spaces\ -locale%important pair_sigma_finite = M1?: sigma_finite_measure M1 + M2?: sigma_finite_measure M2 +locale%unimportant pair_sigma_finite = M1?: sigma_finite_measure M1 + M2?: sigma_finite_measure M2 for M1 :: "'a measure" and M2 :: "'b measure" -lemma%unimportant (in pair_sigma_finite) measurable_emeasure_Pair1: +lemma (in pair_sigma_finite) measurable_emeasure_Pair1: "Q \ sets (M1 \\<^sub>M M2) \ (\x. emeasure M2 (Pair x -` Q)) \ borel_measurable M1" using M2.measurable_emeasure_Pair . -lemma%important (in pair_sigma_finite) measurable_emeasure_Pair2: +lemma (in pair_sigma_finite) measurable_emeasure_Pair2: assumes Q: "Q \ sets (M1 \\<^sub>M M2)" shows "(\y. emeasure M1 ((\x. (x, y)) -` Q)) \ borel_measurable M2" -proof%unimportant - +proof - have "(\(x, y). (y, x)) -` Q \ space (M2 \\<^sub>M M1) \ sets (M2 \\<^sub>M M1)" using Q measurable_pair_swap' by (auto intro: measurable_sets) note M1.measurable_emeasure_Pair[OF this] @@ -356,11 +356,11 @@ ultimately show ?thesis by simp qed -lemma%important (in pair_sigma_finite) sigma_finite_up_in_pair_measure_generator: +proposition (in pair_sigma_finite) sigma_finite_up_in_pair_measure_generator: defines "E \ {A \ B | A B. A \ sets M1 \ B \ sets M2}" shows "\F::nat \ ('a \ 'b) set. range F \ E \ incseq F \ (\i. F i) = space M1 \ space M2 \ (\i. emeasure (M1 \\<^sub>M M2) (F i) \ \)" -proof%unimportant - +proof - from M1.sigma_finite_incseq guess F1 . note F1 = this from M2.sigma_finite_incseq guess F2 . note F2 = this from F1 F2 have space: "space M1 = (\i. F1 i)" "space M2 = (\i. F2 i)" by auto @@ -394,7 +394,7 @@ qed qed -sublocale%important pair_sigma_finite \ P?: sigma_finite_measure "M1 \\<^sub>M M2" +sublocale%unimportant pair_sigma_finite \ P?: sigma_finite_measure "M1 \\<^sub>M M2" proof from M1.sigma_finite_countable guess F1 .. moreover from M2.sigma_finite_countable guess F2 .. @@ -404,7 +404,7 @@ (auto simp: M2.emeasure_pair_measure_Times space_pair_measure set_eq_iff subset_eq ennreal_mult_eq_top_iff) qed -lemma%unimportant sigma_finite_pair_measure: +lemma sigma_finite_pair_measure: assumes A: "sigma_finite_measure A" and B: "sigma_finite_measure B" shows "sigma_finite_measure (A \\<^sub>M B)" proof - @@ -414,14 +414,14 @@ show ?thesis .. qed -lemma%unimportant sets_pair_swap: +lemma sets_pair_swap: assumes "A \ sets (M1 \\<^sub>M M2)" shows "(\(x, y). (y, x)) -` A \ space (M2 \\<^sub>M M1) \ sets (M2 \\<^sub>M M1)" using measurable_pair_swap' assms by (rule measurable_sets) -lemma%important (in pair_sigma_finite) distr_pair_swap: +lemma (in pair_sigma_finite) distr_pair_swap: "M1 \\<^sub>M M2 = distr (M2 \\<^sub>M M1) (M1 \\<^sub>M M2) (\(x, y). (y, x))" (is "?P = ?D") -proof%unimportant - +proof - from sigma_finite_up_in_pair_measure_generator guess F :: "nat \ ('a \ 'b) set" .. note F = this let ?E = "{a \ b |a b. a \ sets M1 \ b \ sets M2}" show ?thesis @@ -446,11 +446,11 @@ qed qed -lemma%unimportant (in pair_sigma_finite) emeasure_pair_measure_alt2: +lemma (in pair_sigma_finite) emeasure_pair_measure_alt2: assumes A: "A \ sets (M1 \\<^sub>M M2)" shows "emeasure (M1 \\<^sub>M M2) A = (\\<^sup>+y. emeasure M1 ((\x. (x, y)) -` A) \M2)" (is "_ = ?\ A") -proof%unimportant - +proof - have [simp]: "\y. (Pair y -` ((\(x, y). (y, x)) -` A \ space (M2 \\<^sub>M M1))) = (\x. (x, y)) -` A" using sets.sets_into_space[OF A] by (auto simp: space_pair_measure) show ?thesis using A @@ -459,7 +459,7 @@ M1.emeasure_pair_measure_alt emeasure_distr[OF measurable_pair_swap' A]) qed -lemma%unimportant (in pair_sigma_finite) AE_pair: +lemma (in pair_sigma_finite) AE_pair: assumes "AE x in (M1 \\<^sub>M M2). Q x" shows "AE x in M1. (AE y in M2. Q (x, y))" proof - @@ -485,11 +485,11 @@ qed qed -lemma%important (in pair_sigma_finite) AE_pair_measure: +lemma (in pair_sigma_finite) AE_pair_measure: assumes "{x\space (M1 \\<^sub>M M2). P x} \ sets (M1 \\<^sub>M M2)" assumes ae: "AE x in M1. AE y in M2. P (x, y)" shows "AE x in M1 \\<^sub>M M2. P x" -proof%unimportant (subst AE_iff_measurable[OF _ refl]) +proof (subst AE_iff_measurable[OF _ refl]) show "{x\space (M1 \\<^sub>M M2). \ P x} \ sets (M1 \\<^sub>M M2)" by (rule sets.sets_Collect) fact then have "emeasure (M1 \\<^sub>M M2) {x \ space (M1 \\<^sub>M M2). \ P x} = @@ -505,12 +505,12 @@ finally show "emeasure (M1 \\<^sub>M M2) {x \ space (M1 \\<^sub>M M2). \ P x} = 0" by simp qed -lemma%unimportant (in pair_sigma_finite) AE_pair_iff: +lemma (in pair_sigma_finite) AE_pair_iff: "{x\space (M1 \\<^sub>M M2). P (fst x) (snd x)} \ sets (M1 \\<^sub>M M2) \ (AE x in M1. AE y in M2. P x y) \ (AE x in (M1 \\<^sub>M M2). P (fst x) (snd x))" using AE_pair[of "\x. P (fst x) (snd x)"] AE_pair_measure[of "\x. P (fst x) (snd x)"] by auto -lemma%unimportant (in pair_sigma_finite) AE_commute: +lemma (in pair_sigma_finite) AE_commute: assumes P: "{x\space (M1 \\<^sub>M M2). P (fst x) (snd x)} \ sets (M1 \\<^sub>M M2)" shows "(AE x in M1. AE y in M2. P x y) \ (AE y in M2. AE x in M1. P x y)" proof - @@ -533,14 +533,14 @@ subsection%important "Fubinis theorem" -lemma%unimportant measurable_compose_Pair1: +lemma measurable_compose_Pair1: "x \ space M1 \ g \ measurable (M1 \\<^sub>M M2) L \ (\y. g (x, y)) \ measurable M2 L" by simp -lemma%unimportant (in sigma_finite_measure) borel_measurable_nn_integral_fst: +lemma (in sigma_finite_measure) borel_measurable_nn_integral_fst: assumes f: "f \ borel_measurable (M1 \\<^sub>M M)" shows "(\x. \\<^sup>+ y. f (x, y) \M) \ borel_measurable M1" -using f proof%unimportant induct +using f proof induct case (cong u v) then have "\w x. w \ space M1 \ x \ space M \ u (w, x) = v (w, x)" by (auto simp: space_pair_measure) @@ -561,7 +561,7 @@ nn_integral_monotone_convergence_SUP incseq_def le_fun_def cong: measurable_cong) -lemma%unimportant (in sigma_finite_measure) nn_integral_fst: +lemma (in sigma_finite_measure) nn_integral_fst: assumes f: "f \ borel_measurable (M1 \\<^sub>M M)" shows "(\\<^sup>+ x. \\<^sup>+ y. f (x, y) \M \M1) = integral\<^sup>N (M1 \\<^sub>M M) f" (is "?I f = _") using f proof induct @@ -575,14 +575,14 @@ borel_measurable_nn_integral_fst nn_integral_mono incseq_def le_fun_def cong: nn_integral_cong) -lemma%unimportant (in sigma_finite_measure) borel_measurable_nn_integral[measurable (raw)]: +lemma (in sigma_finite_measure) borel_measurable_nn_integral[measurable (raw)]: "case_prod f \ borel_measurable (N \\<^sub>M M) \ (\x. \\<^sup>+ y. f x y \M) \ borel_measurable N" using borel_measurable_nn_integral_fst[of "case_prod f" N] by simp -lemma%important (in pair_sigma_finite) nn_integral_snd: +proposition (in pair_sigma_finite) nn_integral_snd: assumes f[measurable]: "f \ borel_measurable (M1 \\<^sub>M M2)" shows "(\\<^sup>+ y. (\\<^sup>+ x. f (x, y) \M1) \M2) = integral\<^sup>N (M1 \\<^sub>M M2) f" -proof%unimportant - +proof - note measurable_pair_swap[OF f] from M1.nn_integral_fst[OF this] have "(\\<^sup>+ y. (\\<^sup>+ x. f (x, y) \M1) \M2) = (\\<^sup>+ (x, y). f (y, x) \(M2 \\<^sub>M M1))" @@ -592,24 +592,24 @@ finally show ?thesis . qed -lemma%important (in pair_sigma_finite) Fubini: +theorem (in pair_sigma_finite) Fubini: assumes f: "f \ borel_measurable (M1 \\<^sub>M M2)" shows "(\\<^sup>+ y. (\\<^sup>+ x. f (x, y) \M1) \M2) = (\\<^sup>+ x. (\\<^sup>+ y. f (x, y) \M2) \M1)" unfolding nn_integral_snd[OF assms] M2.nn_integral_fst[OF assms] .. -lemma%important (in pair_sigma_finite) Fubini': +theorem (in pair_sigma_finite) Fubini': assumes f: "case_prod f \ borel_measurable (M1 \\<^sub>M M2)" shows "(\\<^sup>+ y. (\\<^sup>+ x. f x y \M1) \M2) = (\\<^sup>+ x. (\\<^sup>+ y. f x y \M2) \M1)" using Fubini[OF f] by simp subsection%important \Products on counting spaces, densities and distributions\ -lemma%important sigma_prod: +proposition sigma_prod: assumes X_cover: "\E\A. countable E \ X = \E" and A: "A \ Pow X" assumes Y_cover: "\E\B. countable E \ Y = \E" and B: "B \ Pow Y" shows "sigma X A \\<^sub>M sigma Y B = sigma (X \ Y) {a \ b | a b. a \ A \ b \ B}" (is "?P = ?S") -proof%unimportant (rule measure_eqI) +proof (rule measure_eqI) 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}}" @@ -662,7 +662,7 @@ by (simp add: emeasure_pair_measure_alt emeasure_sigma) qed -lemma%unimportant sigma_sets_pair_measure_generator_finite: +lemma sigma_sets_pair_measure_generator_finite: assumes "finite A" and "finite B" shows "sigma_sets (A \ B) { a \ b | a b. a \ A \ b \ B} = Pow (A \ B)" (is "sigma_sets ?prod ?sets = _") @@ -686,14 +686,14 @@ show "a \ A" and "b \ B" by auto qed -lemma%important sets_pair_eq: +proposition sets_pair_eq: assumes Ea: "Ea \ Pow (space A)" "sets A = sigma_sets (space A) Ea" and Ca: "countable Ca" "Ca \ Ea" "\Ca = space A" and Eb: "Eb \ Pow (space B)" "sets B = sigma_sets (space B) Eb" and Cb: "countable Cb" "Cb \ Eb" "\Cb = space B" shows "sets (A \\<^sub>M B) = sets (sigma (space A \ space B) { a \ b | a b. a \ Ea \ b \ Eb })" (is "_ = sets (sigma ?\ ?E)") -proof%unimportant +proof show "sets (sigma ?\ ?E) \ sets (A \\<^sub>M B)" using Ea(1) Eb(1) by (subst sigma_le_sets) (auto simp: Ea(2) Eb(2)) have "?E \ Pow ?\" @@ -733,10 +733,10 @@ finally show "sets (A \\<^sub>M B) \ sets (sigma ?\ ?E)" . qed -lemma%important borel_prod: +proposition borel_prod: "(borel \\<^sub>M borel) = (borel :: ('a::second_countable_topology \ 'b::second_countable_topology) measure)" (is "?P = ?B") -proof%unimportant - +proof - have "?B = sigma UNIV {A \ B | A B. open A \ open B}" by (rule second_countable_borel_measurable[OF open_prod_generated]) also have "\ = ?P" @@ -745,10 +745,10 @@ finally show ?thesis .. qed -lemma%important pair_measure_count_space: +proposition pair_measure_count_space: assumes A: "finite A" and B: "finite B" shows "count_space A \\<^sub>M count_space B = count_space (A \ B)" (is "?P = ?C") -proof%unimportant (rule measure_eqI) +proof (rule measure_eqI) interpret A: finite_measure "count_space A" by (rule finite_measure_count_space) fact interpret B: finite_measure "count_space B" by (rule finite_measure_count_space) fact interpret P: pair_sigma_finite "count_space A" "count_space B" .. @@ -776,14 +776,14 @@ qed -lemma%unimportant emeasure_prod_count_space: +lemma emeasure_prod_count_space: assumes A: "A \ sets (count_space UNIV \\<^sub>M M)" (is "A \ sets (?A \\<^sub>M ?B)") shows "emeasure (?A \\<^sub>M ?B) A = (\\<^sup>+ x. \\<^sup>+ y. indicator A (x, y) \?B \?A)" by (rule emeasure_measure_of[OF pair_measure_def]) (auto simp: countably_additive_def positive_def suminf_indicator A nn_integral_suminf[symmetric] dest: sets.sets_into_space) -lemma%unimportant emeasure_prod_count_space_single[simp]: "emeasure (count_space UNIV \\<^sub>M count_space UNIV) {x} = 1" +lemma emeasure_prod_count_space_single[simp]: "emeasure (count_space UNIV \\<^sub>M count_space UNIV) {x} = 1" proof - have [simp]: "\a b x y. indicator {(a, b)} (x, y) = (indicator {a} x * indicator {b} y::ennreal)" by (auto split: split_indicator) @@ -791,11 +791,11 @@ by (cases x) (auto simp: emeasure_prod_count_space nn_integral_cmult sets_Pair) qed -lemma%important emeasure_count_space_prod_eq: +lemma emeasure_count_space_prod_eq: fixes A :: "('a \ 'b) set" assumes A: "A \ sets (count_space UNIV \\<^sub>M count_space UNIV)" (is "A \ sets (?A \\<^sub>M ?B)") shows "emeasure (?A \\<^sub>M ?B) A = emeasure (count_space UNIV) A" -proof%unimportant - +proof - { fix A :: "('a \ 'b) set" assume "countable A" then have "emeasure (?A \\<^sub>M ?B) (\a\A. {a}) = (\\<^sup>+a. emeasure (?A \\<^sub>M ?B) {a} \count_space A)" by (intro emeasure_UN_countable) (auto simp: sets_Pair disjoint_family_on_def) @@ -822,7 +822,7 @@ qed qed -lemma%unimportant nn_integral_count_space_prod_eq: +lemma nn_integral_count_space_prod_eq: "nn_integral (count_space UNIV \\<^sub>M count_space UNIV) f = nn_integral (count_space UNIV) f" (is "nn_integral ?P f = _") proof cases @@ -874,12 +874,12 @@ by (simp add: top_unique) qed -lemma%important pair_measure_density: +theorem pair_measure_density: assumes f: "f \ borel_measurable M1" assumes g: "g \ borel_measurable M2" assumes "sigma_finite_measure M2" "sigma_finite_measure (density M2 g)" shows "density M1 f \\<^sub>M density M2 g = density (M1 \\<^sub>M M2) (\(x,y). f x * g y)" (is "?L = ?R") -proof%unimportant (rule measure_eqI) +proof (rule measure_eqI) interpret M2: sigma_finite_measure M2 by fact interpret D2: sigma_finite_measure "density M2 g" by fact @@ -894,7 +894,7 @@ cong: nn_integral_cong) qed simp -lemma%unimportant sigma_finite_measure_distr: +lemma sigma_finite_measure_distr: assumes "sigma_finite_measure (distr M N f)" and f: "f \ measurable M N" shows "sigma_finite_measure M" proof - @@ -909,7 +909,7 @@ qed qed -lemma%unimportant pair_measure_distr: +lemma pair_measure_distr: assumes f: "f \ measurable M S" and g: "g \ measurable N T" assumes "sigma_finite_measure (distr N T g)" shows "distr M S f \\<^sub>M distr N T g = distr (M \\<^sub>M N) (S \\<^sub>M T) (\(x, y). (f x, g y))" (is "?P = ?D") @@ -924,12 +924,12 @@ intro!: nn_integral_cong arg_cong[where f="emeasure N"]) qed simp -lemma%important pair_measure_eqI: +lemma pair_measure_eqI: assumes "sigma_finite_measure M1" "sigma_finite_measure M2" assumes sets: "sets (M1 \\<^sub>M M2) = sets M" assumes emeasure: "\A B. A \ sets M1 \ B \ sets M2 \ emeasure M1 A * emeasure M2 B = emeasure M (A \ B)" shows "M1 \\<^sub>M M2 = M" -proof%unimportant - +proof - interpret M1: sigma_finite_measure M1 by fact interpret M2: sigma_finite_measure M2 by fact interpret pair_sigma_finite M1 M2 .. @@ -959,11 +959,11 @@ qed qed -lemma%important sets_pair_countable: +lemma sets_pair_countable: assumes "countable S1" "countable S2" assumes M: "sets M = Pow S1" and N: "sets N = Pow S2" shows "sets (M \\<^sub>M N) = Pow (S1 \ S2)" -proof%unimportant auto +proof auto fix x a b assume x: "x \ sets (M \\<^sub>M N)" "(a, b) \ x" from sets.sets_into_space[OF x(1)] x(2) sets_eq_imp_space_eq[of N "count_space S2"] sets_eq_imp_space_eq[of M "count_space S1"] M N @@ -980,10 +980,10 @@ finally show "X \ sets (M \\<^sub>M N)" . qed -lemma%important pair_measure_countable: +lemma pair_measure_countable: assumes "countable S1" "countable S2" shows "count_space S1 \\<^sub>M count_space S2 = count_space (S1 \ S2)" -proof%unimportant (rule pair_measure_eqI) +proof (rule pair_measure_eqI) show "sigma_finite_measure (count_space S1)" "sigma_finite_measure (count_space S2)" using assms by (auto intro!: sigma_finite_measure_count_space_countable) show "sets (count_space S1 \\<^sub>M count_space S2) = sets (count_space (S1 \ S2))" @@ -995,10 +995,10 @@ by (subst (1 2 3) emeasure_count_space) (auto simp: finite_cartesian_product_iff ennreal_mult_top ennreal_top_mult) qed -lemma%important nn_integral_fst_count_space: +proposition nn_integral_fst_count_space: "(\\<^sup>+ x. \\<^sup>+ y. f (x, y) \count_space UNIV \count_space UNIV) = integral\<^sup>N (count_space UNIV) f" (is "?lhs = ?rhs") -proof%unimportant(cases) +proof(cases) assume *: "countable {xy. f xy \ 0}" let ?A = "fst ` {xy. f xy \ 0}" let ?B = "snd ` {xy. f xy \ 0}" @@ -1073,7 +1073,7 @@ ultimately show ?thesis by simp qed -lemma nn_integral_snd_count_space: +proposition nn_integral_snd_count_space: "(\\<^sup>+ y. \\<^sup>+ x. f (x, y) \count_space UNIV \count_space UNIV) = integral\<^sup>N (count_space UNIV) f" (is "?lhs = ?rhs") proof - @@ -1088,7 +1088,7 @@ finally show ?thesis . qed -lemma%unimportant measurable_pair_measure_countable1: +lemma measurable_pair_measure_countable1: assumes "countable A" and [measurable]: "\x. x \ A \ (\y. f (x, y)) \ measurable N K" shows "f \ measurable (count_space A \\<^sub>M N) K" @@ -1097,11 +1097,11 @@ subsection%important \Product of Borel spaces\ -lemma%important borel_Times: +theorem borel_Times: fixes A :: "'a::topological_space set" and B :: "'b::topological_space set" assumes A: "A \ sets borel" and B: "B \ sets borel" shows "A \ B \ sets borel" -proof%unimportant - +proof - have "A \ B = (A\UNIV) \ (UNIV \ B)" by auto moreover @@ -1146,7 +1146,7 @@ by auto qed -lemma%unimportant finite_measure_pair_measure: +lemma finite_measure_pair_measure: assumes "finite_measure M" "finite_measure N" shows "finite_measure (N \\<^sub>M M)" proof (rule finite_measureI) diff -r e61b0b819d28 -r 3417a8f154eb src/HOL/Analysis/Bochner_Integration.thy --- a/src/HOL/Analysis/Bochner_Integration.thy Sun Jan 13 20:25:41 2019 +0100 +++ b/src/HOL/Analysis/Bochner_Integration.thy Mon Jan 14 11:59:19 2019 +0000 @@ -15,12 +15,12 @@ \ -lemma%important borel_measurable_implies_sequence_metric: +proposition borel_measurable_implies_sequence_metric: fixes f :: "'a \ 'b :: {metric_space, second_countable_topology}" assumes [measurable]: "f \ borel_measurable M" shows "\F. (\i. simple_function M (F i)) \ (\x\space M. (\i. F i x) \ f x) \ (\i. \x\space M. dist (F i x) z \ 2 * dist (f x) z)" -proof%unimportant - +proof - obtain D :: "'b set" where "countable D" and D: "\X. open X \ X \ {} \ \d\D. d \ X" by (erule countable_dense_setE) @@ -155,14 +155,14 @@ qed qed -lemma%unimportant +lemma fixes f :: "'a \ 'b::semiring_1" assumes "finite A" shows sum_mult_indicator[simp]: "(\x \ A. f x * indicator (B x) (g x)) = (\x\{x\A. g x \ B x}. f x)" and sum_indicator_mult[simp]: "(\x \ A. indicator (B x) (g x) * f x) = (\x\{x\A. g x \ B x}. f x)" unfolding indicator_def using assms by (auto intro!: sum.mono_neutral_cong_right split: if_split_asm) -lemma%unimportant borel_measurable_induct_real[consumes 2, case_names set mult add seq]: +lemma borel_measurable_induct_real[consumes 2, case_names set mult add seq]: fixes P :: "('a \ real) \ bool" assumes u: "u \ borel_measurable M" "\x. 0 \ u x" assumes set: "\A. A \ sets M \ P (indicator A)" @@ -227,7 +227,7 @@ qed qed -lemma%unimportant scaleR_cong_right: +lemma scaleR_cong_right: fixes x :: "'a :: real_vector" shows "(x \ 0 \ r = p) \ r *\<^sub>R x = p *\<^sub>R x" by (cases "x = 0") auto @@ -236,7 +236,7 @@ "simple_function M f \ emeasure M {y\space M. f y \ 0} \ \ \ simple_bochner_integrable M f" -lemma%unimportant simple_bochner_integrable_compose2: +lemma simple_bochner_integrable_compose2: assumes p_0: "p 0 0 = 0" shows "simple_bochner_integrable M f \ simple_bochner_integrable M g \ simple_bochner_integrable M (\x. p (f x) (g x))" @@ -261,7 +261,7 @@ using fin by (auto simp: top_unique) qed -lemma%unimportant simple_function_finite_support: +lemma simple_function_finite_support: assumes f: "simple_function M f" and fin: "(\\<^sup>+x. f x \M) < \" and nn: "\x. 0 \ f x" shows "emeasure M {x\space M. f x \ 0} \ \" proof cases @@ -296,7 +296,7 @@ show ?thesis unfolding * by simp qed -lemma%unimportant simple_bochner_integrableI_bounded: +lemma simple_bochner_integrableI_bounded: assumes f: "simple_function M f" and fin: "(\\<^sup>+x. norm (f x) \M) < \" shows "simple_bochner_integrable M f" proof @@ -312,13 +312,13 @@ definition%important simple_bochner_integral :: "'a measure \ ('a \ 'b::real_vector) \ 'b" where "simple_bochner_integral M f = (\y\f`space M. measure M {x\space M. f x = y} *\<^sub>R y)" -lemma%important simple_bochner_integral_partition: +proposition simple_bochner_integral_partition: assumes f: "simple_bochner_integrable M f" and g: "simple_function M g" assumes sub: "\x y. x \ space M \ y \ space M \ g x = g y \ f x = f y" assumes v: "\x. x \ space M \ f x = v (g x)" shows "simple_bochner_integral M f = (\y\g ` space M. measure M {x\space M. g x = y} *\<^sub>R v y)" (is "_ = ?r") -proof%unimportant - +proof - from f g have [simp]: "finite (f`space M)" "finite (g`space M)" by (auto simp: simple_function_def elim: simple_bochner_integrable.cases) @@ -394,7 +394,7 @@ by (simp add: sum.distrib[symmetric] scaleR_add_right) qed -lemma%unimportant simple_bochner_integral_linear: +lemma simple_bochner_integral_linear: assumes "linear f" assumes g: "simple_bochner_integrable M g" shows "simple_bochner_integral M (\x. f (g x)) = f (simple_bochner_integral M g)" @@ -484,14 +484,14 @@ finally show ?thesis . qed -lemma%important simple_bochner_integral_bounded: +lemma simple_bochner_integral_bounded: fixes f :: "'a \ 'b::{real_normed_vector, second_countable_topology}" assumes f[measurable]: "f \ borel_measurable M" assumes s: "simple_bochner_integrable M s" and t: "simple_bochner_integrable M t" shows "ennreal (norm (simple_bochner_integral M s - simple_bochner_integral M t)) \ (\\<^sup>+ x. norm (f x - s x) \M) + (\\<^sup>+ x. norm (f x - t x) \M)" (is "ennreal (norm (?s - ?t)) \ ?S + ?T") -proof%unimportant - +proof - have [measurable]: "s \ borel_measurable M" "t \ borel_measurable M" using s t by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases) @@ -520,13 +520,13 @@ (\i. simple_bochner_integral M (s i)) \ x \ has_bochner_integral M f x" -lemma%unimportant has_bochner_integral_cong: +lemma has_bochner_integral_cong: assumes "M = N" "\x. x \ space N \ f x = g x" "x = y" shows "has_bochner_integral M f x \ has_bochner_integral N g y" unfolding has_bochner_integral.simps assms(1,3) using assms(2) by (simp cong: measurable_cong_simp nn_integral_cong_simp) -lemma%unimportant has_bochner_integral_cong_AE: +lemma has_bochner_integral_cong_AE: "f \ borel_measurable M \ g \ borel_measurable M \ (AE x in M. f x = g x) \ has_bochner_integral M f x \ has_bochner_integral M g x" unfolding has_bochner_integral.simps @@ -534,22 +534,22 @@ nn_integral_cong_AE) auto -lemma%unimportant borel_measurable_has_bochner_integral: +lemma borel_measurable_has_bochner_integral: "has_bochner_integral M f x \ f \ borel_measurable M" by (rule has_bochner_integral.cases) -lemma%unimportant borel_measurable_has_bochner_integral'[measurable_dest]: +lemma borel_measurable_has_bochner_integral'[measurable_dest]: "has_bochner_integral M f x \ g \ measurable N M \ (\x. f (g x)) \ borel_measurable N" using borel_measurable_has_bochner_integral[measurable] by measurable -lemma%unimportant has_bochner_integral_simple_bochner_integrable: +lemma has_bochner_integral_simple_bochner_integrable: "simple_bochner_integrable M f \ has_bochner_integral M f (simple_bochner_integral M f)" by (rule has_bochner_integral.intros[where s="\_. f"]) (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases simp: zero_ennreal_def[symmetric]) -lemma%unimportant has_bochner_integral_real_indicator: +lemma has_bochner_integral_real_indicator: assumes [measurable]: "A \ sets M" and A: "emeasure M A < \" shows "has_bochner_integral M (indicator A) (measure M A)" proof - @@ -567,7 +567,7 @@ by (metis has_bochner_integral_simple_bochner_integrable) qed -lemma%unimportant has_bochner_integral_add[intro]: +lemma has_bochner_integral_add[intro]: "has_bochner_integral M f x \ has_bochner_integral M g y \ has_bochner_integral M (\x. f x + g x) (x + y)" proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases) @@ -604,7 +604,7 @@ qed qed (auto simp: simple_bochner_integral_add tendsto_add) -lemma%unimportant has_bochner_integral_bounded_linear: +lemma has_bochner_integral_bounded_linear: assumes "bounded_linear T" shows "has_bochner_integral M f x \ has_bochner_integral M (\x. T (f x)) (T x)" proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases) @@ -650,79 +650,79 @@ by (auto intro!: T.tendsto simp: simple_bochner_integral_linear T.linear_axioms) qed -lemma%unimportant has_bochner_integral_zero[intro]: "has_bochner_integral M (\x. 0) 0" +lemma has_bochner_integral_zero[intro]: "has_bochner_integral M (\x. 0) 0" by (auto intro!: has_bochner_integral.intros[where s="\_ _. 0"] simp: zero_ennreal_def[symmetric] simple_bochner_integrable.simps simple_bochner_integral_def image_constant_conv) -lemma%unimportant has_bochner_integral_scaleR_left[intro]: +lemma has_bochner_integral_scaleR_left[intro]: "(c \ 0 \ has_bochner_integral M f x) \ has_bochner_integral M (\x. f x *\<^sub>R c) (x *\<^sub>R c)" by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_scaleR_left]) -lemma%unimportant has_bochner_integral_scaleR_right[intro]: +lemma has_bochner_integral_scaleR_right[intro]: "(c \ 0 \ has_bochner_integral M f x) \ has_bochner_integral M (\x. c *\<^sub>R f x) (c *\<^sub>R x)" by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_scaleR_right]) -lemma%unimportant has_bochner_integral_mult_left[intro]: +lemma has_bochner_integral_mult_left[intro]: fixes c :: "_::{real_normed_algebra,second_countable_topology}" shows "(c \ 0 \ has_bochner_integral M f x) \ has_bochner_integral M (\x. f x * c) (x * c)" by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_mult_left]) -lemma%unimportant has_bochner_integral_mult_right[intro]: +lemma has_bochner_integral_mult_right[intro]: fixes c :: "_::{real_normed_algebra,second_countable_topology}" shows "(c \ 0 \ has_bochner_integral M f x) \ has_bochner_integral M (\x. c * f x) (c * x)" by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_mult_right]) -lemmas%unimportant has_bochner_integral_divide = +lemmas has_bochner_integral_divide = has_bochner_integral_bounded_linear[OF bounded_linear_divide] -lemma%unimportant has_bochner_integral_divide_zero[intro]: +lemma has_bochner_integral_divide_zero[intro]: fixes c :: "_::{real_normed_field, field, second_countable_topology}" shows "(c \ 0 \ has_bochner_integral M f x) \ has_bochner_integral M (\x. f x / c) (x / c)" using has_bochner_integral_divide by (cases "c = 0") auto -lemma%unimportant has_bochner_integral_inner_left[intro]: +lemma has_bochner_integral_inner_left[intro]: "(c \ 0 \ has_bochner_integral M f x) \ has_bochner_integral M (\x. f x \ c) (x \ c)" by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_inner_left]) -lemma%unimportant has_bochner_integral_inner_right[intro]: +lemma has_bochner_integral_inner_right[intro]: "(c \ 0 \ has_bochner_integral M f x) \ has_bochner_integral M (\x. c \ f x) (c \ x)" by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_inner_right]) -lemmas%unimportant has_bochner_integral_minus = +lemmas has_bochner_integral_minus = has_bochner_integral_bounded_linear[OF bounded_linear_minus[OF bounded_linear_ident]] -lemmas%unimportant has_bochner_integral_Re = +lemmas has_bochner_integral_Re = has_bochner_integral_bounded_linear[OF bounded_linear_Re] -lemmas%unimportant has_bochner_integral_Im = +lemmas has_bochner_integral_Im = has_bochner_integral_bounded_linear[OF bounded_linear_Im] -lemmas%unimportant has_bochner_integral_cnj = +lemmas has_bochner_integral_cnj = has_bochner_integral_bounded_linear[OF bounded_linear_cnj] -lemmas%unimportant has_bochner_integral_of_real = +lemmas has_bochner_integral_of_real = has_bochner_integral_bounded_linear[OF bounded_linear_of_real] -lemmas%unimportant has_bochner_integral_fst = +lemmas has_bochner_integral_fst = has_bochner_integral_bounded_linear[OF bounded_linear_fst] -lemmas%unimportant has_bochner_integral_snd = +lemmas has_bochner_integral_snd = has_bochner_integral_bounded_linear[OF bounded_linear_snd] -lemma%unimportant has_bochner_integral_indicator: +lemma has_bochner_integral_indicator: "A \ sets M \ emeasure M A < \ \ has_bochner_integral M (\x. indicator A x *\<^sub>R c) (measure M A *\<^sub>R c)" by (intro has_bochner_integral_scaleR_left has_bochner_integral_real_indicator) -lemma%unimportant has_bochner_integral_diff: +lemma has_bochner_integral_diff: "has_bochner_integral M f x \ has_bochner_integral M g y \ has_bochner_integral M (\x. f x - g x) (x - y)" unfolding diff_conv_add_uminus by (intro has_bochner_integral_add has_bochner_integral_minus) -lemma%unimportant has_bochner_integral_sum: +lemma has_bochner_integral_sum: "(\i. i \ I \ has_bochner_integral M (f i) (x i)) \ has_bochner_integral M (\x. \i\I. f i x) (\i\I. x i)" by (induct I rule: infinite_finite_induct) auto -lemma%important has_bochner_integral_implies_finite_norm: +proposition has_bochner_integral_implies_finite_norm: "has_bochner_integral M f x \ (\\<^sup>+x. norm (f x) \M) < \" -proof%unimportant (elim has_bochner_integral.cases) +proof (elim has_bochner_integral.cases) fix s v assume [measurable]: "f \ borel_measurable M" and s: "\i. simple_bochner_integrable M (s i)" and lim_0: "(\i. \\<^sup>+ x. ennreal (norm (f x - s i x)) \M) \ 0" @@ -756,10 +756,10 @@ finally show "(\\<^sup>+ x. ennreal (norm (f x)) \M) < \" . qed -lemma%important has_bochner_integral_norm_bound: +proposition has_bochner_integral_norm_bound: assumes i: "has_bochner_integral M f x" shows "norm x \ (\\<^sup>+x. norm (f x) \M)" -using assms proof%unimportant +using assms proof fix s assume x: "(\i. simple_bochner_integral M (s i)) \ x" (is "?s \ x") and s[simp]: "\i. simple_bochner_integrable M (s i)" and @@ -797,9 +797,9 @@ qed qed -lemma%important has_bochner_integral_eq: +lemma has_bochner_integral_eq: "has_bochner_integral M f x \ has_bochner_integral M f y \ x = y" -proof%unimportant (elim has_bochner_integral.cases) +proof (elim has_bochner_integral.cases) assume f[measurable]: "f \ borel_measurable M" fix s t @@ -834,7 +834,7 @@ then show "x = y" by simp qed -lemma%unimportant has_bochner_integralI_AE: +lemma has_bochner_integralI_AE: assumes f: "has_bochner_integral M f x" and g: "g \ borel_measurable M" and ae: "AE x in M. f x = g x" @@ -848,7 +848,7 @@ finally show "(\i. \\<^sup>+ x. ennreal (norm (g x - s i x)) \M) \ 0" . qed (auto intro: g) -lemma%unimportant has_bochner_integral_eq_AE: +lemma has_bochner_integral_eq_AE: assumes f: "has_bochner_integral M f x" and g: "has_bochner_integral M g y" and ae: "AE x in M. f x = g x" @@ -860,7 +860,7 @@ by (rule has_bochner_integral_eq) qed -lemma%unimportant simple_bochner_integrable_restrict_space: +lemma simple_bochner_integrable_restrict_space: fixes f :: "_ \ 'b::real_normed_vector" assumes \: "\ \ space M \ sets M" shows "simple_bochner_integrable (restrict_space M \) f \ @@ -869,13 +869,13 @@ simple_function_restrict_space[OF \] emeasure_restrict_space[OF \] Collect_restrict indicator_eq_0_iff conj_left_commute) -lemma%important simple_bochner_integral_restrict_space: +lemma simple_bochner_integral_restrict_space: fixes f :: "_ \ 'b::real_normed_vector" assumes \: "\ \ space M \ sets M" assumes f: "simple_bochner_integrable (restrict_space M \) f" shows "simple_bochner_integral (restrict_space M \) f = simple_bochner_integral M (\x. indicator \ x *\<^sub>R f x)" -proof%unimportant - +proof - have "finite ((\x. indicator \ x *\<^sub>R f x)`space M)" using f simple_bochner_integrable_restrict_space[OF \, of f] by (simp add: simple_bochner_integrable.simps simple_function_def) @@ -910,155 +910,155 @@ translations "LINT x|M. f" == "CONST lebesgue_integral M (\x. f)" -lemma%unimportant has_bochner_integral_integral_eq: "has_bochner_integral M f x \ integral\<^sup>L M f = x" +lemma has_bochner_integral_integral_eq: "has_bochner_integral M f x \ integral\<^sup>L M f = x" by (metis the_equality has_bochner_integral_eq lebesgue_integral_def) -lemma%unimportant has_bochner_integral_integrable: +lemma has_bochner_integral_integrable: "integrable M f \ has_bochner_integral M f (integral\<^sup>L M f)" by (auto simp: has_bochner_integral_integral_eq integrable.simps) -lemma%unimportant has_bochner_integral_iff: +lemma has_bochner_integral_iff: "has_bochner_integral M f x \ integrable M f \ integral\<^sup>L M f = x" by (metis has_bochner_integral_integrable has_bochner_integral_integral_eq integrable.intros) -lemma%unimportant simple_bochner_integrable_eq_integral: +lemma simple_bochner_integrable_eq_integral: "simple_bochner_integrable M f \ simple_bochner_integral M f = integral\<^sup>L M f" using has_bochner_integral_simple_bochner_integrable[of M f] by (simp add: has_bochner_integral_integral_eq) -lemma%unimportant not_integrable_integral_eq: "\ integrable M f \ integral\<^sup>L M f = 0" +lemma not_integrable_integral_eq: "\ integrable M f \ integral\<^sup>L M f = 0" unfolding integrable.simps lebesgue_integral_def by (auto intro!: arg_cong[where f=The]) -lemma%unimportant integral_eq_cases: +lemma integral_eq_cases: "integrable M f \ integrable N g \ (integrable M f \ integrable N g \ integral\<^sup>L M f = integral\<^sup>L N g) \ integral\<^sup>L M f = integral\<^sup>L N g" by (metis not_integrable_integral_eq) -lemma%unimportant borel_measurable_integrable[measurable_dest]: "integrable M f \ f \ borel_measurable M" +lemma borel_measurable_integrable[measurable_dest]: "integrable M f \ f \ borel_measurable M" by (auto elim: integrable.cases has_bochner_integral.cases) -lemma%unimportant borel_measurable_integrable'[measurable_dest]: +lemma borel_measurable_integrable'[measurable_dest]: "integrable M f \ g \ measurable N M \ (\x. f (g x)) \ borel_measurable N" using borel_measurable_integrable[measurable] by measurable -lemma%unimportant integrable_cong: +lemma integrable_cong: "M = N \ (\x. x \ space N \ f x = g x) \ integrable M f \ integrable N g" by (simp cong: has_bochner_integral_cong add: integrable.simps) -lemma%unimportant integrable_cong_AE: +lemma integrable_cong_AE: "f \ borel_measurable M \ g \ borel_measurable M \ AE x in M. f x = g x \ integrable M f \ integrable M g" unfolding integrable.simps by (intro has_bochner_integral_cong_AE arg_cong[where f=Ex] ext) -lemma%unimportant integrable_cong_AE_imp: +lemma integrable_cong_AE_imp: "integrable M g \ f \ borel_measurable M \ (AE x in M. g x = f x) \ integrable M f" using integrable_cong_AE[of f M g] by (auto simp: eq_commute) -lemma%unimportant integral_cong: +lemma integral_cong: "M = N \ (\x. x \ space N \ f x = g x) \ integral\<^sup>L M f = integral\<^sup>L N g" by (simp cong: has_bochner_integral_cong cong del: if_weak_cong add: lebesgue_integral_def) -lemma%unimportant integral_cong_AE: +lemma integral_cong_AE: "f \ borel_measurable M \ g \ borel_measurable M \ AE x in M. f x = g x \ integral\<^sup>L M f = integral\<^sup>L M g" unfolding lebesgue_integral_def by (rule arg_cong[where x="has_bochner_integral M f"]) (intro has_bochner_integral_cong_AE ext) -lemma%unimportant integrable_add[simp, intro]: "integrable M f \ integrable M g \ integrable M (\x. f x + g x)" +lemma integrable_add[simp, intro]: "integrable M f \ integrable M g \ integrable M (\x. f x + g x)" by (auto simp: integrable.simps) -lemma%unimportant integrable_zero[simp, intro]: "integrable M (\x. 0)" +lemma integrable_zero[simp, intro]: "integrable M (\x. 0)" by (metis has_bochner_integral_zero integrable.simps) -lemma%unimportant integrable_sum[simp, intro]: "(\i. i \ I \ integrable M (f i)) \ integrable M (\x. \i\I. f i x)" +lemma integrable_sum[simp, intro]: "(\i. i \ I \ integrable M (f i)) \ integrable M (\x. \i\I. f i x)" by (metis has_bochner_integral_sum integrable.simps) -lemma%unimportant integrable_indicator[simp, intro]: "A \ sets M \ emeasure M A < \ \ +lemma integrable_indicator[simp, intro]: "A \ sets M \ emeasure M A < \ \ integrable M (\x. indicator A x *\<^sub>R c)" by (metis has_bochner_integral_indicator integrable.simps) -lemma%unimportant integrable_real_indicator[simp, intro]: "A \ sets M \ emeasure M A < \ \ +lemma integrable_real_indicator[simp, intro]: "A \ sets M \ emeasure M A < \ \ integrable M (indicator A :: 'a \ real)" by (metis has_bochner_integral_real_indicator integrable.simps) -lemma%unimportant integrable_diff[simp, intro]: "integrable M f \ integrable M g \ integrable M (\x. f x - g x)" +lemma integrable_diff[simp, intro]: "integrable M f \ integrable M g \ integrable M (\x. f x - g x)" by (auto simp: integrable.simps intro: has_bochner_integral_diff) -lemma%unimportant integrable_bounded_linear: "bounded_linear T \ integrable M f \ integrable M (\x. T (f x))" +lemma integrable_bounded_linear: "bounded_linear T \ integrable M f \ integrable M (\x. T (f x))" by (auto simp: integrable.simps intro: has_bochner_integral_bounded_linear) -lemma%unimportant integrable_scaleR_left[simp, intro]: "(c \ 0 \ integrable M f) \ integrable M (\x. f x *\<^sub>R c)" +lemma integrable_scaleR_left[simp, intro]: "(c \ 0 \ integrable M f) \ integrable M (\x. f x *\<^sub>R c)" unfolding integrable.simps by fastforce -lemma%unimportant integrable_scaleR_right[simp, intro]: "(c \ 0 \ integrable M f) \ integrable M (\x. c *\<^sub>R f x)" +lemma integrable_scaleR_right[simp, intro]: "(c \ 0 \ integrable M f) \ integrable M (\x. c *\<^sub>R f x)" unfolding integrable.simps by fastforce -lemma%unimportant integrable_mult_left[simp, intro]: +lemma integrable_mult_left[simp, intro]: fixes c :: "_::{real_normed_algebra,second_countable_topology}" shows "(c \ 0 \ integrable M f) \ integrable M (\x. f x * c)" unfolding integrable.simps by fastforce -lemma%unimportant integrable_mult_right[simp, intro]: +lemma integrable_mult_right[simp, intro]: fixes c :: "_::{real_normed_algebra,second_countable_topology}" shows "(c \ 0 \ integrable M f) \ integrable M (\x. c * f x)" unfolding integrable.simps by fastforce -lemma%unimportant integrable_divide_zero[simp, intro]: +lemma integrable_divide_zero[simp, intro]: fixes c :: "_::{real_normed_field, field, second_countable_topology}" shows "(c \ 0 \ integrable M f) \ integrable M (\x. f x / c)" unfolding integrable.simps by fastforce -lemma%unimportant integrable_inner_left[simp, intro]: +lemma integrable_inner_left[simp, intro]: "(c \ 0 \ integrable M f) \ integrable M (\x. f x \ c)" unfolding integrable.simps by fastforce -lemma%unimportant integrable_inner_right[simp, intro]: +lemma integrable_inner_right[simp, intro]: "(c \ 0 \ integrable M f) \ integrable M (\x. c \ f x)" unfolding integrable.simps by fastforce -lemmas%unimportant integrable_minus[simp, intro] = +lemmas integrable_minus[simp, intro] = integrable_bounded_linear[OF bounded_linear_minus[OF bounded_linear_ident]] -lemmas%unimportant integrable_divide[simp, intro] = +lemmas integrable_divide[simp, intro] = integrable_bounded_linear[OF bounded_linear_divide] -lemmas%unimportant integrable_Re[simp, intro] = +lemmas integrable_Re[simp, intro] = integrable_bounded_linear[OF bounded_linear_Re] -lemmas%unimportant integrable_Im[simp, intro] = +lemmas integrable_Im[simp, intro] = integrable_bounded_linear[OF bounded_linear_Im] -lemmas%unimportant integrable_cnj[simp, intro] = +lemmas integrable_cnj[simp, intro] = integrable_bounded_linear[OF bounded_linear_cnj] -lemmas%unimportant integrable_of_real[simp, intro] = +lemmas integrable_of_real[simp, intro] = integrable_bounded_linear[OF bounded_linear_of_real] -lemmas%unimportant integrable_fst[simp, intro] = +lemmas integrable_fst[simp, intro] = integrable_bounded_linear[OF bounded_linear_fst] -lemmas%unimportant integrable_snd[simp, intro] = +lemmas integrable_snd[simp, intro] = integrable_bounded_linear[OF bounded_linear_snd] -lemma%unimportant integral_zero[simp]: "integral\<^sup>L M (\x. 0) = 0" +lemma integral_zero[simp]: "integral\<^sup>L M (\x. 0) = 0" by (intro has_bochner_integral_integral_eq has_bochner_integral_zero) -lemma%unimportant integral_add[simp]: "integrable M f \ integrable M g \ +lemma integral_add[simp]: "integrable M f \ integrable M g \ integral\<^sup>L M (\x. f x + g x) = integral\<^sup>L M f + integral\<^sup>L M g" by (intro has_bochner_integral_integral_eq has_bochner_integral_add has_bochner_integral_integrable) -lemma%unimportant integral_diff[simp]: "integrable M f \ integrable M g \ +lemma integral_diff[simp]: "integrable M f \ integrable M g \ integral\<^sup>L M (\x. f x - g x) = integral\<^sup>L M f - integral\<^sup>L M g" by (intro has_bochner_integral_integral_eq has_bochner_integral_diff has_bochner_integral_integrable) -lemma%unimportant integral_sum: "(\i. i \ I \ integrable M (f i)) \ +lemma integral_sum: "(\i. i \ I \ integrable M (f i)) \ integral\<^sup>L M (\x. \i\I. f i x) = (\i\I. integral\<^sup>L M (f i))" by (intro has_bochner_integral_integral_eq has_bochner_integral_sum has_bochner_integral_integrable) -lemma%unimportant integral_sum'[simp]: "(\i. i \ I =simp=> integrable M (f i)) \ +lemma integral_sum'[simp]: "(\i. i \ I =simp=> integrable M (f i)) \ integral\<^sup>L M (\x. \i\I. f i x) = (\i\I. integral\<^sup>L M (f i))" unfolding simp_implies_def by (rule integral_sum) -lemma%unimportant integral_bounded_linear: "bounded_linear T \ integrable M f \ +lemma integral_bounded_linear: "bounded_linear T \ integrable M f \ integral\<^sup>L M (\x. T (f x)) = T (integral\<^sup>L M f)" by (metis has_bochner_integral_bounded_linear has_bochner_integral_integrable has_bochner_integral_integral_eq) -lemma%unimportant integral_bounded_linear': +lemma integral_bounded_linear': assumes T: "bounded_linear T" and T': "bounded_linear T'" assumes *: "\ (\x. T x = 0) \ (\x. T' (T x) = x)" shows "integral\<^sup>L M (\x. T (f x)) = T (integral\<^sup>L M f)" @@ -1085,76 +1085,76 @@ qed qed -lemma%unimportant integral_scaleR_left[simp]: "(c \ 0 \ integrable M f) \ (\ x. f x *\<^sub>R c \M) = integral\<^sup>L M f *\<^sub>R c" +lemma integral_scaleR_left[simp]: "(c \ 0 \ integrable M f) \ (\ x. f x *\<^sub>R c \M) = integral\<^sup>L M f *\<^sub>R c" by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_scaleR_left) -lemma%unimportant integral_scaleR_right[simp]: "(\ x. c *\<^sub>R f x \M) = c *\<^sub>R integral\<^sup>L M f" +lemma integral_scaleR_right[simp]: "(\ x. c *\<^sub>R f x \M) = c *\<^sub>R integral\<^sup>L M f" by (rule integral_bounded_linear'[OF bounded_linear_scaleR_right bounded_linear_scaleR_right[of "1 / c"]]) simp -lemma%unimportant integral_mult_left[simp]: +lemma integral_mult_left[simp]: fixes c :: "_::{real_normed_algebra,second_countable_topology}" shows "(c \ 0 \ integrable M f) \ (\ x. f x * c \M) = integral\<^sup>L M f * c" by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_mult_left) -lemma%unimportant integral_mult_right[simp]: +lemma integral_mult_right[simp]: fixes c :: "_::{real_normed_algebra,second_countable_topology}" shows "(c \ 0 \ integrable M f) \ (\ x. c * f x \M) = c * integral\<^sup>L M f" by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_mult_right) -lemma%unimportant integral_mult_left_zero[simp]: +lemma integral_mult_left_zero[simp]: fixes c :: "_::{real_normed_field,second_countable_topology}" shows "(\ x. f x * c \M) = integral\<^sup>L M f * c" by (rule integral_bounded_linear'[OF bounded_linear_mult_left bounded_linear_mult_left[of "1 / c"]]) simp -lemma%unimportant integral_mult_right_zero[simp]: +lemma integral_mult_right_zero[simp]: fixes c :: "_::{real_normed_field,second_countable_topology}" shows "(\ x. c * f x \M) = c * integral\<^sup>L M f" by (rule integral_bounded_linear'[OF bounded_linear_mult_right bounded_linear_mult_right[of "1 / c"]]) simp -lemma%unimportant integral_inner_left[simp]: "(c \ 0 \ integrable M f) \ (\ x. f x \ c \M) = integral\<^sup>L M f \ c" +lemma integral_inner_left[simp]: "(c \ 0 \ integrable M f) \ (\ x. f x \ c \M) = integral\<^sup>L M f \ c" by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_left) -lemma%unimportant integral_inner_right[simp]: "(c \ 0 \ integrable M f) \ (\ x. c \ f x \M) = c \ integral\<^sup>L M f" +lemma integral_inner_right[simp]: "(c \ 0 \ integrable M f) \ (\ x. c \ f x \M) = c \ integral\<^sup>L M f" by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_right) -lemma%unimportant integral_divide_zero[simp]: +lemma integral_divide_zero[simp]: fixes c :: "_::{real_normed_field, field, second_countable_topology}" shows "integral\<^sup>L M (\x. f x / c) = integral\<^sup>L M f / c" by (rule integral_bounded_linear'[OF bounded_linear_divide bounded_linear_mult_left[of c]]) simp -lemma%unimportant integral_minus[simp]: "integral\<^sup>L M (\x. - f x) = - integral\<^sup>L M f" +lemma integral_minus[simp]: "integral\<^sup>L M (\x. - f x) = - integral\<^sup>L M f" by (rule integral_bounded_linear'[OF bounded_linear_minus[OF bounded_linear_ident] bounded_linear_minus[OF bounded_linear_ident]]) simp -lemma%unimportant integral_complex_of_real[simp]: "integral\<^sup>L M (\x. complex_of_real (f x)) = of_real (integral\<^sup>L M f)" +lemma integral_complex_of_real[simp]: "integral\<^sup>L M (\x. complex_of_real (f x)) = of_real (integral\<^sup>L M f)" by (rule integral_bounded_linear'[OF bounded_linear_of_real bounded_linear_Re]) simp -lemma%unimportant integral_cnj[simp]: "integral\<^sup>L M (\x. cnj (f x)) = cnj (integral\<^sup>L M f)" +lemma integral_cnj[simp]: "integral\<^sup>L M (\x. cnj (f x)) = cnj (integral\<^sup>L M f)" by (rule integral_bounded_linear'[OF bounded_linear_cnj bounded_linear_cnj]) simp -lemmas%unimportant integral_divide[simp] = +lemmas integral_divide[simp] = integral_bounded_linear[OF bounded_linear_divide] -lemmas%unimportant integral_Re[simp] = +lemmas integral_Re[simp] = integral_bounded_linear[OF bounded_linear_Re] -lemmas%unimportant integral_Im[simp] = +lemmas integral_Im[simp] = integral_bounded_linear[OF bounded_linear_Im] -lemmas%unimportant integral_of_real[simp] = +lemmas integral_of_real[simp] = integral_bounded_linear[OF bounded_linear_of_real] -lemmas%unimportant integral_fst[simp] = +lemmas integral_fst[simp] = integral_bounded_linear[OF bounded_linear_fst] -lemmas%unimportant integral_snd[simp] = +lemmas integral_snd[simp] = integral_bounded_linear[OF bounded_linear_snd] -lemma%unimportant integral_norm_bound_ennreal: +lemma integral_norm_bound_ennreal: "integrable M f \ norm (integral\<^sup>L M f) \ (\\<^sup>+x. norm (f x) \M)" by (metis has_bochner_integral_integrable has_bochner_integral_norm_bound) -lemma%important integrableI_sequence: +lemma integrableI_sequence: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes f[measurable]: "f \ borel_measurable M" assumes s: "\i. simple_bochner_integrable M (s i)" assumes lim: "(\i. \\<^sup>+x. norm (f x - s i x) \M) \ 0" (is "?S \ 0") shows "integrable M f" -proof%unimportant - +proof - let ?s = "\n. simple_bochner_integral M (s n)" have "\x. ?s \ x" @@ -1184,7 +1184,7 @@ by (rule, rule) fact+ qed -lemma%important nn_integral_dominated_convergence_norm: +proposition nn_integral_dominated_convergence_norm: fixes u' :: "_ \ _::{real_normed_vector, second_countable_topology}" assumes [measurable]: "\i. u i \ borel_measurable M" "u' \ borel_measurable M" "w \ borel_measurable M" @@ -1192,7 +1192,7 @@ and w: "(\\<^sup>+x. w x \M) < \" and u': "AE x in M. (\i. u i x) \ u' x" shows "(\i. (\\<^sup>+x. norm (u' x - u i x) \M)) \ 0" -proof%unimportant - +proof - have "AE x in M. \j. norm (u j x) \ w x" unfolding AE_all_countable by rule fact with u' have bnd: "AE x in M. \j. norm (u' x - u j x) \ 2 * w x" @@ -1225,11 +1225,11 @@ then show ?thesis by simp qed -lemma%important integrableI_bounded: +proposition integrableI_bounded: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes f[measurable]: "f \ borel_measurable M" and fin: "(\\<^sup>+x. norm (f x) \M) < \" shows "integrable M f" -proof%unimportant - +proof - from borel_measurable_implies_sequence_metric[OF f, of 0] obtain s where s: "\i. simple_function M (s i)" and pointwise: "\x. x \ space M \ (\i. s i x) \ f x" and @@ -1266,14 +1266,14 @@ qed fact qed -lemma%important integrableI_bounded_set: +lemma integrableI_bounded_set: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes [measurable]: "A \ sets M" "f \ borel_measurable M" assumes finite: "emeasure M A < \" and bnd: "AE x in M. x \ A \ norm (f x) \ B" and null: "AE x in M. x \ A \ f x = 0" shows "integrable M f" -proof%unimportant (rule integrableI_bounded) +proof (rule integrableI_bounded) { fix x :: 'b have "norm x \ B \ 0 \ B" using norm_ge_zero[of x] by arith } with bnd null have "(\\<^sup>+ x. ennreal (norm (f x)) \M) \ (\\<^sup>+ x. ennreal (max 0 B) * indicator A x \M)" @@ -1283,37 +1283,37 @@ finally show "(\\<^sup>+ x. ennreal (norm (f x)) \M) < \" . qed simp -lemma%unimportant integrableI_bounded_set_indicator: +lemma integrableI_bounded_set_indicator: fixes f :: "'a \ 'b::{banach, second_countable_topology}" shows "A \ sets M \ f \ borel_measurable M \ emeasure M A < \ \ (AE x in M. x \ A \ norm (f x) \ B) \ integrable M (\x. indicator A x *\<^sub>R f x)" by (rule integrableI_bounded_set[where A=A]) auto -lemma%important integrableI_nonneg: +lemma integrableI_nonneg: fixes f :: "'a \ real" assumes "f \ borel_measurable M" "AE x in M. 0 \ f x" "(\\<^sup>+x. f x \M) < \" shows "integrable M f" -proof%unimportant - +proof - have "(\\<^sup>+x. norm (f x) \M) = (\\<^sup>+x. f x \M)" using assms by (intro nn_integral_cong_AE) auto then show ?thesis using assms by (intro integrableI_bounded) auto qed -lemma%important integrable_iff_bounded: +lemma integrable_iff_bounded: fixes f :: "'a \ 'b::{banach, second_countable_topology}" shows "integrable M f \ f \ borel_measurable M \ (\\<^sup>+x. norm (f x) \M) < \" using integrableI_bounded[of f M] has_bochner_integral_implies_finite_norm[of M f] unfolding integrable.simps has_bochner_integral.simps[abs_def] by auto -lemma%important integrable_bound: +lemma integrable_bound: fixes f :: "'a \ 'b::{banach, second_countable_topology}" and g :: "'a \ 'c::{banach, second_countable_topology}" shows "integrable M f \ g \ borel_measurable M \ (AE x in M. norm (g x) \ norm (f x)) \ integrable M g" unfolding integrable_iff_bounded -proof%unimportant safe +proof safe assume "f \ borel_measurable M" "g \ borel_measurable M" assume "AE x in M. norm (g x) \ norm (f x)" then have "(\\<^sup>+ x. ennreal (norm (g x)) \M) \ (\\<^sup>+ x. ennreal (norm (f x)) \M)" @@ -1322,71 +1322,71 @@ finally show "(\\<^sup>+ x. ennreal (norm (g x)) \M) < \" . qed -lemma%unimportant integrable_mult_indicator: +lemma integrable_mult_indicator: fixes f :: "'a \ 'b::{banach, second_countable_topology}" shows "A \ sets M \ integrable M f \ integrable M (\x. indicator A x *\<^sub>R f x)" by (rule integrable_bound[of M f]) (auto split: split_indicator) -lemma%unimportant integrable_real_mult_indicator: +lemma integrable_real_mult_indicator: fixes f :: "'a \ real" shows "A \ sets M \ integrable M f \ integrable M (\x. f x * indicator A x)" using integrable_mult_indicator[of A M f] by (simp add: mult_ac) -lemma%unimportant integrable_abs[simp, intro]: +lemma integrable_abs[simp, intro]: fixes f :: "'a \ real" assumes [measurable]: "integrable M f" shows "integrable M (\x. \f x\)" using assms by (rule integrable_bound) auto -lemma%unimportant integrable_norm[simp, intro]: +lemma integrable_norm[simp, intro]: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes [measurable]: "integrable M f" shows "integrable M (\x. norm (f x))" using assms by (rule integrable_bound) auto -lemma%unimportant integrable_norm_cancel: +lemma integrable_norm_cancel: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes [measurable]: "integrable M (\x. norm (f x))" "f \ borel_measurable M" shows "integrable M f" using assms by (rule integrable_bound) auto -lemma%unimportant integrable_norm_iff: +lemma integrable_norm_iff: fixes f :: "'a \ 'b::{banach, second_countable_topology}" shows "f \ borel_measurable M \ integrable M (\x. norm (f x)) \ integrable M f" by (auto intro: integrable_norm_cancel) -lemma%unimportant integrable_abs_cancel: +lemma integrable_abs_cancel: fixes f :: "'a \ real" assumes [measurable]: "integrable M (\x. \f x\)" "f \ borel_measurable M" shows "integrable M f" using assms by (rule integrable_bound) auto -lemma%unimportant integrable_abs_iff: +lemma integrable_abs_iff: fixes f :: "'a \ real" shows "f \ borel_measurable M \ integrable M (\x. \f x\) \ integrable M f" by (auto intro: integrable_abs_cancel) -lemma%unimportant integrable_max[simp, intro]: +lemma integrable_max[simp, intro]: fixes f :: "'a \ real" assumes fg[measurable]: "integrable M f" "integrable M g" shows "integrable M (\x. max (f x) (g x))" using integrable_add[OF integrable_norm[OF fg(1)] integrable_norm[OF fg(2)]] by (rule integrable_bound) auto -lemma%unimportant integrable_min[simp, intro]: +lemma integrable_min[simp, intro]: fixes f :: "'a \ real" assumes fg[measurable]: "integrable M f" "integrable M g" shows "integrable M (\x. min (f x) (g x))" using integrable_add[OF integrable_norm[OF fg(1)] integrable_norm[OF fg(2)]] by (rule integrable_bound) auto -lemma%unimportant integral_minus_iff[simp]: +lemma integral_minus_iff[simp]: "integrable M (\x. - f x ::'a::{banach, second_countable_topology}) \ integrable M f" unfolding integrable_iff_bounded by (auto intro: borel_measurable_uminus[of "\x. - f x" M, simplified]) -lemma%unimportant integrable_indicator_iff: +lemma integrable_indicator_iff: "integrable M (indicator A::_ \ real) \ A \ space M \ sets M \ emeasure M (A \ space M) < \" by (simp add: integrable_iff_bounded borel_measurable_indicator_iff ennreal_indicator nn_integral_indicator' cong: conj_cong) -lemma%unimportant integral_indicator[simp]: "integral\<^sup>L M (indicator A) = measure M (A \ space M)" +lemma integral_indicator[simp]: "integral\<^sup>L M (indicator A) = measure M (A \ space M)" proof cases assume *: "A \ space M \ sets M \ emeasure M (A \ space M) < \" have "integral\<^sup>L M (indicator A) = integral\<^sup>L M (indicator (A \ space M))" @@ -1405,7 +1405,7 @@ finally show ?thesis . qed -lemma%unimportant integrable_discrete_difference: +lemma integrable_discrete_difference: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes X: "countable X" assumes null: "\x. x \ X \ emeasure M {x} = 0" @@ -1429,7 +1429,7 @@ by simp qed -lemma%unimportant integral_discrete_difference: +lemma integral_discrete_difference: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes X: "countable X" assumes null: "\x. x \ X \ emeasure M {x} = 0" @@ -1453,7 +1453,7 @@ qed qed -lemma%unimportant has_bochner_integral_discrete_difference: +lemma has_bochner_integral_discrete_difference: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes X: "countable X" assumes null: "\x. x \ X \ emeasure M {x} = 0" @@ -1464,7 +1464,7 @@ using integral_discrete_difference[of X M f g, OF assms] by (metis has_bochner_integral_iff) -lemma%important (*FIX ME needs name *) +lemma (*FIX ME needs name *) fixes f :: "'a \ 'b::{banach, second_countable_topology}" and w :: "'a \ real" assumes "f \ borel_measurable M" "\i. s i \ borel_measurable M" "integrable M w" assumes lim: "AE x in M. (\i. s i x) \ f x" @@ -1472,7 +1472,7 @@ shows integrable_dominated_convergence: "integrable M f" and integrable_dominated_convergence2: "\i. integrable M (s i)" and integral_dominated_convergence: "(\i. integral\<^sup>L M (s i)) \ integral\<^sup>L M f" -proof%unimportant - +proof - have w_nonneg: "AE x in M. 0 \ w x" using bound[of 0] by eventually_elim (auto intro: norm_ge_zero order_trans) then have "(\\<^sup>+x. w x \M) = (\\<^sup>+x. norm (w x) \M)" @@ -1539,7 +1539,7 @@ assumes bound: "\\<^sub>F i in at_top. AE x in M. norm (s i x) \ w x" begin -lemma%unimportant integral_dominated_convergence_at_top: "((\t. integral\<^sup>L M (s t)) \ integral\<^sup>L M f) at_top" +lemma integral_dominated_convergence_at_top: "((\t. integral\<^sup>L M (s t)) \ integral\<^sup>L M f) at_top" proof (rule tendsto_at_topI_sequentially) fix X :: "nat \ real" assume X: "filterlim X at_top sequentially" from filterlim_iff[THEN iffD1, OF this, rule_format, OF bound] @@ -1560,7 +1560,7 @@ qed fact+ qed -lemma%unimportant integrable_dominated_convergence_at_top: "integrable M f" +lemma integrable_dominated_convergence_at_top: "integrable M f" proof - from bound obtain N where w: "\n. N \ n \ AE x in M. norm (s n x) \ w x" by (auto simp: eventually_at_top_linorder) @@ -1581,13 +1581,13 @@ end -lemma%unimportant integrable_mult_left_iff: +lemma integrable_mult_left_iff: fixes f :: "'a \ real" shows "integrable M (\x. c * f x) \ c = 0 \ integrable M f" using integrable_mult_left[of c M f] integrable_mult_left[of "1 / c" M "\x. c * f x"] by (cases "c = 0") auto -lemma%unimportant integrableI_nn_integral_finite: +lemma integrableI_nn_integral_finite: assumes [measurable]: "f \ borel_measurable M" and nonneg: "AE x in M. 0 \ f x" and finite: "(\\<^sup>+x. f x \M) = ennreal x" @@ -1599,7 +1599,7 @@ by auto qed simp -lemma%unimportant integral_nonneg_AE: +lemma integral_nonneg_AE: fixes f :: "'a \ real" assumes nonneg: "AE x in M. 0 \ f x" shows "0 \ integral\<^sup>L M f" @@ -1635,16 +1635,16 @@ finally show ?thesis . qed (simp add: not_integrable_integral_eq) -lemma%unimportant integral_nonneg[simp]: +lemma integral_nonneg[simp]: fixes f :: "'a \ real" shows "(\x. x \ space M \ 0 \ f x) \ 0 \ integral\<^sup>L M f" by (intro integral_nonneg_AE) auto -lemma%important nn_integral_eq_integral: +proposition nn_integral_eq_integral: assumes f: "integrable M f" assumes nonneg: "AE x in M. 0 \ f x" shows "(\\<^sup>+ x. f x \M) = integral\<^sup>L M f" -proof%unimportant - +proof - { fix f :: "'a \ real" assume f: "f \ borel_measurable M" "\x. 0 \ f x" "integrable M f" then have "(\\<^sup>+ x. f x \M) = integral\<^sup>L M f" proof (induct rule: borel_measurable_induct_real) @@ -1687,7 +1687,7 @@ finally show ?thesis . qed -lemma%unimportant nn_integral_eq_integrable: +lemma nn_integral_eq_integrable: assumes f: "f \ M \\<^sub>M borel" "AE x in M. 0 \ f x" and "0 \ x" shows "(\\<^sup>+x. f x \M) = ennreal x \ (integrable M f \ integral\<^sup>L M f = x)" proof (safe intro!: nn_integral_eq_integral assms) @@ -1697,7 +1697,7 @@ by (simp_all add: * assms integral_nonneg_AE) qed -lemma%unimportant (* FIX ME needs name*) +lemma (* FIX ME needs name*) fixes f :: "_ \ _ \ 'a :: {banach, second_countable_topology}" assumes integrable[measurable]: "\i. integrable M (f i)" and summable: "AE x in M. summable (\i. norm (f i x))" @@ -1748,10 +1748,10 @@ unfolding sums_iff by auto qed -lemma%important integral_norm_bound [simp]: +proposition integral_norm_bound [simp]: fixes f :: "_ \ 'a :: {banach, second_countable_topology}" shows "norm (integral\<^sup>L M f) \ (\x. norm (f x) \M)" -proof%unimportant (cases "integrable M f") +proof (cases "integrable M f") case True then show ?thesis using nn_integral_eq_integral[of M "\x. norm (f x)"] integral_norm_bound_ennreal[of M f] by (simp add: integral_nonneg_AE) @@ -1762,11 +1762,11 @@ ultimately show ?thesis by simp qed -lemma%unimportant integral_abs_bound [simp]: +proposition integral_abs_bound [simp]: fixes f :: "'a \ real" shows "abs (\x. f x \M) \ (\x. \f x\ \M)" using integral_norm_bound[of M f] by auto -lemma%unimportant integral_eq_nn_integral: +lemma integral_eq_nn_integral: assumes [measurable]: "f \ borel_measurable M" assumes nonneg: "AE x in M. 0 \ f x" shows "integral\<^sup>L M f = enn2real (\\<^sup>+ x. ennreal (f x) \M)" @@ -1787,7 +1787,7 @@ by (simp add: integral_nonneg_AE) qed -lemma%unimportant enn2real_nn_integral_eq_integral: +lemma enn2real_nn_integral_eq_integral: assumes eq: "AE x in M. f x = ennreal (g x)" and nn: "AE x in M. 0 \ g x" and fin: "(\\<^sup>+x. f x \M) < top" and [measurable]: "g \ M \\<^sub>M borel" @@ -1812,20 +1812,20 @@ using nn by (simp add: integral_nonneg_AE) qed -lemma%unimportant has_bochner_integral_nn_integral: +lemma has_bochner_integral_nn_integral: assumes "f \ borel_measurable M" "AE x in M. 0 \ f x" "0 \ x" assumes "(\\<^sup>+x. f x \M) = ennreal x" shows "has_bochner_integral M f x" unfolding has_bochner_integral_iff using assms by (auto simp: assms integral_eq_nn_integral intro: integrableI_nn_integral_finite) -lemma%unimportant integrableI_simple_bochner_integrable: +lemma integrableI_simple_bochner_integrable: fixes f :: "'a \ 'b::{banach, second_countable_topology}" shows "simple_bochner_integrable M f \ integrable M f" by (intro integrableI_sequence[where s="\_. f"] borel_measurable_simple_function) (auto simp: zero_ennreal_def[symmetric] simple_bochner_integrable.simps) -lemma%important integrable_induct[consumes 1, case_names base add lim, induct pred: integrable]: +proposition integrable_induct[consumes 1, case_names base add lim, induct pred: integrable]: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes "integrable M f" assumes base: "\A c. A \ sets M \ emeasure M A < \ \ P (\x. indicator A x *\<^sub>R c)" @@ -1834,7 +1834,7 @@ (\x. x \ space M \ (\i. s i x) \ f x) \ (\i x. x \ space M \ norm (s i x) \ 2 * norm (f x)) \ integrable M f \ P f" shows "P f" -proof%unimportant - +proof - from \integrable M f\ have f: "f \ borel_measurable M" "(\\<^sup>+x. norm (f x) \M) < \" unfolding integrable_iff_bounded by auto from borel_measurable_implies_sequence_metric[OF f(1)] @@ -1895,12 +1895,12 @@ qed fact qed -lemma%unimportant integral_eq_zero_AE: +lemma integral_eq_zero_AE: "(AE x in M. f x = 0) \ integral\<^sup>L M f = 0" using integral_cong_AE[of f M "\_. 0"] by (cases "integrable M f") (simp_all add: not_integrable_integral_eq) -lemma%unimportant integral_nonneg_eq_0_iff_AE: +lemma integral_nonneg_eq_0_iff_AE: fixes f :: "_ \ real" assumes f[measurable]: "integrable M f" and nonneg: "AE x in M. 0 \ f x" shows "integral\<^sup>L M f = 0 \ (AE x in M. f x = 0)" @@ -1914,7 +1914,7 @@ by auto qed (auto simp add: integral_eq_zero_AE) -lemma%unimportant integral_mono_AE: +lemma integral_mono_AE: fixes f :: "'a \ real" assumes "integrable M f" "integrable M g" "AE x in M. f x \ g x" shows "integral\<^sup>L M f \ integral\<^sup>L M g" @@ -1926,7 +1926,7 @@ finally show ?thesis by simp qed -lemma%unimportant integral_mono: +lemma integral_mono: fixes f :: "'a \ real" shows "integrable M f \ integrable M g \ (\x. x \ space M \ f x \ g x) \ integral\<^sup>L M f \ integral\<^sup>L M g" @@ -1936,11 +1936,11 @@ integrability assumption. The price to pay is that the upper function has to be nonnegative, but this is often true and easy to check in computations.\ -lemma%important integral_mono_AE': +lemma integral_mono_AE': fixes f::"_ \ real" assumes "integrable M f" "AE x in M. g x \ f x" "AE x in M. 0 \ f x" shows "(\x. g x \M) \ (\x. f x \M)" -proof%unimportant (cases "integrable M g") +proof (cases "integrable M g") case True show ?thesis by (rule integral_mono_AE, auto simp add: assms True) next @@ -1950,16 +1950,16 @@ finally show ?thesis by simp qed -lemma%important integral_mono': +lemma integral_mono': fixes f::"_ \ real" assumes "integrable M f" "\x. x \ space M \ g x \ f x" "\x. x \ space M \ 0 \ f x" shows "(\x. g x \M) \ (\x. f x \M)" by (rule integral_mono_AE', insert assms, auto) -lemma%important (in finite_measure) integrable_measure: +lemma (in finite_measure) integrable_measure: assumes I: "disjoint_family_on X I" "countable I" shows "integrable (count_space I) (\i. measure M (X i))" -proof%unimportant - +proof - have "(\\<^sup>+i. measure M (X i) \count_space I) = (\\<^sup>+i. measure M (if X i \ sets M then X i else {}) \count_space I)" by (auto intro!: nn_integral_cong measure_notin_sets) also have "\ = measure M (\i\I. if X i \ sets M then X i else {})" @@ -1969,7 +1969,7 @@ by (auto intro!: integrableI_bounded) qed -lemma%unimportant integrableI_real_bounded: +lemma integrableI_real_bounded: assumes f: "f \ borel_measurable M" and ae: "AE x in M. 0 \ f x" and fin: "integral\<^sup>N M f < \" shows "integrable M f" proof (rule integrableI_bounded) @@ -1979,13 +1979,13 @@ finally show "(\\<^sup>+ x. ennreal (norm (f x)) \M) < \" . qed fact -lemma%unimportant nn_integral_nonneg_infinite: +lemma nn_integral_nonneg_infinite: fixes f::"'a \ real" assumes "f \ borel_measurable M" "\ integrable M f" "AE x in M. f x \ 0" shows "(\\<^sup>+x. f x \M) = \" using assms integrableI_real_bounded less_top by auto -lemma%unimportant integral_real_bounded: +lemma integral_real_bounded: assumes "0 \ r" "integral\<^sup>N M f \ ennreal r" shows "integral\<^sup>L M f \ r" proof cases @@ -2009,22 +2009,22 @@ using \0 \ r\ by (simp add: not_integrable_integral_eq) qed -lemma%unimportant integrable_MIN: +lemma integrable_MIN: fixes f:: "_ \ _ \ real" shows "\ finite I; I \ {}; \i. i \ I \ integrable M (f i) \ \ integrable M (\x. MIN i\I. f i x)" by (induct rule: finite_ne_induct) simp+ -lemma%unimportant integrable_MAX: +lemma integrable_MAX: fixes f:: "_ \ _ \ real" shows "\ finite I; I \ {}; \i. i \ I \ integrable M (f i) \ \ integrable M (\x. MAX i\I. f i x)" by (induct rule: finite_ne_induct) simp+ -lemma%important integral_Markov_inequality: +theorem integral_Markov_inequality: assumes [measurable]: "integrable M u" and "AE x in M. 0 \ u x" "0 < (c::real)" shows "(emeasure M) {x\space M. u x \ c} \ (1/c) * (\x. u x \M)" -proof%unimportant - +proof - have "(\\<^sup>+ x. ennreal(u x) * indicator (space M) x \M) \ (\\<^sup>+ x. u x \M)" by (rule nn_integral_mono_AE, auto simp add: \c>0\ less_eq_real_def) also have "... = (\x. u x \M)" @@ -2044,7 +2044,7 @@ using \0 by (simp add: ennreal_mult'[symmetric]) qed -lemma%unimportant integral_ineq_eq_0_then_AE: +lemma integral_ineq_eq_0_then_AE: fixes f::"_ \ real" assumes "AE x in M. f x \ g x" "integrable M f" "integrable M g" "(\x. f x \M) = (\x. g x \M)" @@ -2057,7 +2057,7 @@ then show ?thesis unfolding h_def by auto qed -lemma%unimportant not_AE_zero_int_E: +lemma not_AE_zero_int_E: fixes f::"'a \ real" assumes "AE x in M. f x \ 0" "(\x. f x \M) > 0" and [measurable]: "f \ borel_measurable M" @@ -2069,12 +2069,12 @@ then show False using assms(2) by simp qed -lemma%important tendsto_L1_int: +proposition tendsto_L1_int: fixes u :: "_ \ _ \ 'b::{banach, second_countable_topology}" assumes [measurable]: "\n. integrable M (u n)" "integrable M f" and "((\n. (\\<^sup>+x. norm(u n x - f x) \M)) \ 0) F" shows "((\n. (\x. u n x \M)) \ (\x. f x \M)) F" -proof%unimportant - +proof - have "((\n. norm((\x. u n x \M) - (\x. f x \M))) \ (0::ennreal)) F" proof (rule tendsto_sandwich[of "\_. 0", where ?h = "\n. (\\<^sup>+x. norm(u n x - f x) \M)"], auto simp add: assms) { @@ -2103,12 +2103,12 @@ text \The next lemma asserts that, if a sequence of functions converges in \L\<^sup>1\, then it admits a subsequence that converges almost everywhere.\ -lemma%important tendsto_L1_AE_subseq: +proposition tendsto_L1_AE_subseq: fixes u :: "nat \ 'a \ 'b::{banach, second_countable_topology}" assumes [measurable]: "\n. integrable M (u n)" and "(\n. (\x. norm(u n x) \M)) \ 0" shows "\r::nat\nat. strict_mono r \ (AE x in M. (\n. u (r n) x) \ 0)" -proof%unimportant - +proof - { fix k have "eventually (\n. (\x. norm(u n x) \M) < (1/2)^k) sequentially" @@ -2203,7 +2203,7 @@ subsection%important \Restricted measure spaces\ -lemma%unimportant integrable_restrict_space: +lemma integrable_restrict_space: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes \[simp]: "\ \ space M \ sets M" shows "integrable (restrict_space M \) f \ integrable M (\x. indicator \ x *\<^sub>R f x)" @@ -2212,11 +2212,11 @@ nn_integral_restrict_space[OF \] by (simp add: ac_simps ennreal_indicator ennreal_mult) -lemma%important integral_restrict_space: +lemma integral_restrict_space: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes \[simp]: "\ \ space M \ sets M" shows "integral\<^sup>L (restrict_space M \) f = integral\<^sup>L M (\x. indicator \ x *\<^sub>R f x)" -proof%unimportant (rule integral_eq_cases) +proof (rule integral_eq_cases) assume "integrable (restrict_space M \) f" then show ?thesis proof induct @@ -2243,7 +2243,7 @@ qed qed (simp add: integrable_restrict_space) -lemma%unimportant integral_empty: +lemma integral_empty: assumes "space M = {}" shows "integral\<^sup>L M f = 0" proof - @@ -2254,7 +2254,7 @@ subsection%important \Measure spaces with an associated density\ -lemma%unimportant integrable_density: +lemma integrable_density: fixes f :: "'a \ 'b::{banach, second_countable_topology}" and g :: "'a \ real" assumes [measurable]: "f \ borel_measurable M" "g \ borel_measurable M" and nn: "AE x in M. 0 \ g x" @@ -2265,12 +2265,12 @@ apply (auto simp: ennreal_mult) done -lemma%important integral_density: +lemma integral_density: fixes f :: "'a \ 'b::{banach, second_countable_topology}" and g :: "'a \ real" assumes f: "f \ borel_measurable M" and g[measurable]: "g \ borel_measurable M" "AE x in M. 0 \ g x" shows "integral\<^sup>L (density M g) f = integral\<^sup>L M (\x. g x *\<^sub>R f x)" -proof%unimportant (rule integral_eq_cases) +proof (rule integral_eq_cases) assume "integrable (density M g) f" then show ?thesis proof induct @@ -2325,14 +2325,14 @@ qed qed (simp add: f g integrable_density) -lemma%unimportant (*FIX ME needs name *) +lemma (*FIX ME needs name *) fixes g :: "'a \ real" assumes "f \ borel_measurable M" "AE x in M. 0 \ f x" "g \ borel_measurable M" shows integral_real_density: "integral\<^sup>L (density M f) g = (\ x. f x * g x \M)" and integrable_real_density: "integrable (density M f) g \ integrable M (\x. f x * g x)" using assms integral_density[of g M f] integrable_density[of g M f] by auto -lemma%important has_bochner_integral_density: +lemma has_bochner_integral_density: fixes f :: "'a \ 'b::{banach, second_countable_topology}" and g :: "'a \ real" shows "f \ borel_measurable M \ g \ borel_measurable M \ (AE x in M. 0 \ g x) \ has_bochner_integral M (\x. g x *\<^sub>R f x) x \ has_bochner_integral (density M g) f x" @@ -2340,23 +2340,23 @@ subsection%important \Distributions\ -lemma%unimportant integrable_distr_eq: +lemma integrable_distr_eq: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes [measurable]: "g \ measurable M N" "f \ borel_measurable N" shows "integrable (distr M N g) f \ integrable M (\x. f (g x))" unfolding integrable_iff_bounded by (simp_all add: nn_integral_distr) -lemma%unimportant integrable_distr: +lemma integrable_distr: fixes f :: "'a \ 'b::{banach, second_countable_topology}" shows "T \ measurable M M' \ integrable (distr M M' T) f \ integrable M (\x. f (T x))" by (subst integrable_distr_eq[symmetric, where g=T]) (auto dest: borel_measurable_integrable) -lemma%important integral_distr: +lemma integral_distr: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes g[measurable]: "g \ measurable M N" and f: "f \ borel_measurable N" shows "integral\<^sup>L (distr M N g) f = integral\<^sup>L M (\x. f (g x))" -proof%unimportant (rule integral_eq_cases) +proof (rule integral_eq_cases) assume "integrable (distr M N g) f" then show ?thesis proof induct @@ -2404,27 +2404,27 @@ qed qed (simp add: f g integrable_distr_eq) -lemma%important has_bochner_integral_distr: +lemma has_bochner_integral_distr: fixes f :: "'a \ 'b::{banach, second_countable_topology}" shows "f \ borel_measurable N \ g \ measurable M N \ has_bochner_integral M (\x. f (g x)) x \ has_bochner_integral (distr M N g) f x" - by%unimportant (simp add: has_bochner_integral_iff integrable_distr_eq integral_distr) + by (simp add: has_bochner_integral_iff integrable_distr_eq integral_distr) subsection%important \Lebesgue integration on \<^const>\count_space\\ -lemma%unimportant integrable_count_space: +lemma integrable_count_space: fixes f :: "'a \ 'b::{banach,second_countable_topology}" shows "finite X \ integrable (count_space X) f" by (auto simp: nn_integral_count_space integrable_iff_bounded) -lemma%unimportant measure_count_space[simp]: +lemma measure_count_space[simp]: "B \ A \ finite B \ measure (count_space A) B = card B" unfolding measure_def by (subst emeasure_count_space ) auto -lemma%important lebesgue_integral_count_space_finite_support: +lemma lebesgue_integral_count_space_finite_support: assumes f: "finite {a\A. f a \ 0}" shows "(\x. f x \count_space A) = (\a | a \ A \ f a \ 0. f a)" -proof%unimportant - +proof - have eq: "\x. x \ A \ (\a | x = a \ a \ A \ f a \ 0. f a) = (\x\{x}. f x)" by (intro sum.mono_neutral_cong_left) auto @@ -2436,17 +2436,17 @@ by auto qed -lemma%unimportant lebesgue_integral_count_space_finite: "finite A \ (\x. f x \count_space A) = (\a\A. f a)" +lemma lebesgue_integral_count_space_finite: "finite A \ (\x. f x \count_space A) = (\a\A. f a)" by (subst lebesgue_integral_count_space_finite_support) (auto intro!: sum.mono_neutral_cong_left) -lemma%unimportant integrable_count_space_nat_iff: +lemma integrable_count_space_nat_iff: fixes f :: "nat \ _::{banach,second_countable_topology}" shows "integrable (count_space UNIV) f \ summable (\x. norm (f x))" by (auto simp add: integrable_iff_bounded nn_integral_count_space_nat ennreal_suminf_neq_top intro: summable_suminf_not_top) -lemma%unimportant sums_integral_count_space_nat: +lemma sums_integral_count_space_nat: fixes f :: "nat \ _::{banach,second_countable_topology}" assumes *: "integrable (count_space UNIV) f" shows "f sums (integral\<^sup>L (count_space UNIV) f)" @@ -2471,18 +2471,18 @@ finally show ?thesis . qed -lemma%unimportant integral_count_space_nat: +lemma integral_count_space_nat: fixes f :: "nat \ _::{banach,second_countable_topology}" shows "integrable (count_space UNIV) f \ integral\<^sup>L (count_space UNIV) f = (\x. f x)" using sums_integral_count_space_nat by (rule sums_unique) -lemma%unimportant integrable_bij_count_space: +lemma integrable_bij_count_space: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes g: "bij_betw g A B" shows "integrable (count_space A) (\x. f (g x)) \ integrable (count_space B) f" unfolding integrable_iff_bounded by (subst nn_integral_bij_count_space[OF g]) auto -lemma%important integral_bij_count_space: +lemma integral_bij_count_space: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes g: "bij_betw g A B" shows "integral\<^sup>L (count_space A) (\x. f (g x)) = integral\<^sup>L (count_space B) f" @@ -2492,23 +2492,23 @@ apply auto done -lemma%important has_bochner_integral_count_space_nat: +lemma has_bochner_integral_count_space_nat: fixes f :: "nat \ _::{banach,second_countable_topology}" shows "has_bochner_integral (count_space UNIV) f x \ f sums x" unfolding has_bochner_integral_iff by (auto intro!: sums_integral_count_space_nat) subsection%important \Point measure\ -lemma%unimportant lebesgue_integral_point_measure_finite: +lemma lebesgue_integral_point_measure_finite: fixes g :: "'a \ 'b::{banach, second_countable_topology}" shows "finite A \ (\a. a \ A \ 0 \ f a) \ integral\<^sup>L (point_measure A f) g = (\a\A. f a *\<^sub>R g a)" by (simp add: lebesgue_integral_count_space_finite AE_count_space integral_density point_measure_def) -lemma%important integrable_point_measure_finite: +proposition integrable_point_measure_finite: fixes g :: "'a \ 'b::{banach, second_countable_topology}" and f :: "'a \ real" shows "finite A \ integrable (point_measure A f) g" - unfolding%unimportant point_measure_def + unfolding point_measure_def apply (subst density_cong[where f'="\x. ennreal (max 0 (f x))"]) apply (auto split: split_max simp: ennreal_neg) apply (subst integrable_density) @@ -2517,24 +2517,23 @@ subsection%important \Lebesgue integration on \<^const>\null_measure\\ -lemma%unimportant has_bochner_integral_null_measure_iff[iff]: +lemma has_bochner_integral_null_measure_iff[iff]: "has_bochner_integral (null_measure M) f 0 \ f \ borel_measurable M" by (auto simp add: has_bochner_integral.simps simple_bochner_integral_def[abs_def] intro!: exI[of _ "\n x. 0"] simple_bochner_integrable.intros) -lemma%important integrable_null_measure_iff[iff]: "integrable (null_measure M) f \ f \ borel_measurable M" - by%unimportant (auto simp add: integrable.simps) - -lemma%unimportant integral_null_measure[simp]: "integral\<^sup>L (null_measure M) f = 0" +lemma integrable_null_measure_iff[iff]: "integrable (null_measure M) f \ f \ borel_measurable M" + by (auto simp add: integrable.simps) + +lemma integral_null_measure[simp]: "integral\<^sup>L (null_measure M) f = 0" by (cases "integrable (null_measure M) f") (auto simp add: not_integrable_integral_eq has_bochner_integral_integral_eq) subsection%important \Legacy lemmas for the real-valued Lebesgue integral\ - -lemma%important real_lebesgue_integral_def: +theorem real_lebesgue_integral_def: assumes f[measurable]: "integrable M f" shows "integral\<^sup>L M f = enn2real (\\<^sup>+x. f x \M) - enn2real (\\<^sup>+x. ennreal (- f x) \M)" -proof%unimportant - +proof - have "integral\<^sup>L M f = integral\<^sup>L M (\x. max 0 (f x) - max 0 (- f x))" by (auto intro!: arg_cong[where f="integral\<^sup>L M"]) also have "\ = integral\<^sup>L M (\x. max 0 (f x)) - integral\<^sup>L M (\x. max 0 (- f x))" @@ -2546,11 +2545,11 @@ finally show ?thesis . qed -lemma%important real_integrable_def: +theorem real_integrable_def: "integrable M f \ f \ borel_measurable M \ (\\<^sup>+ x. ennreal (f x) \M) \ \ \ (\\<^sup>+ x. ennreal (- f x) \M) \ \" unfolding integrable_iff_bounded -proof%unimportant (safe del: notI) +proof (safe del: notI) assume *: "(\\<^sup>+ x. ennreal (norm (f x)) \M) < \" have "(\\<^sup>+ x. ennreal (f x) \M) \ (\\<^sup>+ x. ennreal (norm (f x)) \M)" by (intro nn_integral_mono) auto @@ -2574,12 +2573,12 @@ finally show "(\\<^sup>+ x. norm (f x) \M) < \" . qed -lemma%unimportant integrableD[dest]: +lemma integrableD[dest]: assumes "integrable M f" shows "f \ borel_measurable M" "(\\<^sup>+ x. ennreal (f x) \M) \ \" "(\\<^sup>+ x. ennreal (- f x) \M) \ \" using assms unfolding real_integrable_def by auto -lemma%unimportant integrableE: +lemma integrableE: assumes "integrable M f" obtains r q where "0 \ r" "0 \ q" "(\\<^sup>+x. ennreal (f x)\M) = ennreal r" @@ -2588,7 +2587,7 @@ using assms unfolding real_integrable_def real_lebesgue_integral_def[OF assms] by (cases rule: ennreal2_cases[of "(\\<^sup>+x. ennreal (-f x)\M)" "(\\<^sup>+x. ennreal (f x)\M)"]) auto -lemma%important integral_monotone_convergence_nonneg: +lemma integral_monotone_convergence_nonneg: fixes f :: "nat \ 'a \ real" assumes i: "\i. integrable M (f i)" and mono: "AE x in M. mono (\n. f n x)" and pos: "\i. AE x in M. 0 \ f i x" @@ -2597,7 +2596,7 @@ and u: "u \ borel_measurable M" shows "integrable M u" and "integral\<^sup>L M u = x" -proof%unimportant - +proof - have nn: "AE x in M. \i. 0 \ f i x" using pos unfolding AE_all_countable by auto with lim have u_nn: "AE x in M. 0 \ u x" @@ -2629,7 +2628,7 @@ by (auto simp: real_integrable_def real_lebesgue_integral_def u) qed -lemma%unimportant (*FIX ME needs name *) +lemma (*FIX ME needs name *) fixes f :: "nat \ 'a \ real" assumes f: "\i. integrable M (f i)" and mono: "AE x in M. mono (\n. f n x)" and lim: "AE x in M. (\i. f i x) \ u x" @@ -2660,7 +2659,7 @@ by (metis has_bochner_integral_integrable) qed -lemma%unimportant integral_norm_eq_0_iff: +lemma integral_norm_eq_0_iff: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes f[measurable]: "integrable M f" shows "(\x. norm (f x) \M) = 0 \ emeasure M {x\space M. f x \ 0} = 0" @@ -2675,18 +2674,18 @@ by simp qed -lemma%unimportant integral_0_iff: +lemma integral_0_iff: fixes f :: "'a \ real" shows "integrable M f \ (\x. \f x\ \M) = 0 \ emeasure M {x\space M. f x \ 0} = 0" using integral_norm_eq_0_iff[of M f] by simp -lemma%unimportant (in finite_measure) integrable_const[intro!, simp]: "integrable M (\x. a)" +lemma (in finite_measure) integrable_const[intro!, simp]: "integrable M (\x. a)" using integrable_indicator[of "space M" M a] by (simp cong: integrable_cong add: less_top[symmetric]) -lemma%important lebesgue_integral_const[simp]: +lemma lebesgue_integral_const[simp]: fixes a :: "'a :: {banach, second_countable_topology}" shows "(\x. a \M) = measure M (space M) *\<^sub>R a" -proof%unimportant - +proof - { assume "emeasure M (space M) = \" "a \ 0" then have ?thesis by (auto simp add: not_integrable_integral_eq ennreal_mult_less_top measure_def integrable_iff_bounded) } @@ -2704,7 +2703,7 @@ ultimately show ?thesis by blast qed -lemma%unimportant (in finite_measure) integrable_const_bound: +lemma (in finite_measure) integrable_const_bound: fixes f :: "'a \ 'b::{banach,second_countable_topology}" shows "AE x in M. norm (f x) \ B \ f \ borel_measurable M \ integrable M f" apply (rule integrable_bound[OF integrable_const[of B], of f]) @@ -2713,19 +2712,19 @@ apply auto done -lemma%unimportant (in finite_measure) integral_bounded_eq_bound_then_AE: +lemma (in finite_measure) integral_bounded_eq_bound_then_AE: assumes "AE x in M. f x \ (c::real)" "integrable M f" "(\x. f x \M) = c * measure M (space M)" shows "AE x in M. f x = c" apply (rule integral_ineq_eq_0_then_AE) using assms by auto -lemma%important integral_indicator_finite_real: +lemma integral_indicator_finite_real: fixes f :: "'a \ real" assumes [simp]: "finite A" assumes [measurable]: "\a. a \ A \ {a} \ sets M" assumes finite: "\a. a \ A \ emeasure M {a} < \" shows "(\x. f x * indicator A x \M) = (\a\A. f a * measure M {a})" -proof%unimportant - +proof - have "(\x. f x * indicator A x \M) = (\x. (\a\A. f a * indicator {a} x) \M)" proof (intro integral_cong refl) fix x show "f x * indicator A x = (\a\A. f a * indicator {a} x)" @@ -2736,7 +2735,7 @@ finally show ?thesis . qed -lemma%unimportant (in finite_measure) ennreal_integral_real: +lemma (in finite_measure) ennreal_integral_real: assumes [measurable]: "f \ borel_measurable M" assumes ae: "AE x in M. f x \ ennreal B" "0 \ B" shows "ennreal (\x. enn2real (f x) \M) = (\\<^sup>+x. f x \M)" @@ -2747,7 +2746,7 @@ using ae by (intro nn_integral_cong_AE) (auto simp: le_less_trans[OF _ ennreal_less_top]) qed auto -lemma%unimportant (in finite_measure) integral_less_AE: +lemma (in finite_measure) integral_less_AE: fixes X Y :: "'a \ real" assumes int: "integrable M X" "integrable M Y" assumes A: "(emeasure M) A \ 0" "A \ sets M" "AE x in M. x \ A \ X x \ Y x" @@ -2778,14 +2777,14 @@ ultimately show ?thesis by auto qed -lemma%unimportant (in finite_measure) integral_less_AE_space: +lemma (in finite_measure) integral_less_AE_space: fixes X Y :: "'a \ real" assumes int: "integrable M X" "integrable M Y" assumes gt: "AE x in M. X x < Y x" "emeasure M (space M) \ 0" shows "integral\<^sup>L M X < integral\<^sup>L M Y" using gt by (intro integral_less_AE[OF int, where A="space M"]) auto -lemma%unimportant tendsto_integral_at_top: +lemma tendsto_integral_at_top: fixes f :: "real \ 'a::{banach, second_countable_topology}" assumes [measurable_cong]: "sets M = sets borel" and f[measurable]: "integrable M f" shows "((\y. \ x. indicator {.. y} x *\<^sub>R f x \M) \ \ x. f x \M) at_top" @@ -2809,7 +2808,7 @@ qed auto qed -lemma%unimportant (*FIX ME needs name *) +lemma (*FIX ME needs name *) fixes f :: "real \ real" assumes M: "sets M = sets borel" assumes nonneg: "AE x in M. 0 \ f x" @@ -2842,28 +2841,28 @@ subsection%important \Product measure\ -lemma%important (in sigma_finite_measure) borel_measurable_lebesgue_integrable[measurable (raw)]: +lemma (in sigma_finite_measure) borel_measurable_lebesgue_integrable[measurable (raw)]: fixes f :: "_ \ _ \ _::{banach, second_countable_topology}" assumes [measurable]: "case_prod f \ borel_measurable (N \\<^sub>M M)" shows "Measurable.pred N (\x. integrable M (f x))" -proof%unimportant - +proof - have [simp]: "\x. x \ space N \ integrable M (f x) \ (\\<^sup>+y. norm (f x y) \M) < \" unfolding integrable_iff_bounded by simp show ?thesis by (simp cong: measurable_cong) qed -lemma%unimportant (in sigma_finite_measure) measurable_measure[measurable (raw)]: +lemma (in sigma_finite_measure) measurable_measure[measurable (raw)]: "(\x. x \ space N \ A x \ space M) \ {x \ space (N \\<^sub>M M). snd x \ A (fst x)} \ sets (N \\<^sub>M M) \ (\x. measure M (A x)) \ borel_measurable N" unfolding measure_def by (intro measurable_emeasure borel_measurable_enn2real) auto -lemma%important (in sigma_finite_measure) borel_measurable_lebesgue_integral[measurable (raw)]: +proposition (in sigma_finite_measure) borel_measurable_lebesgue_integral[measurable (raw)]: fixes f :: "_ \ _ \ _::{banach, second_countable_topology}" assumes f[measurable]: "case_prod f \ borel_measurable (N \\<^sub>M M)" shows "(\x. \y. f x y \M) \ borel_measurable N" -proof%unimportant - +proof - from borel_measurable_implies_sequence_metric[OF f, of 0] guess s .. then have s: "\i. simple_function (N \\<^sub>M M) (s i)" "\x y. x \ space N \ y \ space M \ (\i. s i (x, y)) \ f x y" @@ -2934,7 +2933,7 @@ qed qed -lemma%unimportant (in pair_sigma_finite) integrable_product_swap: +lemma (in pair_sigma_finite) integrable_product_swap: fixes f :: "_ \ _::{banach, second_countable_topology}" assumes "integrable (M1 \\<^sub>M M2) f" shows "integrable (M2 \\<^sub>M M1) (\(x,y). f (y,x))" @@ -2946,7 +2945,7 @@ (simp add: distr_pair_swap[symmetric] assms) qed -lemma%unimportant (in pair_sigma_finite) integrable_product_swap_iff: +lemma (in pair_sigma_finite) integrable_product_swap_iff: fixes f :: "_ \ _::{banach, second_countable_topology}" shows "integrable (M2 \\<^sub>M M1) (\(x,y). f (y,x)) \ integrable (M1 \\<^sub>M M2) f" proof - @@ -2955,7 +2954,7 @@ show ?thesis by auto qed -lemma%unimportant (in pair_sigma_finite) integral_product_swap: +lemma (in pair_sigma_finite) integral_product_swap: fixes f :: "_ \ _::{banach, second_countable_topology}" assumes f: "f \ borel_measurable (M1 \\<^sub>M M2)" shows "(\(x,y). f (y,x) \(M2 \\<^sub>M M1)) = integral\<^sup>L (M1 \\<^sub>M M2) f" @@ -2965,13 +2964,13 @@ by (simp add: integral_distr[symmetric, OF measurable_pair_swap' f] distr_pair_swap[symmetric]) qed -lemma%important (in pair_sigma_finite) Fubini_integrable: +theorem (in pair_sigma_finite) Fubini_integrable: fixes f :: "_ \ _::{banach, second_countable_topology}" assumes f[measurable]: "f \ borel_measurable (M1 \\<^sub>M M2)" and integ1: "integrable M1 (\x. \ y. norm (f (x, y)) \M2)" and integ2: "AE x in M1. integrable M2 (\y. f (x, y))" shows "integrable (M1 \\<^sub>M M2) f" -proof%unimportant (rule integrableI_bounded) +proof (rule integrableI_bounded) have "(\\<^sup>+ p. norm (f p) \(M1 \\<^sub>M M2)) = (\\<^sup>+ x. (\\<^sup>+ y. norm (f (x, y)) \M2) \M1)" by (simp add: M2.nn_integral_fst [symmetric]) also have "\ = (\\<^sup>+ x. \\y. norm (f (x, y)) \M2\ \M1)" @@ -2992,7 +2991,7 @@ finally show "(\\<^sup>+ p. norm (f p) \(M1 \\<^sub>M M2)) < \" . qed fact -lemma%unimportant (in pair_sigma_finite) emeasure_pair_measure_finite: +lemma (in pair_sigma_finite) emeasure_pair_measure_finite: assumes A: "A \ sets (M1 \\<^sub>M M2)" and finite: "emeasure (M1 \\<^sub>M M2) A < \" shows "AE x in M1. emeasure M2 {y\space M2. (x, y) \ A} < \" proof - @@ -3006,7 +3005,7 @@ ultimately show ?thesis by (auto simp: less_top) qed -lemma%unimportant (in pair_sigma_finite) AE_integrable_fst': +lemma (in pair_sigma_finite) AE_integrable_fst': fixes f :: "_ \ _::{banach, second_countable_topology}" assumes f[measurable]: "integrable (M1 \\<^sub>M M2) f" shows "AE x in M1. integrable M2 (\y. f (x, y))" @@ -3023,7 +3022,7 @@ (auto simp: integrable_iff_bounded measurable_compose[OF _ borel_measurable_integrable[OF f]] less_top) qed -lemma%unimportant (in pair_sigma_finite) integrable_fst': +lemma (in pair_sigma_finite) integrable_fst': fixes f :: "_ \ _::{banach, second_countable_topology}" assumes f[measurable]: "integrable (M1 \\<^sub>M M2) f" shows "integrable M1 (\x. \y. f (x, y) \M2)" @@ -3040,11 +3039,11 @@ finally show "(\\<^sup>+ x. ennreal (norm (\ y. f (x, y) \M2)) \M1) < \" . qed -lemma%important (in pair_sigma_finite) integral_fst': +proposition (in pair_sigma_finite) integral_fst': fixes f :: "_ \ _::{banach, second_countable_topology}" assumes f: "integrable (M1 \\<^sub>M M2) f" shows "(\x. (\y. f (x, y) \M2) \M1) = integral\<^sup>L (M1 \\<^sub>M M2) f" -using f proof%unimportant induct +using f proof induct case (base A c) have A[measurable]: "A \ sets (M1 \\<^sub>M M2)" by fact @@ -3153,7 +3152,7 @@ qed qed -lemma%unimportant (in pair_sigma_finite) (* FIX ME needs name *) +lemma (in pair_sigma_finite) (* FIX ME needs name *) fixes f :: "_ \ _ \ _::{banach, second_countable_topology}" assumes f: "integrable (M1 \\<^sub>M M2) (case_prod f)" shows AE_integrable_fst: "AE x in M1. integrable M2 (\y. f x y)" (is "?AE") @@ -3161,7 +3160,7 @@ and integral_fst: "(\x. (\y. f x y \M2) \M1) = integral\<^sup>L (M1 \\<^sub>M M2) (\(x, y). f x y)" (is "?EQ") using AE_integrable_fst'[OF f] integrable_fst'[OF f] integral_fst'[OF f] by auto -lemma%unimportant (in pair_sigma_finite) (* FIX ME needs name *) +lemma (in pair_sigma_finite) (* FIX ME needs name *) fixes f :: "_ \ _ \ _::{banach, second_countable_topology}" assumes f[measurable]: "integrable (M1 \\<^sub>M M2) (case_prod f)" shows AE_integrable_snd: "AE y in M2. integrable M1 (\x. f x y)" (is "?AE") @@ -3177,13 +3176,13 @@ using integral_product_swap[of "case_prod f"] by simp qed -lemma%unimportant (in pair_sigma_finite) Fubini_integral: +proposition (in pair_sigma_finite) Fubini_integral: fixes f :: "_ \ _ \ _ :: {banach, second_countable_topology}" assumes f: "integrable (M1 \\<^sub>M M2) (case_prod f)" shows "(\y. (\x. f x y \M1) \M2) = (\x. (\y. f x y \M2) \M1)" unfolding integral_snd[OF assms] integral_fst[OF assms] .. -lemma%unimportant (in product_sigma_finite) product_integral_singleton: +lemma (in product_sigma_finite) product_integral_singleton: fixes f :: "_ \ _::{banach, second_countable_topology}" shows "f \ borel_measurable (M i) \ (\x. f (x i) \Pi\<^sub>M {i} M) = integral\<^sup>L (M i) f" apply (subst distr_singleton[symmetric]) @@ -3191,7 +3190,7 @@ apply simp_all done -lemma%unimportant (in product_sigma_finite) product_integral_fold: +lemma (in product_sigma_finite) product_integral_fold: fixes f :: "_ \ _::{banach, second_countable_topology}" assumes IJ[simp]: "I \ J = {}" and fin: "finite I" "finite J" and f: "integrable (Pi\<^sub>M (I \ J) M) f" @@ -3218,12 +3217,12 @@ done qed -lemma%important (in product_sigma_finite) product_integral_insert: +lemma (in product_sigma_finite) product_integral_insert: fixes f :: "_ \ _::{banach, second_countable_topology}" assumes I: "finite I" "i \ I" and f: "integrable (Pi\<^sub>M (insert i I) M) f" shows "integral\<^sup>L (Pi\<^sub>M (insert i I) M) f = (\x. (\y. f (x(i:=y)) \M i) \Pi\<^sub>M I M)" -proof%unimportant - +proof - have "integral\<^sup>L (Pi\<^sub>M (insert i I) M) f = integral\<^sup>L (Pi\<^sub>M (I \ {i}) M) f" by simp also have "\ = (\x. (\y. f (merge I {i} (x,y)) \Pi\<^sub>M {i} M) \Pi\<^sub>M I M)" @@ -3242,11 +3241,11 @@ finally show ?thesis . qed -lemma%important (in product_sigma_finite) product_integrable_prod: +lemma (in product_sigma_finite) product_integrable_prod: fixes f :: "'i \ 'a \ _::{real_normed_field,banach,second_countable_topology}" assumes [simp]: "finite I" and integrable: "\i. i \ I \ integrable (M i) (f i)" shows "integrable (Pi\<^sub>M I M) (\x. (\i\I. f i (x i)))" (is "integrable _ ?f") -proof%unimportant (unfold integrable_iff_bounded, intro conjI) +proof (unfold integrable_iff_bounded, intro conjI) interpret finite_product_sigma_finite M I by standard fact show "?f \ borel_measurable (Pi\<^sub>M I M)" @@ -3261,11 +3260,11 @@ finally show "(\\<^sup>+ x. ennreal (norm (\i\I. f i (x i))) \Pi\<^sub>M I M) < \" . qed -lemma%important (in product_sigma_finite) product_integral_prod: +lemma (in product_sigma_finite) product_integral_prod: fixes f :: "'i \ 'a \ _::{real_normed_field,banach,second_countable_topology}" assumes "finite I" and integrable: "\i. i \ I \ integrable (M i) (f i)" shows "(\x. (\i\I. f i (x i)) \Pi\<^sub>M I M) = (\i\I. integral\<^sup>L (M i) (f i))" -using assms proof%unimportant induct +using assms proof induct case empty interpret finite_measure "Pi\<^sub>M {} M" by rule (simp add: space_PiM) @@ -3284,7 +3283,7 @@ by (simp add: * insert prod subset_insertI) qed -lemma%unimportant integrable_subalgebra: +lemma integrable_subalgebra: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes borel: "f \ borel_measurable N" and N: "sets N \ sets M" "space N = space M" "\A. A \ sets N \ emeasure N A = emeasure M A" @@ -3296,12 +3295,12 @@ using assms by (auto simp: integrable_iff_bounded nn_integral_subalgebra) qed -lemma%important integral_subalgebra: +lemma integral_subalgebra: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes borel: "f \ borel_measurable N" and N: "sets N \ sets M" "space N = space M" "\A. A \ sets N \ emeasure N A = emeasure M A" shows "integral\<^sup>L N f = integral\<^sup>L M f" -proof%unimportant cases +proof cases assume "integrable N f" then show ?thesis proof induct diff -r e61b0b819d28 -r 3417a8f154eb src/HOL/Analysis/Borel_Space.thy --- a/src/HOL/Analysis/Borel_Space.thy Sun Jan 13 20:25:41 2019 +0100 +++ b/src/HOL/Analysis/Borel_Space.thy Mon Jan 14 11:59:19 2019 +0000 @@ -10,15 +10,15 @@ Measurable Derivative Ordered_Euclidean_Space Extended_Real_Limits begin -lemma%unimportant sets_Collect_eventually_sequentially[measurable]: +lemma sets_Collect_eventually_sequentially[measurable]: "(\i. {x\space M. P x i} \ sets M) \ {x\space M. eventually (P x) sequentially} \ sets M" unfolding eventually_sequentially by simp -lemma%unimportant topological_basis_trivial: "topological_basis {A. open A}" +lemma topological_basis_trivial: "topological_basis {A. open A}" by (auto simp: topological_basis_def) lemma%important open_prod_generated: "open = generate_topology {A \ B | A B. open A \ open B}" -proof%unimportant - +proof - have "{A \ B :: ('a \ 'b) set | A B. open A \ open B} = ((\(a, b). a \ b) ` ({A. open A} \ {A. open A}))" by auto then show ?thesis @@ -27,31 +27,31 @@ definition%important "mono_on f A \ \r s. r \ A \ s \ A \ r \ s \ f r \ f s" -lemma%unimportant mono_onI: +lemma mono_onI: "(\r s. r \ A \ s \ A \ r \ s \ f r \ f s) \ mono_on f A" unfolding mono_on_def by simp -lemma%unimportant mono_onD: +lemma mono_onD: "\mono_on f A; r \ A; s \ A; r \ s\ \ f r \ f s" unfolding mono_on_def by simp -lemma%unimportant mono_imp_mono_on: "mono f \ mono_on f A" +lemma mono_imp_mono_on: "mono f \ mono_on f A" unfolding mono_def mono_on_def by auto -lemma%unimportant mono_on_subset: "mono_on f A \ B \ A \ mono_on f B" +lemma mono_on_subset: "mono_on f A \ B \ A \ mono_on f B" unfolding mono_on_def by auto definition%important "strict_mono_on f A \ \r s. r \ A \ s \ A \ r < s \ f r < f s" -lemma%unimportant strict_mono_onI: +lemma strict_mono_onI: "(\r s. r \ A \ s \ A \ r < s \ f r < f s) \ strict_mono_on f A" unfolding strict_mono_on_def by simp -lemma%unimportant strict_mono_onD: +lemma strict_mono_onD: "\strict_mono_on f A; r \ A; s \ A; r < s\ \ f r < f s" unfolding strict_mono_on_def by simp -lemma%unimportant mono_on_greaterD: +lemma mono_on_greaterD: assumes "mono_on g A" "x \ A" "y \ A" "g x > (g (y::_::linorder) :: _ :: linorder)" shows "x > y" proof (rule ccontr) @@ -61,7 +61,7 @@ with assms(4) show False by simp qed -lemma%unimportant strict_mono_inv: +lemma strict_mono_inv: fixes f :: "('a::linorder) \ ('b::linorder)" assumes "strict_mono f" and "surj f" and inv: "\x. g (f x) = x" shows "strict_mono g" @@ -72,7 +72,7 @@ with inv show "g x < g y" by simp qed -lemma%unimportant strict_mono_on_imp_inj_on: +lemma strict_mono_on_imp_inj_on: assumes "strict_mono_on (f :: (_ :: linorder) \ (_ :: preorder)) A" shows "inj_on f A" proof (rule inj_onI) @@ -82,7 +82,7 @@ (auto dest: strict_mono_onD[OF assms, of x y] strict_mono_onD[OF assms, of y x]) qed -lemma%unimportant strict_mono_on_leD: +lemma strict_mono_on_leD: assumes "strict_mono_on (f :: (_ :: linorder) \ _ :: preorder) A" "x \ A" "y \ A" "x \ y" shows "f x \ f y" proof (insert le_less_linear[of y x], elim disjE) @@ -91,17 +91,17 @@ thus ?thesis by (rule less_imp_le) qed (insert assms, simp) -lemma%unimportant strict_mono_on_eqD: +lemma strict_mono_on_eqD: fixes f :: "(_ :: linorder) \ (_ :: preorder)" assumes "strict_mono_on f A" "f x = f y" "x \ A" "y \ A" shows "y = x" using assms by (rule_tac linorder_cases[of x y]) (auto dest: strict_mono_onD) -lemma%important mono_on_imp_deriv_nonneg: +proposition mono_on_imp_deriv_nonneg: assumes mono: "mono_on f A" and deriv: "(f has_real_derivative D) (at x)" assumes "x \ interior A" shows "D \ 0" -proof%unimportant (rule tendsto_lowerbound) +proof (rule tendsto_lowerbound) let ?A' = "(\y. y - x) ` interior A" from deriv show "((\h. (f (x + h) - f x) / h) \ D) (at 0)" by (simp add: field_has_derivative_at has_field_derivative_def) @@ -124,16 +124,16 @@ qed qed simp -lemma%unimportant strict_mono_on_imp_mono_on: +lemma strict_mono_on_imp_mono_on: "strict_mono_on (f :: (_ :: linorder) \ _ :: preorder) A \ mono_on f A" by (rule mono_onI, rule strict_mono_on_leD) -lemma%important mono_on_ctble_discont: +proposition mono_on_ctble_discont: fixes f :: "real \ real" fixes A :: "real set" assumes "mono_on f A" shows "countable {a\A. \ continuous (at a within A) f}" -proof%unimportant - +proof - have mono: "\x y. x \ A \ y \ A \ x \ y \ f x \ f y" using \mono_on f A\ by (simp add: mono_on_def) have "\a \ {a\A. \ continuous (at a within A) f}. \q :: nat \ rat. @@ -196,12 +196,12 @@ by (rule countableI') qed -lemma%important mono_on_ctble_discont_open: +lemma mono_on_ctble_discont_open: fixes f :: "real \ real" fixes A :: "real set" assumes "open A" "mono_on f A" shows "countable {a\A. \isCont f a}" -proof%unimportant - +proof - have "{a\A. \isCont f a} = {a\A. \(continuous (at a within A) f)}" by (auto simp add: continuous_within_open [OF _ \open A\]) thus ?thesis @@ -209,23 +209,23 @@ by (rule mono_on_ctble_discont, rule assms) qed -lemma%important mono_ctble_discont: +lemma mono_ctble_discont: fixes f :: "real \ real" assumes "mono f" shows "countable {a. \ isCont f a}" -using%unimportant assms mono_on_ctble_discont [of f UNIV] unfolding mono_on_def mono_def by auto + using assms mono_on_ctble_discont [of f UNIV] unfolding mono_on_def mono_def by auto -lemma%important has_real_derivative_imp_continuous_on: +lemma has_real_derivative_imp_continuous_on: assumes "\x. x \ A \ (f has_real_derivative f' x) (at x)" shows "continuous_on A f" apply (intro differentiable_imp_continuous_on, unfold differentiable_on_def) using assms differentiable_at_withinI real_differentiable_def by blast -lemma%important closure_contains_Sup: +lemma closure_contains_Sup: fixes S :: "real set" assumes "S \ {}" "bdd_above S" shows "Sup S \ closure S" -proof%unimportant - +proof - have "Inf (uminus ` S) \ closure (uminus ` S)" using assms by (intro closure_contains_Inf) auto also have "Inf (uminus ` S) = -Sup S" by (simp add: Inf_real_def) @@ -234,22 +234,22 @@ finally show ?thesis by auto qed -lemma%unimportant closed_contains_Sup: +lemma closed_contains_Sup: fixes S :: "real set" shows "S \ {} \ bdd_above S \ closed S \ Sup S \ S" by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup) -lemma%unimportant closed_subset_contains_Sup: +lemma closed_subset_contains_Sup: fixes A C :: "real set" shows "closed C \ A \ C \ A \ {} \ bdd_above A \ Sup A \ C" by (metis closure_contains_Sup closure_minimal subset_eq) -lemma%important deriv_nonneg_imp_mono: +proposition deriv_nonneg_imp_mono: assumes deriv: "\x. x \ {a..b} \ (g has_real_derivative g' x) (at x)" assumes nonneg: "\x. x \ {a..b} \ g' x \ 0" assumes ab: "a \ b" shows "g a \ g b" -proof%unimportant (cases "a < b") +proof (cases "a < b") assume "a < b" from deriv have "\x. \x \ a; x \ b\ \ (g has_real_derivative g' x) (at x)" by simp with MVT2[OF \a < b\] and deriv @@ -258,11 +258,11 @@ with g_ab show ?thesis by simp qed (insert ab, simp) -lemma%important continuous_interval_vimage_Int: +lemma continuous_interval_vimage_Int: assumes "continuous_on {a::real..b} g" and mono: "\x y. a \ x \ x \ y \ y \ b \ g x \ g y" assumes "a \ b" "(c::real) \ d" "{c..d} \ {g a..g b}" obtains c' d' where "{a..b} \ g -` {c..d} = {c'..d'}" "c' \ d'" "g c' = c" "g d' = d" -proof%unimportant- +proof- let ?A = "{a..b} \ g -` {c..d}" from IVT'[of g a c b, OF _ _ \a \ b\ assms(1)] assms(4,5) obtain c'' where c'': "c'' \ ?A" "g c'' = c" by auto @@ -301,41 +301,41 @@ abbreviation "borel_measurable M \ measurable M borel" -lemma%important in_borel_measurable: +lemma in_borel_measurable: "f \ borel_measurable M \ (\S \ sigma_sets UNIV {S. open S}. f -` S \ space M \ sets M)" - by%unimportant (auto simp add: measurable_def borel_def) + by (auto simp add: measurable_def borel_def) -lemma%important in_borel_measurable_borel: +lemma in_borel_measurable_borel: "f \ borel_measurable M \ (\S \ sets borel. f -` S \ space M \ sets M)" - by%unimportant (auto simp add: measurable_def borel_def) + by (auto simp add: measurable_def borel_def) -lemma%unimportant space_borel[simp]: "space borel = UNIV" +lemma space_borel[simp]: "space borel = UNIV" unfolding borel_def by auto -lemma%unimportant space_in_borel[measurable]: "UNIV \ sets borel" +lemma space_in_borel[measurable]: "UNIV \ sets borel" unfolding borel_def by auto -lemma%unimportant sets_borel: "sets borel = sigma_sets UNIV {S. open S}" +lemma sets_borel: "sets borel = sigma_sets UNIV {S. open S}" unfolding borel_def by (rule sets_measure_of) simp -lemma%unimportant measurable_sets_borel: +lemma measurable_sets_borel: "\f \ measurable borel M; A \ sets M\ \ f -` A \ sets borel" by (drule (1) measurable_sets) simp -lemma%unimportant pred_Collect_borel[measurable (raw)]: "Measurable.pred borel P \ {x. P x} \ sets borel" +lemma pred_Collect_borel[measurable (raw)]: "Measurable.pred borel P \ {x. P x} \ sets borel" unfolding borel_def pred_def by auto -lemma%unimportant borel_open[measurable (raw generic)]: +lemma borel_open[measurable (raw generic)]: assumes "open A" shows "A \ sets borel" proof - have "A \ {S. open S}" unfolding mem_Collect_eq using assms . thus ?thesis unfolding borel_def by auto qed -lemma%unimportant borel_closed[measurable (raw generic)]: +lemma borel_closed[measurable (raw generic)]: assumes "closed A" shows "A \ sets borel" proof - have "space borel - (- A) \ sets borel" @@ -343,11 +343,11 @@ thus ?thesis by simp qed -lemma%unimportant borel_singleton[measurable]: +lemma borel_singleton[measurable]: "A \ sets borel \ insert x A \ sets (borel :: 'a::t1_space measure)" unfolding insert_def by (rule sets.Un) auto -lemma%unimportant sets_borel_eq_count_space: "sets (borel :: 'a::{countable, t2_space} measure) = count_space UNIV" +lemma sets_borel_eq_count_space: "sets (borel :: 'a::{countable, t2_space} measure) = count_space UNIV" proof - have "(\a\A. {a}) \ sets borel" for A :: "'a set" by (intro sets.countable_UN') auto @@ -355,16 +355,16 @@ by auto qed -lemma%unimportant borel_comp[measurable]: "A \ sets borel \ - A \ sets borel" +lemma borel_comp[measurable]: "A \ sets borel \ - A \ sets borel" unfolding Compl_eq_Diff_UNIV by simp -lemma%unimportant borel_measurable_vimage: +lemma borel_measurable_vimage: fixes f :: "'a \ 'x::t2_space" assumes borel[measurable]: "f \ borel_measurable M" shows "f -` {x} \ space M \ sets M" by simp -lemma%unimportant borel_measurableI: +lemma borel_measurableI: fixes f :: "'a \ 'x::topological_space" assumes "\S. open S \ f -` S \ space M \ sets M" shows "f \ borel_measurable M" @@ -374,30 +374,30 @@ using assms[of S] by simp qed -lemma%unimportant borel_measurable_const: +lemma borel_measurable_const: "(\x. c) \ borel_measurable M" by auto -lemma%unimportant borel_measurable_indicator: +lemma borel_measurable_indicator: assumes A: "A \ sets M" shows "indicator A \ borel_measurable M" unfolding indicator_def [abs_def] using A by (auto intro!: measurable_If_set) -lemma%unimportant borel_measurable_count_space[measurable (raw)]: +lemma borel_measurable_count_space[measurable (raw)]: "f \ borel_measurable (count_space S)" unfolding measurable_def by auto -lemma%unimportant borel_measurable_indicator'[measurable (raw)]: +lemma borel_measurable_indicator'[measurable (raw)]: assumes [measurable]: "{x\space M. f x \ A x} \ sets M" shows "(\x. indicator (A x) (f x)) \ borel_measurable M" unfolding indicator_def[abs_def] by (auto intro!: measurable_If) -lemma%important borel_measurable_indicator_iff: +lemma borel_measurable_indicator_iff: "(indicator A :: 'a \ 'x::{t1_space, zero_neq_one}) \ borel_measurable M \ A \ space M \ sets M" (is "?I \ borel_measurable M \ _") -proof%unimportant +proof assume "?I \ borel_measurable M" then have "?I -` {1} \ space M \ sets M" unfolding measurable_def by auto @@ -412,12 +412,12 @@ ultimately show "?I \ borel_measurable M" by auto qed -lemma%unimportant borel_measurable_subalgebra: +lemma borel_measurable_subalgebra: assumes "sets N \ sets M" "space N = space M" "f \ borel_measurable N" shows "f \ borel_measurable M" using assms unfolding measurable_def by auto -lemma%unimportant borel_measurable_restrict_space_iff_ereal: +lemma borel_measurable_restrict_space_iff_ereal: fixes f :: "'a \ ereal" assumes \[measurable, simp]: "\ \ space M \ sets M" shows "f \ borel_measurable (restrict_space M \) \ @@ -425,7 +425,7 @@ by (subst measurable_restrict_space_iff) (auto simp: indicator_def if_distrib[where f="\x. a * x" for a] cong del: if_weak_cong) -lemma%unimportant borel_measurable_restrict_space_iff_ennreal: +lemma borel_measurable_restrict_space_iff_ennreal: fixes f :: "'a \ ennreal" assumes \[measurable, simp]: "\ \ space M \ sets M" shows "f \ borel_measurable (restrict_space M \) \ @@ -433,7 +433,7 @@ by (subst measurable_restrict_space_iff) (auto simp: indicator_def if_distrib[where f="\x. a * x" for a] cong del: if_weak_cong) -lemma%unimportant borel_measurable_restrict_space_iff: +lemma borel_measurable_restrict_space_iff: fixes f :: "'a \ 'b::real_normed_vector" assumes \[measurable, simp]: "\ \ space M \ sets M" shows "f \ borel_measurable (restrict_space M \) \ @@ -442,27 +442,27 @@ (auto simp: indicator_def if_distrib[where f="\x. x *\<^sub>R a" for a] ac_simps cong del: if_weak_cong) -lemma%unimportant cbox_borel[measurable]: "cbox a b \ sets borel" +lemma cbox_borel[measurable]: "cbox a b \ sets borel" by (auto intro: borel_closed) -lemma%unimportant box_borel[measurable]: "box a b \ sets borel" +lemma box_borel[measurable]: "box a b \ sets borel" by (auto intro: borel_open) -lemma%unimportant borel_compact: "compact (A::'a::t2_space set) \ A \ sets borel" +lemma borel_compact: "compact (A::'a::t2_space set) \ A \ sets borel" by (auto intro: borel_closed dest!: compact_imp_closed) -lemma%unimportant borel_sigma_sets_subset: +lemma borel_sigma_sets_subset: "A \ sets borel \ sigma_sets UNIV A \ sets borel" using sets.sigma_sets_subset[of A borel] by simp -lemma%important borel_eq_sigmaI1: +lemma borel_eq_sigmaI1: fixes F :: "'i \ 'a::topological_space set" and X :: "'a::topological_space set set" assumes borel_eq: "borel = sigma UNIV X" assumes X: "\x. x \ X \ x \ sets (sigma UNIV (F ` A))" assumes F: "\i. i \ A \ F i \ sets borel" shows "borel = sigma UNIV (F ` A)" unfolding borel_def -proof%unimportant (intro sigma_eqI antisym) +proof (intro sigma_eqI antisym) have borel_rev_eq: "sigma_sets UNIV {S::'a set. open S} = sets borel" unfolding borel_def by simp also have "\ = sigma_sets UNIV X" @@ -474,7 +474,7 @@ unfolding borel_rev_eq using F by (intro borel_sigma_sets_subset) auto qed auto -lemma%unimportant borel_eq_sigmaI2: +lemma borel_eq_sigmaI2: fixes F :: "'i \ 'j \ 'a::topological_space set" and G :: "'l \ 'k \ 'a::topological_space set" assumes borel_eq: "borel = sigma UNIV ((\(i, j). G i j)`B)" @@ -484,7 +484,7 @@ using assms by (intro borel_eq_sigmaI1[where X="(\(i, j). G i j) ` B" and F="(\(i, j). F i j)"]) auto -lemma%unimportant borel_eq_sigmaI3: +lemma borel_eq_sigmaI3: fixes F :: "'i \ 'j \ 'a::topological_space set" and X :: "'a::topological_space set set" assumes borel_eq: "borel = sigma UNIV X" assumes X: "\x. x \ X \ x \ sets (sigma UNIV ((\(i, j). F i j) ` A))" @@ -492,7 +492,7 @@ shows "borel = sigma UNIV ((\(i, j). F i j) ` A)" using assms by (intro borel_eq_sigmaI1[where X=X and F="(\(i, j). F i j)"]) auto -lemma%unimportant borel_eq_sigmaI4: +lemma borel_eq_sigmaI4: fixes F :: "'i \ 'a::topological_space set" and G :: "'l \ 'k \ 'a::topological_space set" assumes borel_eq: "borel = sigma UNIV ((\(i, j). G i j)`A)" @@ -501,7 +501,7 @@ shows "borel = sigma UNIV (range F)" using assms by (intro borel_eq_sigmaI1[where X="(\(i, j). G i j) ` A" and F=F]) auto -lemma%unimportant borel_eq_sigmaI5: +lemma borel_eq_sigmaI5: fixes F :: "'i \ 'j \ 'a::topological_space set" and G :: "'l \ 'a::topological_space set" assumes borel_eq: "borel = sigma UNIV (range G)" assumes X: "\i. G i \ sets (sigma UNIV (range (\(i, j). F i j)))" @@ -509,12 +509,12 @@ shows "borel = sigma UNIV (range (\(i, j). F i j))" using assms by (intro borel_eq_sigmaI1[where X="range G" and F="(\(i, j). F i j)"]) auto -lemma%important second_countable_borel_measurable: +lemma second_countable_borel_measurable: fixes X :: "'a::second_countable_topology set set" assumes eq: "open = generate_topology X" shows "borel = sigma UNIV X" unfolding borel_def -proof%unimportant (intro sigma_eqI sigma_sets_eqI) +proof (intro sigma_eqI sigma_sets_eqI) interpret X: sigma_algebra UNIV "sigma_sets UNIV X" by (rule sigma_algebra_sigma_sets) simp @@ -553,7 +553,7 @@ qed auto qed (auto simp: eq intro: generate_topology.Basis) -lemma%unimportant borel_eq_closed: "borel = sigma UNIV (Collect closed)" +lemma borel_eq_closed: "borel = sigma UNIV (Collect closed)" unfolding borel_def proof (intro sigma_eqI sigma_sets_eqI, safe) fix x :: "'a set" assume "open x" @@ -569,13 +569,13 @@ finally show "x \ sigma_sets UNIV (Collect open)" by simp qed simp_all -lemma%important borel_eq_countable_basis: +lemma borel_eq_countable_basis: fixes B::"'a::topological_space set set" assumes "countable B" assumes "topological_basis B" shows "borel = sigma UNIV B" unfolding borel_def -proof%unimportant (intro sigma_eqI sigma_sets_eqI, safe) +proof (intro sigma_eqI sigma_sets_eqI, safe) interpret countable_basis using assms by unfold_locales fix X::"'a set" assume "open X" from open_countable_basisE[OF this] guess B' . note B' = this @@ -587,7 +587,7 @@ thus "b \ sigma_sets UNIV (Collect open)" by auto qed simp_all -lemma%unimportant borel_measurable_continuous_on_restrict: +lemma borel_measurable_continuous_on_restrict: fixes f :: "'a::topological_space \ 'b::topological_space" assumes f: "continuous_on A f" shows "f \ borel_measurable (restrict_space borel A)" @@ -599,16 +599,16 @@ by (force simp add: sets_restrict_space space_restrict_space) qed -lemma%unimportant borel_measurable_continuous_on1: "continuous_on UNIV f \ f \ borel_measurable borel" +lemma borel_measurable_continuous_on1: "continuous_on UNIV f \ f \ borel_measurable borel" by (drule borel_measurable_continuous_on_restrict) simp -lemma%unimportant borel_measurable_continuous_on_if: +lemma borel_measurable_continuous_on_if: "A \ sets borel \ continuous_on A f \ continuous_on (- A) g \ (\x. if x \ A then f x else g x) \ borel_measurable borel" by (auto simp add: measurable_If_restrict_space_iff Collect_neg_eq intro!: borel_measurable_continuous_on_restrict) -lemma%unimportant borel_measurable_continuous_countable_exceptions: +lemma borel_measurable_continuous_countable_exceptions: fixes f :: "'a::t1_space \ 'b::topological_space" assumes X: "countable X" assumes "continuous_on (- X) f" @@ -620,23 +620,23 @@ by (intro borel_measurable_continuous_on_if assms continuous_intros) qed auto -lemma%unimportant borel_measurable_continuous_on: +lemma borel_measurable_continuous_on: assumes f: "continuous_on UNIV f" and g: "g \ borel_measurable M" shows "(\x. f (g x)) \ borel_measurable M" using measurable_comp[OF g borel_measurable_continuous_on1[OF f]] by (simp add: comp_def) -lemma%unimportant borel_measurable_continuous_on_indicator: +lemma borel_measurable_continuous_on_indicator: fixes f g :: "'a::topological_space \ 'b::real_normed_vector" shows "A \ sets borel \ continuous_on A f \ (\x. indicator A x *\<^sub>R f x) \ borel_measurable borel" by (subst borel_measurable_restrict_space_iff[symmetric]) (auto intro: borel_measurable_continuous_on_restrict) -lemma%important borel_measurable_Pair[measurable (raw)]: +lemma borel_measurable_Pair[measurable (raw)]: fixes f :: "'a \ 'b::second_countable_topology" and g :: "'a \ 'c::second_countable_topology" assumes f[measurable]: "f \ borel_measurable M" assumes g[measurable]: "g \ borel_measurable M" shows "(\x. (f x, g x)) \ borel_measurable M" -proof%unimportant (subst borel_eq_countable_basis) +proof (subst borel_eq_countable_basis) let ?B = "SOME B::'b set set. countable B \ topological_basis B" let ?C = "SOME B::'c set set. countable B \ topological_basis B" let ?P = "(\(b, c). b \ c) ` (?B \ ?C)" @@ -657,13 +657,13 @@ qed auto qed -lemma%important borel_measurable_continuous_Pair: +lemma borel_measurable_continuous_Pair: fixes f :: "'a \ 'b::second_countable_topology" and g :: "'a \ 'c::second_countable_topology" assumes [measurable]: "f \ borel_measurable M" assumes [measurable]: "g \ borel_measurable M" assumes H: "continuous_on UNIV (\x. H (fst x) (snd x))" shows "(\x. H (f x) (g x)) \ borel_measurable M" -proof%unimportant - +proof - have eq: "(\x. H (f x) (g x)) = (\x. (\x. H (fst x) (snd x)) (f x, g x))" by auto show ?thesis unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto @@ -671,7 +671,7 @@ subsection%important \Borel spaces on order topologies\ -lemma%unimportant [measurable]: +lemma [measurable]: fixes a b :: "'a::linorder_topology" shows lessThan_borel: "{..< a} \ sets borel" and greaterThan_borel: "{a <..} \ sets borel" @@ -685,7 +685,7 @@ by (blast intro: borel_open borel_closed open_lessThan open_greaterThan open_greaterThanLessThan closed_atMost closed_atLeast closed_atLeastAtMost)+ -lemma%unimportant borel_Iio: +lemma borel_Iio: "borel = sigma UNIV (range lessThan :: 'a::{linorder_topology, second_countable_topology} set set)" unfolding second_countable_borel_measurable[OF open_generated_order] proof (intro sigma_eqI sigma_sets_eqI) @@ -723,7 +723,7 @@ qed auto qed auto -lemma%unimportant borel_Ioi: +lemma borel_Ioi: "borel = sigma UNIV (range greaterThan :: 'a::{linorder_topology, second_countable_topology} set set)" unfolding second_countable_borel_measurable[OF open_generated_order] proof (intro sigma_eqI sigma_sets_eqI) @@ -761,29 +761,29 @@ qed auto qed auto -lemma%unimportant borel_measurableI_less: +lemma borel_measurableI_less: fixes f :: "'a \ 'b::{linorder_topology, second_countable_topology}" shows "(\y. {x\space M. f x < y} \ sets M) \ f \ borel_measurable M" unfolding borel_Iio by (rule measurable_measure_of) (auto simp: Int_def conj_commute) -lemma%important borel_measurableI_greater: +lemma borel_measurableI_greater: fixes f :: "'a \ 'b::{linorder_topology, second_countable_topology}" shows "(\y. {x\space M. y < f x} \ sets M) \ f \ borel_measurable M" unfolding borel_Ioi - by%unimportant (rule measurable_measure_of) (auto simp: Int_def conj_commute) + by (rule measurable_measure_of) (auto simp: Int_def conj_commute) -lemma%unimportant borel_measurableI_le: +lemma borel_measurableI_le: fixes f :: "'a \ 'b::{linorder_topology, second_countable_topology}" shows "(\y. {x\space M. f x \ y} \ sets M) \ f \ borel_measurable M" by (rule borel_measurableI_greater) (auto simp: not_le[symmetric]) -lemma%unimportant borel_measurableI_ge: +lemma borel_measurableI_ge: fixes f :: "'a \ 'b::{linorder_topology, second_countable_topology}" shows "(\y. {x\space M. y \ f x} \ sets M) \ f \ borel_measurable M" by (rule borel_measurableI_less) (auto simp: not_le[symmetric]) -lemma%unimportant borel_measurable_less[measurable]: +lemma borel_measurable_less[measurable]: fixes f :: "'a \ 'b::{second_countable_topology, linorder_topology}" assumes "f \ borel_measurable M" assumes "g \ borel_measurable M" @@ -797,7 +797,7 @@ finally show ?thesis . qed -lemma%important +lemma (* FIX ME needs name *) fixes f :: "'a \ 'b::{second_countable_topology, linorder_topology}" assumes f[measurable]: "f \ borel_measurable M" assumes g[measurable]: "g \ borel_measurable M" @@ -805,23 +805,23 @@ and borel_measurable_eq[measurable]: "{w \ space M. f w = g w} \ sets M" and borel_measurable_neq: "{w \ space M. f w \ g w} \ sets M" unfolding eq_iff not_less[symmetric] - by%unimportant measurable + by measurable -lemma%important borel_measurable_SUP[measurable (raw)]: +lemma borel_measurable_SUP[measurable (raw)]: fixes F :: "_ \ _ \ _::{complete_linorder, linorder_topology, second_countable_topology}" assumes [simp]: "countable I" assumes [measurable]: "\i. i \ I \ F i \ borel_measurable M" shows "(\x. SUP i\I. F i x) \ borel_measurable M" - by%unimportant (rule borel_measurableI_greater) (simp add: less_SUP_iff) + by (rule borel_measurableI_greater) (simp add: less_SUP_iff) -lemma%unimportant borel_measurable_INF[measurable (raw)]: +lemma borel_measurable_INF[measurable (raw)]: fixes F :: "_ \ _ \ _::{complete_linorder, linorder_topology, second_countable_topology}" assumes [simp]: "countable I" assumes [measurable]: "\i. i \ I \ F i \ borel_measurable M" shows "(\x. INF i\I. F i x) \ borel_measurable M" by (rule borel_measurableI_less) (simp add: INF_less_iff) -lemma%unimportant borel_measurable_cSUP[measurable (raw)]: +lemma borel_measurable_cSUP[measurable (raw)]: fixes F :: "_ \ _ \ 'a::{conditionally_complete_linorder, linorder_topology, second_countable_topology}" assumes [simp]: "countable I" assumes [measurable]: "\i. i \ I \ F i \ borel_measurable M" @@ -843,13 +843,13 @@ qed qed -lemma%important borel_measurable_cINF[measurable (raw)]: +lemma borel_measurable_cINF[measurable (raw)]: fixes F :: "_ \ _ \ 'a::{conditionally_complete_linorder, linorder_topology, second_countable_topology}" assumes [simp]: "countable I" assumes [measurable]: "\i. i \ I \ F i \ borel_measurable M" assumes bdd: "\x. x \ space M \ bdd_below ((\i. F i x) ` I)" shows "(\x. INF i\I. F i x) \ borel_measurable M" -proof%unimportant cases +proof cases assume "I = {}" then show ?thesis unfolding \I = {}\ image_empty by simp next @@ -865,7 +865,7 @@ qed qed -lemma%unimportant borel_measurable_lfp[consumes 1, case_names continuity step]: +lemma borel_measurable_lfp[consumes 1, case_names continuity step]: fixes F :: "('a \ 'b) \ ('a \ 'b::{complete_linorder, linorder_topology, second_countable_topology})" assumes "sup_continuous F" assumes *: "\f. f \ borel_measurable M \ F f \ borel_measurable M" @@ -882,7 +882,7 @@ finally show ?thesis . qed -lemma%unimportant borel_measurable_gfp[consumes 1, case_names continuity step]: +lemma borel_measurable_gfp[consumes 1, case_names continuity step]: fixes F :: "('a \ 'b) \ ('a \ 'b::{complete_linorder, linorder_topology, second_countable_topology})" assumes "inf_continuous F" assumes *: "\f. f \ borel_measurable M \ F f \ borel_measurable M" @@ -899,56 +899,56 @@ finally show ?thesis . qed -lemma%unimportant borel_measurable_max[measurable (raw)]: +lemma borel_measurable_max[measurable (raw)]: "f \ borel_measurable M \ g \ borel_measurable M \ (\x. max (g x) (f x) :: 'b::{second_countable_topology, linorder_topology}) \ borel_measurable M" by (rule borel_measurableI_less) simp -lemma%unimportant borel_measurable_min[measurable (raw)]: +lemma borel_measurable_min[measurable (raw)]: "f \ borel_measurable M \ g \ borel_measurable M \ (\x. min (g x) (f x) :: 'b::{second_countable_topology, linorder_topology}) \ borel_measurable M" by (rule borel_measurableI_greater) simp -lemma%unimportant borel_measurable_Min[measurable (raw)]: +lemma borel_measurable_Min[measurable (raw)]: "finite I \ (\i. i \ I \ f i \ borel_measurable M) \ (\x. Min ((\i. f i x)`I) :: 'b::{second_countable_topology, linorder_topology}) \ borel_measurable M" proof (induct I rule: finite_induct) case (insert i I) then show ?case by (cases "I = {}") auto qed auto -lemma%unimportant borel_measurable_Max[measurable (raw)]: +lemma borel_measurable_Max[measurable (raw)]: "finite I \ (\i. i \ I \ f i \ borel_measurable M) \ (\x. Max ((\i. f i x)`I) :: 'b::{second_countable_topology, linorder_topology}) \ borel_measurable M" proof (induct I rule: finite_induct) case (insert i I) then show ?case by (cases "I = {}") auto qed auto -lemma%unimportant borel_measurable_sup[measurable (raw)]: +lemma borel_measurable_sup[measurable (raw)]: "f \ borel_measurable M \ g \ borel_measurable M \ (\x. sup (g x) (f x) :: 'b::{lattice, second_countable_topology, linorder_topology}) \ borel_measurable M" unfolding sup_max by measurable -lemma%unimportant borel_measurable_inf[measurable (raw)]: +lemma borel_measurable_inf[measurable (raw)]: "f \ borel_measurable M \ g \ borel_measurable M \ (\x. inf (g x) (f x) :: 'b::{lattice, second_countable_topology, linorder_topology}) \ borel_measurable M" unfolding inf_min by measurable -lemma%unimportant [measurable (raw)]: +lemma [measurable (raw)]: (*FIXME needs name *) fixes f :: "nat \ 'a \ 'b::{complete_linorder, second_countable_topology, linorder_topology}" assumes "\i. f i \ borel_measurable M" shows borel_measurable_liminf: "(\x. liminf (\i. f i x)) \ borel_measurable M" and borel_measurable_limsup: "(\x. limsup (\i. f i x)) \ borel_measurable M" unfolding liminf_SUP_INF limsup_INF_SUP using assms by auto -lemma%unimportant measurable_convergent[measurable (raw)]: +lemma measurable_convergent[measurable (raw)]: 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%unimportant sets_Collect_convergent[measurable]: +lemma sets_Collect_convergent[measurable]: 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%unimportant borel_measurable_lim[measurable (raw)]: +lemma borel_measurable_lim[measurable (raw)]: 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" @@ -959,7 +959,7 @@ by simp qed -lemma%unimportant borel_measurable_LIMSEQ_order: +lemma borel_measurable_LIMSEQ_order: 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" @@ -972,14 +972,14 @@ subsection%important \Borel spaces on topological monoids\ -lemma%unimportant borel_measurable_add[measurable (raw)]: +lemma borel_measurable_add[measurable (raw)]: fixes f g :: "'a \ 'b::{second_countable_topology, topological_monoid_add}" assumes f: "f \ borel_measurable M" assumes g: "g \ borel_measurable M" shows "(\x. f x + g x) \ borel_measurable M" using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) -lemma%unimportant borel_measurable_sum[measurable (raw)]: +lemma borel_measurable_sum[measurable (raw)]: fixes f :: "'c \ 'a \ 'b::{second_countable_topology, topological_comm_monoid_add}" assumes "\i. i \ S \ f i \ borel_measurable M" shows "(\x. \i\S. f i x) \ borel_measurable M" @@ -988,7 +988,7 @@ thus ?thesis using assms by induct auto qed simp -lemma%important borel_measurable_suminf_order[measurable (raw)]: +lemma borel_measurable_suminf_order[measurable (raw)]: 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" @@ -996,22 +996,22 @@ subsection%important \Borel spaces on Euclidean spaces\ -lemma%important borel_measurable_inner[measurable (raw)]: +lemma borel_measurable_inner[measurable (raw)]: fixes f g :: "'a \ 'b::{second_countable_topology, real_inner}" assumes "f \ borel_measurable M" assumes "g \ borel_measurable M" shows "(\x. f x \ g x) \ borel_measurable M" using assms - by%unimportant (rule borel_measurable_continuous_Pair) (intro continuous_intros) + by (rule borel_measurable_continuous_Pair) (intro continuous_intros) notation eucl_less (infix " x \ b} = {x. a {..b}" +lemma box_oc: "{x. a x \ b} = {x. a {..b}" and box_co: "{x. a \ x \ x {x. x sets borel" and "{x. a sets borel" @@ -1023,7 +1023,7 @@ unfolding box_oc box_co by (auto intro: borel_open borel_closed) -lemma%unimportant (*FIX ME this has no name *) +lemma (*FIX ME this has no name *) fixes i :: "'a::{second_countable_topology, real_inner}" shows hafspace_less_borel: "{x. a < x \ i} \ sets borel" and hafspace_greater_borel: "{x. x \ i < a} \ sets borel" @@ -1031,7 +1031,7 @@ and hafspace_greater_eq_borel: "{x. x \ i \ a} \ sets borel" by simp_all -lemma%unimportant borel_eq_box: +lemma borel_eq_box: "borel = sigma UNIV (range (\ (a, b). box a b :: 'a :: euclidean_space set))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI1[OF borel_def]) @@ -1044,7 +1044,7 @@ done qed (auto simp: box_def) -lemma%unimportant halfspace_gt_in_halfspace: +lemma halfspace_gt_in_halfspace: assumes i: "i \ A" shows "{x::'a. a < x \ i} \ sigma_sets UNIV ((\ (a, i). {x::'a::euclidean_space. x \ i < a}) ` (UNIV \ A))" @@ -1070,7 +1070,7 @@ by (auto intro!: Diff sigma_sets_Inter i) qed -lemma%unimportant borel_eq_halfspace_less: +lemma borel_eq_halfspace_less: "borel = sigma UNIV ((\(a, i). {x::'a::euclidean_space. x \ i < a}) ` (UNIV \ Basis))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI2[OF borel_eq_box]) @@ -1083,7 +1083,7 @@ finally show "box a b \ sets ?SIGMA" . qed auto -lemma%unimportant borel_eq_halfspace_le: +lemma borel_eq_halfspace_le: "borel = sigma UNIV ((\ (a, i). {x::'a::euclidean_space. x \ i \ a}) ` (UNIV \ Basis))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less]) @@ -1107,7 +1107,7 @@ by (intro sets.countable_UN) (auto intro: i) qed auto -lemma%unimportant borel_eq_halfspace_ge: +lemma borel_eq_halfspace_ge: "borel = sigma UNIV ((\ (a, i). {x::'a::euclidean_space. a \ x \ i}) ` (UNIV \ Basis))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less]) @@ -1117,10 +1117,10 @@ using i by (intro sets.compl_sets) auto qed auto -lemma%important borel_eq_halfspace_greater: +lemma borel_eq_halfspace_greater: "borel = sigma UNIV ((\ (a, i). {x::'a::euclidean_space. a < x \ i}) ` (UNIV \ Basis))" (is "_ = ?SIGMA") -proof%unimportant (rule borel_eq_sigmaI2[OF borel_eq_halfspace_le]) +proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_le]) fix a :: real and i :: 'a assume "(a, i) \ (UNIV \ Basis)" then have i: "i \ Basis" by auto have *: "{x::'a. x\i \ a} = space ?SIGMA - {x::'a. a < x\i}" by auto @@ -1128,7 +1128,7 @@ by (intro sets.compl_sets) (auto intro: i) qed auto -lemma%unimportant borel_eq_atMost: +lemma borel_eq_atMost: "borel = sigma UNIV (range (\a. {..a::'a::ordered_euclidean_space}))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le]) @@ -1147,7 +1147,7 @@ by (intro sets.countable_UN) auto qed auto -lemma%unimportant borel_eq_greaterThan: +lemma borel_eq_greaterThan: "borel = sigma UNIV (range (\a::'a::ordered_euclidean_space. {x. a a::'a::ordered_euclidean_space. {x. x (a,b). {a..b} ::'a::ordered_euclidean_space set))" (is "_ = ?SIGMA") -proof%unimportant (rule borel_eq_sigmaI5[OF borel_eq_atMost]) +proof (rule borel_eq_sigmaI5[OF borel_eq_atMost]) fix a::'a have *: "{..a} = (\n::nat. {- real n *\<^sub>R One .. a})" proof (safe, simp_all add: eucl_le[where 'a='a]) @@ -1222,12 +1222,12 @@ (auto intro!: sigma_sets_top) qed auto -lemma%important borel_set_induct[consumes 1, case_names empty interval compl union]: +lemma borel_set_induct[consumes 1, case_names empty interval compl union]: assumes "A \ sets borel" assumes empty: "P {}" and int: "\a b. a \ b \ P {a..b}" and compl: "\A. A \ sets borel \ P A \ P (-A)" and un: "\f. disjoint_family f \ (\i. f i \ sets borel) \ (\i. P (f i)) \ P (\i::nat. f i)" shows "P (A::real set)" -proof%unimportant - +proof - let ?G = "range (\(a,b). {a..b::real})" have "Int_stable ?G" "?G \ Pow UNIV" "A \ sigma_sets UNIV ?G" using assms(1) by (auto simp add: borel_eq_atLeastAtMost Int_stable_def) @@ -1244,7 +1244,7 @@ qed (auto intro: empty compl simp: Compl_eq_Diff_UNIV[symmetric] borel_eq_atLeastAtMost) qed -lemma%unimportant borel_sigma_sets_Ioc: "borel = sigma UNIV (range (\(a, b). {a <.. b::real}))" +lemma borel_sigma_sets_Ioc: "borel = sigma UNIV (range (\(a, b). {a <.. b::real}))" proof (rule borel_eq_sigmaI5[OF borel_eq_atMost]) fix i :: real have "{..i} = (\j::nat. {-j <.. i})" @@ -1254,10 +1254,10 @@ finally show "{..i} \ sets (sigma UNIV (range (\(i, j). {i<..j})))" . qed simp -lemma%unimportant eucl_lessThan: "{x::real. x (a, b). {a ..< b :: real}))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI5[OF borel_eq_lessThan]) have move_uminus: "\x y::real. -x \ y \ -y \ x" by auto @@ -1268,7 +1268,7 @@ by (auto intro: sigma_sets.intros(2-) simp: eucl_lessThan) qed auto -lemma%unimportant borel_measurable_halfspacesI: +lemma borel_measurable_halfspacesI: fixes f :: "'a \ 'c::euclidean_space" assumes F: "borel = sigma UNIV (F ` (UNIV \ Basis))" and S_eq: "\a i. S a i = f -` F (a,i) \ space M" @@ -1283,47 +1283,47 @@ by (auto intro!: measurable_measure_of simp: S_eq F) qed -lemma%unimportant borel_measurable_iff_halfspace_le: +lemma borel_measurable_iff_halfspace_le: fixes f :: "'a \ 'c::euclidean_space" shows "f \ borel_measurable M = (\i\Basis. \a. {w \ space M. f w \ i \ a} \ sets M)" by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_le]) auto -lemma%unimportant borel_measurable_iff_halfspace_less: +lemma borel_measurable_iff_halfspace_less: fixes f :: "'a \ 'c::euclidean_space" shows "f \ borel_measurable M \ (\i\Basis. \a. {w \ space M. f w \ i < a} \ sets M)" by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_less]) auto -lemma%unimportant borel_measurable_iff_halfspace_ge: +lemma borel_measurable_iff_halfspace_ge: fixes f :: "'a \ 'c::euclidean_space" shows "f \ borel_measurable M = (\i\Basis. \a. {w \ space M. a \ f w \ i} \ sets M)" by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_ge]) auto -lemma%unimportant borel_measurable_iff_halfspace_greater: +lemma borel_measurable_iff_halfspace_greater: fixes f :: "'a \ 'c::euclidean_space" shows "f \ borel_measurable M \ (\i\Basis. \a. {w \ space M. a < f w \ i} \ sets M)" by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_greater]) auto -lemma%unimportant borel_measurable_iff_le: +lemma borel_measurable_iff_le: "(f::'a \ real) \ borel_measurable M = (\a. {w \ space M. f w \ a} \ sets M)" using borel_measurable_iff_halfspace_le[where 'c=real] by simp -lemma%unimportant borel_measurable_iff_less: +lemma borel_measurable_iff_less: "(f::'a \ real) \ borel_measurable M = (\a. {w \ space M. f w < a} \ sets M)" using borel_measurable_iff_halfspace_less[where 'c=real] by simp -lemma%unimportant borel_measurable_iff_ge: +lemma borel_measurable_iff_ge: "(f::'a \ real) \ borel_measurable M = (\a. {w \ space M. a \ f w} \ sets M)" using borel_measurable_iff_halfspace_ge[where 'c=real] by simp -lemma%unimportant borel_measurable_iff_greater: +lemma borel_measurable_iff_greater: "(f::'a \ real) \ borel_measurable M = (\a. {w \ space M. a < f w} \ sets M)" using borel_measurable_iff_halfspace_greater[where 'c=real] by simp -lemma%important borel_measurable_euclidean_space: +lemma borel_measurable_euclidean_space: fixes f :: "'a \ 'c::euclidean_space" shows "f \ borel_measurable M \ (\i\Basis. (\x. f x \ i) \ borel_measurable M)" -proof%unimportant safe +proof safe assume f: "\i\Basis. (\x. f x \ i) \ borel_measurable M" then show "f \ borel_measurable M" by (subst borel_measurable_iff_halfspace_le) auto @@ -1331,64 +1331,64 @@ subsection%important "Borel measurable operators" -lemma%important borel_measurable_norm[measurable]: "norm \ borel_measurable borel" - by%unimportant (intro borel_measurable_continuous_on1 continuous_intros) +lemma borel_measurable_norm[measurable]: "norm \ borel_measurable borel" + by (intro borel_measurable_continuous_on1 continuous_intros) -lemma%unimportant borel_measurable_sgn [measurable]: "(sgn::'a::real_normed_vector \ 'a) \ borel_measurable borel" +lemma borel_measurable_sgn [measurable]: "(sgn::'a::real_normed_vector \ 'a) \ borel_measurable borel" by (rule borel_measurable_continuous_countable_exceptions[where X="{0}"]) (auto intro!: continuous_on_sgn continuous_on_id) -lemma%important borel_measurable_uminus[measurable (raw)]: +lemma borel_measurable_uminus[measurable (raw)]: fixes g :: "'a \ 'b::{second_countable_topology, real_normed_vector}" assumes g: "g \ borel_measurable M" shows "(\x. - g x) \ borel_measurable M" - by%unimportant (rule borel_measurable_continuous_on[OF _ g]) (intro continuous_intros) + by (rule borel_measurable_continuous_on[OF _ g]) (intro continuous_intros) -lemma%important borel_measurable_diff[measurable (raw)]: +lemma borel_measurable_diff[measurable (raw)]: fixes f :: "'a \ 'b::{second_countable_topology, real_normed_vector}" assumes f: "f \ borel_measurable M" assumes g: "g \ borel_measurable M" shows "(\x. f x - g x) \ borel_measurable M" - using%unimportant borel_measurable_add [of f M "- g"] assms by (simp add: fun_Compl_def) + using borel_measurable_add [of f M "- g"] assms by (simp add: fun_Compl_def) -lemma%unimportant borel_measurable_times[measurable (raw)]: +lemma borel_measurable_times[measurable (raw)]: fixes f :: "'a \ 'b::{second_countable_topology, real_normed_algebra}" assumes f: "f \ borel_measurable M" assumes g: "g \ borel_measurable M" shows "(\x. f x * g x) \ borel_measurable M" using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) -lemma%important borel_measurable_prod[measurable (raw)]: +lemma borel_measurable_prod[measurable (raw)]: fixes f :: "'c \ 'a \ 'b::{second_countable_topology, real_normed_field}" assumes "\i. i \ S \ f i \ borel_measurable M" shows "(\x. \i\S. f i x) \ borel_measurable M" -proof%unimportant cases +proof cases assume "finite S" thus ?thesis using assms by induct auto qed simp -lemma%important borel_measurable_dist[measurable (raw)]: +lemma borel_measurable_dist[measurable (raw)]: fixes g f :: "'a \ 'b::{second_countable_topology, metric_space}" assumes f: "f \ borel_measurable M" assumes g: "g \ borel_measurable M" shows "(\x. dist (f x) (g x)) \ borel_measurable M" - using%unimportant f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) + using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) -lemma%unimportant borel_measurable_scaleR[measurable (raw)]: +lemma borel_measurable_scaleR[measurable (raw)]: fixes g :: "'a \ 'b::{second_countable_topology, real_normed_vector}" assumes f: "f \ borel_measurable M" assumes g: "g \ borel_measurable M" shows "(\x. f x *\<^sub>R g x) \ borel_measurable M" using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) -lemma%unimportant borel_measurable_uminus_eq [simp]: +lemma borel_measurable_uminus_eq [simp]: fixes f :: "'a \ 'b::{second_countable_topology, real_normed_vector}" shows "(\x. - f x) \ borel_measurable M \ f \ borel_measurable M" (is "?l = ?r") proof assume ?l from borel_measurable_uminus[OF this] show ?r by simp qed auto -lemma%unimportant affine_borel_measurable_vector: +lemma affine_borel_measurable_vector: fixes f :: "'a \ 'x::real_normed_vector" assumes "f \ borel_measurable M" shows "(\x. a + b *\<^sub>R f x) \ borel_measurable M" @@ -1409,15 +1409,15 @@ qed simp qed -lemma%unimportant borel_measurable_const_scaleR[measurable (raw)]: +lemma borel_measurable_const_scaleR[measurable (raw)]: "f \ borel_measurable M \ (\x. b *\<^sub>R f x ::'a::real_normed_vector) \ borel_measurable M" using affine_borel_measurable_vector[of f M 0 b] by simp -lemma%unimportant borel_measurable_const_add[measurable (raw)]: +lemma borel_measurable_const_add[measurable (raw)]: "f \ borel_measurable M \ (\x. a + f x ::'a::real_normed_vector) \ borel_measurable M" using affine_borel_measurable_vector[of f M a 1] by simp -lemma%unimportant borel_measurable_inverse[measurable (raw)]: +lemma borel_measurable_inverse[measurable (raw)]: fixes f :: "'a \ 'b::real_normed_div_algebra" assumes f: "f \ borel_measurable M" shows "(\x. inverse (f x)) \ borel_measurable M" @@ -1426,27 +1426,27 @@ apply (auto intro!: continuous_on_inverse continuous_on_id) done -lemma%unimportant borel_measurable_divide[measurable (raw)]: +lemma borel_measurable_divide[measurable (raw)]: "f \ borel_measurable M \ g \ borel_measurable M \ (\x. f x / g x::'b::{second_countable_topology, real_normed_div_algebra}) \ borel_measurable M" by (simp add: divide_inverse) -lemma%unimportant borel_measurable_abs[measurable (raw)]: +lemma borel_measurable_abs[measurable (raw)]: "f \ borel_measurable M \ (\x. \f x :: real\) \ borel_measurable M" unfolding abs_real_def by simp -lemma%unimportant borel_measurable_nth[measurable (raw)]: +lemma borel_measurable_nth[measurable (raw)]: "(\x::real^'n. x $ i) \ borel_measurable borel" by (simp add: cart_eq_inner_axis) -lemma%important convex_measurable: +lemma convex_measurable: fixes A :: "'a :: euclidean_space set" shows "X \ borel_measurable M \ X ` space M \ A \ open A \ convex_on A q \ (\x. q (X x)) \ borel_measurable M" - by%unimportant (rule measurable_compose[where f=X and N="restrict_space borel A"]) + by (rule measurable_compose[where f=X and N="restrict_space borel A"]) (auto intro!: borel_measurable_continuous_on_restrict convex_on_continuous measurable_restrict_space2) -lemma%unimportant borel_measurable_ln[measurable (raw)]: +lemma borel_measurable_ln[measurable (raw)]: assumes f: "f \ borel_measurable M" shows "(\x. ln (f x :: real)) \ borel_measurable M" apply (rule measurable_compose[OF f]) @@ -1454,15 +1454,15 @@ apply (auto intro!: continuous_on_ln continuous_on_id) done -lemma%unimportant borel_measurable_log[measurable (raw)]: +lemma borel_measurable_log[measurable (raw)]: "f \ borel_measurable M \ g \ borel_measurable M \ (\x. log (g x) (f x)) \ borel_measurable M" unfolding log_def by auto -lemma%unimportant borel_measurable_exp[measurable]: +lemma borel_measurable_exp[measurable]: "(exp::'a::{real_normed_field,banach}\'a) \ borel_measurable borel" by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI isCont_exp) -lemma%unimportant measurable_real_floor[measurable]: +lemma measurable_real_floor[measurable]: "(floor :: real \ int) \ measurable borel (count_space UNIV)" proof - have "\a x. \x\ = a \ (real_of_int a \ x \ x < real_of_int (a + 1))" @@ -1471,41 +1471,41 @@ by (auto simp: vimage_def measurable_count_space_eq2_countable) qed -lemma%unimportant measurable_real_ceiling[measurable]: +lemma measurable_real_ceiling[measurable]: "(ceiling :: real \ int) \ measurable borel (count_space UNIV)" unfolding ceiling_def[abs_def] by simp -lemma%unimportant borel_measurable_real_floor: "(\x::real. real_of_int \x\) \ borel_measurable borel" +lemma borel_measurable_real_floor: "(\x::real. real_of_int \x\) \ borel_measurable borel" by simp -lemma%unimportant borel_measurable_root [measurable]: "root n \ borel_measurable borel" +lemma borel_measurable_root [measurable]: "root n \ borel_measurable borel" by (intro borel_measurable_continuous_on1 continuous_intros) -lemma%unimportant borel_measurable_sqrt [measurable]: "sqrt \ borel_measurable borel" +lemma borel_measurable_sqrt [measurable]: "sqrt \ borel_measurable borel" by (intro borel_measurable_continuous_on1 continuous_intros) -lemma%unimportant borel_measurable_power [measurable (raw)]: +lemma borel_measurable_power [measurable (raw)]: fixes f :: "_ \ 'b::{power,real_normed_algebra}" assumes f: "f \ borel_measurable M" shows "(\x. (f x) ^ n) \ borel_measurable M" by (intro borel_measurable_continuous_on [OF _ f] continuous_intros) -lemma%unimportant borel_measurable_Re [measurable]: "Re \ borel_measurable borel" +lemma borel_measurable_Re [measurable]: "Re \ borel_measurable borel" by (intro borel_measurable_continuous_on1 continuous_intros) -lemma%unimportant borel_measurable_Im [measurable]: "Im \ borel_measurable borel" +lemma borel_measurable_Im [measurable]: "Im \ borel_measurable borel" by (intro borel_measurable_continuous_on1 continuous_intros) -lemma%unimportant borel_measurable_of_real [measurable]: "(of_real :: _ \ (_::real_normed_algebra)) \ borel_measurable borel" +lemma borel_measurable_of_real [measurable]: "(of_real :: _ \ (_::real_normed_algebra)) \ borel_measurable borel" by (intro borel_measurable_continuous_on1 continuous_intros) -lemma%unimportant borel_measurable_sin [measurable]: "(sin :: _ \ (_::{real_normed_field,banach})) \ borel_measurable borel" +lemma borel_measurable_sin [measurable]: "(sin :: _ \ (_::{real_normed_field,banach})) \ borel_measurable borel" by (intro borel_measurable_continuous_on1 continuous_intros) -lemma%unimportant borel_measurable_cos [measurable]: "(cos :: _ \ (_::{real_normed_field,banach})) \ borel_measurable borel" +lemma borel_measurable_cos [measurable]: "(cos :: _ \ (_::{real_normed_field,banach})) \ borel_measurable borel" by (intro borel_measurable_continuous_on1 continuous_intros) -lemma%unimportant borel_measurable_arctan [measurable]: "arctan \ borel_measurable borel" +lemma borel_measurable_arctan [measurable]: "arctan \ borel_measurable borel" by (intro borel_measurable_continuous_on1 continuous_intros) lemma%important borel_measurable_complex_iff: @@ -1517,21 +1517,21 @@ apply auto done -lemma%important powr_real_measurable [measurable]: +lemma powr_real_measurable [measurable]: assumes "f \ measurable M borel" "g \ measurable M borel" shows "(\x. f x powr g x :: real) \ measurable M borel" - using%unimportant assms by (simp_all add: powr_def) + using assms by (simp_all add: powr_def) -lemma%unimportant measurable_of_bool[measurable]: "of_bool \ count_space UNIV \\<^sub>M borel" +lemma measurable_of_bool[measurable]: "of_bool \ count_space UNIV \\<^sub>M borel" by simp subsection%important "Borel space on the extended reals" -lemma%unimportant borel_measurable_ereal[measurable (raw)]: +lemma borel_measurable_ereal[measurable (raw)]: assumes f: "f \ borel_measurable M" shows "(\x. ereal (f x)) \ borel_measurable M" using continuous_on_ereal f by (rule borel_measurable_continuous_on) (rule continuous_on_id) -lemma%unimportant borel_measurable_real_of_ereal[measurable (raw)]: +lemma borel_measurable_real_of_ereal[measurable (raw)]: fixes f :: "'a \ ereal" assumes f: "f \ borel_measurable M" shows "(\x. real_of_ereal (f x)) \ borel_measurable M" @@ -1540,7 +1540,7 @@ apply (auto intro: continuous_on_real simp: Compl_eq_Diff_UNIV) done -lemma%unimportant borel_measurable_ereal_cases: +lemma borel_measurable_ereal_cases: fixes f :: "'a \ ereal" assumes f: "f \ borel_measurable M" assumes H: "(\x. H (ereal (real_of_ereal (f x)))) \ borel_measurable M" @@ -1551,20 +1551,20 @@ with f H show ?thesis by simp qed -lemma%unimportant (*FIX ME needs a name *) +lemma (*FIX ME needs a name *) fixes f :: "'a \ ereal" assumes f[measurable]: "f \ borel_measurable M" shows borel_measurable_ereal_abs[measurable(raw)]: "(\x. \f x\) \ borel_measurable M" and borel_measurable_ereal_inverse[measurable(raw)]: "(\x. inverse (f x) :: ereal) \ borel_measurable M" and borel_measurable_uminus_ereal[measurable(raw)]: "(\x. - f x :: ereal) \ borel_measurable M" by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If) -lemma%unimportant borel_measurable_uminus_eq_ereal[simp]: +lemma borel_measurable_uminus_eq_ereal[simp]: "(\x. - f x :: ereal) \ borel_measurable M \ f \ borel_measurable M" (is "?l = ?r") proof assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp qed auto -lemma%important set_Collect_ereal2: +lemma set_Collect_ereal2: fixes f g :: "'a \ ereal" assumes f: "f \ borel_measurable M" assumes g: "g \ borel_measurable M" @@ -1574,7 +1574,7 @@ "{x \ space borel. H (ereal x) (-\)} \ sets borel" "{x \ space borel. H (ereal x) (\)} \ sets borel" shows "{x \ space M. H (f x) (g x)} \ sets M" -proof%unimportant - +proof - let ?G = "\y x. if g x = \ then H y \ else if g x = -\ then H y (-\) else H y (ereal (real_of_ereal (g x)))" let ?F = "\x. if f x = \ then ?G \ x else if f x = -\ then ?G (-\) x else ?G (ereal (real_of_ereal (f x))) x" { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto } @@ -1583,7 +1583,7 @@ by (subst *) (simp del: space_borel split del: if_split) qed -lemma%unimportant borel_measurable_ereal_iff: +lemma borel_measurable_ereal_iff: shows "(\x. ereal (f x)) \ borel_measurable M \ f \ borel_measurable M" proof assume "(\x. ereal (f x)) \ borel_measurable M" @@ -1591,15 +1591,15 @@ show "f \ borel_measurable M" by auto qed auto -lemma%unimportant borel_measurable_erealD[measurable_dest]: +lemma borel_measurable_erealD[measurable_dest]: "(\x. ereal (f x)) \ borel_measurable M \ g \ measurable N M \ (\x. f (g x)) \ borel_measurable N" unfolding borel_measurable_ereal_iff by simp -lemma%important borel_measurable_ereal_iff_real: +theorem borel_measurable_ereal_iff_real: fixes f :: "'a \ ereal" shows "f \ borel_measurable M \ ((\x. real_of_ereal (f x)) \ borel_measurable M \ f -` {\} \ space M \ sets M \ f -` {-\} \ space M \ sets M)" -proof%unimportant safe +proof safe assume *: "(\x. real_of_ereal (f x)) \ borel_measurable M" "f -` {\} \ space M \ sets M" "f -` {-\} \ space M \ sets M" have "f -` {\} \ space M = {x\space M. f x = \}" "f -` {-\} \ space M = {x\space M. f x = -\}" by auto with * have **: "{x\space M. f x = \} \ sets M" "{x\space M. f x = -\} \ sets M" by simp_all @@ -1609,15 +1609,15 @@ finally show "f \ borel_measurable M" . qed simp_all -lemma%unimportant borel_measurable_ereal_iff_Iio: +lemma borel_measurable_ereal_iff_Iio: "(f::'a \ ereal) \ borel_measurable M \ (\a. f -` {..< a} \ space M \ sets M)" by (auto simp: borel_Iio measurable_iff_measure_of) -lemma%unimportant borel_measurable_ereal_iff_Ioi: +lemma borel_measurable_ereal_iff_Ioi: "(f::'a \ ereal) \ borel_measurable M \ (\a. f -` {a <..} \ space M \ sets M)" by (auto simp: borel_Ioi measurable_iff_measure_of) -lemma%unimportant vimage_sets_compl_iff: +lemma vimage_sets_compl_iff: "f -` A \ space M \ sets M \ f -` (- A) \ space M \ sets M" proof - { fix A assume "f -` A \ space M \ sets M" @@ -1627,15 +1627,15 @@ by (metis double_complement) qed -lemma%unimportant borel_measurable_iff_Iic_ereal: +lemma borel_measurable_iff_Iic_ereal: "(f::'a\ereal) \ borel_measurable M \ (\a. f -` {..a} \ space M \ sets M)" unfolding borel_measurable_ereal_iff_Ioi vimage_sets_compl_iff[where A="{a <..}" for a] by simp -lemma%unimportant borel_measurable_iff_Ici_ereal: +lemma borel_measurable_iff_Ici_ereal: "(f::'a \ ereal) \ borel_measurable M \ (\a. f -` {a..} \ space M \ sets M)" unfolding borel_measurable_ereal_iff_Iio vimage_sets_compl_iff[where A="{..< a}" for a] by simp -lemma%important borel_measurable_ereal2: +lemma borel_measurable_ereal2: fixes f g :: "'a \ ereal" assumes f: "f \ borel_measurable M" assumes g: "g \ borel_measurable M" @@ -1645,7 +1645,7 @@ "(\x. H (ereal (real_of_ereal (f x))) (-\)) \ borel_measurable M" "(\x. H (ereal (real_of_ereal (f x))) (\)) \ borel_measurable M" shows "(\x. H (f x) (g x)) \ borel_measurable M" -proof%unimportant - +proof - let ?G = "\y x. if g x = \ then H y \ else if g x = - \ then H y (-\) else H y (ereal (real_of_ereal (g x)))" let ?F = "\x. if f x = \ then ?G \ x else if f x = - \ then ?G (-\) x else ?G (ereal (real_of_ereal (f x))) x" { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto } @@ -1653,14 +1653,14 @@ from assms show ?thesis unfolding * by simp qed -lemma%unimportant [measurable(raw)]: +lemma [measurable(raw)]: fixes f :: "'a \ ereal" assumes [measurable]: "f \ borel_measurable M" "g \ borel_measurable M" shows borel_measurable_ereal_add: "(\x. f x + g x) \ borel_measurable M" and borel_measurable_ereal_times: "(\x. f x * g x) \ borel_measurable M" by (simp_all add: borel_measurable_ereal2) -lemma%unimportant [measurable(raw)]: +lemma [measurable(raw)]: fixes f g :: "'a \ ereal" assumes "f \ borel_measurable M" assumes "g \ borel_measurable M" @@ -1668,19 +1668,19 @@ and borel_measurable_ereal_divide: "(\x. f x / g x) \ borel_measurable M" using assms by (simp_all add: minus_ereal_def divide_ereal_def) -lemma%unimportant borel_measurable_ereal_sum[measurable (raw)]: +lemma borel_measurable_ereal_sum[measurable (raw)]: fixes f :: "'c \ 'a \ ereal" assumes "\i. i \ S \ f i \ borel_measurable M" shows "(\x. \i\S. f i x) \ borel_measurable M" using assms by (induction S rule: infinite_finite_induct) auto -lemma%unimportant borel_measurable_ereal_prod[measurable (raw)]: +lemma borel_measurable_ereal_prod[measurable (raw)]: fixes f :: "'c \ 'a \ ereal" assumes "\i. i \ S \ f i \ borel_measurable M" shows "(\x. \i\S. f i x) \ borel_measurable M" using assms by (induction S rule: infinite_finite_induct) auto -lemma%unimportant borel_measurable_extreal_suminf[measurable (raw)]: +lemma borel_measurable_extreal_suminf[measurable (raw)]: fixes f :: "nat \ 'a \ ereal" assumes [measurable]: "\i. f i \ borel_measurable M" shows "(\x. (\i. f i x)) \ borel_measurable M" @@ -1691,19 +1691,19 @@ text \ \<^type>\ennreal\ is a topological monoid, so no rules for plus are required, also all order statements are usually done on type classes. \ -lemma%unimportant measurable_enn2ereal[measurable]: "enn2ereal \ borel \\<^sub>M borel" +lemma measurable_enn2ereal[measurable]: "enn2ereal \ borel \\<^sub>M borel" by (intro borel_measurable_continuous_on1 continuous_on_enn2ereal) -lemma%unimportant measurable_e2ennreal[measurable]: "e2ennreal \ borel \\<^sub>M borel" +lemma measurable_e2ennreal[measurable]: "e2ennreal \ borel \\<^sub>M borel" by (intro borel_measurable_continuous_on1 continuous_on_e2ennreal) -lemma%unimportant borel_measurable_enn2real[measurable (raw)]: +lemma borel_measurable_enn2real[measurable (raw)]: "f \ M \\<^sub>M borel \ (\x. enn2real (f x)) \ M \\<^sub>M borel" unfolding enn2real_def[abs_def] by measurable definition%important [simp]: "is_borel f M \ f \ borel_measurable M" -lemma%unimportant is_borel_transfer[transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) (=) is_borel is_borel" +lemma is_borel_transfer[transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) (=) is_borel is_borel" unfolding is_borel_def[abs_def] proof (safe intro!: rel_funI ext dest!: rel_fun_eq_pcr_ennreal[THEN iffD1]) fix f and M :: "'a measure" @@ -1715,14 +1715,14 @@ includes ennreal.lifting begin -lemma%unimportant measurable_ennreal[measurable]: "ennreal \ borel \\<^sub>M borel" +lemma measurable_ennreal[measurable]: "ennreal \ borel \\<^sub>M borel" unfolding is_borel_def[symmetric] by transfer simp -lemma%important borel_measurable_ennreal_iff[simp]: +lemma borel_measurable_ennreal_iff[simp]: assumes [simp]: "\x. x \ space M \ 0 \ f x" shows "(\x. ennreal (f x)) \ M \\<^sub>M borel \ f \ M \\<^sub>M borel" -proof%unimportant safe +proof safe assume "(\x. ennreal (f x)) \ M \\<^sub>M borel" then have "(\x. enn2real (ennreal (f x))) \ M \\<^sub>M borel" by measurable @@ -1730,31 +1730,31 @@ by (rule measurable_cong[THEN iffD1, rotated]) auto qed measurable -lemma%unimportant borel_measurable_times_ennreal[measurable (raw)]: +lemma borel_measurable_times_ennreal[measurable (raw)]: fixes f g :: "'a \ ennreal" shows "f \ M \\<^sub>M borel \ g \ M \\<^sub>M borel \ (\x. f x * g x) \ M \\<^sub>M borel" unfolding is_borel_def[symmetric] by transfer simp -lemma%unimportant borel_measurable_inverse_ennreal[measurable (raw)]: +lemma borel_measurable_inverse_ennreal[measurable (raw)]: fixes f :: "'a \ ennreal" shows "f \ M \\<^sub>M borel \ (\x. inverse (f x)) \ M \\<^sub>M borel" unfolding is_borel_def[symmetric] by transfer simp -lemma%unimportant borel_measurable_divide_ennreal[measurable (raw)]: +lemma borel_measurable_divide_ennreal[measurable (raw)]: fixes f :: "'a \ ennreal" shows "f \ M \\<^sub>M borel \ g \ M \\<^sub>M borel \ (\x. f x / g x) \ M \\<^sub>M borel" unfolding divide_ennreal_def by simp -lemma%unimportant borel_measurable_minus_ennreal[measurable (raw)]: +lemma borel_measurable_minus_ennreal[measurable (raw)]: fixes f :: "'a \ ennreal" shows "f \ M \\<^sub>M borel \ g \ M \\<^sub>M borel \ (\x. f x - g x) \ M \\<^sub>M borel" unfolding is_borel_def[symmetric] by transfer simp -lemma%important borel_measurable_prod_ennreal[measurable (raw)]: +lemma borel_measurable_prod_ennreal[measurable (raw)]: fixes f :: "'c \ 'a \ ennreal" assumes "\i. i \ S \ f i \ borel_measurable M" shows "(\x. \i\S. f i x) \ borel_measurable M" - using%unimportant assms by (induction S rule: infinite_finite_induct) auto + using assms by (induction S rule: infinite_finite_induct) auto end @@ -1762,12 +1762,12 @@ subsection%important \LIMSEQ is borel measurable\ -lemma%important borel_measurable_LIMSEQ_real: +lemma borel_measurable_LIMSEQ_real: fixes u :: "nat \ 'a \ real" 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" -proof%unimportant - +proof - have "\x. x \ space M \ liminf (\n. ereal (u n x)) = ereal (u' x)" using u' by (simp add: lim_imp_Liminf) moreover from u have "(\x. liminf (\n. ereal (u n x))) \ borel_measurable M" @@ -1775,13 +1775,13 @@ ultimately show ?thesis by (simp cong: measurable_cong add: borel_measurable_ereal_iff) qed -lemma%important borel_measurable_LIMSEQ_metric: +lemma borel_measurable_LIMSEQ_metric: fixes f :: "nat \ 'a \ 'b :: metric_space" assumes [measurable]: "\i. f i \ borel_measurable M" assumes lim: "\x. x \ space M \ (\i. f i x) \ g x" shows "g \ borel_measurable M" unfolding borel_eq_closed -proof%unimportant (safe intro!: measurable_measure_of) +proof (safe intro!: measurable_measure_of) fix A :: "'b set" assume "closed A" have [measurable]: "(\x. infdist (g x) A) \ borel_measurable M" @@ -1806,13 +1806,13 @@ qed simp qed auto -lemma%important sets_Collect_Cauchy[measurable]: +lemma sets_Collect_Cauchy[measurable]: fixes f :: "nat \ 'a => 'b::{metric_space, second_countable_topology}" assumes f[measurable]: "\i. f i \ borel_measurable M" shows "{x\space M. Cauchy (\i. f i x)} \ sets M" unfolding metric_Cauchy_iff2 using f by auto -lemma%unimportant borel_measurable_lim_metric[measurable (raw)]: +lemma borel_measurable_lim_metric[measurable (raw)]: fixes f :: "nat \ 'a \ 'b::{banach, second_countable_topology}" assumes f[measurable]: "\i. f i \ borel_measurable M" shows "(\x. lim (\i. f i x)) \ borel_measurable M" @@ -1834,17 +1834,17 @@ unfolding * by measurable qed -lemma%unimportant borel_measurable_suminf[measurable (raw)]: +lemma borel_measurable_suminf[measurable (raw)]: fixes f :: "nat \ 'a \ 'b::{banach, second_countable_topology}" 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 -lemma%unimportant Collect_closed_imp_pred_borel: "closed {x. P x} \ Measurable.pred borel P" +lemma Collect_closed_imp_pred_borel: "closed {x. P x} \ Measurable.pred borel P" by (simp add: pred_def) (* Proof by Jeremy Avigad and Luke Serafin *) -lemma%unimportant isCont_borel_pred[measurable]: +lemma isCont_borel_pred[measurable]: fixes f :: "'b::metric_space \ 'a::metric_space" shows "Measurable.pred borel (isCont f)" proof (subst measurable_cong) @@ -1895,21 +1895,21 @@ qed (intro pred_intros_countable closed_Collect_all closed_Collect_le open_Collect_less Collect_closed_imp_pred_borel closed_Collect_imp open_Collect_conj continuous_intros) -lemma%unimportant isCont_borel: +lemma isCont_borel: fixes f :: "'b::metric_space \ 'a::metric_space" shows "{x. isCont f x} \ sets borel" by simp -lemma%important is_real_interval: +lemma is_real_interval: assumes S: "is_interval S" shows "\a b::real. S = {} \ S = UNIV \ S = {.. S = {..b} \ S = {a<..} \ S = {a..} \ S = {a<.. S = {a<..b} \ S = {a.. S = {a..b}" using S unfolding is_interval_1 by (blast intro: interval_cases) -lemma%important real_interval_borel_measurable: +lemma real_interval_borel_measurable: assumes "is_interval (S::real set)" shows "S \ sets borel" -proof%unimportant - +proof - from assms is_real_interval have "\a b::real. S = {} \ S = UNIV \ S = {.. S = {..b} \ S = {a<..} \ S = {a..} \ S = {a<.. S = {a<..b} \ S = {a.. S = {a..b}" by auto then guess a .. @@ -1921,7 +1921,7 @@ text \The next lemmas hold in any second countable linorder (including ennreal or ereal for instance), but in the current state they are restricted to reals.\ -lemma%important borel_measurable_mono_on_fnc: +lemma borel_measurable_mono_on_fnc: fixes f :: "real \ real" and A :: "real set" assumes "mono_on f A" shows "f \ borel_measurable (restrict_space borel A)" @@ -1932,18 +1932,18 @@ intro!: borel_measurable_continuous_on_restrict intro: continuous_within_subset) done -lemma%unimportant borel_measurable_piecewise_mono: +lemma borel_measurable_piecewise_mono: fixes f::"real \ real" and C::"real set set" assumes "countable C" "\c. c \ C \ c \ sets borel" "\c. c \ C \ mono_on f c" "(\C) = UNIV" shows "f \ borel_measurable borel" by (rule measurable_piecewise_restrict[of C], auto intro: borel_measurable_mono_on_fnc simp: assms) -lemma%unimportant borel_measurable_mono: +lemma borel_measurable_mono: fixes f :: "real \ real" shows "mono f \ f \ borel_measurable borel" using borel_measurable_mono_on_fnc[of f UNIV] by (simp add: mono_def mono_on_def) -lemma%unimportant measurable_bdd_below_real[measurable (raw)]: +lemma measurable_bdd_below_real[measurable (raw)]: fixes F :: "'a \ 'i \ real" assumes [simp]: "countable I" and [measurable]: "\i. i \ I \ F i \ M \\<^sub>M borel" shows "Measurable.pred M (\x. bdd_below ((\i. F i x)`I))" @@ -1954,12 +1954,12 @@ using countable_int by measurable qed -lemma%important borel_measurable_cINF_real[measurable (raw)]: +lemma borel_measurable_cINF_real[measurable (raw)]: fixes F :: "_ \ _ \ real" assumes [simp]: "countable I" assumes F[measurable]: "\i. i \ I \ F i \ borel_measurable M" shows "(\x. INF i\I. F i x) \ borel_measurable M" -proof%unimportant (rule measurable_piecewise_restrict) +proof (rule measurable_piecewise_restrict) let ?\ = "{x\space M. bdd_below ((\i. F i x)`I)}" show "countable {?\, - ?\}" "space M \ \{?\, - ?\}" "\X. X \ {?\, - ?\} \ X \ space M \ sets M" by auto @@ -1979,7 +1979,7 @@ qed qed -lemma%unimportant borel_Ici: "borel = sigma UNIV (range (\x::real. {x ..}))" +lemma borel_Ici: "borel = sigma UNIV (range (\x::real. {x ..}))" proof (safe intro!: borel_eq_sigmaI1[OF borel_Iio]) fix x :: real have eq: "{.. 'b::{second_countable_topology, linorder_topology}" shows "f \ borel_measurable M \ g \ borel_measurable M \ Measurable.pred M (\w. f w < g w)" unfolding Measurable.pred_def by (rule borel_measurable_less) @@ -1996,19 +1996,19 @@ no_notation eucl_less (infix " _ \ 'a::{second_countable_topology, dense_linorder, linorder_topology}" assumes "finite I" and [measurable]: "\i. f i \ borel_measurable M" shows "(\x. Max{f i x |i. i \ I}) \ borel_measurable M" -by%unimportant (simp add: borel_measurable_Max[OF assms(1), where ?f=f and ?M=M] Setcompr_eq_image) + by (simp add: borel_measurable_Max[OF assms(1), where ?f=f and ?M=M] Setcompr_eq_image) -lemma%unimportant measurable_compose_n [measurable (raw)]: +lemma measurable_compose_n [measurable (raw)]: assumes "T \ measurable M M" shows "(T^^n) \ measurable M M" by (induction n, auto simp add: measurable_compose[OF _ assms]) -lemma%unimportant measurable_real_imp_nat: +lemma measurable_real_imp_nat: fixes f::"'a \ nat" assumes [measurable]: "(\x. real(f x)) \ borel_measurable M" shows "f \ measurable M (count_space UNIV)" @@ -2020,7 +2020,7 @@ then show ?thesis using measurable_count_space_eq2_countable by blast qed -lemma%unimportant measurable_equality_set [measurable]: +lemma measurable_equality_set [measurable]: fixes f g::"_\ 'a::{second_countable_topology, t2_space}" assumes [measurable]: "f \ borel_measurable M" "g \ borel_measurable M" shows "{x \ space M. f x = g x} \ sets M" @@ -2035,7 +2035,7 @@ then show ?thesis unfolding A_def by simp qed -lemma%unimportant measurable_inequality_set [measurable]: +lemma measurable_inequality_set [measurable]: fixes f g::"_ \ 'a::{second_countable_topology, linorder_topology}" assumes [measurable]: "f \ borel_measurable M" "g \ borel_measurable M" shows "{x \ space M. f x \ g x} \ sets M" @@ -2063,7 +2063,7 @@ ultimately show "{x \ space M. f x > g x} \ sets M" using * by (metis (mono_tags, lifting) measurable_sets) qed -lemma%unimportant measurable_limit [measurable]: +proposition measurable_limit [measurable]: fixes f::"nat \ 'a \ 'b::first_countable_topology" assumes [measurable]: "\n::nat. f n \ borel_measurable M" shows "Measurable.pred M (\x. (\n. f n x) \ c)" @@ -2103,11 +2103,11 @@ then show ?thesis by auto qed -lemma%important measurable_limit2 [measurable]: +lemma measurable_limit2 [measurable]: fixes u::"nat \ 'a \ real" assumes [measurable]: "\n. u n \ borel_measurable M" "v \ borel_measurable M" shows "Measurable.pred M (\x. (\n. u n x) \ v x)" -proof%unimportant - +proof - define w where "w = (\n x. u n x - v x)" have [measurable]: "w n \ borel_measurable M" for n unfolding w_def by auto have "((\n. u n x) \ v x) \ ((\n. w n x) \ 0)" for x @@ -2115,7 +2115,7 @@ then show ?thesis using measurable_limit by auto qed -lemma%unimportant measurable_P_restriction [measurable (raw)]: +lemma measurable_P_restriction [measurable (raw)]: assumes [measurable]: "Measurable.pred M P" "A \ sets M" shows "{x \ A. P x} \ sets M" proof - @@ -2124,7 +2124,7 @@ then show ?thesis by auto qed -lemma%unimportant measurable_sum_nat [measurable (raw)]: +lemma measurable_sum_nat [measurable (raw)]: fixes f :: "'c \ 'a \ nat" assumes "\i. i \ S \ f i \ measurable M (count_space UNIV)" shows "(\x. \i\S. f i x) \ measurable M (count_space UNIV)" @@ -2134,7 +2134,7 @@ qed simp -lemma%unimportant measurable_abs_powr [measurable]: +lemma measurable_abs_powr [measurable]: fixes p::real assumes [measurable]: "f \ borel_measurable M" shows "(\x. \f x\ powr p) \ borel_measurable M" @@ -2142,7 +2142,7 @@ text \The next one is a variation around \measurable_restrict_space\.\ -lemma%unimportant measurable_restrict_space3: +lemma measurable_restrict_space3: assumes "f \ measurable M N" and "f \ A \ B" shows "f \ measurable (restrict_space M A) (restrict_space N B)" @@ -2154,12 +2154,12 @@ text \The next one is a variation around \measurable_piecewise_restrict\.\ -lemma%important measurable_piecewise_restrict2: +lemma measurable_piecewise_restrict2: assumes [measurable]: "\n. A n \ sets M" and "space M = (\(n::nat). A n)" "\n. \h \ measurable M N. (\x \ A n. f x = h x)" shows "f \ measurable M N" -proof%unimportant (rule measurableI) +proof (rule measurableI) fix B assume [measurable]: "B \ sets N" { fix n::nat diff -r e61b0b819d28 -r 3417a8f154eb src/HOL/Analysis/Caratheodory.thy --- a/src/HOL/Analysis/Caratheodory.thy Sun Jan 13 20:25:41 2019 +0100 +++ b/src/HOL/Analysis/Caratheodory.thy Mon Jan 14 11:59:19 2019 +0000 @@ -13,7 +13,7 @@ Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson. \ -lemma%unimportant suminf_ennreal_2dimen: +lemma suminf_ennreal_2dimen: fixes f:: "nat \ nat \ ennreal" assumes "\m. g m = (\n. f (m,n))" shows "(\i. f (prod_decode i)) = suminf g" @@ -60,7 +60,7 @@ where "lambda_system \ M f = {l \ M. \x \ M. f (l \ x) + f ((\ - l) \ x) = f x}" -lemma%unimportant (in algebra) lambda_system_eq: +lemma (in algebra) lambda_system_eq: "lambda_system \ M f = {l \ M. \x \ M. f (x \ l) + f (x - l) = f x}" proof - have [simp]: "\l x. l \ M \ x \ M \ (\ - l) \ x = x - l" @@ -69,13 +69,13 @@ by (auto simp add: lambda_system_def) (metis Int_commute)+ qed -lemma%unimportant (in algebra) lambda_system_empty: "positive M f \ {} \ lambda_system \ M f" +lemma (in algebra) lambda_system_empty: "positive M f \ {} \ lambda_system \ M f" by (auto simp add: positive_def lambda_system_eq) -lemma%unimportant lambda_system_sets: "x \ lambda_system \ M f \ x \ M" +lemma lambda_system_sets: "x \ lambda_system \ M f \ x \ M" by (simp add: lambda_system_def) -lemma%unimportant (in algebra) lambda_system_Compl: +lemma (in algebra) lambda_system_Compl: fixes f:: "'a set \ ennreal" assumes x: "x \ lambda_system \ M f" shows "\ - x \ lambda_system \ M f" @@ -88,7 +88,7 @@ by (force simp add: lambda_system_def ac_simps) qed -lemma%unimportant (in algebra) lambda_system_Int: +lemma (in algebra) lambda_system_Int: fixes f:: "'a set \ ennreal" assumes xl: "x \ lambda_system \ M f" and yl: "y \ lambda_system \ M f" shows "x \ y \ lambda_system \ M f" @@ -122,7 +122,7 @@ qed qed -lemma%unimportant (in algebra) lambda_system_Un: +lemma (in algebra) lambda_system_Un: fixes f:: "'a set \ ennreal" assumes xl: "x \ lambda_system \ M f" and yl: "y \ lambda_system \ M f" shows "x \ y \ lambda_system \ M f" @@ -136,7 +136,7 @@ by (metis lambda_system_Compl lambda_system_Int xl yl) qed -lemma%unimportant (in algebra) lambda_system_algebra: +lemma (in algebra) lambda_system_algebra: "positive M f \ algebra \ (lambda_system \ M f)" apply (auto simp add: algebra_iff_Un) apply (metis lambda_system_sets set_mp sets_into_space) @@ -145,7 +145,7 @@ apply (metis lambda_system_Un) done -lemma%unimportant (in algebra) lambda_system_strong_additive: +lemma (in algebra) lambda_system_strong_additive: assumes z: "z \ M" and disj: "x \ y = {}" and xl: "x \ lambda_system \ M f" and yl: "y \ lambda_system \ M f" shows "f (z \ (x \ y)) = f (z \ x) + f (z \ y)" @@ -160,7 +160,7 @@ by (simp add: lambda_system_eq) qed -lemma%unimportant (in algebra) lambda_system_additive: "additive (lambda_system \ M f) f" +lemma (in algebra) lambda_system_additive: "additive (lambda_system \ M f) f" proof (auto simp add: additive_def) fix x and y assume disj: "x \ y = {}" @@ -171,13 +171,13 @@ by (simp add: Un) qed -lemma%unimportant lambda_system_increasing: "increasing M f \ increasing (lambda_system \ M f) f" +lemma lambda_system_increasing: "increasing M f \ increasing (lambda_system \ M f) f" by (simp add: increasing_def lambda_system_def) -lemma%unimportant lambda_system_positive: "positive M f \ positive (lambda_system \ M f) f" +lemma lambda_system_positive: "positive M f \ positive (lambda_system \ M f) f" by (simp add: positive_def lambda_system_def) -lemma%unimportant (in algebra) lambda_system_strong_sum: +lemma (in algebra) lambda_system_strong_sum: fixes A:: "nat \ 'a set" and f :: "'a set \ ennreal" assumes f: "positive M f" and a: "a \ M" and A: "range A \ lambda_system \ M f" @@ -199,12 +199,12 @@ by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4]) qed -lemma%important (in sigma_algebra) lambda_system_caratheodory: +proposition (in sigma_algebra) lambda_system_caratheodory: assumes oms: "outer_measure_space M f" and A: "range A \ lambda_system \ M f" and disj: "disjoint_family A" shows "(\i. A i) \ lambda_system \ M f \ (\i. f (A i)) = f (\i. A i)" -proof%unimportant - +proof - have pos: "positive M f" and inc: "increasing M f" and csa: "countably_subadditive M f" by (metis oms outer_measure_space_def)+ @@ -274,11 +274,11 @@ by (simp add: lambda_system_eq sums_iff U_eq U_in) qed -lemma%important (in sigma_algebra) caratheodory_lemma: +proposition (in sigma_algebra) caratheodory_lemma: assumes oms: "outer_measure_space M f" defines "L \ lambda_system \ M f" shows "measure_space \ L f" -proof%unimportant - +proof - have pos: "positive M f" by (metis oms outer_measure_space_def) have alg: "algebra \ L" @@ -301,7 +301,7 @@ "outer_measure M f X = (INF A\{A. range A \ M \ disjoint_family A \ X \ (\i. A i)}. \i. f (A i))" -lemma%unimportant (in ring_of_sets) outer_measure_agrees: +lemma (in ring_of_sets) outer_measure_agrees: assumes posf: "positive M f" and ca: "countably_additive M f" and s: "s \ M" shows "outer_measure M f s = f s" unfolding outer_measure_def @@ -326,19 +326,19 @@ (auto simp: disjoint_family_on_def) qed -lemma%unimportant outer_measure_empty: +lemma outer_measure_empty: "positive M f \ {} \ M \ outer_measure M f {} = 0" unfolding outer_measure_def by (intro antisym INF_lower2[of "\_. {}"]) (auto simp: disjoint_family_on_def positive_def) -lemma%unimportant (in ring_of_sets) positive_outer_measure: +lemma (in ring_of_sets) positive_outer_measure: assumes "positive M f" shows "positive (Pow \) (outer_measure M f)" unfolding positive_def by (auto simp: assms outer_measure_empty) -lemma%unimportant (in ring_of_sets) increasing_outer_measure: "increasing (Pow \) (outer_measure M f)" +lemma (in ring_of_sets) increasing_outer_measure: "increasing (Pow \) (outer_measure M f)" by (force simp: increasing_def outer_measure_def intro!: INF_greatest intro: INF_lower) -lemma%unimportant (in ring_of_sets) outer_measure_le: +lemma (in ring_of_sets) outer_measure_le: assumes pos: "positive M f" and inc: "increasing M f" and A: "range A \ M" and X: "X \ (\i. A i)" shows "outer_measure M f X \ (\i. f (A i))" unfolding outer_measure_def @@ -351,11 +351,11 @@ by (blast intro!: suminf_le) qed (auto simp: X UN_disjointed_eq disjoint_family_disjointed) -lemma%unimportant (in ring_of_sets) outer_measure_close: +lemma (in ring_of_sets) outer_measure_close: "outer_measure M f X < e \ \A. range A \ M \ disjoint_family A \ X \ (\i. A i) \ (\i. f (A i)) < e" unfolding outer_measure_def INF_less_iff by auto -lemma%unimportant (in ring_of_sets) countably_subadditive_outer_measure: +lemma (in ring_of_sets) countably_subadditive_outer_measure: assumes posf: "positive M f" and inc: "increasing M f" shows "countably_subadditive (Pow \) (outer_measure M f)" proof (simp add: countably_subadditive_def, safe) @@ -398,12 +398,12 @@ qed qed -lemma%unimportant (in ring_of_sets) outer_measure_space_outer_measure: +lemma (in ring_of_sets) outer_measure_space_outer_measure: "positive M f \ increasing M f \ outer_measure_space (Pow \) (outer_measure M f)" by (simp add: outer_measure_space_def positive_outer_measure increasing_outer_measure countably_subadditive_outer_measure) -lemma%unimportant (in ring_of_sets) algebra_subset_lambda_system: +lemma (in ring_of_sets) algebra_subset_lambda_system: assumes posf: "positive M f" and inc: "increasing M f" and add: "additive M f" shows "M \ lambda_system \ (Pow \) (outer_measure M f)" @@ -457,15 +457,15 @@ by (rule order_antisym) qed -lemma%unimportant measure_down: "measure_space \ N \ \ sigma_algebra \ M \ M \ N \ measure_space \ M \" +lemma measure_down: "measure_space \ N \ \ sigma_algebra \ M \ M \ N \ measure_space \ M \" by (auto simp add: measure_space_def positive_def countably_additive_def subset_eq) subsection%important \Caratheodory's theorem\ -theorem%important (in ring_of_sets) caratheodory': +theorem (in ring_of_sets) caratheodory': assumes posf: "positive M f" and ca: "countably_additive M f" shows "\\ :: 'a set \ ennreal. (\s \ M. \ s = f s) \ measure_space \ (sigma_sets \ M) \" -proof%unimportant - +proof - have inc: "increasing M f" by (metis additive_increasing ca countably_additive_additive posf) let ?O = "outer_measure M f" @@ -489,11 +489,11 @@ by (intro exI[of _ ?O]) auto qed -lemma%important (in ring_of_sets) caratheodory_empty_continuous: +lemma (in ring_of_sets) caratheodory_empty_continuous: assumes f: "positive M f" "additive M f" and fin: "\A. A \ M \ f A \ \" assumes cont: "\A. range A \ M \ decseq A \ (\i. A i) = {} \ (\i. f (A i)) \ 0" shows "\\ :: 'a set \ ennreal. (\s \ M. \ s = f s) \ measure_space \ (sigma_sets \ M) \" -proof%unimportant (intro caratheodory' empty_continuous_imp_countably_additive f) +proof (intro caratheodory' empty_continuous_imp_countably_additive f) show "\A\M. f A \ \" using fin by auto qed (rule cont) @@ -504,22 +504,22 @@ (f {} = 0) \ (\a\M. 0 \ f a) \ (\C\M. disjoint C \ finite C \ \C \ M \ f (\C) = (\c\C. f c))" -lemma%unimportant volumeI: +lemma volumeI: assumes "f {} = 0" assumes "\a. a \ M \ 0 \ f a" assumes "\C. C \ M \ disjoint C \ finite C \ \C \ M \ f (\C) = (\c\C. f c)" shows "volume M f" using assms by (auto simp: volume_def) -lemma%unimportant volume_positive: +lemma volume_positive: "volume M f \ a \ M \ 0 \ f a" by (auto simp: volume_def) -lemma%unimportant volume_empty: +lemma volume_empty: "volume M f \ f {} = 0" by (auto simp: volume_def) -lemma%unimportant volume_finite_additive: +proposition volume_finite_additive: assumes "volume M f" assumes A: "\i. i \ I \ A i \ M" "disjoint_family_on A I" "finite I" "\(A ` I) \ M" shows "f (\(A ` I)) = (\i\I. f (A i))" @@ -540,7 +540,7 @@ by simp qed -lemma%unimportant (in ring_of_sets) volume_additiveI: +lemma (in ring_of_sets) volume_additiveI: assumes pos: "\a. a \ M \ 0 \ \ a" assumes [simp]: "\ {} = 0" assumes add: "\a b. a \ M \ b \ M \ a \ b = {} \ \ (a \ b) = \ a + \ b" @@ -557,10 +557,10 @@ qed simp qed fact+ -lemma%important (in semiring_of_sets) extend_volume: +proposition (in semiring_of_sets) extend_volume: assumes "volume M \" shows "\\'. volume generated_ring \' \ (\a\M. \' a = \ a)" -proof%unimportant - +proof - let ?R = generated_ring have "\a\?R. \m. \C\M. a = \C \ finite C \ disjoint C \ m = (\c\C. \ c)" by (auto simp: generated_ring_def) @@ -637,10 +637,10 @@ subsubsection%important \Caratheodory on semirings\ -theorem%important (in semiring_of_sets) caratheodory: +theorem (in semiring_of_sets) caratheodory: assumes pos: "positive M \" and ca: "countably_additive M \" shows "\\' :: 'a set \ ennreal. (\s \ M. \' s = \ s) \ measure_space \ (sigma_sets \ M) \'" -proof%unimportant - +proof - have "volume M \" proof (rule volumeI) { fix a assume "a \ M" then show "0 \ \ a" @@ -816,7 +816,7 @@ by (intro exI[of _ \']) (auto intro: generated_ringI_Basic) qed -lemma%important extend_measure_caratheodory: +lemma extend_measure_caratheodory: fixes G :: "'i \ 'a set" assumes M: "M = extend_measure \ I G \" assumes "i \ I" @@ -828,7 +828,7 @@ (\i. G (A i)) = G j \ (\n. \ (A n)) = \ j" shows "emeasure M (G i) = \ i" -proof%unimportant - +proof - interpret semiring_of_sets \ "G ` I" by fact have "\g\G`I. \i\I. g = G i" @@ -861,7 +861,7 @@ qed fact qed -lemma%important extend_measure_caratheodory_pair: +proposition extend_measure_caratheodory_pair: fixes G :: "'i \ 'j \ 'a set" assumes M: "M = extend_measure \ {(a, b). P a b} (\(a, b). G a b) (\(a, b). \ a b)" assumes "P i j" @@ -873,7 +873,7 @@ (\n. P (A n) (B n)) \ P j k \ disjoint_family (\n. G (A n) (B n)) \ (\i. G (A i) (B i)) = G j k \ (\n. \ (A n) (B n)) = \ j k" shows "emeasure M (G i j) = \ i j" -proof%unimportant - +proof - have "emeasure M ((\(a, b). G a b) (i, j)) = (\(a, b). \ a b) (i, j)" proof (rule extend_measure_caratheodory[OF M]) show "semiring_of_sets \ ((\(a, b). G a b) ` {(a, b). P a b})"