# HG changeset patch # User wenzelm # Date 1568903912 -7200 # Node ID dea35c31a0b852f73e157f0f428c45325195b1dc # Parent 91587befabfd945eb3554d26179e9718564cbf8e# Parent 561b11865cb586ba7c48b9d933b9e0eb3837a037 merged diff -r 561b11865cb5 -r dea35c31a0b8 src/HOL/Analysis/Change_Of_Vars.thy --- a/src/HOL/Analysis/Change_Of_Vars.thy Thu Sep 19 16:38:05 2019 +0200 +++ b/src/HOL/Analysis/Change_Of_Vars.thy Thu Sep 19 16:38:32 2019 +0200 @@ -9,41 +9,6 @@ begin -subsection \Orthogonal Transformation of Balls\ - -lemma image_orthogonal_transformation_ball: - fixes f :: "'a::euclidean_space \ 'a" - assumes "orthogonal_transformation f" - shows "f ` ball x r = ball (f x) r" -proof (intro equalityI subsetI) - fix y assume "y \ f ` ball x r" - with assms show "y \ ball (f x) r" - by (auto simp: orthogonal_transformation_isometry) -next - fix y assume y: "y \ ball (f x) r" - then obtain z where z: "y = f z" - using assms orthogonal_transformation_surj by blast - with y assms show "y \ f ` ball x r" - by (auto simp: orthogonal_transformation_isometry) -qed - -lemma image_orthogonal_transformation_cball: - fixes f :: "'a::euclidean_space \ 'a" - assumes "orthogonal_transformation f" - shows "f ` cball x r = cball (f x) r" -proof (intro equalityI subsetI) - fix y assume "y \ f ` cball x r" - with assms show "y \ cball (f x) r" - by (auto simp: orthogonal_transformation_isometry) -next - fix y assume y: "y \ cball (f x) r" - then obtain z where z: "y = f z" - using assms orthogonal_transformation_surj by blast - with y assms show "y \ f ` cball x r" - by (auto simp: orthogonal_transformation_isometry) -qed - - subsection \Measurable Shear and Stretch\ proposition diff -r 561b11865cb5 -r dea35c31a0b8 src/HOL/Analysis/Complex_Transcendental.thy --- a/src/HOL/Analysis/Complex_Transcendental.thy Thu Sep 19 16:38:05 2019 +0200 +++ b/src/HOL/Analysis/Complex_Transcendental.thy Thu Sep 19 16:38:32 2019 +0200 @@ -2568,12 +2568,23 @@ apply (simp add: lim_sequentially dist_norm Ln_Reals_eq norm_powr_real_powr norm_divide) done -lemma lim_ln_over_n: "((\n. ln(real_of_nat n) / of_nat n) \ 0) sequentially" +lemma lim_ln_over_n [tendsto_intros]: "((\n. ln(real_of_nat n) / of_nat n) \ 0) sequentially" using lim_ln_over_power [of 1, THEN filterlim_sequentially_Suc [THEN iffD2]] apply (subst filterlim_sequentially_Suc [symmetric]) apply (simp add: lim_sequentially dist_norm) done +lemma lim_log_over_n [tendsto_intros]: + "(\n. log k n/n) \ 0" +proof - + have *: "log k n/n = (1/ln k) * (ln n / n)" for n + unfolding log_def by auto + have "(\n. (1/ln k) * (ln n / n)) \ (1/ln k) * 0" + by (intro tendsto_intros) + then show ?thesis + unfolding * by auto +qed + lemma lim_1_over_complex_power: assumes "0 < Re s" shows "(\n. 1 / of_nat n powr s) \ 0" diff -r 561b11865cb5 -r dea35c31a0b8 src/HOL/Analysis/Derivative.thy --- a/src/HOL/Analysis/Derivative.thy Thu Sep 19 16:38:05 2019 +0200 +++ b/src/HOL/Analysis/Derivative.thy Thu Sep 19 16:38:32 2019 +0200 @@ -233,6 +233,12 @@ unfolding frechet_derivative_works has_derivative_def by (auto intro: bounded_linear.linear) +lemma frechet_derivative_const [simp]: "frechet_derivative (\x. c) (at a) = (\x. 0)" + using differentiable_const frechet_derivative_works has_derivative_const has_derivative_unique by blast + +lemma frechet_derivative_id [simp]: "frechet_derivative id (at a) = id" + using differentiable_def frechet_derivative_works has_derivative_id has_derivative_unique by blast + subsection \Differentiability implies continuity\ @@ -485,6 +491,11 @@ "(f has_derivative f') (at x) \ f' = frechet_derivative f (at x)" using differentiable_def frechet_derivative_works has_derivative_unique by blast +lemma frechet_derivative_compose: + "frechet_derivative (f o g) (at x) = frechet_derivative (f) (at (g x)) o frechet_derivative g (at x)" + if "g differentiable at x" "f differentiable at (g x)" + by (metis diff_chain_at frechet_derivative_at frechet_derivative_works that) + lemma frechet_derivative_within_cbox: fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" assumes "\i. i\Basis \ a\i < b\i" @@ -494,6 +505,11 @@ using assms by (metis Derivative.differentiableI frechet_derivative_unique_within_closed_interval frechet_derivative_works) +lemma frechet_derivative_transform_within_open: + "frechet_derivative f (at x) = frechet_derivative g (at x)" + if "f differentiable at x" "open X" "x \ X" "\x. x \ X \ f x = g x" + by (meson frechet_derivative_at frechet_derivative_works has_derivative_transform_within_open that) + subsection \Derivatives of local minima and maxima are zero\ diff -r 561b11865cb5 -r dea35c31a0b8 src/HOL/Analysis/Elementary_Metric_Spaces.thy --- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Thu Sep 19 16:38:05 2019 +0200 +++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Thu Sep 19 16:38:32 2019 +0200 @@ -2000,6 +2000,11 @@ lemma infdist_zero[simp]: "a \ A \ infdist a A = 0" by (auto intro!: antisym infdist_nonneg infdist_le2) +lemma infdist_Un_min: + assumes "A \ {}" "B \ {}" + shows "infdist x (A \ B) = min (infdist x A) (infdist x B)" +using assms by (simp add: infdist_def cINF_union inf_real_def) + lemma infdist_triangle: "infdist x A \ infdist y A + dist x y" proof (cases "A = {}") case True @@ -2041,6 +2046,9 @@ finally show ?thesis by simp qed +lemma infdist_triangle_abs: "\infdist x A - infdist y A\ \ dist x y" + by (metis (full_types) abs_diff_le_iff diff_le_eq dist_commute infdist_triangle) + lemma in_closure_iff_infdist_zero: assumes "A \ {}" shows "x \ closure A \ infdist x A = 0" @@ -2179,6 +2187,11 @@ shows "continuous F (\x. infdist (f x) A)" using assms unfolding continuous_def by (rule tendsto_infdist) +lemma continuous_on_infdist [continuous_intros]: + assumes "continuous_on S f" + shows "continuous_on S (\x. infdist (f x) A)" +using assms unfolding continuous_on by (auto intro: tendsto_infdist) + lemma compact_infdist_le: fixes A::"'a::heine_borel set" assumes "A \ {}" @@ -3231,8 +3244,14 @@ by (auto simp: setdist_def infdist_def) qed -lemma continuous_on_infdist [continuous_intros]: "continuous_on B (\y. infdist y A)" - by (simp add: continuous_on_setdist infdist_eq_setdist) +lemma infdist_mono: + assumes "A \ B" "A \ {}" + shows "infdist x B \ infdist x A" + by (simp add: assms infdist_eq_setdist setdist_subset_right) + +lemma infdist_singleton [simp]: + "infdist x {y} = dist x y" + by (simp add: infdist_eq_setdist) proposition setdist_attains_inf: assumes "compact B" "B \ {}" @@ -3244,7 +3263,7 @@ next case False obtain y where "y \ B" and min: "\y'. y' \ B \ infdist y A \ infdist y' A" - using continuous_attains_inf [OF assms continuous_on_infdist] by blast + by (metis continuous_attains_inf [OF assms continuous_on_infdist] continuous_on_id) show thesis proof have "setdist A B = (INF y\B. infdist y A)" @@ -3266,4 +3285,4 @@ qed (fact \y \ B\) qed -end \ No newline at end of file +end diff -r 561b11865cb5 -r dea35c31a0b8 src/HOL/Analysis/Elementary_Normed_Spaces.thy --- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy Thu Sep 19 16:38:05 2019 +0200 +++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy Thu Sep 19 16:38:32 2019 +0200 @@ -9,17 +9,13 @@ theory Elementary_Normed_Spaces imports "HOL-Library.FuncSet" - Elementary_Metric_Spaces Linear_Algebra + Elementary_Metric_Spaces Cartesian_Space Connected begin +subsection \Orthogonal Transformation of Balls\ subsection\<^marker>\tag unimportant\ \Various Lemmas Combining Imports\ -lemma countable_PiE: - "finite I \ (\i. i \ I \ countable (F i)) \ countable (Pi\<^sub>E I F)" - by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq) - - lemma open_sums: fixes T :: "('b::real_normed_vector) set" assumes "open S \ open T" @@ -53,6 +49,38 @@ qed qed +lemma image_orthogonal_transformation_ball: + fixes f :: "'a::euclidean_space \ 'a" + assumes "orthogonal_transformation f" + shows "f ` ball x r = ball (f x) r" +proof (intro equalityI subsetI) + fix y assume "y \ f ` ball x r" + with assms show "y \ ball (f x) r" + by (auto simp: orthogonal_transformation_isometry) +next + fix y assume y: "y \ ball (f x) r" + then obtain z where z: "y = f z" + using assms orthogonal_transformation_surj by blast + with y assms show "y \ f ` ball x r" + by (auto simp: orthogonal_transformation_isometry) +qed + +lemma image_orthogonal_transformation_cball: + fixes f :: "'a::euclidean_space \ 'a" + assumes "orthogonal_transformation f" + shows "f ` cball x r = cball (f x) r" +proof (intro equalityI subsetI) + fix y assume "y \ f ` cball x r" + with assms show "y \ cball (f x) r" + by (auto simp: orthogonal_transformation_isometry) +next + fix y assume y: "y \ cball (f x) r" + then obtain z where z: "y = f z" + using assms orthogonal_transformation_surj by blast + with y assms show "y \ f ` cball x r" + by (auto simp: orthogonal_transformation_isometry) +qed + subsection \Support\ diff -r 561b11865cb5 -r dea35c31a0b8 src/HOL/Analysis/Elementary_Topology.thy --- a/src/HOL/Analysis/Elementary_Topology.thy Thu Sep 19 16:38:05 2019 +0200 +++ b/src/HOL/Analysis/Elementary_Topology.thy Thu Sep 19 16:38:32 2019 +0200 @@ -2479,6 +2479,14 @@ unfolding homeomorphism_def by (intro conjI ballI continuous_on_compose) (auto simp: image_iff) +lemma homeomorphism_cong: + "homeomorphism X' Y' f' g'" + if "homeomorphism X Y f g" "X' = X" "Y' = Y" "\x. x \ X \ f' x = f x" "\y. y \ Y \ g' y = g y" + using that by (auto simp add: homeomorphism_def) + +lemma homeomorphism_empty [simp]: + "homeomorphism {} {} f g" + unfolding homeomorphism_def by auto lemma homeomorphism_symD: "homeomorphism S t f g \ homeomorphism t S g f" by (simp add: homeomorphism_def) diff -r 561b11865cb5 -r dea35c31a0b8 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Sep 19 16:38:05 2019 +0200 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Sep 19 16:38:32 2019 +0200 @@ -1108,6 +1108,48 @@ shows "\f absolutely_integrable_on S; {a..b} \ S\ \ f absolutely_integrable_on {a..b}" using absolutely_integrable_on_subcbox by fastforce +lemma integrable_subinterval: + fixes f :: "real \ 'a::euclidean_space" + assumes "integrable (lebesgue_on {a..b}) f" + and "{c..d} \ {a..b}" + shows "integrable (lebesgue_on {c..d}) f" +proof (rule absolutely_integrable_imp_integrable) + show "f absolutely_integrable_on {c..d}" + proof - + have "f integrable_on {c..d}" + using assms integrable_on_lebesgue_on integrable_on_subinterval by fastforce + moreover have "(\x. norm (f x)) integrable_on {c..d}" + proof (rule integrable_on_subinterval) + show "(\x. norm (f x)) integrable_on {a..b}" + by (simp add: assms integrable_on_lebesgue_on) + qed (use assms in auto) + ultimately show ?thesis + by (auto simp: absolutely_integrable_on_def) + qed +qed auto + +lemma indefinite_integral_continuous_real: + fixes f :: "real \ 'a::euclidean_space" + assumes "integrable (lebesgue_on {a..b}) f" + shows "continuous_on {a..b} (\x. integral\<^sup>L (lebesgue_on {a..x}) f)" +proof - + have "f integrable_on {a..b}" + by (simp add: assms integrable_on_lebesgue_on) + then have "continuous_on {a..b} (\x. integral {a..x} f)" + using indefinite_integral_continuous_1 by blast + moreover have "integral\<^sup>L (lebesgue_on {a..x}) f = integral {a..x} f" if "a \ x" "x \ b" for x + proof - + have "{a..x} \ {a..b}" + using that by auto + then have "integrable (lebesgue_on {a..x}) f" + using integrable_subinterval assms by blast + then show "integral\<^sup>L (lebesgue_on {a..x}) f = integral {a..x} f" + by (simp add: lebesgue_integral_eq_integral) + qed + ultimately show ?thesis + by (metis (no_types, lifting) atLeastAtMost_iff continuous_on_cong) +qed + lemma lmeasurable_iff_integrable_on: "S \ lmeasurable \ (\x. 1::real) integrable_on S" by (subst absolutely_integrable_on_iff_nonneg[symmetric]) (simp_all add: lmeasurable_iff_integrable set_integrable_def) @@ -3132,21 +3174,8 @@ qed qed - subsection\Lemmas about absolute integrability\ -text\FIXME Redundant!\ -lemma absolutely_integrable_add[intro]: - fixes f g :: "'n::euclidean_space \ 'm::euclidean_space" - shows "f absolutely_integrable_on s \ g absolutely_integrable_on s \ (\x. f x + g x) absolutely_integrable_on s" - by (rule set_integral_add) - -text\FIXME Redundant!\ -lemma absolutely_integrable_diff[intro]: - fixes f g :: "'n::euclidean_space \ 'm::euclidean_space" - shows "f absolutely_integrable_on s \ g absolutely_integrable_on s \ (\x. f x - g x) absolutely_integrable_on s" - by (rule set_integral_diff) - lemma absolutely_integrable_linear: fixes f :: "'m::euclidean_space \ 'n::euclidean_space" and h :: "'n::euclidean_space \ 'p::euclidean_space" @@ -3375,8 +3404,8 @@ qed moreover have "(\x. (1 / 2) *\<^sub>R (f x + g x + (\i\Basis. \f x \ i - g x \ i\ *\<^sub>R i))) absolutely_integrable_on S" - apply (intro absolutely_integrable_add absolutely_integrable_scaleR_left assms) - using absolutely_integrable_abs [OF absolutely_integrable_diff [OF assms]] + apply (intro set_integral_add absolutely_integrable_scaleR_left assms) + using absolutely_integrable_abs [OF set_integral_diff(1) [OF assms]] apply (simp add: algebra_simps) done ultimately show ?thesis by metis @@ -3410,8 +3439,8 @@ qed moreover have "(\x. (1 / 2) *\<^sub>R (f x + g x - (\i\Basis. \f x \ i - g x \ i\ *\<^sub>R i))) absolutely_integrable_on S" - apply (intro absolutely_integrable_add absolutely_integrable_diff absolutely_integrable_scaleR_left assms) - using absolutely_integrable_abs [OF absolutely_integrable_diff [OF assms]] + apply (intro set_integral_add set_integral_diff absolutely_integrable_scaleR_left assms) + using absolutely_integrable_abs [OF set_integral_diff(1) [OF assms]] apply (simp add: algebra_simps) done ultimately show ?thesis by metis @@ -3450,7 +3479,7 @@ shows "f absolutely_integrable_on A" proof - have "(\x. g x - (g x - f x)) absolutely_integrable_on A" - apply (rule absolutely_integrable_diff [OF g nonnegative_absolutely_integrable]) + apply (rule set_integral_diff [OF g nonnegative_absolutely_integrable]) using Henstock_Kurzweil_Integration.integrable_diff absolutely_integrable_on_def f g apply blast by (simp add: comp inner_diff_left) then show ?thesis @@ -3464,7 +3493,7 @@ shows "g absolutely_integrable_on A" proof - have "(\x. f x + (g x - f x)) absolutely_integrable_on A" - apply (rule absolutely_integrable_add [OF f nonnegative_absolutely_integrable]) + apply (rule set_integral_add [OF f nonnegative_absolutely_integrable]) using Henstock_Kurzweil_Integration.integrable_diff absolutely_integrable_on_def f g apply blast by (simp add: comp inner_diff_left) then show ?thesis @@ -4495,6 +4524,22 @@ by (auto simp: has_bochner_integral_restrict_space) qed +lemma has_bochner_integral_reflect_real[simp]: + fixes f :: "real \ 'a::euclidean_space" + shows "has_bochner_integral (lebesgue_on {-b..-a}) (\x. f(-x)) i \ has_bochner_integral (lebesgue_on {a..b}) f i" + by (auto simp: dest: has_bochner_integral_reflect_real_lemma) + +lemma integrable_reflect_real[simp]: + fixes f :: "real \ 'a::euclidean_space" + shows "integrable (lebesgue_on {-b..-a}) (\x. f(-x)) \ integrable (lebesgue_on {a..b}) f" + by (metis has_bochner_integral_iff has_bochner_integral_reflect_real) + +lemma integral_reflect_real[simp]: + fixes f :: "real \ 'a::euclidean_space" + shows "integral\<^sup>L (lebesgue_on {-b .. -a}) (\x. f(-x)) = integral\<^sup>L (lebesgue_on {a..b::real}) f" + using has_bochner_integral_reflect_real [of b a f] + by (metis has_bochner_integral_iff not_integrable_integral_eq) + subsection\More results on integrability\ lemma integrable_on_all_intervals_UNIV: @@ -4790,15 +4835,24 @@ "(\x. if x \ T then f x else 0) absolutely_integrable_on UNIV" using S T absolutely_integrable_restrict_UNIV by blast+ then have "(\x. (if x \ S then f x else 0) + (if x \ T then f x else 0)) absolutely_integrable_on UNIV" - by (rule absolutely_integrable_add) + by (rule set_integral_add) then have "(\x. ((if x \ S then f x else 0) + (if x \ T then f x else 0)) - (if x \ ?ST then f x else 0)) absolutely_integrable_on UNIV" - using Int by (rule absolutely_integrable_diff) + using Int by (rule set_integral_diff) then have "(\x. if x \ S \ T then f x else 0) absolutely_integrable_on UNIV" by (rule absolutely_integrable_spike) (auto intro: empty_imp_negligible) then show ?thesis unfolding absolutely_integrable_restrict_UNIV . qed +lemma absolutely_integrable_on_combine: + fixes f :: "real \ 'a::euclidean_space" + assumes "f absolutely_integrable_on {a..c}" + and "f absolutely_integrable_on {c..b}" + and "a \ c" + and "c \ b" + shows "f absolutely_integrable_on {a..b}" + by (metis absolutely_integrable_Un assms ivl_disj_un_two_touch(4)) + lemma uniform_limit_set_lebesgue_integral_at_top: fixes f :: "'a \ real \ 'b::{banach, second_countable_topology}" and g :: "real \ real" diff -r 561b11865cb5 -r dea35c31a0b8 src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy --- a/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Thu Sep 19 16:38:05 2019 +0200 +++ b/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Thu Sep 19 16:38:32 2019 +0200 @@ -860,32 +860,6 @@ qed (auto simp: conF) qed - -lemma measurable_on_preimage_lemma0: - fixes f :: "'a::euclidean_space \ real" - assumes "m \ \" and f: "m / 2^n \ (f x)" "(f x) < (m+1) / 2^n" and m: "\m\ \ 2^(2 * n)" - shows "(\k\{k \ \. \k\ \ 2^(2 * n)}. - (k / 2^n) * indicator {y. k / 2^n \ f y \ f y < (k+1) / 2^n} x) - = (m / 2^n)" (is "?lhs = ?rhs") -proof - - have "?lhs = (\k\{m}. (k / 2^n) * indicator {y. k / 2^n \ f y \ f y < (k+1) / 2^n} x)" - proof (intro sum.mono_neutral_right ballI) - show "finite {k::real. k \ \ \ \k\ \ 2^(2 * n)}" - using finite_abs_int_segment by blast - show "(i / 2^n) * indicat_real {y. i / 2^n \ f y \ f y < (i+1) / 2^n} x = 0" - if "i \ {N \ \. \N\ \ 2^(2 * n)} - {m}" for i - using f m \m \ \\ that Ints_eq_abs_less1 [of i m] - by (auto simp: indicator_def divide_simps) - qed (auto simp: assms) - also have "\ = ?rhs" - using assms by (auto simp: indicator_def) - finally show ?thesis . -qed - -(*see HOL Light's lebesgue_measurable BUT OUR lmeasurable IS NOT THE SAME. It's more like "sets lebesgue" - `lebesgue_measurable s <=> (indicator s) measurable_on (:real^N)`;; -*) - proposition indicator_measurable_on: assumes "S \ sets lebesgue" shows "indicat_real S measurable_on UNIV" @@ -1615,6 +1589,7 @@ qed subsection \Measurability on generalisations of the binary product\ + lemma measurable_on_bilinear: fixes h :: "'a::euclidean_space \ 'b::euclidean_space \ 'c::euclidean_space" assumes h: "bilinear h" and f: "f measurable_on S" and g: "g measurable_on S" @@ -1663,4 +1638,72 @@ shows "(\x. f x * g x) absolutely_integrable_on S" using absolutely_integrable_bounded_measurable_product bilinear_times assms by blast + +lemma borel_measurable_AE: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + assumes "f \ borel_measurable lebesgue" and ae: "AE x in lebesgue. f x = g x" + shows "g \ borel_measurable lebesgue" +proof - + obtain N where N: "N \ null_sets lebesgue" "\x. x \ N \ f x = g x" + using ae unfolding completion.AE_iff_null_sets by auto + have "f measurable_on UNIV" + by (simp add: assms lebesgue_measurable_imp_measurable_on) + then have "g measurable_on UNIV" + by (metis Diff_iff N measurable_on_spike negligible_iff_null_sets) + then show ?thesis + using measurable_on_imp_borel_measurable_lebesgue_UNIV by blast +qed + +lemma has_bochner_integral_combine: + fixes f :: "real \ 'a::euclidean_space" + assumes "a \ c" "c \ b" + and ac: "has_bochner_integral (lebesgue_on {a..c}) f i" + and cb: "has_bochner_integral (lebesgue_on {c..b}) f j" + shows "has_bochner_integral (lebesgue_on {a..b}) f(i + j)" +proof - + have i: "has_bochner_integral lebesgue (\x. indicator {a..c} x *\<^sub>R f x) i" + and j: "has_bochner_integral lebesgue (\x. indicator {c..b} x *\<^sub>R f x) j" + using assms by (auto simp: has_bochner_integral_restrict_space) + have AE: "AE x in lebesgue. indicat_real {a..c} x *\<^sub>R f x + indicat_real {c..b} x *\<^sub>R f x = indicat_real {a..b} x *\<^sub>R f x" + proof (rule AE_I') + have eq: "indicat_real {a..c} x *\<^sub>R f x + indicat_real {c..b} x *\<^sub>R f x = indicat_real {a..b} x *\<^sub>R f x" if "x \ c" for x + using assms that by (auto simp: indicator_def) + then show "{x \ space lebesgue. indicat_real {a..c} x *\<^sub>R f x + indicat_real {c..b} x *\<^sub>R f x \ indicat_real {a..b} x *\<^sub>R f x} \ {c}" + by auto + qed auto + have "has_bochner_integral lebesgue (\x. indicator {a..b} x *\<^sub>R f x) (i + j)" + proof (rule has_bochner_integralI_AE [OF has_bochner_integral_add [OF i j] _ AE]) + have eq: "indicat_real {a..c} x *\<^sub>R f x + indicat_real {c..b} x *\<^sub>R f x = indicat_real {a..b} x *\<^sub>R f x" if "x \ c" for x + using assms that by (auto simp: indicator_def) + show "(\x. indicat_real {a..b} x *\<^sub>R f x) \ borel_measurable lebesgue" + proof (rule borel_measurable_AE [OF borel_measurable_add AE]) + show "(\x. indicator {a..c} x *\<^sub>R f x) \ borel_measurable lebesgue" + "(\x. indicator {c..b} x *\<^sub>R f x) \ borel_measurable lebesgue" + using i j by auto + qed + qed + then show ?thesis + by (simp add: has_bochner_integral_restrict_space) +qed + +lemma integrable_combine: + fixes f :: "real \ 'a::euclidean_space" + assumes "integrable (lebesgue_on {a..c}) f" "integrable (lebesgue_on {c..b}) f" + and "a \ c" "c \ b" + shows "integrable (lebesgue_on {a..b}) f" + using assms has_bochner_integral_combine has_bochner_integral_iff by blast + +lemma integral_combine: + fixes f :: "real \ 'a::euclidean_space" + assumes f: "integrable (lebesgue_on {a..b}) f" and "a \ c" "c \ b" + shows "integral\<^sup>L (lebesgue_on {a..b}) f = integral\<^sup>L (lebesgue_on {a..c}) f + integral\<^sup>L (lebesgue_on {c..b}) f" +proof - + have i: "has_bochner_integral (lebesgue_on {a..c}) f(integral\<^sup>L (lebesgue_on {a..c}) f)" + using integrable_subinterval \c \ b\ f has_bochner_integral_iff by fastforce + have j: "has_bochner_integral (lebesgue_on {c..b}) f(integral\<^sup>L (lebesgue_on {c..b}) f)" + using integrable_subinterval \a \ c\ f has_bochner_integral_iff by fastforce + show ?thesis + by (meson \a \ c\ \c \ b\ has_bochner_integral_combine has_bochner_integral_iff i j) +qed + end diff -r 561b11865cb5 -r dea35c31a0b8 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Sep 19 16:38:05 2019 +0200 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Sep 19 16:38:32 2019 +0200 @@ -6935,6 +6935,19 @@ by (intro has_integral_substitution_strong[of "{}" a b g c d] assms) (auto intro: DERIV_continuous_on assms) +lemma integral_shift: + fixes f :: "real \ 'a::euclidean_space" + assumes cont: "continuous_on {a + c..b + c} f" + shows "integral {a..b} (f \ (\x. x + c)) = integral {a + c..b + c} f" +proof (cases "a \ b") + case True + have "((\x. 1 *\<^sub>R f (x + c)) has_integral integral {a+c..b+c} f) {a..b}" + using True cont + by (intro has_integral_substitution[where c = "a + c" and d = "b + c"]) + (auto intro!: derivative_eq_intros) + thus ?thesis by (simp add: has_integral_iff o_def) +qed auto + subsection \Compute a double integral using iterated integrals and switching the order of integration\ diff -r 561b11865cb5 -r dea35c31a0b8 src/HOL/Analysis/Improper_Integral.thy --- a/src/HOL/Analysis/Improper_Integral.thy Thu Sep 19 16:38:05 2019 +0200 +++ b/src/HOL/Analysis/Improper_Integral.thy Thu Sep 19 16:38:32 2019 +0200 @@ -1757,13 +1757,11 @@ have I_int [simp]: "?I \ box a b = ?I" using 1 by (simp add: Int_absorb2) have int_fI: "f integrable_on ?I" - apply (rule integrable_subinterval [OF int_f order_refl]) - using "*" box_subset_cbox by blast + by (metis I_int inf_le2 int_f) then have "(\x. f x \ j) integrable_on ?I" by (simp add: integrable_component) moreover have "g integrable_on ?I" - apply (rule integrable_subinterval [OF int_gab]) - using "*" box_subset_cbox by blast + by (metis I_int inf.orderI int_gab integrable_on_open_interval integrable_on_subcbox) moreover have "\integral ?I (\x. f x \ j)\ \ norm (integral ?I f)" by (simp add: Basis_le_norm int_fI \j \ Basis\) @@ -1837,13 +1835,11 @@ have I_int [simp]: "?I \ box a b = ?I" using 1 by (simp add: Int_absorb2) have int_fI: "f integrable_on ?I" - apply (rule integrable_subinterval [OF int_f order_refl]) - using "*" box_subset_cbox by blast + by (simp add: inf.orderI int_f) then have "(\x. f x \ j) integrable_on ?I" by (simp add: integrable_component) moreover have "g integrable_on ?I" - apply (rule integrable_subinterval [OF int_gab]) - using "*" box_subset_cbox by blast + by (metis I_int inf.orderI int_gab integrable_on_open_interval integrable_on_subcbox) moreover have "\integral ?I (\x. f x \ j)\ \ norm (integral ?I f)" by (simp add: Basis_le_norm int_fI \j \ Basis\) @@ -2268,6 +2264,5 @@ using second_mean_value_theorem_full [where g=g, OF assms] by (metis (full_types) integral_unique) - end diff -r 561b11865cb5 -r dea35c31a0b8 src/HOL/Analysis/Lebesgue_Measure.thy --- a/src/HOL/Analysis/Lebesgue_Measure.thy Thu Sep 19 16:38:05 2019 +0200 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy Thu Sep 19 16:38:32 2019 +0200 @@ -1219,8 +1219,10 @@ finally show ?thesis . qed -lemma lborel_distr_plus: "distr lborel borel ((+) c) = (lborel :: real measure)" - by (subst lborel_real_affine[of 1 c]) (auto simp: density_1 one_ennreal_def[symmetric]) +lemma lborel_distr_plus: + fixes c :: "'a::euclidean_space" + shows "distr lborel borel ((+) c) = lborel" +by (subst lborel_affine[of 1 c], auto simp: density_1) interpretation lborel: sigma_finite_measure lborel by (rule sigma_finite_lborel) diff -r 561b11865cb5 -r dea35c31a0b8 src/HOL/Analysis/Measure_Space.thy --- a/src/HOL/Analysis/Measure_Space.thy Thu Sep 19 16:38:05 2019 +0200 +++ b/src/HOL/Analysis/Measure_Space.thy Thu Sep 19 16:38:32 2019 +0200 @@ -472,10 +472,23 @@ "a \ sets M \ b \ sets M \ a \ b = {} \ emeasure M a + emeasure M b = emeasure M (a \ b)" using additiveD[OF emeasure_additive] .. -lemma emeasure_Union: +lemma emeasure_Un: "A \ sets M \ B \ sets M \ emeasure M (A \ B) = emeasure M A + emeasure M (B - A)" using plus_emeasure[of A M "B - A"] by auto +lemma emeasure_Un_Int: + assumes "A \ sets M" "B \ sets M" + shows "emeasure M A + emeasure M B = emeasure M (A \ B) + emeasure M (A \ B)" +proof - + have "A = (A-B) \ (A \ B)" by auto + then have "emeasure M A = emeasure M (A-B) + emeasure M (A \ B)" + by (metis Diff_Diff_Int Diff_disjoint assms plus_emeasure sets.Diff) + moreover have "A \ B = (A-B) \ B" by auto + then have "emeasure M (A \ B) = emeasure M (A-B) + emeasure M B" + by (metis Diff_disjoint Int_commute assms plus_emeasure sets.Diff) + ultimately show ?thesis by (metis add.assoc add.commute) +qed + lemma sum_emeasure: "F`I \ sets M \ disjoint_family_on F I \ finite I \ (\i\I. emeasure M (F i)) = emeasure M (\i\I. F i)" @@ -987,6 +1000,18 @@ by (subst plus_emeasure[symmetric]) auto qed +lemma emeasure_Un': + assumes "A \ sets M" "B \ sets M" "A \ B \ null_sets M" + shows "emeasure M (A \ B) = emeasure M A + emeasure M B" +proof - + have "A \ B = A \ (B - A \ B)" by blast + also have "emeasure M \ = emeasure M A + emeasure M (B - A \ B)" + using assms by (subst plus_emeasure) auto + also have "emeasure M (B - A \ B) = emeasure M B" + using assms by (intro emeasure_Diff_null_set) auto + finally show ?thesis . +qed + subsection \The almost everywhere filter (i.e.\ quantifier)\ definition\<^marker>\tag important\ ae_filter :: "'a measure \ 'a filter" where diff -r 561b11865cb5 -r dea35c31a0b8 src/HOL/Analysis/Set_Integral.thy --- a/src/HOL/Analysis/Set_Integral.thy Thu Sep 19 16:38:05 2019 +0200 +++ b/src/HOL/Analysis/Set_Integral.thy Thu Sep 19 16:38:32 2019 +0200 @@ -173,12 +173,30 @@ unfolding set_integrable_def using integrable_mult_right[of a M "\x. indicator A x *\<^sub>R f x"] by simp +lemma set_integrable_mult_right_iff [simp]: + fixes a :: "'a::{real_normed_field, second_countable_topology}" + assumes "a \ 0" + shows "set_integrable M A (\t. a * f t) \ set_integrable M A f" +proof + assume "set_integrable M A (\t. a * f t)" + then have "set_integrable M A (\t. 1/a * (a * f t))" + using set_integrable_mult_right by blast + then show "set_integrable M A f" + using assms by auto +qed auto + lemma set_integrable_mult_left [simp, intro]: fixes a :: "'a::{real_normed_field, second_countable_topology}" shows "(a \ 0 \ set_integrable M A f) \ set_integrable M A (\t. f t * a)" unfolding set_integrable_def using integrable_mult_left[of a M "\x. indicator A x *\<^sub>R f x"] by simp +lemma set_integrable_mult_left_iff [simp]: + fixes a :: "'a::{real_normed_field, second_countable_topology}" + assumes "a \ 0" + shows "set_integrable M A (\t. f t * a) \ set_integrable M A f" + using assms by (subst set_integrable_mult_right_iff [symmetric]) (auto simp: mult.commute) + lemma set_integrable_divide [simp, intro]: fixes a :: "'a::{real_normed_field, field, second_countable_topology}" assumes "a \ 0 \ set_integrable M A f" @@ -192,6 +210,12 @@ unfolding set_integrable_def . qed +lemma set_integrable_mult_divide_iff [simp]: + fixes a :: "'a::{real_normed_field, second_countable_topology}" + assumes "a \ 0" + shows "set_integrable M A (\t. f t / a) \ set_integrable M A f" + by (simp add: divide_inverse assms) + lemma set_integral_add [simp, intro]: fixes f g :: "_ \ _ :: {banach, second_countable_topology}" assumes "set_integrable M A f" "set_integrable M A g" @@ -205,8 +229,6 @@ (LINT x:A|M. f x) - (LINT x:A|M. g x)" using assms unfolding set_integrable_def set_lebesgue_integral_def by (simp_all add: scaleR_diff_right) -(* question: why do we have this for negation, but multiplication by a constant - requires an integrability assumption? *) lemma set_integral_uminus: "set_integrable M A f \ LINT x:A|M. - f x = - (LINT x:A|M. f x)" unfolding set_integrable_def set_lebesgue_integral_def by (subst integral_minus[symmetric]) simp_all diff -r 561b11865cb5 -r dea35c31a0b8 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Thu Sep 19 16:38:05 2019 +0200 +++ b/src/HOL/Finite_Set.thy Thu Sep 19 16:38:32 2019 +0200 @@ -1493,12 +1493,11 @@ using card_Un_Int [of A B] by simp lemma card_Un_le: "card (A \ B) \ card A + card B" - apply (cases "finite A") - apply (cases "finite B") - apply (use le_iff_add card_Un_Int in blast) - apply simp - apply simp - done +proof (cases "finite A \ finite B") + case True + then show ?thesis + using le_iff_add card_Un_Int [of A B] by auto +qed auto lemma card_Diff_subset: assumes "finite B" diff -r 561b11865cb5 -r dea35c31a0b8 src/HOL/Groups_Big.thy --- a/src/HOL/Groups_Big.thy Thu Sep 19 16:38:05 2019 +0200 +++ b/src/HOL/Groups_Big.thy Thu Sep 19 16:38:32 2019 +0200 @@ -1187,6 +1187,16 @@ using assms card_eq_0_iff finite_UnionD by fastforce qed +lemma card_UN_le: + assumes "finite I" + shows "card(\i\I. A i) \ (\i\I. card(A i))" + using assms +proof induction + case (insert i I) + then show ?case + using card_Un_le nat_add_left_cancel_le by (force intro: order_trans) +qed auto + lemma sum_multicount_gen: assumes "finite s" "finite t" "\j\t. (card {i\s. R i j} = k j)" shows "sum (\i. (card {j\t. R i j})) s = sum k t" diff -r 561b11865cb5 -r dea35c31a0b8 src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Thu Sep 19 16:38:05 2019 +0200 +++ b/src/HOL/Library/Extended_Real.thy Thu Sep 19 16:38:32 2019 +0200 @@ -1725,13 +1725,44 @@ by (cases a b c rule: ereal3_cases) (auto simp: field_simps zero_less_mult_iff) -lemma ereal_inverse_real: "\z\ \ \ \ z \ 0 \ ereal (inverse (real_of_ereal z)) = inverse z" - by (cases z) simp_all +lemma ereal_inverse_real [simp]: "\z\ \ \ \ z \ 0 \ ereal (inverse (real_of_ereal z)) = inverse z" + by auto lemma ereal_inverse_mult: "a \ 0 \ b \ 0 \ inverse (a * (b::ereal)) = inverse a * inverse b" by (cases a; cases b) auto +lemma inverse_eq_infinity_iff_eq_zero [simp]: + "1/(x::ereal) = \ \ x = 0" +by (simp add: divide_ereal_def) + +lemma ereal_distrib_left: + fixes a b c :: ereal + assumes "a \ \ \ b \ -\" + and "a \ -\