--- a/src/HOL/Analysis/Abstract_Topology.thy Thu Aug 15 21:18:06 2019 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy Thu Aug 15 21:46:43 2019 +0200
@@ -3985,7 +3985,7 @@
ultimately
have "\<forall>\<^sub>F x in at a within T. f x = g x"
by eventually_elim (auto simp: \<open>S = _\<close> eq)
- then show ?thesis using f
+ with f show ?thesis
by (rule Lim_transform_eventually)
qed
--- a/src/HOL/Analysis/Bochner_Integration.thy Thu Aug 15 21:18:06 2019 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy Thu Aug 15 21:46:43 2019 +0200
@@ -1581,12 +1581,17 @@
end
-lemma integrable_mult_left_iff:
+lemma integrable_mult_left_iff [simp]:
fixes f :: "'a \<Rightarrow> real"
shows "integrable M (\<lambda>x. c * f x) \<longleftrightarrow> c = 0 \<or> integrable M f"
using integrable_mult_left[of c M f] integrable_mult_left[of "1 / c" M "\<lambda>x. c * f x"]
by (cases "c = 0") auto
+lemma integrable_mult_right_iff [simp]:
+ fixes f :: "'a \<Rightarrow> real"
+ shows "integrable M (\<lambda>x. f x * c) \<longleftrightarrow> c = 0 \<or> integrable M f"
+ using integrable_mult_left_iff [of M c f] by (simp add: mult.commute)
+
lemma integrableI_nn_integral_finite:
assumes [measurable]: "f \<in> borel_measurable M"
and nonneg: "AE x in M. 0 \<le> f x"
@@ -2939,7 +2944,7 @@
have "(\<integral>\<^sup>+ y. ennreal (norm (s i (x, y))) \<partial>M) \<le> (\<integral>\<^sup>+ y. 2 * norm (f x y) \<partial>M)"
using x s by (intro nn_integral_mono) auto
also have "(\<integral>\<^sup>+ y. 2 * norm (f x y) \<partial>M) < \<infinity>"
- using int_2f by (simp add: integrable_iff_bounded)
+ using int_2f unfolding integrable_iff_bounded by simp
finally show "(\<integral>\<^sup>+ xa. ennreal (norm (s i (x, xa))) \<partial>M) < \<infinity>" .
qed
then have "integral\<^sup>L M (\<lambda>y. s i (x, y)) = simple_bochner_integral M (\<lambda>y. s i (x, y))"
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Aug 15 21:18:06 2019 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Aug 15 21:46:43 2019 +0200
@@ -6481,7 +6481,7 @@
have "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u/(u - z)^(Suc k)) * (w - z)^k)
sums contour_integral (circlepath z r) (\<lambda>u. f u/(u - w))"
unfolding sums_def
- apply (intro Lim_transform_eventually [OF eq] contour_integral_uniform_limit_circlepath [OF eventuallyI ul] cic)
+ apply (intro Lim_transform_eventually [OF _ eq] contour_integral_uniform_limit_circlepath [OF eventuallyI ul] cic)
using \<open>0 < r\<close> apply auto
done
then have "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u/(u - z)^(Suc k)) * (w - z)^k)
@@ -6715,7 +6715,7 @@
then have tendsto_0: "((\<lambda>n. 1 / (2 * of_real pi * \<i>) * (?conint (\<lambda>x. f n x / (x - w)\<^sup>2) - ?conint (\<lambda>x. g x / (x - w)\<^sup>2))) \<longlongrightarrow> 0) F"
using Lim_null by (force intro!: tendsto_mult_right_zero)
have "((\<lambda>n. f' n w - g' w) \<longlongrightarrow> 0) F"
- apply (rule Lim_transform_eventually [OF _ tendsto_0])
+ apply (rule Lim_transform_eventually [OF tendsto_0])
apply (force simp: divide_simps intro: eq_f' eventually_mono [OF cont])
done
then show ?thesis using Lim_null by blast
--- a/src/HOL/Analysis/Change_Of_Vars.thy Thu Aug 15 21:18:06 2019 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Thu Aug 15 21:46:43 2019 +0200
@@ -2012,7 +2012,7 @@
by auto
qed
then show ?thesis
- unfolding borel_measurable_lebesgue_preimage_borel borel_measurable_UNIV [OF assms, symmetric]
+ unfolding borel_measurable_lebesgue_preimage_borel borel_measurable_if [OF assms, symmetric]
by blast
qed
@@ -2508,9 +2508,9 @@
apply (intro borel_measurable_abs borel_measurable_det_Jacobian [OF h_lmeas, where f=g])
by (meson der_g IntD2 has_derivative_within_subset inf_le2)
then have "(\<lambda>x. if x \<in> {t. h n (g t) = y} \<inter> S then ?D x else 0) \<in> borel_measurable lebesgue"
- by (rule borel_measurable_If_I [OF _ h_lmeas])
+ by (rule borel_measurable_if_I [OF _ h_lmeas])
then show "(\<lambda>x. if x \<in> {t. h n (g t) = y} then ?D x else 0) \<in> borel_measurable (lebesgue_on S)"
- by (simp add: if_if_eq_conj Int_commute borel_measurable_UNIV [OF S, symmetric])
+ by (simp add: if_if_eq_conj Int_commute borel_measurable_if [OF S, symmetric])
show "(\<lambda>x. ?D x *\<^sub>R f (g x) /\<^sub>R y) integrable_on S"
by (rule integrable_cmul) (use det_int_fg in auto)
show "norm (if x \<in> {t. h n (g t) = y} then ?D x else 0) \<le> ?D x *\<^sub>R f (g x) /\<^sub>R y"
@@ -2671,7 +2671,7 @@
also have "\<dots> \<in> borel_measurable lebesgue"
by (rule Df_borel)
finally have *: "(\<lambda>x. \<bar>?D x\<bar> * f (g x)) \<in> borel_measurable (lebesgue_on S')"
- by (simp add: borel_measurable_If_D)
+ by (simp add: borel_measurable_if_D)
have "?h \<in> borel_measurable (lebesgue_on S')"
by (intro * S' der_gS' borel_measurable_det_Jacobian measurable) (blast intro: der_gS')
moreover have "?h x = f(g x)" if "x \<in> S'" for x
--- a/src/HOL/Analysis/Conformal_Mappings.thy Thu Aug 15 21:18:06 2019 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Thu Aug 15 21:46:43 2019 +0200
@@ -4476,7 +4476,7 @@
hence "(zor_poly f z0 \<longlongrightarrow> zor_poly f z0 z0) (at z0)"
unfolding isCont_def .
ultimately have "((\<lambda>w. f w * (w - z0) powr - n) \<longlongrightarrow> zor_poly f z0 z0) (at z0)"
- by (rule Lim_transform_eventually)
+ by (blast intro: Lim_transform_eventually)
hence "((\<lambda>x. f (g x) * (g x - z0) powr - n) \<longlongrightarrow> zor_poly f z0 z0) F"
by (rule filterlim_compose[OF _ g])
from tendsto_unique[OF \<open>F \<noteq> bot\<close> this lim] show ?thesis .
@@ -4505,7 +4505,7 @@
hence "(zor_poly f z0 \<longlongrightarrow> zor_poly f z0 z0) (at z0)"
unfolding isCont_def .
ultimately have "((\<lambda>w. f w / (w - z0) ^ nat n) \<longlongrightarrow> zor_poly f z0 z0) (at z0)"
- by (rule Lim_transform_eventually)
+ by (blast intro: Lim_transform_eventually)
hence "((\<lambda>x. f (g x) / (g x - z0) ^ nat n) \<longlongrightarrow> zor_poly f z0 z0) F"
by (rule filterlim_compose[OF _ g])
from tendsto_unique[OF \<open>F \<noteq> bot\<close> this lim] show ?thesis .
@@ -4537,7 +4537,7 @@
hence "(zor_poly f z0 \<longlongrightarrow> zor_poly f z0 z0) (at z0)"
unfolding isCont_def .
ultimately have "((\<lambda>w. f w * (w - z0) ^ nat (-n)) \<longlongrightarrow> zor_poly f z0 z0) (at z0)"
- by (rule Lim_transform_eventually)
+ by (blast intro: Lim_transform_eventually)
hence "((\<lambda>x. f (g x) * (g x - z0) ^ nat (-n)) \<longlongrightarrow> zor_poly f z0 z0) F"
by (rule filterlim_compose[OF _ g])
from tendsto_unique[OF \<open>F \<noteq> bot\<close> this lim] show ?thesis .
@@ -4577,7 +4577,7 @@
moreover have "((\<lambda>w. ((f w - f z) / (w - z)) / ((g w - g z) / (w - z))) \<longlongrightarrow> f' / g') (at z)"
by (intro tendsto_divide has_field_derivativeD assms)
ultimately have "((\<lambda>w. f w / g w) \<longlongrightarrow> f' / g') (at z)"
- by (rule Lim_transform_eventually)
+ by (blast intro: Lim_transform_eventually)
with assms show ?thesis by simp
qed
--- a/src/HOL/Analysis/Derivative.thy Thu Aug 15 21:18:06 2019 +0200
+++ b/src/HOL/Analysis/Derivative.thy Thu Aug 15 21:46:43 2019 +0200
@@ -2373,11 +2373,11 @@
qed
ultimately have "((\<lambda>y. (exp ((y - t) *\<^sub>R A) - 1 - (y - t) *\<^sub>R A) /\<^sub>R norm (y - t)) \<longlongrightarrow> 0) (at t within T)"
- by (rule Lim_transform_eventually[rotated])
+ by (rule Lim_transform_eventually)
from tendsto_mult_right_zero[OF this, where c="exp (t *\<^sub>R A)"]
show "((\<lambda>y. (exp (y *\<^sub>R A) - exp (t *\<^sub>R A) - (y - t) *\<^sub>R (exp (t *\<^sub>R A) * A)) /\<^sub>R norm (y - t)) \<longlongrightarrow> 0)
(at t within T)"
- by (rule Lim_transform_eventually[rotated])
+ by (rule Lim_transform_eventually)
(auto simp: algebra_simps divide_simps exp_add_commuting[symmetric])
qed (rule bounded_linear_scaleR_left)
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy Thu Aug 15 21:18:06 2019 +0200
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy Thu Aug 15 21:46:43 2019 +0200
@@ -495,9 +495,9 @@
done
lemma Lim_transform_within_set_eq:
- fixes a l :: "'a::real_normed_vector"
- shows "eventually (\<lambda>x. x \<in> s \<longleftrightarrow> x \<in> t) (at a)
- \<Longrightarrow> ((f \<longlongrightarrow> l) (at a within s) \<longleftrightarrow> (f \<longlongrightarrow> l) (at a within t))"
+ fixes a :: "'a::metric_space" and l :: "'b::metric_space"
+ shows "eventually (\<lambda>x. x \<in> S \<longleftrightarrow> x \<in> T) (at a)
+ \<Longrightarrow> ((f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow> (f \<longlongrightarrow> l) (at a within T))"
by (force intro: Lim_transform_within_set elim: eventually_mono)
lemma Lim_null:
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Aug 15 21:18:06 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Aug 15 21:46:43 2019 +0200
@@ -557,8 +557,8 @@
shows "integral\<^sup>N lborel f = I"
proof -
from f_borel have "(\<lambda>x. ennreal (f x)) \<in> borel_measurable lborel" by auto
- from borel_measurable_implies_simple_function_sequence'[OF this]
- obtain F where F: "\<And>i. simple_function lborel (F i)" "incseq F"
+ from borel_measurable_implies_simple_function_sequence'[OF this]
+ obtain F where F: "\<And>i. simple_function lborel (F i)" "incseq F"
"\<And>i x. F i x < top" "\<And>x. (SUP i. F i x) = ennreal (f x)"
by blast
then have [measurable]: "\<And>i. F i \<in> borel_measurable lborel"
@@ -876,7 +876,7 @@
lemma borel_integrable_atLeastAtMost':
fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
assumes f: "continuous_on {a..b} f"
- shows "set_integrable lborel {a..b} f"
+ shows "set_integrable lborel {a..b} f"
unfolding set_integrable_def
by (intro borel_integrable_compact compact_Icc f)
@@ -909,7 +909,7 @@
proof -
let ?f = "\<lambda>x. indicator S x *\<^sub>R f x"
have "(?f has_integral LINT x : S | lborel. f x) UNIV"
- using assms has_integral_integral_lborel
+ using assms has_integral_integral_lborel
unfolding set_integrable_def set_lebesgue_integral_def by blast
hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
apply (subst has_integral_restrict_UNIV [symmetric])
@@ -927,7 +927,7 @@
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes f: "set_integrable lebesgue S f"
shows "(f has_integral (LINT x:S|lebesgue. f x)) S"
- using has_integral_integral_lebesgue f
+ using has_integral_integral_lebesgue f
by (fastforce simp add: set_integrable_def set_lebesgue_integral_def indicator_def if_distrib[of "\<lambda>x. x *\<^sub>R f _"] cong: if_cong)
lemma set_lebesgue_integral_eq_integral:
@@ -1031,7 +1031,7 @@
then have "f absolutely_integrable_on S"
using absolutely_integrable_restrict_UNIV by blast
}
- then show ?thesis
+ then show ?thesis
unfolding absolutely_integrable_on_def by auto
qed
@@ -1043,7 +1043,7 @@
proof (cases "c=0")
case False
then show ?thesis
- unfolding absolutely_integrable_on_def
+ unfolding absolutely_integrable_on_def
by (simp add: norm_mult)
qed auto
@@ -1087,6 +1087,27 @@
shows "f absolutely_integrable_on T"
using absolutely_integrable_spike_set_eq f neg by blast
+lemma absolutely_integrable_reflect[simp]:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ shows "(\<lambda>x. f(-x)) absolutely_integrable_on cbox (-b) (-a) \<longleftrightarrow> f absolutely_integrable_on cbox a b"
+ apply (auto simp: absolutely_integrable_on_def dest: integrable_reflect [THEN iffD1])
+ unfolding integrable_on_def by auto
+
+lemma absolutely_integrable_reflect_real[simp]:
+ fixes f :: "real \<Rightarrow> 'b::euclidean_space"
+ shows "(\<lambda>x. f(-x)) absolutely_integrable_on {-b .. -a} \<longleftrightarrow> f absolutely_integrable_on {a..b::real}"
+ unfolding box_real[symmetric] by (rule absolutely_integrable_reflect)
+
+lemma absolutely_integrable_on_subcbox:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ shows "\<lbrakk>f absolutely_integrable_on S; cbox a b \<subseteq> S\<rbrakk> \<Longrightarrow> f absolutely_integrable_on cbox a b"
+ by (meson absolutely_integrable_on_def integrable_on_subcbox)
+
+lemma absolutely_integrable_on_subinterval:
+ fixes f :: "real \<Rightarrow> 'b::euclidean_space"
+ shows "\<lbrakk>f absolutely_integrable_on S; {a..b} \<subseteq> S\<rbrakk> \<Longrightarrow> f absolutely_integrable_on {a..b}"
+ using absolutely_integrable_on_subcbox by fastforce
+
lemma lmeasurable_iff_integrable_on: "S \<in> lmeasurable \<longleftrightarrow> (\<lambda>x. 1::real) integrable_on S"
by (subst absolutely_integrable_on_iff_nonneg[symmetric])
(simp_all add: lmeasurable_iff_integrable set_integrable_def)
@@ -1598,7 +1619,7 @@
by blast
have e22: "0 < e/2 / (2 * B * real DIM('M)) ^ DIM('N)"
using \<open>0 < e\<close> \<open>0 < B\<close> by (simp add: divide_simps)
- obtain T where "open T" "S \<subseteq> T" "(T - S) \<in> lmeasurable"
+ obtain T where "open T" "S \<subseteq> T" "(T - S) \<in> lmeasurable"
"measure lebesgue (T - S) < e/2 / (2 * B * DIM('M)) ^ DIM('N)"
using sets_lebesgue_outer_open [OF \<open>S \<in> sets lebesgue\<close> e22]
by (metis emeasure_eq_measure2 ennreal_leI linorder_not_le)
@@ -1752,7 +1773,7 @@
finally show "\<Union>\<D>' \<subseteq> T" .
show "T \<in> lmeasurable"
using \<open>S \<in> lmeasurable\<close> \<open>S \<subseteq> T\<close> \<open>T - S \<in> lmeasurable\<close> fmeasurable_Diff_D by blast
- qed
+ qed
have "sum (measure lebesgue) \<D>' = sum content \<D>'"
using \<open>\<D>' \<subseteq> \<D>\<close> cbox by (force intro: sum.cong)
then have "(2 * B * DIM('M)) ^ DIM('N) * sum (measure lebesgue) \<D>' =
@@ -2140,7 +2161,7 @@
fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
assumes f: "set_integrable M k f" shows "set_integrable M k (\<lambda>x. norm (f x))"
using integrable_norm f by (force simp add: set_integrable_def)
-
+
lemma absolutely_integrable_bounded_variation:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes f: "f absolutely_integrable_on UNIV"
@@ -2208,7 +2229,7 @@
using d' by force
show "x \<notin> \<Union>{i \<in> d. x \<notin> i}"
by auto
- qed
+ qed
then show ?thesis
by force
qed
@@ -2216,13 +2237,13 @@
by metis
have "e/2 > 0"
using e by auto
- with Henstock_lemma[OF f]
+ with Henstock_lemma[OF f]
obtain \<gamma> where g: "gauge \<gamma>"
- "\<And>p. \<lbrakk>p tagged_partial_division_of cbox a b; \<gamma> fine p\<rbrakk>
+ "\<And>p. \<lbrakk>p tagged_partial_division_of cbox a b; \<gamma> fine p\<rbrakk>
\<Longrightarrow> (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x - integral k f)) < e/2"
- by (metis (no_types, lifting))
+ by (metis (no_types, lifting))
let ?g = "\<lambda>x. \<gamma> x \<inter> ball x (k x)"
- show ?thesis
+ show ?thesis
proof (intro exI conjI allI impI)
show "gauge ?g"
using g(1) k(1) by (auto simp: gauge_def)
@@ -2275,9 +2296,9 @@
unfolding p'_def using d' by blast
have "y \<in> \<Union>{K. \<exists>x. (x, K) \<in> p'}" if y: "y \<in> cbox a b" for y
proof -
- obtain x l where xl: "(x, l) \<in> p" "y \<in> l"
+ obtain x l where xl: "(x, l) \<in> p" "y \<in> l"
using y unfolding p'(6)[symmetric] by auto
- obtain i where i: "i \<in> d" "y \<in> i"
+ obtain i where i: "i \<in> d" "y \<in> i"
using y unfolding d'(6)[symmetric] by auto
have "x \<in> i"
using fineD[OF p(3) xl(1)] using k(2) i xl by auto
@@ -2290,12 +2311,12 @@
using * by auto
next
show "cbox a b \<subseteq> \<Union>{k. \<exists>x. (x, k) \<in> p'}"
- proof
+ proof
fix y
assume y: "y \<in> cbox a b"
- obtain x L where xl: "(x, L) \<in> p" "y \<in> L"
+ obtain x L where xl: "(x, L) \<in> p" "y \<in> L"
using y unfolding p'(6)[symmetric] by auto
- obtain I where i: "I \<in> d" "y \<in> I"
+ obtain I where i: "I \<in> d" "y \<in> I"
using y unfolding d'(6)[symmetric] by auto
have "x \<in> I"
using fineD[OF p(3) xl(1)] using k(2) i xl by auto
@@ -2323,7 +2344,7 @@
moreover have "\<exists>y i l. (x, K) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}"
if xK: "(x,K) \<in> p'" for x K
proof -
- obtain i l where il: "x \<in> i" "i \<in> d" "(x, l) \<in> p" "K = i \<inter> l"
+ obtain i l where il: "x \<in> i" "i \<in> d" "(x, l) \<in> p" "K = i \<inter> l"
using xK unfolding p'_def by auto
then show ?thesis
using p'(2) by fastforce
@@ -2378,7 +2399,7 @@
show ?thesis
apply (rule sum.mono_neutral_left)
apply (simp add: snd_p(1))
- unfolding d'_def uv using * by auto
+ unfolding d'_def uv using * by auto
qed
also have "\<dots> = (\<Sum>l\<in>snd ` p. norm (integral (K \<inter> l) f))"
proof -
@@ -2388,8 +2409,8 @@
have "interior (K \<inter> l) \<subseteq> interior (l \<inter> y)"
by (metis Int_lower2 interior_mono le_inf_iff that(4))
then have "interior (K \<inter> l) = {}"
- by (simp add: snd_p(5) that)
- moreover from d'(4)[OF k] snd_p(4)[OF that(1)]
+ by (simp add: snd_p(5) that)
+ moreover from d'(4)[OF k] snd_p(4)[OF that(1)]
obtain u1 v1 u2 v2
where uv: "K = cbox u1 u2" "l = cbox v1 v2" by metis
ultimately show ?thesis
@@ -2449,7 +2470,7 @@
then show ?thesis by auto
qed
have 1: "\<exists>i l. snd (a, b) = i \<inter> l \<and> i \<in> d \<and> l \<in> snd ` p" if "(a, b) \<in> p'" for a b
- using that
+ using that
apply (clarsimp simp: p'_def image_iff)
by (metis (no_types, hide_lams) snd_conv)
show ?thesis
@@ -2494,7 +2515,7 @@
by auto
then show "\<bar>content (l1 \<inter> k1)\<bar> * norm (f x1) = 0"
unfolding uv Int_interval content_eq_0_interior[symmetric] by auto
- qed
+ qed
then show ?thesis
unfolding *
apply (subst sum.reindex_nontrivial [OF fin_pd])
@@ -2551,7 +2572,7 @@
finally show ?thesis .
qed
qed (rule d)
- qed
+ qed
qed
then show ?thesis
using absolutely_integrable_onI [OF f has_integral_integrable] has_integral[of _ ?S]
@@ -2598,7 +2619,7 @@
then obtain d K where ddiv: "d division_of \<Union>d" and "K = (\<Sum>k\<in>d. norm (integral k f))"
"Sup (sum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union> d}) - e < K"
by (auto simp add: image_iff not_le)
- then have d: "Sup (sum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union> d}) - e
+ then have d: "Sup (sum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union> d}) - e
< (\<Sum>k\<in>d. norm (integral k f))"
by auto
note d'=division_ofD[OF ddiv]
@@ -2644,7 +2665,7 @@
and d1: "\<And>p. \<lbrakk>p tagged_division_of (cbox a b); d1 fine p\<rbrakk> \<Longrightarrow>
norm ((\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm (f x))) < e/2"
unfolding has_integral_integral has_integral by meson
- obtain d2 where "gauge d2"
+ obtain d2 where "gauge d2"
and d2: "\<And>p. \<lbrakk>p tagged_partial_division_of (cbox a b); d2 fine p\<rbrakk> \<Longrightarrow>
(\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x - integral k f)) < e/2"
by (blast intro: Henstock_lemma [OF f(1) \<open>e/2>0\<close>])
@@ -3171,6 +3192,11 @@
using absolutely_integrable_integrable_bound
by (simp add: absolutely_integrable_on_def continuous_on_norm integrable_continuous)
+lemma absolutely_integrable_continuous_real:
+ fixes f :: "real \<Rightarrow> 'b::euclidean_space"
+ shows "continuous_on {a..b} f \<Longrightarrow> f absolutely_integrable_on {a..b}"
+ by (metis absolutely_integrable_continuous box_real(2))
+
lemma continuous_imp_integrable:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "continuous_on (cbox a b) f"
@@ -3261,13 +3287,13 @@
(\<lambda>x. norm(\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f) x)"
by (simp add: sum.delta)
have *: "(\<lambda>y. \<Sum>j\<in>Basis. if j = i then y *\<^sub>R j else 0) \<circ>
- (\<lambda>x. norm (\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f
- absolutely_integrable_on S"
+ (\<lambda>x. norm (\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f
+ absolutely_integrable_on S"
if "i \<in> Basis" for i
proof -
have "bounded_linear (\<lambda>y. \<Sum>j\<in>Basis. if j = i then y *\<^sub>R j else 0)"
by (simp add: linear_linear algebra_simps linearI)
- moreover have "(\<lambda>x. norm (\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f
+ moreover have "(\<lambda>x. norm (\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f
absolutely_integrable_on S"
unfolding o_def
apply (rule absolutely_integrable_norm [unfolded o_def])
@@ -3290,14 +3316,14 @@
shows "f absolutely_integrable_on A"
by (rule absolutely_integrable_integrable_bound [OF _ assms]) auto
-
+
lemma abs_absolutely_integrableI:
assumes f: "f integrable_on S" and fcomp: "(\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x \<bullet> i\<bar> *\<^sub>R i) integrable_on S"
shows "f absolutely_integrable_on S"
proof -
have "(\<lambda>x. (f x \<bullet> i) *\<^sub>R i) absolutely_integrable_on S" if "i \<in> Basis" for i
proof -
- have "(\<lambda>x. \<bar>f x \<bullet> i\<bar>) integrable_on S"
+ have "(\<lambda>x. \<bar>f x \<bullet> i\<bar>) integrable_on S"
using assms integrable_component [OF fcomp, where y=i] that by simp
then have "(\<lambda>x. f x \<bullet> i) absolutely_integrable_on S"
using abs_absolutely_integrableI_1 f integrable_component by blast
@@ -3310,7 +3336,7 @@
by (simp add: euclidean_representation)
qed
-
+
lemma absolutely_integrable_abs_iff:
"f absolutely_integrable_on S \<longleftrightarrow>
f integrable_on S \<and> (\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x \<bullet> i\<bar> *\<^sub>R i) integrable_on S"
@@ -3319,7 +3345,7 @@
assume ?lhs then show ?rhs
using absolutely_integrable_abs absolutely_integrable_on_def by blast
next
- assume ?rhs
+ assume ?rhs
moreover
have "(\<lambda>x. if x \<in> S then \<Sum>i\<in>Basis. \<bar>f x \<bullet> i\<bar> *\<^sub>R i else 0) = (\<lambda>x. \<Sum>i\<in>Basis. \<bar>(if x \<in> S then f x else 0) \<bullet> i\<bar> *\<^sub>R i)"
by force
@@ -3333,7 +3359,7 @@
shows "(\<lambda>x. \<Sum>i\<in>Basis. max (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i)
absolutely_integrable_on S"
proof -
- have "(\<lambda>x. \<Sum>i\<in>Basis. max (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) =
+ have "(\<lambda>x. \<Sum>i\<in>Basis. max (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) =
(\<lambda>x. (1/2) *\<^sub>R (f x + g x + (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))"
proof (rule ext)
fix x
@@ -3347,7 +3373,7 @@
show "(\<Sum>i\<in>Basis. max (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) =
(1 / 2) *\<^sub>R (f x + g x + (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i))" .
qed
- moreover have "(\<lambda>x. (1 / 2) *\<^sub>R (f x + g x + (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))
+ moreover have "(\<lambda>x. (1 / 2) *\<^sub>R (f x + g x + (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^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]]
@@ -3355,7 +3381,7 @@
done
ultimately show ?thesis by metis
qed
-
+
corollary absolutely_integrable_max_1:
fixes f :: "'n::euclidean_space \<Rightarrow> real"
assumes "f absolutely_integrable_on S" "g absolutely_integrable_on S"
@@ -3368,7 +3394,7 @@
shows "(\<lambda>x. \<Sum>i\<in>Basis. min (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i)
absolutely_integrable_on S"
proof -
- have "(\<lambda>x. \<Sum>i\<in>Basis. min (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) =
+ have "(\<lambda>x. \<Sum>i\<in>Basis. min (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) =
(\<lambda>x. (1/2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))"
proof (rule ext)
fix x
@@ -3382,7 +3408,7 @@
show "(\<Sum>i\<in>Basis. min (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) =
(1 / 2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i))" .
qed
- moreover have "(\<lambda>x. (1 / 2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))
+ moreover have "(\<lambda>x. (1 / 2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^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]]
@@ -3390,7 +3416,7 @@
done
ultimately show ?thesis by metis
qed
-
+
corollary absolutely_integrable_min_1:
fixes f :: "'n::euclidean_space \<Rightarrow> real"
assumes "f absolutely_integrable_on S" "g absolutely_integrable_on S"
@@ -3404,7 +3430,7 @@
proof -
have "(\<lambda>x. (f x \<bullet> i) *\<^sub>R i) absolutely_integrable_on A" if "i \<in> Basis" for i
proof -
- have "(\<lambda>x. f x \<bullet> i) integrable_on A"
+ have "(\<lambda>x. f x \<bullet> i) integrable_on A"
by (simp add: assms(1) integrable_component)
then have "(\<lambda>x. f x \<bullet> i) absolutely_integrable_on A"
by (metis that comp nonnegative_absolutely_integrable_1)
@@ -3416,7 +3442,7 @@
then show ?thesis
by (simp add: euclidean_representation)
qed
-
+
lemma absolutely_integrable_component_ubound:
fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
assumes f: "f integrable_on A" and g: "g absolutely_integrable_on A"
@@ -3511,7 +3537,7 @@
using int [OF B'] by (auto simp: image_iff o_def cong: if_cong dest!: has_integral_vec1_I_cbox)
qed
show ?thesis
- using assms
+ using assms
apply (subst has_integral_alt)
apply (subst (asm) has_integral_alt)
apply (simp add: has_integral_vec1_I_cbox split: if_split_asm)
@@ -3632,7 +3658,7 @@
"AE x in lebesgue. norm (indicator S x *\<^sub>R f k x) \<le> indicator S x *\<^sub>R h x" for k
using conv le by (auto intro!: always_eventually split: split_indicator)
have g: "g absolutely_integrable_on S"
- using 1 2 3 4 unfolding set_borel_measurable_def set_integrable_def
+ using 1 2 3 4 unfolding set_borel_measurable_def set_integrable_def
by (rule integrable_dominated_convergence)
then show "g integrable_on S"
by (auto simp: absolutely_integrable_on_def)
@@ -3712,7 +3738,7 @@
assume fb [rule_format]: "\<And>k. \<forall>b\<in>Basis. (\<lambda>x. f k x \<bullet> b) absolutely_integrable_on S" and b: "b \<in> Basis"
show "(\<lambda>x. g x \<bullet> b) integrable_on S"
proof (rule dominated_convergence_integrable_1 [OF fb h])
- fix x
+ fix x
assume "x \<in> S"
show "norm (g x \<bullet> b) \<le> h x"
using norm_nth_le \<open>x \<in> S\<close> b normg order.trans by blast
@@ -3773,7 +3799,7 @@
\<close>
-lemma
+lemma
fixes f :: "real \<Rightarrow> real"
assumes [measurable]: "f \<in> borel_measurable borel"
assumes f: "\<And>x. x \<in> {a..b} \<Longrightarrow> DERIV F x :> f x" "\<And>x. x \<in> {a..b} \<Longrightarrow> 0 \<le> f x" and "a \<le> b"
@@ -4400,7 +4426,7 @@
shows "{x. f x \<in> T} \<in> sets lebesgue"
using assms borel_measurable_vimage_borel [of f UNIV] by auto
-lemma borel_measurable_If_I:
+lemma borel_measurable_if_I:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes f: "f \<in> borel_measurable (lebesgue_on S)" and S: "S \<in> sets lebesgue"
shows "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue"
@@ -4416,7 +4442,7 @@
done
qed
-lemma borel_measurable_If_D:
+lemma borel_measurable_if_D:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue"
shows "f \<in> borel_measurable (lebesgue_on S)"
@@ -4426,11 +4452,11 @@
apply (force simp: space_restrict_space sets_restrict_space image_iff intro: rev_bexI)
done
-lemma borel_measurable_UNIV:
+lemma borel_measurable_if:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "S \<in> sets lebesgue"
shows "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue \<longleftrightarrow> f \<in> borel_measurable (lebesgue_on S)"
- using assms borel_measurable_If_D borel_measurable_If_I by blast
+ using assms borel_measurable_if_D borel_measurable_if_I by blast
lemma borel_measurable_lebesgue_preimage_borel:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -4514,7 +4540,7 @@
show "(\<lambda>x. if x \<in> S then f x else 0) integrable_on cbox a b" for a b
proof (rule measurable_bounded_lemma)
show "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue"
- by (simp add: S borel_measurable_UNIV f)
+ by (simp add: S borel_measurable_if f)
show "(\<lambda>x. if x \<in> S then g x else 0) integrable_on cbox a b"
by (simp add: g integrable_altD(1))
show "norm (if x \<in> S then f x else 0) \<le> (if x \<in> S then g x else 0)" for x
@@ -4556,7 +4582,7 @@
have "(UNIV::'a set) \<in> sets lborel"
by simp
then show ?thesis
- using assms borel_measurable_If_D borel_measurable_UNIV_eq integrable_imp_measurable_weak integrable_restrict_UNIV by blast
+ using assms borel_measurable_if_D borel_measurable_UNIV_eq integrable_imp_measurable_weak integrable_restrict_UNIV by blast
qed
lemma integrable_iff_integrable_on:
@@ -4599,6 +4625,12 @@
apply (simp add: integrable_on_lebesgue_on measurable_bounded_by_integrable_imp_lebesgue_integrable)
using abs_absolutely_integrableI_1 absolutely_integrable_measurable measurable_bounded_by_integrable_imp_integrable_real by blast
+lemma absolutely_integrable_imp_borel_measurable:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "f absolutely_integrable_on S" "S \<in> sets lebesgue"
+ shows "f \<in> borel_measurable (lebesgue_on S)"
+ using absolutely_integrable_measurable assms by blast
+
lemma measurable_bounded_by_integrable_imp_absolutely_integrable:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "f \<in> borel_measurable (lebesgue_on S)" "S \<in> sets lebesgue"
@@ -4772,7 +4804,7 @@
fix e :: real assume e: "e > 0"
have sets [intro]: "A \<in> sets M" if "A \<in> sets borel" for A
using that assms by blast
-
+
have "((\<lambda>b. LINT y:{a..b}|M. g y) \<longlongrightarrow> (LINT y:{a..}|M. g y)) at_top"
by (intro tendsto_set_lebesgue_integral_at_top assms sets) auto
with e obtain b0 :: real where b0: "\<forall>b\<ge>b0. \<bar>(LINT y:{a..}|M. g y) - (LINT y:{a..b}|M. g y)\<bar> < e"
@@ -4792,7 +4824,7 @@
have "eventually (\<lambda>b. b \<ge> b0) at_top" by (rule eventually_ge_at_top)
moreover have "eventually (\<lambda>b. b \<ge> a) at_top" by (rule eventually_ge_at_top)
- ultimately show "eventually (\<lambda>b. \<forall>x\<in>A.
+ ultimately show "eventually (\<lambda>b. \<forall>x\<in>A.
dist (LINT y:{a..b}|M. f x y) (LINT y:{a..}|M. f x y) < e) at_top"
proof eventually_elim
case (elim b)
--- a/src/HOL/Analysis/Extended_Real_Limits.thy Thu Aug 15 21:18:06 2019 +0200
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy Thu Aug 15 21:46:43 2019 +0200
@@ -727,7 +727,7 @@
then have "ereal(1/v n) = 1/u n" using H(2) by simp
}
ultimately have "eventually (\<lambda>n. ereal(1/v n) = 1/u n) F" using ureal eventually_elim2 by force
- with Lim_transform_eventually[OF this lim] show ?thesis by simp
+ with Lim_transform_eventually[OF lim this] show ?thesis by simp
next
case (PInf)
then have "1/l = 0" by auto
@@ -744,7 +744,7 @@
have "(v \<longlongrightarrow> \<infinity>) F" unfolding v_def using MInf assms(1) tendsto_uminus_ereal by fastforce
then have "((\<lambda>n. 1/v n) \<longlongrightarrow> 0) F" using tendsto_inverse_ereal_PInf by auto
then have "((\<lambda>n. -1/v n) \<longlongrightarrow> 0) F" using tendsto_uminus_ereal by fastforce
- then show ?thesis unfolding v_def using Lim_transform_eventually[OF *] \<open> 1/l = 0 \<close> by auto
+ then show ?thesis unfolding v_def using Lim_transform_eventually[OF _ *] \<open> 1/l = 0 \<close> by auto
qed
lemma tendsto_divide_ereal [tendsto_intros]:
--- a/src/HOL/Analysis/Further_Topology.thy Thu Aug 15 21:18:06 2019 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy Thu Aug 15 21:46:43 2019 +0200
@@ -4020,7 +4020,7 @@
apply (auto simp: exp_eq dist_norm norm_mult)
done
then have "((\<lambda>y. (g y - g z) / (y - z)) \<longlongrightarrow> f' / exp (g z)) (at z within S)"
- by (auto intro!: Lim_transform_eventually [OF _ tendsto_divide [OF ee dd]])
+ by (auto intro!: Lim_transform_eventually [OF tendsto_divide [OF ee dd]])
then show ?thesis
by (auto simp: field_differentiable_def has_field_derivative_iff)
qed
@@ -4068,7 +4068,7 @@
apply (auto simp: exp_eq dist_norm norm_mult)
done
then have "((\<lambda>y. (g y - g z) / (y - z)) \<longlongrightarrow> f' / exp (g z)) (at z within S)"
- by (auto intro!: Lim_transform_eventually [OF _ tendsto_divide [OF ee dd]])
+ by (auto intro!: Lim_transform_eventually [OF tendsto_divide [OF ee dd]])
then show ?thesis
by (auto simp: field_differentiable_def has_field_derivative_iff)
qed
--- a/src/HOL/Analysis/Gamma_Function.thy Thu Aug 15 21:18:06 2019 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy Thu Aug 15 21:46:43 2019 +0200
@@ -715,7 +715,7 @@
by (intro tendsto_intros LIMSEQ_n_over_Suc_n) simp_all
hence "(\<lambda>n. of_real (ln (real n / (real n + 1)))) \<longlonglongrightarrow> (0 :: 'a)" by (simp add: add_ac)
hence lim: "(\<lambda>n. of_real (ln (real n)) - of_real (ln (real n + 1))) \<longlonglongrightarrow> (0::'a)"
- proof (rule Lim_transform_eventually [rotated])
+ proof (rule Lim_transform_eventually)
show "eventually (\<lambda>n. of_real (ln (real n / (real n + 1))) =
of_real (ln (real n)) - (of_real (ln (real n + 1)) :: 'a)) at_top"
using eventually_gt_at_top[of "0::nat"] by eventually_elim (simp add: ln_div)
@@ -1118,7 +1118,7 @@
by (intro tendsto_intros lim_inverse_n)
hence "(\<lambda>n. ?f n * rGamma_series z n) \<longlonglongrightarrow> rGamma z" by simp
ultimately have "(\<lambda>n. z * rGamma_series (z + 1) n) \<longlonglongrightarrow> rGamma z"
- by (rule Lim_transform_eventually)
+ by (blast intro: Lim_transform_eventually)
moreover have "(\<lambda>n. z * rGamma_series (z + 1) n) \<longlonglongrightarrow> z * rGamma (z + 1)"
by (intro tendsto_intros)
ultimately show "z * rGamma (z + 1) = rGamma z" using LIMSEQ_unique by blast
@@ -1324,7 +1324,7 @@
(simp_all add: convergent_LIMSEQ_iff rGamma_complex_def)
hence "(\<lambda>n. ?f n * rGamma_series z n) \<longlonglongrightarrow> rGamma z" by simp
ultimately have "(\<lambda>n. z * rGamma_series (z + 1) n) \<longlonglongrightarrow> rGamma z"
- by (rule Lim_transform_eventually)
+ by (blast intro: Lim_transform_eventually)
moreover have "(\<lambda>n. z * rGamma_series (z + 1) n) \<longlonglongrightarrow> z * rGamma (z + 1)"
using rGamma_series_complex_converges
by (auto intro!: tendsto_mult simp: rGamma_complex_def convergent_LIMSEQ_iff)
@@ -2054,7 +2054,7 @@
by (intro tendsto_intros Gamma_series'_LIMSEQ)
(simp_all add: o_def strict_mono_def Gamma_eq_zero_iff)
ultimately have "?h \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
- by (rule Lim_transform_eventually)
+ by (blast intro: Lim_transform_eventually)
} note lim = this
from assms double_in_nonpos_Ints_imp[of z] have z': "2 * z \<notin> \<int>\<^sub>\<le>\<^sub>0" by auto
@@ -2504,7 +2504,7 @@
intro: eventually_mono eventually_gt_at_top[of "0::nat"] dest: pochhammer_eq_0_imp_nonpos_Int)
moreover have "?r' \<longlonglongrightarrow> exp (z * of_real (ln 1))"
by (intro tendsto_intros LIMSEQ_Suc_n_over_n) simp_all
- ultimately show "?r \<longlonglongrightarrow> 1" by (force dest!: Lim_transform_eventually)
+ ultimately show "?r \<longlonglongrightarrow> 1" by (force intro: Lim_transform_eventually)
from eventually_gt_at_top[of "0::nat"]
show "eventually (\<lambda>n. ?r n = Gamma_series_euler' z n / Gamma_series z n) sequentially"
@@ -2901,8 +2901,7 @@
by eventually_elim (simp add: powr_def algebra_simps Ln_of_nat Gamma_series_def)
from this and Gamma_series_LIMSEQ[of z]
have C: "(\<lambda>k. of_nat k powr z * fact k / pochhammer z (k+1)) \<longlonglongrightarrow> Gamma z"
- by (rule Lim_transform_eventually)
-
+ by (blast intro: Lim_transform_eventually)
{
fix x :: real assume x: "x \<ge> 0"
have lim_exp: "(\<lambda>k. (1 - x / real k) ^ k) \<longlonglongrightarrow> exp (-x)"
--- a/src/HOL/Analysis/Harmonic_Numbers.thy Thu Aug 15 21:18:06 2019 +0200
+++ b/src/HOL/Analysis/Harmonic_Numbers.thy Thu Aug 15 21:46:43 2019 +0200
@@ -218,7 +218,7 @@
filterlim_subseq) (auto simp: strict_mono_def)
hence "(\<lambda>n. ?em (2*n) - ?em n + ln (2::real)) \<longlonglongrightarrow> ln 2" by simp
ultimately have "(\<lambda>n. (\<Sum>k<2*n. (-1)^k / real_of_nat (Suc k))) \<longlonglongrightarrow> ln 2"
- by (rule Lim_transform_eventually)
+ by (blast intro: Lim_transform_eventually)
moreover have "summable (\<lambda>k. (-1)^k * inverse (real_of_nat (Suc k)))"
using LIMSEQ_inverse_real_of_nat
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Aug 15 21:18:06 2019 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Aug 15 21:46:43 2019 +0200
@@ -3522,12 +3522,17 @@
and "\<forall>k\<in>Basis. m k \<noteq> 0"
shows "((\<lambda>x. f (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) has_integral
((1/ \<bar>prod m Basis\<bar>) *\<^sub>R i)) ((\<lambda>x. (\<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b)"
-apply (rule has_integral_twiddle[where f=f])
-unfolding zero_less_abs_iff content_image_stretch_interval
-unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a]
-using assms
-by auto
-
+ apply (rule has_integral_twiddle[where f=f])
+ unfolding zero_less_abs_iff content_image_stretch_interval
+ unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a]
+ using assms
+ by auto
+
+lemma has_integral_stretch_real:
+ fixes f :: "real \<Rightarrow> 'b::real_normed_vector"
+ assumes "(f has_integral i) {a..b}" and "m \<noteq> 0"
+ shows "((\<lambda>x. f (m * x)) has_integral (1 / \<bar>m\<bar>) *\<^sub>R i) ((\<lambda>x. x / m) ` {a..b})"
+ using has_integral_stretch [of f i a b "\<lambda>b. m"] assms by simp
lemma integrable_stretch:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
@@ -3605,6 +3610,11 @@
"((\<lambda>x. f (-x)) has_integral i) (cbox (-b) (-a)) \<longleftrightarrow> (f has_integral i) (cbox a b)"
by (auto dest: has_integral_reflect_lemma)
+lemma has_integral_reflect_real[simp]:
+ fixes a b::real
+ shows "((\<lambda>x. f (-x)) has_integral i) {-b..-a} \<longleftrightarrow> (f has_integral i) {a..b}"
+ by (metis has_integral_reflect interval_cbox)
+
lemma integrable_reflect[simp]: "(\<lambda>x. f(-x)) integrable_on cbox (-b) (-a) \<longleftrightarrow> f integrable_on cbox a b"
unfolding integrable_on_def by auto
@@ -3619,7 +3629,6 @@
unfolding box_real[symmetric]
by (rule integral_reflect)
-
subsection \<open>Stronger form of FCT; quite a tedious proof\<close>
lemma split_minus[simp]: "(\<lambda>(x, k). f x k) x - (\<lambda>(x, k). g x k) x = (\<lambda>(x, k). f x k - g x k) x"
@@ -7286,19 +7295,19 @@
thus "bounded (range(\<lambda>k. integral {c..} (f k)))"
by (intro boundedI[of _ "exp (-a*c)/a"]) auto
qed (auto simp: f_def)
-
+ have "(\<lambda>k. exp (-a*c)/a - exp (-a * of_nat k)/a) \<longlonglongrightarrow> exp (-a*c)/a - 0/a"
+ by (intro tendsto_intros filterlim_compose[OF exp_at_bot]
+ filterlim_tendsto_neg_mult_at_bot[OF tendsto_const] filterlim_real_sequentially)+
+ (insert a, simp_all)
+ moreover
from eventually_gt_at_top[of "nat \<lceil>c\<rceil>"] have "eventually (\<lambda>k. of_nat k > c) sequentially"
by eventually_elim linarith
hence "eventually (\<lambda>k. exp (-a*c)/a - exp (-a * of_nat k)/a = integral {c..} (f k)) sequentially"
- by eventually_elim (simp add: integral_f)
- moreover have "(\<lambda>k. exp (-a*c)/a - exp (-a * of_nat k)/a) \<longlonglongrightarrow> exp (-a*c)/a - 0/a"
- by (intro tendsto_intros filterlim_compose[OF exp_at_bot]
- filterlim_tendsto_neg_mult_at_bot[OF tendsto_const] filterlim_real_sequentially)+
- (insert a, simp_all)
+ by eventually_elim (simp add: integral_f)
ultimately have "(\<lambda>k. integral {c..} (f k)) \<longlonglongrightarrow> exp (-a*c)/a - 0/a"
by (rule Lim_transform_eventually)
from LIMSEQ_unique[OF conjunct2[OF A] this]
- have "integral {c..} (\<lambda>x. exp (-a*x)) = exp (-a*c)/a" by simp
+ have "integral {c..} (\<lambda>x. exp (-a*x)) = exp (-a*c)/a" by simp
with conjunct1[OF A] show ?thesis
by (simp add: has_integral_integral)
qed
@@ -7363,7 +7372,7 @@
have "eventually (\<lambda>k. x powr a = f k x) sequentially"
by eventually_elim (insert x, simp add: f_def)
moreover have "(\<lambda>_. x powr a) \<longlonglongrightarrow> x powr a" by simp
- ultimately show ?thesis by (rule Lim_transform_eventually)
+ ultimately show ?thesis by (blast intro: Lim_transform_eventually)
qed (simp_all add: f_def)
next
{
@@ -7390,7 +7399,7 @@
hence "(\<lambda>k. c powr (a + 1) / (a + 1) - inverse (real (Suc k)) powr (a + 1) / (a + 1))
\<longlonglongrightarrow> c powr (a + 1) / (a + 1)" by simp
ultimately have "(\<lambda>k. integral {0..c} (f k)) \<longlonglongrightarrow> c powr (a+1) / (a+1)"
- by (rule Lim_transform_eventually)
+ by (blast intro: Lim_transform_eventually)
with A have "integral {0..c} (\<lambda>x. x powr a) = c powr (a+1) / (a+1)"
by (blast intro: LIMSEQ_unique)
with A show ?thesis by (simp add: has_integral_integral)
@@ -7474,7 +7483,7 @@
by (insert assms, (rule tendsto_intros filterlim_compose[OF tendsto_neg_powr]
filterlim_ident filterlim_real_sequentially | simp)+)
hence "(\<lambda>n. F n - F a) \<longlonglongrightarrow> -F a" by simp
- ultimately have "(\<lambda>n. integral {a..} (f n)) \<longlonglongrightarrow> -F a" by (rule Lim_transform_eventually)
+ ultimately have "(\<lambda>n. integral {a..} (f n)) \<longlonglongrightarrow> -F a" by (blast intro: Lim_transform_eventually)
from conjunct2[OF *] and this
have "integral {a..} (\<lambda>x. x powr e) = -F a" by (rule LIMSEQ_unique)
with conjunct1[OF *] show ?thesis
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Thu Aug 15 21:18:06 2019 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Thu Aug 15 21:46:43 2019 +0200
@@ -417,10 +417,43 @@
shows "f \<in> measurable (lebesgue_on S) M \<longleftrightarrow> g \<in> measurable (lebesgue_on S) M"
by (metis (mono_tags, lifting) IntD1 assms measurable_cong_simp space_restrict_space)
+lemma lebesgue_on_UNIV_eq: "lebesgue_on UNIV = lebesgue"
+proof -
+ have "measure_of UNIV (sets lebesgue) (emeasure lebesgue) = lebesgue"
+ by (metis measure_of_of_measure space_borel space_completion space_lborel)
+ then show ?thesis
+ by (auto simp: restrict_space_def)
+qed
+
lemma integrable_lebesgue_on_UNIV_eq:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{banach, second_countable_topology}"
shows "integrable (lebesgue_on UNIV) f = integrable lebesgue f"
by (auto simp: integrable_restrict_space)
+lemma integral_restrict_Int:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "S \<in> sets lebesgue" "T \<in> sets lebesgue"
+ shows "integral\<^sup>L (lebesgue_on T) (\<lambda>x. if x \<in> S then f x else 0) = integral\<^sup>L (lebesgue_on (S \<inter> T)) f"
+proof -
+ have "(\<lambda>x. indicat_real T x *\<^sub>R (if x \<in> S then f x else 0)) = (\<lambda>x. indicat_real (S \<inter> T) x *\<^sub>R f x)"
+ by (force simp: indicator_def)
+ then show ?thesis
+ by (simp add: assms sets.Int Bochner_Integration.integral_restrict_space)
+qed
+
+lemma integral_restrict:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "S \<subseteq> T" "S \<in> sets lebesgue" "T \<in> sets lebesgue"
+ shows "integral\<^sup>L (lebesgue_on T) (\<lambda>x. if x \<in> S then f x else 0) = integral\<^sup>L (lebesgue_on S) f"
+ using integral_restrict_Int [of S T f] assms
+ by (simp add: Int_absorb2)
+
+lemma integral_restrict_UNIV:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "S \<in> sets lebesgue"
+ shows "integral\<^sup>L lebesgue (\<lambda>x. if x \<in> S then f x else 0) = integral\<^sup>L (lebesgue_on S) f"
+ using integral_restrict_Int [of S UNIV f] assms
+ by (simp add: lebesgue_on_UNIV_eq)
+
text\<^marker>\<open>tag unimportant\<close> \<open>Measurability of continuous functions\<close>
@@ -1027,6 +1060,12 @@
and lmeasurable_box [iff]: "box a b \<in> lmeasurable"
by (auto simp: fmeasurable_def emeasure_lborel_box_eq emeasure_lborel_cbox_eq)
+lemma
+ fixes a::real
+ shows lmeasurable_interval [iff]: "{a..b} \<in> lmeasurable" "{a<..<b} \<in> lmeasurable"
+ apply (metis box_real(2) lmeasurable_cbox)
+ by (metis box_real(1) lmeasurable_box)
+
lemma fmeasurable_compact: "compact S \<Longrightarrow> S \<in> fmeasurable lborel"
using emeasure_compact_finite[of S] by (intro fmeasurableI) (auto simp: borel_compact)
--- a/src/HOL/Analysis/Measure_Space.thy Thu Aug 15 21:18:06 2019 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy Thu Aug 15 21:46:43 2019 +0200
@@ -2335,7 +2335,7 @@
then have eq: "(\<Union>i. F i) = F i"
by auto
with i show ?thesis
- by (auto intro!: Lim_transform_eventually[OF _ tendsto_const] eventually_sequentiallyI[where c=i])
+ by (auto intro!: Lim_transform_eventually[OF tendsto_const] eventually_sequentiallyI[where c=i])
next
assume "\<not> (\<exists>i. \<forall>j\<ge>i. F i = F j)"
then obtain f where f: "\<And>i. i \<le> f i" "\<And>i. F i \<noteq> F (f i)" by metis
--- a/src/HOL/Library/Extended_Real.thy Thu Aug 15 21:18:06 2019 +0200
+++ b/src/HOL/Library/Extended_Real.thy Thu Aug 15 21:46:43 2019 +0200
@@ -3993,7 +3993,7 @@
by (auto intro!: tendsto_inverse)
from real \<open>0 < x\<close> show ?thesis
by (auto simp: at_ereal tendsto_compose_filtermap[symmetric] eventually_at_filter
- intro!: Lim_transform_eventually[OF _ **] t1_space_nhds)
+ intro!: Lim_transform_eventually[OF **] t1_space_nhds)
qed (insert \<open>0 < x\<close>, auto intro!: inverse_infty_ereal_tendsto_0)
lemma inverse_ereal_tendsto_at_right_0: "(inverse \<longlongrightarrow> \<infinity>) (at_right (0::ereal))"
--- a/src/HOL/Library/Landau_Symbols.thy Thu Aug 15 21:18:06 2019 +0200
+++ b/src/HOL/Library/Landau_Symbols.thy Thu Aug 15 21:46:43 2019 +0200
@@ -1676,7 +1676,7 @@
by (intro always_eventually) simp
moreover have "((\<lambda>_. 1) \<longlongrightarrow> 1) F" by simp
ultimately show "((\<lambda>x. if f x = 0 \<and> f x = 0 then 1 else f x / f x) \<longlongrightarrow> 1) F"
- by (rule Lim_transform_eventually)
+ by (simp add: Landau_Symbols.tendsto_eventually)
qed
lemma asymp_equiv_symI:
@@ -1702,7 +1702,7 @@
qed
hence "eventually (\<lambda>x. f x / g x = (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) F"
by eventually_elim simp
- from this and assms show "f \<sim>[F] g" unfolding asymp_equiv_def
+ with assms show "f \<sim>[F] g" unfolding asymp_equiv_def
by (rule Lim_transform_eventually)
qed (simp_all add: asymp_equiv_def)
@@ -1748,10 +1748,10 @@
shows "f \<sim>[F] h"
proof -
let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
- from assms[THEN asymp_equiv_eventually_zeros]
- have "eventually (\<lambda>x. ?T f g x * ?T g h x = ?T f h x) F" by eventually_elim simp
- moreover from tendsto_mult[OF assms[THEN asymp_equivD]]
- have "((\<lambda>x. ?T f g x * ?T g h x) \<longlongrightarrow> 1) F" by simp
+ from tendsto_mult[OF assms[THEN asymp_equivD]]
+ have "((\<lambda>x. ?T f g x * ?T g h x) \<longlongrightarrow> 1) F" by simp
+ moreover from assms[THEN asymp_equiv_eventually_zeros]
+ have "eventually (\<lambda>x. ?T f g x * ?T g h x = ?T f h x) F" by eventually_elim simp
ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually)
qed
@@ -1845,13 +1845,15 @@
shows "(g \<longlongrightarrow> c) F"
proof -
let ?h = "\<lambda>x. (if g x = 0 \<and> f x = 0 then 1 else g x / f x) * f x"
- have "eventually (\<lambda>x. ?h x = g x) F"
- using asymp_equiv_eventually_zeros[OF assms(1)] by eventually_elim simp
- moreover from assms(1) have "g \<sim>[F] f" by (rule asymp_equiv_symI)
+ from assms(1) have "g \<sim>[F] f" by (rule asymp_equiv_symI)
hence "filterlim (\<lambda>x. if g x = 0 \<and> f x = 0 then 1 else g x / f x) (nhds 1) F"
by (rule asymp_equivD)
from tendsto_mult[OF this assms(2)] have "(?h \<longlongrightarrow> c) F" by simp
- ultimately show ?thesis by (rule Lim_transform_eventually)
+ moreover
+ have "eventually (\<lambda>x. ?h x = g x) F"
+ using asymp_equiv_eventually_zeros[OF assms(1)] by eventually_elim simp
+ ultimately show ?thesis
+ by (rule Lim_transform_eventually)
qed
lemma tendsto_asymp_equiv_cong:
@@ -1861,10 +1863,11 @@
{
fix f g :: "'a \<Rightarrow> 'b"
assume *: "f \<sim>[F] g" "(g \<longlongrightarrow> c) F"
+ have "((\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) \<longlongrightarrow> c * 1) F"
+ by (intro tendsto_intros asymp_equivD *)
+ moreover
have "eventually (\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x) = f x) F"
using asymp_equiv_eventually_zeros[OF *(1)] by eventually_elim simp
- moreover have "((\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) \<longlongrightarrow> c * 1) F"
- by (intro tendsto_intros asymp_equivD *)
ultimately have "(f \<longlongrightarrow> c * 1) F"
by (rule Lim_transform_eventually)
}
@@ -1968,11 +1971,11 @@
from assms have "((\<lambda>x. ?T f1 g1 x * ?T f2 g2 x) \<longlongrightarrow> 1 * 1) F"
by (intro tendsto_mult asymp_equivD)
moreover {
- have "eventually (\<lambda>x. ?S x = ?S' x) F"
- using assms[THEN asymp_equiv_eventually_zeros] by eventually_elim auto
- moreover have "(?S \<longlongrightarrow> 0) F"
+ have "(?S \<longlongrightarrow> 0) F"
by (intro filterlim_If assms[THEN A, THEN tendsto_mono[rotated]])
(auto intro: le_infI1 le_infI2)
+ moreover have "eventually (\<lambda>x. ?S x = ?S' x) F"
+ using assms[THEN asymp_equiv_eventually_zeros] by eventually_elim auto
ultimately have "(?S' \<longlongrightarrow> 0) F" by (rule Lim_transform_eventually)
}
ultimately have "(?T (\<lambda>x. f1 x * f2 x) (\<lambda>x. g1 x * g2 x) \<longlongrightarrow> 1 * 1) F"
@@ -2037,12 +2040,12 @@
shows "(\<lambda>x. f x powr y) \<sim>[F] (\<lambda>x. g x powr y)"
proof -
let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
- have "eventually (\<lambda>x. ?T f g x powr y = ?T (\<lambda>x. f x powr y) (\<lambda>x. g x powr y) x) F"
+ have "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1 powr y) F"
+ by (intro tendsto_intros asymp_equivD[OF assms(1)]) simp_all
+ hence "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1) F" by simp
+ moreover have "eventually (\<lambda>x. ?T f g x powr y = ?T (\<lambda>x. f x powr y) (\<lambda>x. g x powr y) x) F"
using asymp_equiv_eventually_zeros[OF assms(1)] assms(2,3)
by eventually_elim (auto simp: powr_divide)
- moreover have "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1 powr y) F"
- by (intro tendsto_intros asymp_equivD[OF assms(1)]) simp_all
- hence "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1) F" by simp
ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually)
qed
--- a/src/HOL/Limits.thy Thu Aug 15 21:18:06 2019 +0200
+++ b/src/HOL/Limits.thy Thu Aug 15 21:46:43 2019 +0200
@@ -1981,7 +1981,7 @@
using Lim_transform Lim_transform2 by blast
lemma Lim_transform_eventually:
- "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f \<longlongrightarrow> l) net \<Longrightarrow> (g \<longlongrightarrow> l) net"
+ "\<lbrakk>(f \<longlongrightarrow> l) F; eventually (\<lambda>x. f x = g x) F\<rbrakk> \<Longrightarrow> (g \<longlongrightarrow> l) F"
using eventually_elim2 by (fastforce simp add: tendsto_def)
lemma Lim_transform_within:
--- a/src/HOL/Probability/Probability_Mass_Function.thy Thu Aug 15 21:18:06 2019 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Thu Aug 15 21:46:43 2019 +0200
@@ -856,7 +856,7 @@
have "integrable (map_pmf (to_nat_on M) M) (\<lambda>n. B)"
by auto
then show "summable (\<lambda>n. pmf (map_pmf (to_nat_on (set_pmf M)) M) n * B)"
- by (simp add: measure_pmf_eq_density integrable_density integrable_count_space_nat_iff summable_rabs_cancel)
+ by (fastforce simp add: measure_pmf_eq_density integrable_density integrable_count_space_nat_iff summable_mult2)
qed
qed simp
qed simp
--- a/src/HOL/Probability/Sinc_Integral.thy Thu Aug 15 21:18:06 2019 +0200
+++ b/src/HOL/Probability/Sinc_Integral.thy Thu Aug 15 21:46:43 2019 +0200
@@ -271,7 +271,7 @@
lemma Si_at_top: "(Si \<longlongrightarrow> pi / 2) at_top"
proof -
- have "\<forall>\<^sub>F t in at_top. pi / 2 - (LBINT u=0..\<infinity>. exp (-(u * t)) * (u * sin t + cos t) / (1 + u^2)) = Si t"
+ have \<dagger>: "\<forall>\<^sub>F t in at_top. pi / 2 - (LBINT u=0..\<infinity>. exp (-(u * t)) * (u * sin t + cos t) / (1 + u^2)) = Si t"
using eventually_ge_at_top[of 0]
proof eventually_elim
fix t :: real assume "t \<ge> 0"
@@ -326,8 +326,8 @@
using Si_at_top_integrable[OF \<open>0\<le>t\<close>] by (simp add: integrable_I0i_1_div_plus_square LBINT_I0i_1_div_plus_square)
finally show "pi / 2 - (LBINT u=0..\<infinity>. exp (-(u * t)) * (u * sin t + cos t) / (1 + u^2)) = Si t" ..
qed
- then show ?thesis
- by (rule Lim_transform_eventually)
+ show ?thesis
+ by (rule Lim_transform_eventually [OF _ \<dagger>])
(auto intro!: tendsto_eq_intros Si_at_top_LBINT)
qed
--- a/src/HOL/Transcendental.thy Thu Aug 15 21:18:06 2019 +0200
+++ b/src/HOL/Transcendental.thy Thu Aug 15 21:46:43 2019 +0200
@@ -4135,6 +4135,15 @@
using that by (auto elim: evenE)
qed
+lemma sin_zero_pi_iff:
+ fixes x::real
+ assumes "\<bar>x\<bar> < pi"
+ shows "sin x = 0 \<longleftrightarrow> x = 0"
+proof
+ show "x = 0" if "sin x = 0"
+ using that assms by (auto simp: sin_zero_iff)
+qed auto
+
lemma cos_zero_iff_int: "cos x = 0 \<longleftrightarrow> (\<exists>n. odd n \<and> x = of_int n * (pi/2))"
proof -
have 1: "\<And>n. odd n \<Longrightarrow> \<exists>i. odd i \<and> real n = real_of_int i"