--- 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>
--- 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:
--- 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