# HG changeset patch
# User eberlm
# Date 1465832392 -7200
# Node ID 3951a15a05d1285f423ee10399d3828035f09fa6
# Parent  52792bb9126e34f84a487359aa22cc067c922e56
Integral form of Gamma function

diff -r 52792bb9126e -r 3951a15a05d1 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Jun 13 15:23:12 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Jun 13 17:39:52 2016 +0200
@@ -1588,8 +1588,8 @@
 
 lemma powr_of_real:
   fixes x::real and y::real
-  shows "0 < x \<Longrightarrow> of_real x powr (of_real y::complex) = of_real (x powr y)"
-  by (simp add: powr_def) (metis exp_of_real of_real_mult Ln_of_real)
+  shows "0 \<le> x \<Longrightarrow> of_real x powr (of_real y::complex) = of_real (x powr y)"
+  by (simp_all add: powr_def exp_eq_polar)
 
 lemma norm_powr_real_mono:
     "\<lbrakk>w \<in> \<real>; 1 < Re w\<rbrakk>
diff -r 52792bb9126e -r 3951a15a05d1 src/HOL/Multivariate_Analysis/Gamma.thy
--- a/src/HOL/Multivariate_Analysis/Gamma.thy	Mon Jun 13 15:23:12 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Gamma.thy	Mon Jun 13 17:39:52 2016 +0200
@@ -2604,6 +2604,211 @@
 qed
 
 
