--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Aug 25 13:01:13 2017 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Aug 25 23:30:36 2017 +0100
@@ -1623,20 +1623,16 @@
unfolding less_cSUP_iff[OF D] by auto
note d' = division_ofD[OF this(1)]
- have "\<forall>x. \<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
- proof
- fix x
- have "\<exists>da>0. \<forall>xa\<in>\<Union>{i \<in> d. x \<notin> i}. da \<le> dist x xa"
+ have "\<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}" for x
+ proof -
+ have "\<exists>d'>0. \<forall>x'\<in>\<Union>{i \<in> d. x \<notin> i}. d' \<le> dist x x'"
proof (rule separate_point_closed)
show "closed (\<Union>{i \<in> d. x \<notin> i})"
- apply (rule closed_Union)
- apply (simp add: d'(1))
- using d'(4) apply auto
- done
+ using d' by force
show "x \<notin> \<Union>{i \<in> d. x \<notin> i}"
by auto
qed
- then show "\<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
+ then show ?thesis
by force
qed
then obtain k where k: "\<And>x. 0 < k x" "\<And>i x. \<lbrakk>i \<in> d; x \<notin> i\<rbrakk> \<Longrightarrow> ball x (k x) \<inter> i = {}"
@@ -1680,8 +1676,7 @@
show "x \<in> K" and "K \<subseteq> cbox a b"
using p'(2-3)[OF il(3)] il by auto
show "\<exists>a b. K = cbox a b"
- unfolding il using p'(4)[OF il(3)] d'(4)[OF il(2)]
- by (meson Int_interval)
+ unfolding il using p'(4)[OF il(3)] d'(4)[OF il(2)] by (meson Int_interval)
next
fix x1 K1
assume "(x1, K1) \<in> p'"
@@ -1710,8 +1705,7 @@
have "x \<in> i"
using fineD[OF p(3) xl(1)] using k(2) i xl by auto
then show ?thesis
- unfolding p'_def
- by (rule_tac X="i \<inter> l" in UnionI) (use i xl in auto)
+ unfolding p'_def by (rule_tac X="i \<inter> l" in UnionI) (use i xl in auto)
qed
show "\<Union>{K. \<exists>x. (x, K) \<in> p'} = cbox a b"
proof
@@ -1738,22 +1732,23 @@
then have sum_less_e2: "(\<Sum>(x,K) \<in> p'. norm (content K *\<^sub>R f x - integral K f)) < e/2"
using g(2) gp' tagged_division_of_def by blast
- have p'alt: "p' = {(x, I \<inter> L) | x I L. (x,L) \<in> p \<and> I \<in> d \<and> I \<inter> L \<noteq> {}}"
+ have XX: "(x, I \<inter> L) \<in> p'" if "(x, L) \<in> p" "I \<in> d" "y \<in> I" "y \<in> L"
+ for x I L y
+ proof -
+ have "x \<in> I"
+ using fineD[OF p(3) that(1)] k(2)[OF that(2), of x] that(3-) by auto
+ then have "(\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> I \<inter> L = i \<inter> l)"
+ using that(1) that(2) by blast
+ then have "(x, I \<inter> L) \<in> p'"
+ by (simp add: p'_def)
+ then show ?thesis
+ using that(3) by auto
+ qed
+ have p'alt: "p' = {(x, I \<inter> L) | x I L. (x,L) \<in> p \<and> I \<in> d \<and> I \<inter> L \<noteq> {}}"
proof (safe, goal_cases)
case prems: (2 _ _ x i l)
- have "x \<in> i"
- using fineD[OF p(3) prems(1)] k(2)[OF prems(2), of x] prems(4-)
- by auto
- then have "(x, i \<inter> l) \<in> p'"
- unfolding p'_def
- using prems
- apply safe
- apply (rule_tac x=x in exI)
- apply (rule_tac x="i \<inter> l" in exI)
- apply auto
- done
then show ?case
- using prems(3) by auto
+ using XX by auto
next
fix x K
assume "(x, K) \<in> p'"
@@ -2027,14 +2022,13 @@
then show False
using prems by auto
qed
- then obtain K where *: "\<exists>x\<in>{d. d division_of \<Union>d}. K = (\<Sum>k\<in>x. norm (integral k f))"
+ then obtain d K where ddiv: "d division_of \<Union>d" and "K = (\<Sum>k\<in>d. norm (integral k f))"
"SUPREMUM {d. d division_of \<Union>d} (sum (\<lambda>k. norm (integral k f))) - e < K"
by (auto simp add: image_iff not_le)
- from this(1) obtain d where "d division_of \<Union>d"
- and "K = (\<Sum>k\<in>d. norm (integral k f))"
+ then have d: "SUPREMUM {d. d division_of \<Union>d} (sum (\<lambda>k. norm (integral k f))) - e
+ < (\<Sum>k\<in>d. norm (integral k f))"
by auto
- note d = this(1) *(2)[unfolded this(2)]
- note d'=division_ofD[OF this(1)]
+ note d'=division_ofD[OF ddiv]
have "bounded (\<Union>d)"
by (rule elementary_bounded,fact)
from this[unfolded bounded_pos] obtain K where
@@ -2051,7 +2045,7 @@
unfolding real_norm_def
apply (rule *[rule_format])
apply safe
- apply (rule d(2))
+ apply (rule d)
proof goal_cases
case 1
have "(\<Sum>k\<in>d. norm (integral k f)) \<le> sum (\<lambda>k. integral k (\<lambda>x. norm (f x))) d"
@@ -2061,31 +2055,15 @@
by (auto simp: absolutely_integrable_on_def integral_norm_bound_integral)
done
also have "\<dots> = integral (\<Union>d) (\<lambda>x. norm (f x))"
- apply (rule integral_combine_division_bottomup[symmetric])
- apply (rule d)
- unfolding forall_in_division[OF d(1)]
- using f_int unfolding absolutely_integrable_on_def
- apply auto
- done
+ apply (rule integral_combine_division_bottomup[OF ddiv, symmetric])
+ using absolutely_integrable_on_def d'(4) f_int by blast
also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0)"
proof -
have "\<Union>d \<subseteq> cbox a b"
- apply rule
- apply (drule K(2)[rule_format])
- apply (rule ab[unfolded subset_eq,rule_format])
- apply (auto simp add: dist_norm)
- done
+ using K(2) ab by fastforce
then show ?thesis
- apply -
- apply (subst if_P)
- apply rule
- apply (rule integral_subset_le)
- defer
- apply (rule integrable_on_subdivision[of _ _ _ "cbox a b"])
- apply (rule d)
- using f_int[of a b] unfolding absolutely_integrable_on_def
- apply auto
- done
+ using integrable_on_subdivision[OF ddiv] f_int[of a b] unfolding absolutely_integrable_on_def
+ by (auto intro!: integral_subset_le)
qed
finally show ?case .
next
@@ -2119,11 +2097,7 @@
show "\<bar>(\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm(f x))\<bar> < e/2"
using d1[OF p(1,2)] by (simp only: real_norm_def)
show "(\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) = (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x))"
- apply (rule sum.cong)
- apply (rule refl)
- unfolding split_paired_all split_conv
- apply (drule tagged_division_ofD(4)[OF p(1)])
- by simp
+ by (auto simp: split_paired_all sum.cong [OF refl])
show "(\<Sum>(x,k) \<in> p. norm (integral k f)) \<le> ?S"
using partial_division_of_tagged_division[of p "cbox a b"] p(1)
apply (subst sum.over_tagged_division_lemma[OF p(1)])
--- a/src/HOL/Analysis/Gamma_Function.thy Fri Aug 25 13:01:13 2017 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy Fri Aug 25 23:30:36 2017 +0100
@@ -719,22 +719,22 @@
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])
- show "eventually (\<lambda>n. of_real (ln (real n / (real n + 1))) =
+ 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)
qed
from summable_Digamma[OF z]
- have "(\<lambda>n. inverse (of_nat (n+1)) - inverse (z + of_nat n))
+ have "(\<lambda>n. inverse (of_nat (n+1)) - inverse (z + of_nat n))
sums (Digamma z + euler_mascheroni)"
by (simp add: Digamma_def summable_sums)
from sums_diff[OF this euler_mascheroni_sum]
have "(\<lambda>n. of_real (ln (real (Suc n) + 1)) - of_real (ln (real n + 1)) - inverse (z + of_nat n))
sums Digamma z" by (simp add: add_ac)
- hence "(\<lambda>m. (\<Sum>n<m. of_real (ln (real (Suc n) + 1)) - of_real (ln (real n + 1))) -
+ hence "(\<lambda>m. (\<Sum>n<m. of_real (ln (real (Suc n) + 1)) - of_real (ln (real n + 1))) -
(\<Sum>n<m. inverse (z + of_nat n))) \<longlonglongrightarrow> Digamma z"
by (simp add: sums_def sum_subtractf)
- also have "(\<lambda>m. (\<Sum>n<m. of_real (ln (real (Suc n) + 1)) - of_real (ln (real n + 1)))) =
+ also have "(\<lambda>m. (\<Sum>n<m. of_real (ln (real (Suc n) + 1)) - of_real (ln (real n + 1)))) =
(\<lambda>m. of_real (ln (m + 1)) :: 'a)"
by (subst sum_lessThan_telescope) simp_all
finally show ?thesis by (rule Lim_transform) (insert lim, simp)
@@ -977,17 +977,17 @@
shows "A \<inter> \<real>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> continuous_on A ln_Gamma"
by (intro continuous_at_imp_continuous_on ballI isCont_ln_Gamma_complex[OF continuous_ident])
fastforce
-
+
lemma deriv_Polygamma:
assumes "z \<notin> \<int>\<^sub>\<le>\<^sub>0"
- shows "deriv (Polygamma m) z =
+ shows "deriv (Polygamma m) z =
Polygamma (Suc m) (z :: 'a :: {real_normed_field,euclidean_space})"
by (intro DERIV_imp_deriv has_field_derivative_Polygamma assms)
thm has_field_derivative_Polygamma
lemma higher_deriv_Polygamma:
assumes "z \<notin> \<int>\<^sub>\<le>\<^sub>0"
- shows "(deriv ^^ n) (Polygamma m) z =
+ shows "(deriv ^^ n) (Polygamma m) z =
Polygamma (m + n) (z :: 'a :: {real_normed_field,euclidean_space})"
proof -
have "eventually (\<lambda>u. (deriv ^^ n) (Polygamma m) u = Polygamma (m + n) u) (nhds z)"
@@ -995,7 +995,7 @@
case (Suc n)
from Suc.IH have "eventually (\<lambda>z. eventually (\<lambda>u. (deriv ^^ n) (Polygamma m) u = Polygamma (m + n) u) (nhds z)) (nhds z)"
by (simp add: eventually_eventually)
- hence "eventually (\<lambda>z. deriv ((deriv ^^ n) (Polygamma m)) z =
+ hence "eventually (\<lambda>z. deriv ((deriv ^^ n) (Polygamma m)) z =
deriv (Polygamma (m + n)) z) (nhds z)"
by eventually_elim (intro deriv_cong_ev refl)
moreover have "eventually (\<lambda>z. z \<in> UNIV - \<int>\<^sub>\<le>\<^sub>0) (nhds z)" using assms
@@ -1478,9 +1478,9 @@
lemma analytic_Gamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Gamma analytic_on A"
by (rule analytic_on_subset[of _ "UNIV - \<int>\<^sub>\<le>\<^sub>0"], subst analytic_on_open)
(auto intro!: holomorphic_Gamma)
-
-
-lemma field_differentiable_ln_Gamma_complex:
+
+
+lemma field_differentiable_ln_Gamma_complex:
"z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> ln_Gamma field_differentiable (at (z::complex) within A)"
by (rule field_differentiable_within_subset[of _ _ UNIV])
(force simp: field_differentiable_def intro!: derivative_intros)+
@@ -1648,8 +1648,8 @@
lemma ln_Gamma_complex_conv_fact: "n > 0 \<Longrightarrow> ln_Gamma (of_nat n :: complex) = ln (fact (n - 1))"
using ln_Gamma_complex_of_real[of "real n"] Gamma_fact[of "n - 1", where 'a = real]
- by (simp add: ln_Gamma_real_pos of_nat_diff Ln_of_real [symmetric])
-
+ by (simp add: ln_Gamma_real_pos of_nat_diff Ln_of_real [symmetric])
+
lemma ln_Gamma_real_conv_fact: "n > 0 \<Longrightarrow> ln_Gamma (real n) = ln (fact (n - 1))"
using Gamma_fact[of "n - 1", where 'a = real]
by (simp add: ln_Gamma_real_pos of_nat_diff Ln_of_real [symmetric])
@@ -1668,14 +1668,14 @@
show "eventually (\<lambda>y. ln_Gamma y = (Re \<circ> ln_Gamma \<circ> of_real) y) (nhds x)"
by (auto elim!: eventually_mono simp: ln_Gamma_complex_of_real interior_open)
qed
-
-lemma field_differentiable_ln_Gamma_real:
+
+lemma field_differentiable_ln_Gamma_real:
"x > 0 \<Longrightarrow> ln_Gamma field_differentiable (at (x::real) within A)"
by (rule field_differentiable_within_subset[of _ _ UNIV])
(auto simp: field_differentiable_def intro!: derivative_intros)+
declare has_field_derivative_ln_Gamma_real[THEN DERIV_chain2, derivative_intros]
-
+
lemma deriv_ln_Gamma_real:
assumes "z > 0"
shows "deriv ln_Gamma z = Digamma (z :: real)"
@@ -1785,12 +1785,12 @@
subsection \<open>The uniqueness of the real Gamma function\<close>
text \<open>
- The following is a proof of the Bohr--Mollerup theorem, which states that
+ The following is a proof of the Bohr--Mollerup theorem, which states that
any log-convex function $G$ on the positive reals that fulfils $G(1) = 1$ and
- satisfies the functional equation $G(x+1) = x G(x)$ must be equal to the
+ satisfies the functional equation $G(x+1) = x G(x)$ must be equal to the
Gamma function.
- In principle, if $G$ is a holomorphic complex function, one could then extend
- this from the positive reals to the entire complex plane (minus the non-positive
+ In principle, if $G$ is a holomorphic complex function, one could then extend
+ this from the positive reals to the entire complex plane (minus the non-positive
integers, where the Gamma function is not defined).
\<close>
@@ -1809,7 +1809,7 @@
private definition S :: "real \<Rightarrow> real \<Rightarrow> real" where
"S x y = (ln (G y) - ln (G x)) / (y - x)"
-private lemma S_eq:
+private lemma S_eq:
"n \<ge> 2 \<Longrightarrow> S (of_nat n) (of_nat n + x) = (ln (G (real n + x)) - ln (fact (n - 1))) / x"
by (subst G_fact [symmetric]) (simp add: S_def add_ac of_nat_diff)
@@ -1821,16 +1821,16 @@
(ln \<circ> G) (real (Suc n) - 1)) / (real (Suc n) + x - (real (Suc n) - 1)) *
(real (Suc n) - (real (Suc n) - 1)) + (ln \<circ> G) (real (Suc n) - 1)"
using x n by (intro convex_onD_Icc' convex_on_subset[OF log_convex_G]) auto
- hence "S (of_nat n) (of_nat (Suc n)) \<le> S (of_nat (Suc n)) (of_nat (Suc n) + x)"
+ hence "S (of_nat n) (of_nat (Suc n)) \<le> S (of_nat (Suc n)) (of_nat (Suc n) + x)"
unfolding S_def using x by (simp add: field_simps)
also have "S (of_nat n) (of_nat (Suc n)) = ln (fact n) - ln (fact (n-1))"
- unfolding S_def using n
+ unfolding S_def using n
by (subst (1 2) G_fact [symmetric]) (simp_all add: add_ac of_nat_diff)
also have "\<dots> = ln (fact n / fact (n-1))" by (subst ln_div) simp_all
also from n have "fact n / fact (n - 1) = n" by (cases n) simp_all
finally have "x * ln (real n) + ln (fact n) \<le> ln (G (real (Suc n) + x))"
using x n by (subst (asm) S_eq) (simp_all add: field_simps)
- also have "x * ln (real n) + ln (fact n) = ln (exp (x * ln (real n)) * fact n)"
+ also have "x * ln (real n) + ln (fact n) = ln (exp (x * ln (real n)) * fact n)"
using x by (simp add: ln_mult)
finally have "exp (x * ln (real n)) * fact n \<le> G (real (Suc n) + x)" using x
by (subst (asm) ln_le_cancel_iff) (simp_all add: G_pos)
@@ -1847,15 +1847,15 @@
proof -
have "(ln \<circ> G) (real n + x) \<le> ((ln \<circ> G) (real n + 1) -
(ln \<circ> G) (real n)) / (real n + 1 - (real n)) *
- ((real n + x) - real n) + (ln \<circ> G) (real n)"
+ ((real n + x) - real n) + (ln \<circ> G) (real n)"
using x n by (intro convex_onD_Icc' convex_on_subset[OF log_convex_G]) auto
- hence "S (of_nat n) (of_nat n + x) \<le> S (of_nat n) (of_nat n + 1)"
+ hence "S (of_nat n) (of_nat n + x) \<le> S (of_nat n) (of_nat n + 1)"
unfolding S_def using x by (simp add: field_simps)
also from n have "S (of_nat n) (of_nat n + 1) = ln (fact n) - ln (fact (n-1))"
by (subst (1 2) G_fact [symmetric]) (simp add: S_def add_ac of_nat_diff)
also have "\<dots> = ln (fact n / (fact (n-1)))" using n by (subst ln_div) simp_all
also from n have "fact n / fact (n - 1) = n" by (cases n) simp_all
- finally have "ln (G (real n + x)) \<le> x * ln (real n) + ln (fact (n - 1))"
+ finally have "ln (G (real n + x)) \<le> x * ln (real n) + ln (fact (n - 1))"
using x n by (subst (asm) S_eq) (simp_all add: field_simps)
also have "\<dots> = ln (exp (x * ln (real n)) * fact (n - 1))" using x
by (simp add: ln_mult)
@@ -1867,7 +1867,7 @@
finally have "G x \<le> exp (x * ln (real n)) * fact (n- 1) / pochhammer x n"
using x by (simp add: field_simps pochhammer_pos)
also from n have "fact (n - 1) = fact n / n" by (cases n) simp_all
- also have "exp (x * ln (real n)) * \<dots> / pochhammer x n =
+ also have "exp (x * ln (real n)) * \<dots> / pochhammer x n =
Gamma_series x n * (1 + x / real n)" using n x
by (simp add: Gamma_series_def divide_simps pochhammer_Suc)
finally show ?thesis .
@@ -1886,7 +1886,7 @@
show "G x \<le> Gamma x"
proof (rule tendsto_lowerbound)
have "(\<lambda>n. Gamma_series x n * (1 + x / real n)) \<longlonglongrightarrow> Gamma x * (1 + 0)"
- by (rule tendsto_intros real_tendsto_divide_at_top
+ by (rule tendsto_intros real_tendsto_divide_at_top
Gamma_series_LIMSEQ filterlim_real_sequentially)+
thus "(\<lambda>n. Gamma_series x n * (1 + x / real n)) \<longlonglongrightarrow> Gamma x" by simp
next
@@ -1907,7 +1907,7 @@
with Suc show ?case using G_plus1[of "real n + x"] Gamma_plus1[of "real n + x"]
by (auto simp: add_ac)
qed (simp_all add: G_eq_Gamma_aux)
-
+
show ?thesis
proof (cases "frac x = 0")
case True
@@ -2129,9 +2129,9 @@
also have "g \<circ> (\<lambda>x. x - of_int n) = g" by (intro ext) (simp add: g.minus_of_int)
finally show "(g has_field_derivative (h z * g z)) (at z)" by (simp add: z h_def)
qed
-
+
have g_holo [holomorphic_intros]: "g holomorphic_on A" for A
- by (rule holomorphic_on_subset[of _ UNIV])
+ by (rule holomorphic_on_subset[of _ UNIV])
(force simp: holomorphic_on_open intro!: derivative_intros)+
have g_eq: "g (z/2) * g ((z+1)/2) = Gamma (1/2)^2 * g z" if "Re z > -1" "Re z < 2" for z
@@ -2193,10 +2193,10 @@
have g_nz [simp]: "g z \<noteq> 0" for z :: complex
unfolding g_def using Ints_diff[of 1 "1 - z"]
by (auto simp: Gamma_eq_zero_iff sin_eq_0 dest!: nonpos_Ints_Int)
-
+
have h_altdef: "h z = deriv g z / g z" for z :: complex
using DERIV_imp_deriv[OF g_g', of z] by simp
-
+
have h_eq: "h z = (h (z/2) + h ((z+1)/2)) / 2" for z
proof -
have "((\<lambda>t. g (t/2) * g ((t+1)/2)) has_field_derivative
@@ -2485,7 +2485,7 @@
let ?r' = "\<lambda>n. exp (z * of_real (ln (of_nat (Suc n) / of_nat n)))"
from z have z': "z \<noteq> 0" by auto
- have "eventually (\<lambda>n. ?r' n = ?r n) sequentially"
+ have "eventually (\<lambda>n. ?r' n = ?r n) sequentially"
using z by (auto simp: divide_simps Gamma_series_def ring_distribs exp_diff ln_div add_ac
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))"
@@ -2711,7 +2711,7 @@
have "f integrable_on {c..}"
by (rule integrable_spike_finite[of "{c}", OF _ _ A]) (simp_all add: f_def)
ultimately show "f integrable_on {0..}"
- by (rule integrable_union') (insert c, auto simp: max_def)
+ by (rule integrable_Un') (insert c, auto simp: max_def)
qed
lemma Gamma_integral_complex:
@@ -2948,9 +2948,9 @@
theorem wallis: "(\<lambda>n. \<Prod>k=1..n. (4*real k^2) / (4*real k^2 - 1)) \<longlonglongrightarrow> pi / 2"
proof -
- from tendsto_inverse[OF tendsto_mult[OF
+ from tendsto_inverse[OF tendsto_mult[OF
sin_product_formula_real[of "1/2"] tendsto_const[of "2/pi"]]]
- have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) \<longlonglongrightarrow> pi/2"
+ have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) \<longlonglongrightarrow> pi/2"
by (simp add: prod_inversef [symmetric])
also have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) =
(\<lambda>n. (\<Prod>k=1..n. (4*real k^2)/(4*real k^2 - 1)))"
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Aug 25 13:01:13 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Aug 25 23:30:36 2017 +0100
@@ -1,5 +1,6 @@
(* Author: John Harrison
- Author: Robert Himmelmann, TU Muenchen (Translation from HOL light); proofs reworked by LCP
+ Author: Robert Himmelmann, TU Muenchen (Translation from HOL light)
+ Huge cleanup by LCP
*)
section \<open>Henstock-Kurzweil gauge integration in many dimensions.\<close>
@@ -165,23 +166,23 @@
qed
lemma division_of_content_0:
- assumes "content (cbox a b) = 0" "d division_of (cbox a b)"
- shows "\<forall>k\<in>d. content k = 0"
+ assumes "content (cbox a b) = 0" "d division_of (cbox a b)" "K \<in> d"
+ shows "content K = 0"
unfolding forall_in_division[OF assms(2)]
- by (metis antisym_conv assms content_pos_le content_subset division_ofD(2))
+ by (meson assms content_0_subset division_of_def)
lemma sum_content_null:
assumes "content (cbox a b) = 0"
and "p tagged_division_of (cbox a b)"
- shows "(\<Sum>(x,k)\<in>p. content k *\<^sub>R f x) = (0::'a::real_normed_vector)"
+ shows "(\<Sum>(x,K)\<in>p. content K *\<^sub>R f x) = (0::'a::real_normed_vector)"
proof (rule sum.neutral, rule)
fix y
assume y: "y \<in> p"
- obtain x k where xk: "y = (x, k)"
+ obtain x K where xk: "y = (x, K)"
using surj_pair[of y] by blast
- then obtain c d where k: "k = cbox c d" "k \<subseteq> cbox a b"
+ then obtain c d where k: "K = cbox c d" "K \<subseteq> cbox a b"
by (metis assms(2) tagged_division_ofD(3) tagged_division_ofD(4) y)
- have "(\<lambda>(x, k). content k *\<^sub>R f x) y = content k *\<^sub>R f x"
+ have "(\<lambda>(x',K'). content K' *\<^sub>R f x') y = content K *\<^sub>R f x"
unfolding xk by auto
also have "\<dots> = 0"
using assms(1) content_0_subset k(2) by auto
@@ -5337,11 +5338,10 @@
subsection \<open>Adding integrals over several sets\<close>
-lemma has_integral_union:
+lemma has_integral_Un:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
- assumes "(f has_integral i) s"
- and "(f has_integral j) t"
- and "negligible (s \<inter> t)"
+ assumes f: "(f has_integral i) s" "(f has_integral j) t"
+ and neg: "negligible (s \<inter> t)"
shows "(f has_integral (i + j)) (s \<union> t)"
proof -
note * = has_integral_restrict_UNIV[symmetric, of f]
@@ -5349,28 +5349,28 @@
unfolding *
apply (rule has_integral_spike[OF assms(3)])
defer
- apply (rule has_integral_add[OF assms(1-2)[unfolded *]])
+ apply (rule has_integral_add[OF f[unfolded *]])
apply auto
done
qed
-lemma integrable_union:
+lemma integrable_Un:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b :: banach"
assumes "negligible (A \<inter> B)" "f integrable_on A" "f integrable_on B"
shows "f integrable_on (A \<union> B)"
proof -
from assms obtain y z where "(f has_integral y) A" "(f has_integral z) B"
by (auto simp: integrable_on_def)
- from has_integral_union[OF this assms(1)] show ?thesis by (auto simp: integrable_on_def)
+ from has_integral_Un[OF this assms(1)] show ?thesis by (auto simp: integrable_on_def)
qed
-lemma integrable_union':
+lemma integrable_Un':
fixes f :: "'a::euclidean_space \<Rightarrow> 'b :: banach"
assumes "f integrable_on A" "f integrable_on B" "negligible (A \<inter> B)" "C = A \<union> B"
shows "f integrable_on C"
- using integrable_union[of A B f] assms by simp
-
-lemma has_integral_unions:
+ using integrable_Un[of A B f] assms by simp
+
+lemma has_integral_Union:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
assumes "finite t"
and "\<forall>s\<in>t. (f has_integral (i s)) s"
@@ -5401,22 +5401,12 @@
then show ?case
proof (cases "x \<in> \<Union>t")
case True
- then guess s unfolding Union_iff..note s=this
- then have *: "\<forall>b\<in>t. x \<in> b \<longleftrightarrow> b = s"
+ then obtain s where "s \<in> t" "x \<in> s"
+ by blast
+ moreover then have "\<forall>b\<in>t. x \<in> b \<longleftrightarrow> b = s"
using prems(3) by blast
- show ?thesis
- unfolding if_P[OF True]
- apply (rule trans)
- defer
- apply (rule sum.cong)
- apply (rule refl)
- apply (subst *)
- apply assumption
- apply (rule refl)
- unfolding sum.delta[OF assms(1)]
- using s
- apply auto
- done
+ ultimately show ?thesis
+ by (simp add: sum.delta[OF assms(1)])
qed auto
qed
qed
@@ -5426,36 +5416,29 @@
lemma has_integral_combine_division:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
- assumes "d division_of s"
- and "\<forall>k\<in>d. (f has_integral (i k)) k"
- shows "(f has_integral (sum i d)) s"
+ assumes "d division_of S"
+ and "\<And>k. k \<in> d \<Longrightarrow> (f has_integral (i k)) k"
+ shows "(f has_integral (sum i d)) S"
proof -
note d = division_ofD[OF assms(1)]
+ have neg: "negligible (S \<inter> s')" if "S \<in> d" "s' \<in> d" "S \<noteq> s'" for S s'
+ proof -
+ obtain a c b d where obt: "S = cbox a b" "s' = cbox c d"
+ by (meson \<open>S \<in> d\<close> \<open>s' \<in> d\<close> d(4))
+ from d(5)[OF that] show ?thesis
+ unfolding obt interior_cbox
+ by (metis (no_types, lifting) Diff_empty Int_interval box_Int_box negligible_frontier_interval)
+ qed
show ?thesis
unfolding d(6)[symmetric]
- apply (rule has_integral_unions)
- apply (rule d assms)+
- apply rule
- apply rule
- apply rule
- proof goal_cases
- case prems: (1 s s')
- from d(4)[OF this(1)] d(4)[OF this(2)] guess a c b d by (elim exE) note obt=this
- from d(5)[OF prems] show ?case
- unfolding obt interior_cbox
- apply -
- apply (rule negligible_subset[of "(cbox a b-box a b) \<union> (cbox c d-box c d)"])
- apply (rule negligible_Un negligible_frontier_interval)+
- apply auto
- done
- qed
+ by (auto intro: d neg assms has_integral_Union)
qed
lemma integral_combine_division_bottomup:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
- assumes "d division_of s"
- and "\<forall>k\<in>d. f integrable_on k"
- shows "integral s f = sum (\<lambda>i. integral i f) d"
+ assumes "d division_of S"
+ and "\<And>k. k \<in> d \<Longrightarrow> f integrable_on k"
+ shows "integral S f = sum (\<lambda>i. integral i f) d"
apply (rule integral_unique)
apply (rule has_integral_combine_division[OF assms(1)])
using assms(2)
@@ -5465,12 +5448,11 @@
lemma has_integral_combine_division_topdown:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
- assumes "f integrable_on s"
+ assumes "f integrable_on S"
and "d division_of k"
- and "k \<subseteq> s"
+ and "k \<subseteq> S"
shows "(f has_integral (sum (\<lambda>i. integral i f) d)) k"
apply (rule has_integral_combine_division[OF assms(2)])
- apply safe
unfolding has_integral_integral[symmetric]
proof goal_cases
case (1 k)
@@ -5486,9 +5468,9 @@
lemma integral_combine_division_topdown:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
- assumes "f integrable_on s"
- and "d division_of s"
- shows "integral s f = sum (\<lambda>i. integral i f) d"
+ assumes "f integrable_on S"
+ and "d division_of S"
+ shows "integral S f = sum (\<lambda>i. integral i f) d"
apply (rule integral_unique)
apply (rule has_integral_combine_division_topdown)
using assms
@@ -5497,9 +5479,9 @@
lemma integrable_combine_division:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
- assumes "d division_of s"
+ assumes "d division_of S"
and "\<forall>i\<in>d. f integrable_on i"
- shows "f integrable_on s"
+ shows "f integrable_on S"
using assms(2)
unfolding integrable_on_def
by (metis has_integral_combine_division[OF assms(1)])
@@ -5507,8 +5489,8 @@
lemma integrable_on_subdivision:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
assumes "d division_of i"
- and "f integrable_on s"
- and "i \<subseteq> s"
+ and "f integrable_on S"
+ and "i \<subseteq> S"
shows "f integrable_on i"
apply (rule integrable_combine_division assms)+
apply safe
@@ -5526,16 +5508,16 @@
subsection \<open>Also tagged divisions\<close>
-lemma has_integral_iff: "(f has_integral i) s \<longleftrightarrow> (f integrable_on s \<and> integral s f = i)"
+lemma has_integral_iff: "(f has_integral i) S \<longleftrightarrow> (f integrable_on S \<and> integral S f = i)"
by blast
lemma has_integral_combine_tagged_division:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
- assumes "p tagged_division_of s"
+ assumes "p tagged_division_of S"
and "\<forall>(x,k) \<in> p. (f has_integral (i k)) k"
- shows "(f has_integral (\<Sum>(x,k)\<in>p. i k)) s"
+ shows "(f has_integral (\<Sum>(x,k)\<in>p. i k)) S"
proof -
- have *: "(f has_integral (\<Sum>k\<in>snd`p. integral k f)) s"
+ have *: "(f has_integral (\<Sum>k\<in>snd`p. integral k f)) S"
using assms(2)
apply (intro has_integral_combine_division)
apply (auto simp: has_integral_integral[symmetric] intro: division_of_tagged_division[OF assms(1)])
@@ -5603,8 +5585,9 @@
note p' = tagged_partial_division_ofD[OF p(1)]
have "\<Union>(snd ` p) \<subseteq> cbox a b"
using p'(3) by fastforce
- note partial_division_of_tagged_division[OF p(1)] this
- from partial_division_extend_interval[OF this] guess q . note q=this and q' = division_ofD[OF this(2)]
+ then obtain q where q: "snd ` p \<subseteq> q" "q division_of cbox a b"
+ by (meson p(1) partial_division_extend_interval partial_division_of_tagged_division)
+ note q' = division_ofD[OF this(2)]
define r where "r = q - snd ` p"
have "snd ` p \<inter> r = {}"
unfolding r_def by auto