author paulson Fri, 25 Aug 2017 23:30:36 +0100 changeset 66512 89b6455b63b6 parent 66509 65b6d48fc9a9 child 66513 ca8b18baf0e0
starting to unscramble bounded_variation_absolutely_integrable_interval
```--- 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```