+subsubsection \<open>Integral form\<close>
+
+lemma integrable_Gamma_integral_bound:
+  fixes a c :: real
+  assumes a: "a > -1" and c: "c \<ge> 0"
+  defines "f \<equiv> \<lambda>x. if x \<in> {0..c} then x powr a else exp (-x/2)"
+  shows   "f integrable_on {0..}"
+proof -
+  have "f integrable_on {0..c}"
+    by (rule integrable_spike_finite[of "{}", OF _ _ integrable_on_powr_from_0[of a c]])
+       (insert a c, simp_all add: f_def)
+  moreover have A: "(\<lambda>x. exp (-x/2)) integrable_on {c..}"
+    using integrable_on_exp_minus_to_infinity[of "1/2"] by simp
+  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)
+qed  
+
+lemma Gamma_integral_complex:
+  assumes z: "Re z > 0"
+  shows   "((\<lambda>t. of_real t powr (z - 1) / of_real (exp t)) has_integral Gamma z) {0..}"
+proof -
+  have A: "((\<lambda>t. (of_real t) powr (z - 1) * of_real ((1 - t) ^ n))
+          has_integral (fact n / pochhammer z (n+1))) {0..1}"
+    if "Re z > 0" for n z using that
+  proof (induction n arbitrary: z)
+    case 0
+    have "((\<lambda>t. complex_of_real t powr (z - 1)) has_integral
+            (of_real 1 powr z / z - of_real 0 powr z / z)) {0..1}" using 0
+      by (intro fundamental_theorem_of_calculus_interior)
+         (auto intro!: continuous_intros derivative_eq_intros has_vector_derivative_real_complex)
+    thus ?case by simp
+  next
+    case (Suc n)
+    let ?f = "\<lambda>t. complex_of_real t powr z / z"
+    let ?f' = "\<lambda>t. complex_of_real t powr (z - 1)"
+    let ?g = "\<lambda>t. (1 - complex_of_real t) ^ Suc n"
+    let ?g' = "\<lambda>t. - ((1 - complex_of_real t) ^ n) * of_nat (Suc n)"
+    have "((\<lambda>t. ?f' t * ?g t) has_integral
+            (of_nat (Suc n)) * fact n / pochhammer z (n+2)) {0..1}"
+      (is "(_ has_integral ?I) _")
+    proof (rule integration_by_parts_interior[where f' = ?f' and g = ?g])
+      from Suc.prems show "continuous_on {0..1} ?f" "continuous_on {0..1} ?g"
+        by (auto intro!: continuous_intros)
+    next
+      fix t :: real assume t: "t \<in> {0<..<1}"
+      show "(?f has_vector_derivative ?f' t) (at t)" using t Suc.prems
+        by (auto intro!: derivative_eq_intros has_vector_derivative_real_complex)
+      show "(?g has_vector_derivative ?g' t) (at t)"
+        by (rule has_vector_derivative_real_complex derivative_eq_intros refl)+ simp_all
+    next
+      from Suc.prems have [simp]: "z \<noteq> 0" by auto
+      from Suc.prems have A: "Re (z + of_nat n) > 0" for n by simp
+      have [simp]: "z + of_nat n \<noteq> 0" "z + 1 + of_nat n \<noteq> 0" for n
+        using A[of n] A[of "Suc n"] by (auto simp add: add.assoc simp del: plus_complex.sel)
+      have "((\<lambda>x. of_real x powr z * of_real ((1 - x) ^ n) * (- of_nat (Suc n) / z)) has_integral
+              fact n / pochhammer (z+1) (n+1) * (- of_nat (Suc n) / z)) {0..1}"
+        (is "(?A has_integral ?B) _")
+        using Suc.IH[of "z+1"] Suc.prems by (intro has_integral_mult_left) (simp_all add: add_ac pochhammer_rec)
+      also have "?A = (\<lambda>t. ?f t * ?g' t)" by (intro ext) (simp_all add: field_simps)
+      also have "?B = - (of_nat (Suc n) * fact n / pochhammer z (n+2))"
+        by (simp add: divide_simps setprod_nat_ivl_1_Suc pochhammer_rec
+              setprod_shift_bounds_cl_Suc_ivl del: of_nat_Suc)
+      finally show "((\<lambda>t. ?f t * ?g' t) has_integral (?f 1 * ?g 1 - ?f 0 * ?g 0 - ?I)) {0..1}"
+        by simp
+    qed (simp_all add: bounded_bilinear_mult)
+    thus ?case by simp
+  qed
+
+  have B: "((\<lambda>t. if t \<in> {0..of_nat n} then
+             of_real t powr (z - 1) * (1 - of_real t / of_nat n) ^ n else 0)
+           has_integral (of_nat n powr z * fact n / pochhammer z (n+1))) {0..}" for n
+  proof (cases "n > 0")
+    case [simp]: True
+    hence [simp]: "n \<noteq> 0" by auto
+    with has_integral_affinity01[OF A[OF z, of n], of "inverse (of_nat n)" 0]
+      have "((\<lambda>x. (of_nat n - of_real x) ^ n * (of_real x / of_nat n) powr (z - 1) / of_nat n ^ n)
+              has_integral fact n * of_nat n / pochhammer z (n+1)) ((\<lambda>x. real n * x)`{0..1})"
+      (is "(?f has_integral ?I) ?ivl") by (simp add: field_simps scaleR_conv_of_real)
+    also from True have "((\<lambda>x. real n*x)`{0..1}) = {0..real n}"
+      by (subst image_mult_atLeastAtMost) simp_all
+    also have "?f = (\<lambda>x. (of_real x / of_nat n) powr (z - 1) * (1 - of_real x / of_nat n) ^ n)"
+      using True by (intro ext) (simp add: field_simps)
+    finally have "((\<lambda>x. (of_real x / of_nat n) powr (z - 1) * (1 - of_real x / of_nat n) ^ n)
+                    has_integral ?I) {0..real n}" (is ?P) .
+    also have "?P \<longleftrightarrow> ((\<lambda>x. exp ((z - 1) * of_real (ln (x / of_nat n))) * (1 - of_real x / of_nat n) ^ n)
+                        has_integral ?I) {0..real n}"
+      by (intro has_integral_spike_finite_eq[of "{0}"]) (auto simp: powr_def Ln_of_real [symmetric])
+    also have "\<dots> \<longleftrightarrow> ((\<lambda>x. exp ((z - 1) * of_real (ln x - ln (of_nat n))) * (1 - of_real x / of_nat n) ^ n)
+                        has_integral ?I) {0..real n}"
+      by (intro has_integral_spike_finite_eq[of "{0}"]) (simp_all add: ln_div)
+    finally have \<dots> .
+    note B = has_integral_mult_right[OF this, of "exp ((z - 1) * ln (of_nat n))"]
+    have "((\<lambda>x. exp ((z - 1) * of_real (ln x)) * (1 - of_real x / of_nat n) ^ n)
+            has_integral (?I * exp ((z - 1) * ln (of_nat n)))) {0..real n}" (is ?P)
+      by (insert B, subst (asm) mult.assoc [symmetric], subst (asm) exp_add [symmetric])
+         (simp add: Ln_of_nat algebra_simps)
+    also have "?P \<longleftrightarrow> ((\<lambda>x. of_real x powr (z - 1) * (1 - of_real x / of_nat n) ^ n)
+            has_integral (?I * exp ((z - 1) * ln (of_nat n)))) {0..real n}"
+      by (intro has_integral_spike_finite_eq[of "{0}"]) (simp_all add: powr_def Ln_of_real)
+    also have "fact n * of_nat n / pochhammer z (n+1) * exp ((z - 1) * Ln (of_nat n)) =
+                 (of_nat n powr z * fact n / pochhammer z (n+1))"
+      by (auto simp add: powr_def algebra_simps exp_diff)
+    finally show ?thesis by (subst has_integral_restrict) simp_all
+  next
+    case False
+    thus ?thesis by (subst has_integral_restrict) (simp_all add: has_integral_refl)
+  qed
+
+  have "eventually (\<lambda>n. Gamma_series z n =
+          of_nat n powr z * fact n / pochhammer z (n+1)) sequentially"
+    using eventually_gt_at_top[of "0::nat"]
+    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)
+
+  {
+    fix x :: real assume x: "x \<ge> 0"
+    have lim_exp: "(\<lambda>k. (1 - x / real k) ^ k) \<longlonglongrightarrow> exp (-x)"
+      using tendsto_exp_limit_sequentially[of "-x"] by simp
+    have "(\<lambda>k. of_real x powr (z - 1) * of_real ((1 - x / of_nat k) ^ k))
+            \<longlonglongrightarrow> of_real x powr (z - 1) * of_real (exp (-x))" (is ?P)
+      by (intro tendsto_intros lim_exp)
+    also from eventually_gt_at_top[of "nat \<lceil>x\<rceil>"]
+      have "eventually (\<lambda>k. of_nat k > x) sequentially" by eventually_elim linarith
+    hence "?P \<longleftrightarrow> (\<lambda>k. if x \<le> of_nat k then
+                 of_real x powr (z - 1) * of_real ((1 - x / of_nat k) ^ k) else 0)
+                   \<longlonglongrightarrow> of_real x powr (z - 1) * of_real (exp (-x))"
+      by (intro tendsto_cong) (auto elim!: eventually_mono)
+    finally have \<dots> .
+  }
+  hence D: "\<forall>x\<in>{0..}. (\<lambda>k. if x \<in> {0..real k} then
+              of_real x powr (z - 1) * (1 - of_real x / of_nat k) ^ k else 0)
+             \<longlonglongrightarrow> of_real x powr (z - 1) / of_real (exp x)"
+    by (simp add: exp_minus field_simps cong: if_cong)
+
+  have "((\<lambda>x. (Re z - 1) * (ln x / x)) \<longlongrightarrow> (Re z - 1) * 0) at_top"
+    by (intro tendsto_intros ln_x_over_x_tendsto_0)
+  hence "((\<lambda>x. ((Re z - 1) * ln x) / x) \<longlongrightarrow> 0) at_top" by simp
+  from order_tendstoD(2)[OF this, of "1/2"]
+    have "eventually (\<lambda>x. (Re z - 1) * ln x / x < 1/2) at_top" by simp
+  from eventually_conj[OF this eventually_gt_at_top[of 0]]
+    obtain x0 where "\<forall>x\<ge>x0. (Re z - 1) * ln x / x < 1/2 \<and> x > 0"
+    by (auto simp: eventually_at_top_linorder)
+  hence x0: "x0 > 0" "\<And>x. x \<ge> x0 \<Longrightarrow> (Re z - 1) * ln x < x / 2" by auto
+
+  define h where "h = (\<lambda>x. if x \<in> {0..x0} then x powr (Re z - 1) else exp (-x/2))"
+  have le_h: "x powr (Re z - 1) * exp (-x) \<le> h x" if x: "x \<ge> 0" for x
+  proof (cases "x > x0")
+    case True
+    from True x0(1) have "x powr (Re z - 1) * exp (-x) = exp ((Re z - 1) * ln x - x)"
+      by (simp add: powr_def exp_diff exp_minus field_simps exp_add)
+    also from x0(2)[of x] True have "\<dots> < exp (-x/2)"
+      by (simp add: field_simps)
+    finally show ?thesis using True by (auto simp add: h_def)
+  next
+    case False
+    from x have "x powr (Re z - 1) * exp (- x) \<le> x powr (Re z - 1) * 1"
+      by (intro mult_left_mono) simp_all
+    with False show ?thesis by (auto simp add: h_def)
+  qed
+
+  have E: "\<forall>x\<in>{0..}. cmod (if x \<in> {0..real k} then of_real x powr (z - 1) *
+                   (1 - complex_of_real x / of_nat k) ^ k else 0) \<le> h x"
+    (is "\<forall>x\<in>_. ?f x \<le> _") for k
+  proof safe
+    fix x :: real assume x: "x \<ge> 0"
+    {
+      fix x :: real and n :: nat assume x: "x \<le> of_nat n"
+      have "(1 - complex_of_real x / of_nat n) = complex_of_real ((1 - x / of_nat n))" by simp
+      also have "norm \<dots> = \<bar>(1 - x / real n)\<bar>" by (subst norm_of_real) (rule refl)
+      also from x have "\<dots> = (1 - x / real n)" by (intro abs_of_nonneg) (simp_all add: divide_simps)
+      finally have "cmod (1 - complex_of_real x / of_nat n) = 1 - x / real n" .
+    } note D = this
+    from D[of x k] x
+      have "?f x \<le> (if of_nat k \<ge> x \<and> k > 0 then x powr (Re z - 1) * (1 - x / real k) ^ k else 0)"
+      by (auto simp: norm_mult norm_powr_real_powr norm_power intro!: mult_nonneg_nonneg)
+    also have "\<dots> \<le> x powr (Re z - 1) * exp  (-x)"
+      by (auto intro!: mult_left_mono exp_ge_one_minus_x_over_n_power_n)
+    also from x have "\<dots> \<le> h x" by (rule le_h)
+    finally show "?f x \<le> h x" .
+  qed
+  
+  have F: "h integrable_on {0..}" unfolding h_def
+    by (rule integrable_Gamma_integral_bound) (insert assms x0(1), simp_all)
+  show ?thesis
+    by (rule has_integral_dominated_convergence[OF B F E D C])
+qed
+
+lemma Gamma_integral_real:
+  assumes x: "x > (0 :: real)"
+  shows   "((\<lambda>t. t powr (x - 1) / exp t) has_integral Gamma x) {0..}"
+proof -
+  have A: "((\<lambda>t. complex_of_real t powr (complex_of_real x - 1) /
+          complex_of_real (exp t)) has_integral complex_of_real (Gamma x)) {0..}"
+    using Gamma_integral_complex[of x] assms by (simp_all add: Gamma_complex_of_real powr_of_real)
+  have "((\<lambda>t. complex_of_real (t powr (x - 1) / exp t)) has_integral of_real (Gamma x)) {0..}"
+    by (rule has_integral_eq[OF _ A]) (simp_all add: powr_of_real [symmetric])
+  from has_integral_linear[OF this bounded_linear_Re] show ?thesis by (simp add: o_def)
+qed
+
+
+
 subsection \<open>The Weierstraß product formula for the sine\<close>
 
 lemma sin_product_formula_complex:
