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.96 +    by (simp add: divide_simps powr_add [symmetric] of_nat_diff)
    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