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: