src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
 changeset 65578 e4997c181cce parent 65204 d23eded35a33 child 65587 16a8991ab398
```     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Apr 25 08:38:23 2017 +0200
1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Apr 25 16:39:54 2017 +0100
1.3 @@ -2578,36 +2578,38 @@
1.4  proof (rule integrable_uniform_limit, safe)
1.5    fix e :: real
1.6    assume e: "e > 0"
1.7 -  from compact_uniformly_continuous[OF assms compact_cbox,unfolded uniformly_continuous_on_def,rule_format,OF e] guess d ..
1.8 -  note d=conjunctD2[OF this,rule_format]
1.9 -  from fine_division_exists[OF gauge_ball[OF d(1)], of a b] guess p . note p=this
1.10 -  note p' = tagged_division_ofD[OF p(1)]
1.11 +  then obtain d where "0 < d" and d: "\<And>x x'. \<lbrakk>x \<in> cbox a b; x' \<in> cbox a b; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
1.12 +    using compact_uniformly_continuous[OF assms compact_cbox] unfolding uniformly_continuous_on_def by metis
1.13 +  obtain p where ptag: "p tagged_division_of cbox a b" and finep: "(\<lambda>x. ball x d) fine p"
1.14 +    using fine_division_exists[OF gauge_ball[OF \<open>0 < d\<close>], of a b] .
1.15    have *: "\<forall>i\<in>snd ` p. \<exists>g. (\<forall>x\<in>i. norm (f x - g x) \<le> e) \<and> g integrable_on i"
1.16    proof (safe, unfold snd_conv)
1.17      fix x l
1.18      assume as: "(x, l) \<in> p"
1.19 -    from p'(4)[OF this] guess a b by (elim exE) note l=this
1.20 +    obtain a b where l: "l = cbox a b"
1.21 +      using as ptag by blast
1.22 +    then have x: "x \<in> cbox a b"
1.23 +      using as ptag by auto
1.24      show "\<exists>g. (\<forall>x\<in>l. norm (f x - g x) \<le> e) \<and> g integrable_on l"
1.25        apply (rule_tac x="\<lambda>y. f x" in exI)
1.26      proof safe
1.27        show "(\<lambda>y. f x) integrable_on l"
1.28 -        unfolding integrable_on_def l
1.29 -        apply rule
1.30 -        apply (rule has_integral_const)
1.31 -        done
1.32 +        unfolding integrable_on_def l by blast
1.33 +    next
1.34        fix y
1.35        assume y: "y \<in> l"
1.36 -      note fineD[OF p(2) as,unfolded subset_eq,rule_format,OF this]
1.37 -      note d(2)[OF _ _ this[unfolded mem_ball]]
1.38 +      then have "y \<in> ball x d"
1.39 +        using as finep by fastforce
1.40        then show "norm (f y - f x) \<le> e"
1.41 -        using y p'(2-3)[OF as] unfolding dist_norm l norm_minus_commute by fastforce
1.42 +        using d x y as l
1.43 +        by (metis dist_commute dist_norm less_imp_le mem_ball ptag subsetCE tagged_division_ofD(3))
1.44      qed
1.45    qed
1.46    from e have "e \<ge> 0"
1.47      by auto
1.48 -  from approximable_on_division[OF this division_of_tagged_division[OF p(1)] *] guess g .
1.49 -  then show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
1.50 -    by auto
1.51 +  from approximable_on_division[OF this division_of_tagged_division[OF ptag] *]
1.52 +  show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
1.53 +    by metis
1.54  qed
1.55
1.56  lemma integrable_continuous_interval:
1.57 @@ -6278,89 +6280,6 @@
1.58  qed
1.59
1.60
1.61 -subsection \<open>Geometric progression\<close>
1.62 -
1.63 -text \<open>FIXME: Should one or more of these theorems be moved to
1.64 -  \<^file>\<open>~~/src/HOL/Set_Interval.thy\<close>, alongside \<open>geometric_sum\<close>?\<close>
1.65 -
1.66 -lemma sum_gp_basic:
1.67 -  fixes x :: "'a::ring_1"
1.68 -  shows "(1 - x) * sum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
1.69 -proof -
1.70 -  define y where "y = 1 - x"
1.71 -  have "y * (\<Sum>i=0..n. (1 - y) ^ i) = 1 - (1 - y) ^ Suc n"
1.72 -    by (induct n) (simp_all add: algebra_simps)
1.73 -  then show ?thesis
1.74 -    unfolding y_def by simp
1.75 -qed
1.76 -
1.77 -lemma sum_gp_multiplied:
1.78 -  assumes mn: "m \<le> n"
1.79 -  shows "((1::'a::{field}) - x) * sum (op ^ x) {m..n} = x^m - x^ Suc n"
1.80 -  (is "?lhs = ?rhs")
1.81 -proof -
1.82 -  let ?S = "{0..(n - m)}"
1.83 -  from mn have mn': "n - m \<ge> 0"
1.84 -    by arith
1.85 -  let ?f = "op + m"
1.86 -  have i: "inj_on ?f ?S"
1.87 -    unfolding inj_on_def by auto
1.88 -  have f: "?f ` ?S = {m..n}"
1.89 -    using mn
1.90 -    apply (auto simp add: image_iff Bex_def)
1.91 -    apply presburger
1.92 -    done
1.93 -  have th: "op ^ x \<circ> op + m = (\<lambda>i. x^m * x^i)"
1.94 -    by (rule ext) (simp add: power_add power_mult)
1.95 -  from sum.reindex[OF i, of "op ^ x", unfolded f th sum_distrib_left[symmetric]]
1.96 -  have "?lhs = x^m * ((1 - x) * sum (op ^ x) {0..n - m})"
1.97 -    by simp
1.98 -  then show ?thesis
1.99 -    unfolding sum_gp_basic
1.100 -    using mn
1.101 -    by (simp add: field_simps power_add[symmetric])
1.102 -qed
1.103 -
1.104 -lemma sum_gp:
1.105 -  "sum (op ^ (x::'a::{field})) {m .. n} =
1.106 -    (if n < m then 0
1.107 -     else if x = 1 then of_nat ((n + 1) - m)
1.108 -     else (x^ m - x^ (Suc n)) / (1 - x))"
1.109 -proof -
1.110 -  {
1.111 -    assume nm: "n < m"
1.112 -    then have ?thesis by simp
1.113 -  }
1.114 -  moreover
1.115 -  {
1.116 -    assume "\<not> n < m"
1.117 -    then have nm: "m \<le> n"
1.118 -      by arith
1.119 -    {
1.120 -      assume x: "x = 1"
1.121 -      then have ?thesis
1.122 -        by simp
1.123 -    }
1.124 -    moreover
1.125 -    {
1.126 -      assume x: "x \<noteq> 1"
1.127 -      then have nz: "1 - x \<noteq> 0"
1.128 -        by simp
1.129 -      from sum_gp_multiplied[OF nm, of x] nz have ?thesis
1.130 -        by (simp add: field_simps)
1.131 -    }
1.132 -    ultimately have ?thesis by blast
1.133 -  }
1.134 -  ultimately show ?thesis by blast
1.135 -qed
1.136 -
1.137 -lemma sum_gp_offset:
1.138 -  "sum (op ^ (x::'a::{field})) {m .. m+n} =
1.139 -    (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
1.140 -  unfolding sum_gp[of x m "m + n"] power_Suc
1.141 -  by (simp add: field_simps power_add)
1.142 -
1.143 -
1.144  subsection \<open>Monotone convergence (bounded interval first)\<close>
1.145
1.146  lemma monotone_convergence_interval:
```