diff -r 52792bb9126e -r 3951a15a05d1 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Jun 13 15:23:12 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Jun 13 17:39:52 2016 +0200
@@ -9103,6 +9103,22 @@
     done
 qed
 
+lemma integrable_union:
+  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)
+qed
+
+lemma integrable_union':
+  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:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   assumes "finite t"
@@ -12775,4 +12791,181 @@
   finally show ?thesis .
 qed
 
+
+subsection \<open>Definite integrals for exponential and power function\<close>
+
+lemma has_integral_exp_minus_to_infinity: 
+  assumes a: "a > 0"
+  shows   "((\<lambda>x::real. exp (-a*x)) has_integral exp (-a*c)/a) {c..}"
+proof -
+  define f where "f = (\<lambda>k x. if x \<in> {c..real k} then exp (-a*x) else 0)"
+
+  {
+    fix k :: nat assume k: "of_nat k \<ge> c"
+    from k a 
+      have "((\<lambda>x. exp (-a*x)) has_integral (-exp (-a*real k)/a - (-exp (-a*c)/a))) {c..real k}"
+      by (intro fundamental_theorem_of_calculus)
+         (auto intro!: derivative_eq_intros
+               simp: has_field_derivative_iff_has_vector_derivative [symmetric])
+    hence "(f k has_integral (exp (-a*c)/a - exp (-a*real k)/a)) {c..}" unfolding f_def
+      by (subst has_integral_restrict) simp_all
+  } note has_integral_f = this
+
+  have [simp]: "f k = (\<lambda>_. 0)" if "of_nat k < c" for k using that by (auto simp: fun_eq_iff f_def)
+  have integral_f: "integral {c..} (f k) = 
+                      (if real k \<ge> c then exp (-a*c)/a - exp (-a*real k)/a else 0)"
+    for k using integral_unique[OF has_integral_f[of k]] by simp
+
+  have A: "(\<lambda>x. exp (-a*x)) integrable_on {c..} \<and>
+             (\<lambda>k. integral {c..} (f k)) \<longlonglongrightarrow> integral {c..} (\<lambda>x. exp (-a*x))"
+  proof (intro monotone_convergence_increasing allI ballI)
+    fix k ::nat
+    have "(\<lambda>x. exp (-a*x)) integrable_on {c..of_real k}" (is ?P)
+      unfolding f_def by (auto intro!: continuous_intros integrable_continuous_real)
+    hence int: "(f k) integrable_on {c..of_real k}"
+      by (rule integrable_eq[rotated]) (simp add: f_def)
+    show "f k integrable_on {c..}"
+      by (rule integrable_on_superset[OF _ _ int]) (auto simp: f_def)
+  next
+    fix x assume x: "x \<in> {c..}"
+    have "sequentially \<le> principal {nat \<lceil>x\<rceil>..}" unfolding at_top_def by (simp add: Inf_lower)
+    also have "{nat \<lceil>x\<rceil>..} \<subseteq> {k. x \<le> real k}" by auto
+    also have "inf (principal \<dots>) (principal {k. \<not>x \<le> real k}) =
+                 principal ({k. x \<le> real k} \<inter> {k. \<not>x \<le> real k})" by simp
+    also have "{k. x \<le> real k} \<inter> {k. \<not>x \<le> real k} = {}" by blast
+    finally have "inf sequentially (principal {k. \<not>x \<le> real k}) = bot"
+      by (simp add: inf.coboundedI1 bot_unique)
+    with x show "(\<lambda>k. f k x) \<longlonglongrightarrow> exp (-a*x)" unfolding f_def
+      by (intro filterlim_If) auto
+  next
+    have "\<bar>integral {c..} (f k)\<bar> \<le> exp (-a*c)/a" for k
+    proof (cases "c > of_nat k")
+      case False
+      hence "abs (integral {c..} (f k)) = abs (exp (- (a * c)) / a - exp (- (a * real k)) / a)"
+        by (simp add: integral_f)
+      also have "abs (exp (- (a * c)) / a - exp (- (a * real k)) / a) = 
+                   exp (- (a * c)) / a - exp (- (a * real k)) / a" 
+        using False a by (intro abs_of_nonneg) (simp_all add: field_simps)
+      also have "\<dots> \<le> exp (- a * c) / a" using a by simp
+      finally show ?thesis .
+    qed (insert a, simp_all add: integral_f)
+    thus "bounded {integral {c..} (f k) |k. True}"
+      by (intro bounded_realI[of _ "exp (-a*c)/a"]) auto
+  qed (auto simp: f_def)
+
+  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)
+  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
+  with conjunct1[OF A] show ?thesis
+    by (simp add: has_integral_integral)
+qed
+
+lemma integrable_on_exp_minus_to_infinity: "a > 0 \<Longrightarrow> (\<lambda>x. exp (-a*x) :: real) integrable_on {c..}"
+  using has_integral_exp_minus_to_infinity[of a c] unfolding integrable_on_def by blast
+
+lemma has_integral_powr_from_0:
+  assumes a: "a > (-1::real)" and c: "c \<ge> 0"
+  shows   "((\<lambda>x. x powr a) has_integral (c powr (a+1) / (a+1))) {0..c}"
+proof (cases "c = 0")
+  case False
+  define f where "f = (\<lambda>k x. if x \<in> {inverse (of_nat (Suc k))..c} then x powr a else 0)"
+  define F where "F = (\<lambda>k. if inverse (of_nat (Suc k)) \<le> c then 
+                             c powr (a+1)/(a+1) - inverse (real (Suc k)) powr (a+1)/(a+1) else 0)"
+  
+  {
+    fix k :: nat
+    have "(f k has_integral F k) {0..c}"
+    proof (cases "inverse (of_nat (Suc k)) \<le> c")
+      case True
+      {
+        fix x assume x: "x \<ge> inverse (1 + real k)"
+        have "0 < inverse (1 + real k)" by simp
+        also note x
+        finally have "x > 0" .
+      } note x = this
+      hence "((\<lambda>x. x powr a) has_integral c powr (a + 1) / (a + 1) - 
+               inverse (real (Suc k)) powr (a + 1) / (a + 1)) {inverse (real (Suc k))..c}" 
+        using True a by (intro fundamental_theorem_of_calculus)
+           (auto intro!: derivative_eq_intros continuous_on_powr' continuous_on_const 
+             continuous_on_id simp: has_field_derivative_iff_has_vector_derivative [symmetric])
+      with True show ?thesis unfolding f_def F_def by (subst has_integral_restrict) simp_all
+    next
+      case False
+      thus ?thesis unfolding f_def F_def by (subst has_integral_restrict) auto
+    qed
+  } note has_integral_f = this
+  have integral_f: "integral {0..c} (f k) = F k" for k
+    using has_integral_f[of k] by (rule integral_unique) 
+  
+  have A: "(\<lambda>x. x powr a) integrable_on {0..c} \<and> 
+           (\<lambda>k. integral {0..c} (f k)) \<longlonglongrightarrow> integral {0..c} (\<lambda>x. x powr a)"
+  proof (intro monotone_convergence_increasing ballI allI)
+    fix k from has_integral_f[of k] show "f k integrable_on {0..c}"
+      by (auto simp: integrable_on_def)
+  next
+    fix k :: nat and x :: real
+    {
+      assume x: "inverse (real (Suc k)) \<le> x"
+      have "inverse (real (Suc (Suc k))) \<le> inverse (real (Suc k))" by (simp add: field_simps)
+      also note x
+      finally have "inverse (real (Suc (Suc k))) \<le> x" .
+    }
+    thus "f k x \<le> f (Suc k) x" by (auto simp: f_def simp del: of_nat_Suc)
+  next
+    fix x assume x: "x \<in> {0..c}"
+    show "(\<lambda>k. f k x) \<longlonglongrightarrow> x powr a"
+    proof (cases "x = 0")
+      case False
+      with x have "x > 0" by simp
+      from order_tendstoD(2)[OF LIMSEQ_inverse_real_of_nat this]
+        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)
+    qed (simp_all add: f_def)
+  next
+    {
+      fix k
+      from a have "F k \<le> c powr (a + 1) / (a + 1)"
+        by (auto simp add: F_def divide_simps)
+      also from a have "F k \<ge> 0" 
+        by (auto simp: F_def divide_simps simp del: of_nat_Suc intro!: powr_mono2)
+      hence "F k = abs (F k)" by simp
+      finally have "abs (F k) \<le>  c powr (a + 1) / (a + 1)" .
+    }
+    thus "bounded {integral {0..c} (f k) |k. True}"
+      by (intro bounded_realI[of _ "c powr (a+1) / (a+1)"]) (auto simp: integral_f)
+  qed
+
+  from False c have "c > 0" by simp
+  from order_tendstoD(2)[OF LIMSEQ_inverse_real_of_nat this]
+    have "eventually (\<lambda>k. c powr (a + 1) / (a + 1) - inverse (real (Suc k)) powr (a+1) / (a+1) =
+            integral {0..c} (f k)) sequentially"
+    by eventually_elim (simp add: integral_f F_def)
+  moreover have "(\<lambda>k. c powr (a + 1) / (a + 1) - inverse (real (Suc k)) powr (a + 1) / (a + 1))
+                   \<longlonglongrightarrow> c powr (a + 1) / (a + 1) - 0 powr (a + 1) / (a + 1)"
+    using a by (intro tendsto_intros LIMSEQ_inverse_real_of_nat) auto
+  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)
+  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)
+qed (simp_all add: has_integral_refl)
+
+lemma integrable_on_powr_from_0:
+  assumes a: "a > (-1::real)" and c: "c \<ge> 0"
+  shows   "(\<lambda>x. x powr a) integrable_on {0..c}"
+  using has_integral_powr_from_0[OF assms] unfolding integrable_on_def by blast
+
 end