src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
 changeset 63721 492bb53c3420 parent 63680 6e1e8b5abbfa child 63886 685fb01256af
```     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 24 11:02:23 2016 +0200
1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Aug 25 15:50:43 2016 +0200
1.3 @@ -12533,4 +12533,101 @@
1.4    shows   "(\<lambda>x. x powr a) integrable_on {0..c}"
1.5    using has_integral_powr_from_0[OF assms] unfolding integrable_on_def by blast
1.6
1.7 +lemma has_integral_powr_to_inf:
1.8 +  fixes a e :: real
1.9 +  assumes "e < -1" "a > 0"
1.10 +  shows   "((\<lambda>x. x powr e) has_integral -(a powr (e + 1)) / (e + 1)) {a..}"
1.11 +proof -
1.12 +  define f :: "nat \<Rightarrow> real \<Rightarrow> real" where "f = (\<lambda>n x. if x \<in> {a..n} then x powr e else 0)"
1.13 +  define F where "F = (\<lambda>x. x powr (e + 1) / (e + 1))"
1.14 +
1.15 +  have has_integral_f: "(f n has_integral (F n - F a)) {a..}"
1.16 +    if n: "n \<ge> a" for n :: nat
1.17 +  proof -
1.18 +    from n assms have "((\<lambda>x. x powr e) has_integral (F n - F a)) {a..n}"
1.19 +      by (intro fundamental_theorem_of_calculus) (auto intro!: derivative_eq_intros
1.20 +            simp: has_field_derivative_iff_has_vector_derivative [symmetric] F_def)
1.21 +    hence "(f n has_integral (F n - F a)) {a..n}"
1.22 +      by (rule has_integral_eq [rotated]) (simp add: f_def)
1.23 +    thus "(f n has_integral (F n - F a)) {a..}"
1.24 +      by (rule has_integral_on_superset [rotated 2]) (auto simp: f_def)
1.25 +  qed
1.26 +  have integral_f: "integral {a..} (f n) = (if n \<ge> a then F n - F a else 0)" for n :: nat
1.27 +  proof (cases "n \<ge> a")
1.28 +    case True
1.29 +    with has_integral_f[OF this] show ?thesis by (simp add: integral_unique)
1.30 +  next
1.31 +    case False
1.32 +    have "(f n has_integral 0) {a}" by (rule has_integral_refl)
1.33 +    hence "(f n has_integral 0) {a..}"
1.34 +      by (rule has_integral_on_superset [rotated 2]) (insert False, simp_all add: f_def)
1.35 +    with False show ?thesis by (simp add: integral_unique)
1.36 +  qed
1.37 +
1.38 +  have *: "(\<lambda>x. x powr e) integrable_on {a..} \<and>
1.39 +           (\<lambda>n. integral {a..} (f n)) \<longlonglongrightarrow> integral {a..} (\<lambda>x. x powr e)"
1.40 +  proof (intro monotone_convergence_increasing allI ballI)
1.41 +    fix n :: nat
1.42 +    from assms have "(\<lambda>x. x powr e) integrable_on {a..n}"
1.43 +      by (auto intro!: integrable_continuous_real continuous_intros)
1.44 +    hence "f n integrable_on {a..n}"
1.45 +      by (rule integrable_eq [rotated]) (auto simp: f_def)
1.46 +    thus "f n integrable_on {a..}"
1.47 +      by (rule integrable_on_superset [rotated 2]) (auto simp: f_def)
1.48 +  next
1.49 +    fix n :: nat and x :: real
1.50 +    show "f n x \<le> f (Suc n) x" by (auto simp: f_def)
1.51 +  next
1.52 +    fix x :: real assume x: "x \<in> {a..}"
1.53 +    from filterlim_real_sequentially
1.54 +      have "eventually (\<lambda>n. real n \<ge> x) at_top"
1.55 +      by (simp add: filterlim_at_top)
1.56 +    with x have "eventually (\<lambda>n. f n x = x powr e) at_top"
1.57 +      by (auto elim!: eventually_mono simp: f_def)
1.58 +    thus "(\<lambda>n. f n x) \<longlonglongrightarrow> x powr e" by (simp add: Lim_eventually)
1.59 +  next
1.60 +    have "norm (integral {a..} (f n)) \<le> -F a" for n :: nat
1.61 +    proof (cases "n \<ge> a")
1.62 +      case True
1.63 +      with assms have "a powr (e + 1) \<ge> n powr (e + 1)"
1.64 +        by (intro powr_mono2') simp_all
1.65 +      with assms show ?thesis by (auto simp: divide_simps F_def integral_f)
1.66 +    qed (insert assms, simp add: integral_f F_def divide_simps)
1.67 +    thus "bounded {integral {a..} (f n) |n. True}"
1.68 +      unfolding bounded_iff by (intro exI[of _ "-F a"]) auto
1.69 +  qed
1.70 +
1.71 +  from filterlim_real_sequentially
1.72 +    have "eventually (\<lambda>n. real n \<ge> a) at_top"
1.73 +    by (simp add: filterlim_at_top)
1.74 +  hence "eventually (\<lambda>n. F n - F a = integral {a..} (f n)) at_top"
1.75 +    by eventually_elim (simp add: integral_f)
1.76 +  moreover have "(\<lambda>n. F n - F a) \<longlonglongrightarrow> 0 / (e + 1) - F a" unfolding F_def
1.77 +    by (insert assms, (rule tendsto_intros filterlim_compose[OF tendsto_neg_powr]
1.78 +          filterlim_ident filterlim_real_sequentially | simp)+)
1.79 +  hence "(\<lambda>n. F n - F a) \<longlonglongrightarrow> -F a" by simp
1.80 +  ultimately have "(\<lambda>n. integral {a..} (f n)) \<longlonglongrightarrow> -F a" by (rule Lim_transform_eventually)
1.81 +  from conjunct2[OF *] and this
1.82 +    have "integral {a..} (\<lambda>x. x powr e) = -F a" by (rule LIMSEQ_unique)
1.83 +  with conjunct1[OF *] show ?thesis
1.84 +    by (simp add: has_integral_integral F_def)
1.85 +qed
1.86 +
1.87 +lemma has_integral_inverse_power_to_inf:
1.88 +  fixes a :: real and n :: nat
1.89 +  assumes "n > 1" "a > 0"
1.90 +  shows   "((\<lambda>x. 1 / x ^ n) has_integral 1 / (real (n - 1) * a ^ (n - 1))) {a..}"
1.91 +proof -
1.92 +  from assms have "real_of_int (-int n) < -1" by simp
1.93 +  note has_integral_powr_to_inf[OF this \<open>a > 0\<close>]
1.94 +  also have "- (a powr (real_of_int (- int n) + 1)) / (real_of_int (- int n) + 1) =
1.95 +                 1 / (real (n - 1) * a powr (real (n - 1)))" using assms
1.97 +  also from assms have "a powr (real (n - 1)) = a ^ (n - 1)"
1.98 +    by (intro powr_realpow)
1.99 +  finally show ?thesis
1.100 +    by (rule has_integral_eq [rotated])
1.101 +       (insert assms, simp_all add: powr_minus powr_realpow divide_simps)
1.102 +qed
1.103 +
1.104  end
```