3907 norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - i) < e" |
4049 norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - i) < e" |
3908 proof(rule,rule,rule B,safe) case goal1 from B(2)[OF this] guess z .. note z=conjunctD2[OF this] |
4050 proof(rule,rule,rule B,safe) case goal1 from B(2)[OF this] guess z .. note z=conjunctD2[OF this] |
3909 from integral_unique[OF this(1)] show ?case using z(2) by auto qed qed qed |
4051 from integral_unique[OF this(1)] show ?case using z(2) by auto qed qed qed |
3910 |
4052 |
3911 |
4053 |
|
4054 subsection {* Continuity of the integral (for a 1-dimensional interval). *} |
|
4055 |
|
4056 lemma integrable_alt: fixes f::"real^'n \<Rightarrow> 'a::banach" shows |
|
4057 "f integrable_on s \<longleftrightarrow> |
|
4058 (\<forall>a b. (\<lambda>x. if x \<in> s then f x else 0) integrable_on {a..b}) \<and> |
|
4059 (\<forall>e>0. \<exists>B>0. \<forall>a b c d. ball 0 B \<subseteq> {a..b} \<and> ball 0 B \<subseteq> {c..d} |
|
4060 \<longrightarrow> norm(integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - |
|
4061 integral {c..d} (\<lambda>x. if x \<in> s then f x else 0)) < e)" (is "?l = ?r") |
|
4062 proof assume ?l then guess y unfolding integrable_on_def .. note this[unfolded has_integral_alt'[of f]] |
|
4063 note y=conjunctD2[OF this,rule_format] show ?r apply safe apply(rule y) |
|
4064 proof- case goal1 hence "e/2 > 0" by auto from y(2)[OF this] guess B .. note B=conjunctD2[OF this,rule_format] |
|
4065 show ?case apply(rule,rule,rule B) |
|
4066 proof safe case goal1 show ?case apply(rule norm_triangle_half_l) |
|
4067 using B(2)[OF goal1(1)] B(2)[OF goal1(2)] by auto qed qed |
|
4068 |
|
4069 next assume ?r note as = conjunctD2[OF this,rule_format] |
|
4070 have "Cauchy (\<lambda>n. integral ({(\<chi> i. - real n) .. (\<chi> i. real n)}) (\<lambda>x. if x \<in> s then f x else 0))" |
|
4071 proof(unfold Cauchy_def,safe) case goal1 |
|
4072 from as(2)[OF this] guess B .. note B = conjunctD2[OF this,rule_format] |
|
4073 from real_arch_simple[of B] guess N .. note N = this |
|
4074 { fix n assume n:"n \<ge> N" have "ball 0 B \<subseteq> {\<chi> i. - real n..\<chi> i. real n}" apply safe |
|
4075 unfolding mem_ball mem_interval vector_dist_norm |
|
4076 proof case goal1 thus ?case using component_le_norm[of x i] |
|
4077 using n N by(auto simp add:field_simps) qed } |
|
4078 thus ?case apply-apply(rule_tac x=N in exI) apply safe unfolding vector_dist_norm apply(rule B(2)) by auto |
|
4079 qed from this[unfolded convergent_eq_cauchy[THEN sym]] guess i .. |
|
4080 note i = this[unfolded Lim_sequentially, rule_format] |
|
4081 |
|
4082 show ?l unfolding integrable_on_def has_integral_alt'[of f] apply(rule_tac x=i in exI) |
|
4083 apply safe apply(rule as(1)[unfolded integrable_on_def]) |
|
4084 proof- case goal1 hence *:"e/2 > 0" by auto |
|
4085 from i[OF this] guess N .. note N =this[rule_format] |
|
4086 from as(2)[OF *] guess B .. note B=conjunctD2[OF this,rule_format] let ?B = "max (real N) B" |
|
4087 show ?case apply(rule_tac x="?B" in exI) |
|
4088 proof safe show "0 < ?B" using B(1) by auto |
|
4089 fix a b assume ab:"ball 0 ?B \<subseteq> {a..b::real^'n}" |
|
4090 from real_arch_simple[of ?B] guess n .. note n=this |
|
4091 show "norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - i) < e" |
|
4092 apply(rule norm_triangle_half_l) apply(rule B(2)) defer apply(subst norm_minus_commute) |
|
4093 apply(rule N[unfolded vector_dist_norm, of n]) |
|
4094 proof safe show "N \<le> n" using n by auto |
|
4095 fix x::"real^'n" assume x:"x \<in> ball 0 B" hence "x\<in> ball 0 ?B" by auto |
|
4096 thus "x\<in>{a..b}" using ab by blast |
|
4097 show "x\<in>{\<chi> i. - real n..\<chi> i. real n}" using x unfolding mem_interval mem_ball vector_dist_norm apply- |
|
4098 proof case goal1 thus ?case using component_le_norm[of x i] |
|
4099 using n by(auto simp add:field_simps) qed qed qed qed qed |
|
4100 |
|
4101 lemma integrable_altD: fixes f::"real^'n \<Rightarrow> 'a::banach" |
|
4102 assumes "f integrable_on s" |
|
4103 shows "\<And>a b. (\<lambda>x. if x \<in> s then f x else 0) integrable_on {a..b}" |
|
4104 "\<And>e. e>0 \<Longrightarrow> \<exists>B>0. \<forall>a b c d. ball 0 B \<subseteq> {a..b} \<and> ball 0 B \<subseteq> {c..d} |
|
4105 \<longrightarrow> norm(integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - integral {c..d} (\<lambda>x. if x \<in> s then f x else 0)) < e" |
|
4106 using assms[unfolded integrable_alt[of f]] by auto |
|
4107 |
|
4108 lemma integrable_on_subinterval: fixes f::"real^'n \<Rightarrow> 'a::banach" |
|
4109 assumes "f integrable_on s" "{a..b} \<subseteq> s" shows "f integrable_on {a..b}" |
|
4110 apply(rule integrable_eq) defer apply(rule integrable_altD(1)[OF assms(1)]) |
|
4111 using assms(2) by auto |
|
4112 |
|
4113 subsection {* A straddling criterion for integrability. *} |
|
4114 |
|
4115 lemma integrable_straddle_interval: fixes f::"real^'n \<Rightarrow> real" |
|
4116 assumes "\<forall>e>0. \<exists>g h i j. (g has_integral i) ({a..b}) \<and> (h has_integral j) ({a..b}) \<and> |
|
4117 norm(i - j) < e \<and> (\<forall>x\<in>{a..b}. (g x) \<le> (f x) \<and> (f x) \<le>(h x))" |
|
4118 shows "f integrable_on {a..b}" |
|
4119 proof(subst integrable_cauchy,safe) |
|
4120 case goal1 hence e:"e/3 > 0" by auto note assms[rule_format,OF this] |
|
4121 then guess g h i j apply- by(erule exE conjE)+ note obt = this |
|
4122 from obt(1)[unfolded has_integral[of g], rule_format, OF e] guess d1 .. note d1=conjunctD2[OF this,rule_format] |
|
4123 from obt(2)[unfolded has_integral[of h], rule_format, OF e] guess d2 .. note d2=conjunctD2[OF this,rule_format] |
|
4124 show ?case apply(rule_tac x="\<lambda>x. d1 x \<inter> d2 x" in exI) apply(rule conjI gauge_inter d1 d2)+ unfolding fine_inter |
|
4125 proof safe have **:"\<And>i j g1 g2 h1 h2 f1 f2. g1 - h2 \<le> f1 - f2 \<Longrightarrow> f1 - f2 \<le> h1 - g2 \<Longrightarrow> |
|
4126 abs(i - j) < e / 3 \<Longrightarrow> abs(g2 - i) < e / 3 \<Longrightarrow> abs(g1 - i) < e / 3 \<Longrightarrow> |
|
4127 abs(h2 - j) < e / 3 \<Longrightarrow> abs(h1 - j) < e / 3 \<Longrightarrow> abs(f1 - f2) < e" using `e>0` by arith |
|
4128 case goal1 note tagged_division_ofD(2-4) note * = this[OF goal1(1)] this[OF goal1(4)] |
|
4129 |
|
4130 have "(\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p1. content k *\<^sub>R g x) \<ge> 0" |
|
4131 "0 \<le> (\<Sum>(x, k)\<in>p2. content k *\<^sub>R h x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)" |
|
4132 "(\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R g x) \<ge> 0" |
|
4133 "0 \<le> (\<Sum>(x, k)\<in>p1. content k *\<^sub>R h x) - (\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x)" |
|
4134 unfolding setsum_subtractf[THEN sym] apply- apply(rule_tac[!] setsum_nonneg) |
|
4135 apply safe unfolding real_scaleR_def mult.diff_right[THEN sym] |
|
4136 apply(rule_tac[!] mult_nonneg_nonneg) |
|
4137 proof- fix a b assume ab:"(a,b) \<in> p1" |
|
4138 show "0 \<le> content b" using *(3)[OF ab] apply safe using content_pos_le . thus "0 \<le> content b" . |
|
4139 show "0 \<le> f a - g a" "0 \<le> h a - f a" using *(1-2)[OF ab] using obt(4)[rule_format,of a] by auto |
|
4140 next fix a b assume ab:"(a,b) \<in> p2" |
|
4141 show "0 \<le> content b" using *(6)[OF ab] apply safe using content_pos_le . thus "0 \<le> content b" . |
|
4142 show "0 \<le> f a - g a" "0 \<le> h a - f a" using *(4-5)[OF ab] using obt(4)[rule_format,of a] by auto qed |
|
4143 |
|
4144 thus ?case apply- unfolding real_norm_def apply(rule **) defer defer |
|
4145 unfolding real_norm_def[THEN sym] apply(rule obt(3)) |
|
4146 apply(rule d1(2)[OF conjI[OF goal1(4,5)]]) |
|
4147 apply(rule d1(2)[OF conjI[OF goal1(1,2)]]) |
|
4148 apply(rule d2(2)[OF conjI[OF goal1(4,6)]]) |
|
4149 apply(rule d2(2)[OF conjI[OF goal1(1,3)]]) by auto qed qed |
|
4150 |
|
4151 lemma integrable_straddle: fixes f::"real^'n \<Rightarrow> real" |
|
4152 assumes "\<forall>e>0. \<exists>g h i j. (g has_integral i) s \<and> (h has_integral j) s \<and> |
|
4153 norm(i - j) < e \<and> (\<forall>x\<in>s. (g x) \<le>(f x) \<and>(f x) \<le>(h x))" |
|
4154 shows "f integrable_on s" |
|
4155 proof- have "\<And>a b. (\<lambda>x. if x \<in> s then f x else 0) integrable_on {a..b}" |
|
4156 proof(rule integrable_straddle_interval,safe) case goal1 hence *:"e/4 > 0" by auto |
|
4157 from assms[rule_format,OF this] guess g h i j apply-by(erule exE conjE)+ note obt=this |
|
4158 note obt(1)[unfolded has_integral_alt'[of g]] note conjunctD2[OF this, rule_format] |
|
4159 note g = this(1) and this(2)[OF *] from this(2) guess B1 .. note B1 = conjunctD2[OF this,rule_format] |
|
4160 note obt(2)[unfolded has_integral_alt'[of h]] note conjunctD2[OF this, rule_format] |
|
4161 note h = this(1) and this(2)[OF *] from this(2) guess B2 .. note B2 = conjunctD2[OF this,rule_format] |
|
4162 def c \<equiv> "\<chi> i. min (a$i) (- (max B1 B2))" and d \<equiv> "\<chi> i. max (b$i) (max B1 B2)" |
|
4163 have *:"ball 0 B1 \<subseteq> {c..d}" "ball 0 B2 \<subseteq> {c..d}" apply safe unfolding mem_ball mem_interval vector_dist_norm |
|
4164 proof(rule_tac[!] allI) |
|
4165 case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto next |
|
4166 case goal2 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto qed |
|
4167 have **:"\<And>ch cg ag ah::real. norm(ah - ag) \<le> norm(ch - cg) \<Longrightarrow> norm(cg - i) < e / 4 \<Longrightarrow> |
|
4168 norm(ch - j) < e / 4 \<Longrightarrow> norm(ag - ah) < e" |
|
4169 using obt(3) unfolding real_norm_def by arith |
|
4170 show ?case apply(rule_tac x="\<lambda>x. if x \<in> s then g x else 0" in exI) |
|
4171 apply(rule_tac x="\<lambda>x. if x \<in> s then h x else 0" in exI) |
|
4172 apply(rule_tac x="integral {a..b} (\<lambda>x. if x \<in> s then g x else 0)" in exI) |
|
4173 apply(rule_tac x="integral {a..b} (\<lambda>x. if x \<in> s then h x else 0)" in exI) |
|
4174 apply safe apply(rule_tac[1-2] integrable_integral,rule g,rule h) |
|
4175 apply(rule **[OF _ B1(2)[OF *(1)] B2(2)[OF *(2)]]) |
|
4176 proof- have *:"\<And>x f g. (if x \<in> s then f x else 0) - (if x \<in> s then g x else 0) = |
|
4177 (if x \<in> s then f x - g x else (0::real))" by auto |
|
4178 note ** = abs_of_nonneg[OF integral_nonneg[OF integrable_sub, OF h g]] |
|
4179 show " norm (integral {a..b} (\<lambda>x. if x \<in> s then h x else 0) - |
|
4180 integral {a..b} (\<lambda>x. if x \<in> s then g x else 0)) |
|
4181 \<le> norm (integral {c..d} (\<lambda>x. if x \<in> s then h x else 0) - |
|
4182 integral {c..d} (\<lambda>x. if x \<in> s then g x else 0))" |
|
4183 unfolding integral_sub[OF h g,THEN sym] real_norm_def apply(subst **) defer apply(subst **) defer |
|
4184 apply(rule has_integral_subset_le) defer apply(rule integrable_integral integrable_sub h g)+ |
|
4185 proof safe fix x assume "x\<in>{a..b}" thus "x\<in>{c..d}" unfolding mem_interval c_def d_def |
|
4186 apply - apply rule apply(erule_tac x=i in allE) by auto |
|
4187 qed(insert obt(4), auto) qed(insert obt(4), auto) qed note interv = this |
|
4188 |
|
4189 show ?thesis unfolding integrable_alt[of f] apply safe apply(rule interv) |
|
4190 proof- case goal1 hence *:"e/3 > 0" by auto |
|
4191 from assms[rule_format,OF this] guess g h i j apply-by(erule exE conjE)+ note obt=this |
|
4192 note obt(1)[unfolded has_integral_alt'[of g]] note conjunctD2[OF this, rule_format] |
|
4193 note g = this(1) and this(2)[OF *] from this(2) guess B1 .. note B1 = conjunctD2[OF this,rule_format] |
|
4194 note obt(2)[unfolded has_integral_alt'[of h]] note conjunctD2[OF this, rule_format] |
|
4195 note h = this(1) and this(2)[OF *] from this(2) guess B2 .. note B2 = conjunctD2[OF this,rule_format] |
|
4196 show ?case apply(rule_tac x="max B1 B2" in exI) apply safe apply(rule min_max.less_supI1,rule B1) |
|
4197 proof- fix a b c d::"real^'n" assume as:"ball 0 (max B1 B2) \<subseteq> {a..b}" "ball 0 (max B1 B2) \<subseteq> {c..d}" |
|
4198 have **:"ball 0 B1 \<subseteq> ball (0::real^'n) (max B1 B2)" "ball 0 B2 \<subseteq> ball (0::real^'n) (max B1 B2)" by auto |
|
4199 have *:"\<And>ga gc ha hc fa fc::real. abs(ga - i) < e / 3 \<and> abs(gc - i) < e / 3 \<and> abs(ha - j) < e / 3 \<and> |
|
4200 abs(hc - j) < e / 3 \<and> abs(i - j) < e / 3 \<and> ga \<le> fa \<and> fa \<le> ha \<and> gc \<le> fc \<and> fc \<le> hc\<Longrightarrow> abs(fa - fc) < e" by smt |
|
4201 show "norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - integral {c..d} (\<lambda>x. if x \<in> s then f x else 0)) < e" |
|
4202 unfolding real_norm_def apply(rule *, safe) unfolding real_norm_def[THEN sym] |
|
4203 apply(rule B1(2),rule order_trans,rule **,rule as(1)) |
|
4204 apply(rule B1(2),rule order_trans,rule **,rule as(2)) |
|
4205 apply(rule B2(2),rule order_trans,rule **,rule as(1)) |
|
4206 apply(rule B2(2),rule order_trans,rule **,rule as(2)) |
|
4207 apply(rule obt) apply(rule_tac[!] integral_le) using obt |
|
4208 by(auto intro!: h g interv) qed qed qed |
|
4209 |
|
4210 subsection {* Adding integrals over several sets. *} |
|
4211 |
|
4212 lemma has_integral_union: fixes f::"real^'n \<Rightarrow> 'a::banach" |
|
4213 assumes "(f has_integral i) s" "(f has_integral j) t" "negligible(s \<inter> t)" |
|
4214 shows "(f has_integral (i + j)) (s \<union> t)" |
|
4215 proof- note * = has_integral_restrict_univ[THEN sym, of f] |
|
4216 show ?thesis unfolding * apply(rule has_integral_spike[OF assms(3)]) |
|
4217 defer apply(rule has_integral_add[OF assms(1-2)[unfolded *]]) by auto qed |
|
4218 |
|
4219 lemma has_integral_unions: fixes f::"real^'n \<Rightarrow> 'a::banach" |
|
4220 assumes "finite t" "\<forall>s\<in>t. (f has_integral (i s)) s" "\<forall>s\<in>t. \<forall>s'\<in>t. ~(s = s') \<longrightarrow> negligible(s \<inter> s')" |
|
4221 shows "(f has_integral (setsum i t)) (\<Union>t)" |
|
4222 proof- note * = has_integral_restrict_univ[THEN sym, of f] |
|
4223 have **:"negligible (\<Union>((\<lambda>(a,b). a \<inter> b) ` {(a,b). a \<in> t \<and> b \<in> {y. y \<in> t \<and> ~(a = y)}}))" |
|
4224 apply(rule negligible_unions) apply(rule finite_imageI) apply(rule finite_subset[of _ "t \<times> t"]) defer |
|
4225 apply(rule finite_cartesian_product[OF assms(1,1)]) using assms(3) by auto |
|
4226 note assms(2)[unfolded *] note has_integral_setsum[OF assms(1) this] |
|
4227 thus ?thesis unfolding * apply-apply(rule has_integral_spike[OF **]) defer apply assumption |
|
4228 proof safe case goal1 thus ?case |
|
4229 proof(cases "x\<in>\<Union>t") case True then guess s unfolding Union_iff .. note s=this |
|
4230 hence *:"\<forall>b\<in>t. x \<in> b \<longleftrightarrow> b = s" using goal1(3) by blast |
|
4231 show ?thesis unfolding if_P[OF True] apply(rule trans) defer |
|
4232 apply(rule setsum_cong2) apply(subst *, assumption) apply(rule refl) |
|
4233 unfolding setsum_delta[OF assms(1)] using s by auto qed auto qed qed |
|
4234 |
|
4235 subsection {* In particular adding integrals over a division, maybe not of an interval. *} |
|
4236 |
|
4237 lemma has_integral_combine_division: fixes f::"real^'n \<Rightarrow> 'a::banach" |
|
4238 assumes "d division_of s" "\<forall>k\<in>d. (f has_integral (i k)) k" |
|
4239 shows "(f has_integral (setsum i d)) s" |
|
4240 proof- note d = division_ofD[OF assms(1)] |
|
4241 show ?thesis unfolding d(6)[THEN sym] apply(rule has_integral_unions) |
|
4242 apply(rule d assms)+ apply(rule,rule,rule) |
|
4243 proof- case goal1 from d(4)[OF this(1)] d(4)[OF this(2)] |
|
4244 guess a c b d apply-by(erule exE)+ note obt=this |
|
4245 from d(5)[OF goal1] show ?case unfolding obt interior_closed_interval |
|
4246 apply-apply(rule negligible_subset[of "({a..b}-{a<..<b}) \<union> ({c..d}-{c<..<d})"]) |
|
4247 apply(rule negligible_union negligible_frontier_interval)+ by auto qed qed |
|
4248 |
|
4249 lemma integral_combine_division_bottomup: fixes f::"real^'n \<Rightarrow> 'a::banach" |
|
4250 assumes "d division_of s" "\<forall>k\<in>d. f integrable_on k" |
|
4251 shows "integral s f = setsum (\<lambda>i. integral i f) d" |
|
4252 apply(rule integral_unique) apply(rule has_integral_combine_division[OF assms(1)]) |
|
4253 using assms(2) unfolding has_integral_integral . |
|
4254 |
|
4255 lemma has_integral_combine_division_topdown: fixes f::"real^'n \<Rightarrow> 'a::banach" |
|
4256 assumes "f integrable_on s" "d division_of k" "k \<subseteq> s" |
|
4257 shows "(f has_integral (setsum (\<lambda>i. integral i f) d)) k" |
|
4258 apply(rule has_integral_combine_division[OF assms(2)]) |
|
4259 apply safe unfolding has_integral_integral[THEN sym] |
|
4260 proof- case goal1 from division_ofD(2,4)[OF assms(2) this] |
|
4261 show ?case apply safe apply(rule integrable_on_subinterval) |
|
4262 apply(rule assms) using assms(3) by auto qed |
|
4263 |
|
4264 lemma integral_combine_division_topdown: fixes f::"real^'n \<Rightarrow> 'a::banach" |
|
4265 assumes "f integrable_on s" "d division_of s" |
|
4266 shows "integral s f = setsum (\<lambda>i. integral i f) d" |
|
4267 apply(rule integral_unique,rule has_integral_combine_division_topdown) using assms by auto |
|
4268 |
|
4269 lemma integrable_combine_division: fixes f::"real^'n \<Rightarrow> 'a::banach" |
|
4270 assumes "d division_of s" "\<forall>i\<in>d. f integrable_on i" |
|
4271 shows "f integrable_on s" |
|
4272 using assms(2) unfolding integrable_on_def |
|
4273 by(metis has_integral_combine_division[OF assms(1)]) |
|
4274 |
|
4275 lemma integrable_on_subdivision: fixes f::"real^'n \<Rightarrow> 'a::banach" |
|
4276 assumes "d division_of i" "f integrable_on s" "i \<subseteq> s" |
|
4277 shows "f integrable_on i" |
|
4278 apply(rule integrable_combine_division assms)+ |
|
4279 proof safe case goal1 note division_ofD(2,4)[OF assms(1) this] |
|
4280 thus ?case apply safe apply(rule integrable_on_subinterval[OF assms(2)]) |
|
4281 using assms(3) by auto qed |
|
4282 |
|
4283 subsection {* Also tagged divisions. *} |
|
4284 |
|
4285 lemma has_integral_combine_tagged_division: fixes f::"real^'n \<Rightarrow> 'a::banach" |
|
4286 assumes "p tagged_division_of s" "\<forall>(x,k) \<in> p. (f has_integral (i k)) k" |
|
4287 shows "(f has_integral (setsum (\<lambda>(x,k). i k) p)) s" |
|
4288 proof- have *:"(f has_integral (setsum (\<lambda>k. integral k f) (snd ` p))) s" |
|
4289 apply(rule has_integral_combine_division) apply(rule division_of_tagged_division[OF assms(1)]) |
|
4290 using assms(2) unfolding has_integral_integral[THEN sym] by(safe,auto) |
|
4291 thus ?thesis apply- apply(rule subst[where P="\<lambda>i. (f has_integral i) s"]) defer apply assumption |
|
4292 apply(rule trans[of _ "setsum (\<lambda>(x,k). integral k f) p"]) apply(subst eq_commute) |
|
4293 apply(rule setsum_over_tagged_division_lemma[OF assms(1)]) apply(rule integral_null,assumption) |
|
4294 apply(rule setsum_cong2) using assms(2) by auto qed |
|
4295 |
|
4296 lemma integral_combine_tagged_division_bottomup: fixes f::"real^'n \<Rightarrow> 'a::banach" |
|
4297 assumes "p tagged_division_of {a..b}" "\<forall>(x,k)\<in>p. f integrable_on k" |
|
4298 shows "integral {a..b} f = setsum (\<lambda>(x,k). integral k f) p" |
|
4299 apply(rule integral_unique) apply(rule has_integral_combine_tagged_division[OF assms(1)]) |
|
4300 using assms(2) by auto |
|
4301 |
|
4302 lemma has_integral_combine_tagged_division_topdown: fixes f::"real^'n \<Rightarrow> 'a::banach" |
|
4303 assumes "f integrable_on {a..b}" "p tagged_division_of {a..b}" |
|
4304 shows "(f has_integral (setsum (\<lambda>(x,k). integral k f) p)) {a..b}" |
|
4305 apply(rule has_integral_combine_tagged_division[OF assms(2)]) |
|
4306 proof safe case goal1 note tagged_division_ofD(3-4)[OF assms(2) this] |
|
4307 thus ?case using integrable_subinterval[OF assms(1)] by auto qed |
|
4308 |
|
4309 lemma integral_combine_tagged_division_topdown: fixes f::"real^'n \<Rightarrow> 'a::banach" |
|
4310 assumes "f integrable_on {a..b}" "p tagged_division_of {a..b}" |
|
4311 shows "integral {a..b} f = setsum (\<lambda>(x,k). integral k f) p" |
|
4312 apply(rule integral_unique,rule has_integral_combine_tagged_division_topdown) using assms by auto |
|
4313 |
|
4314 subsection {* Henstock's lemma. *} |
|
4315 |
|
4316 lemma henstock_lemma_part1: fixes f::"real^'n \<Rightarrow> 'a::banach" |
|
4317 assumes "f integrable_on {a..b}" "0 < e" "gauge d" |
|
4318 "(\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow> norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral({a..b}) f) < e)" |
|
4319 and p:"p tagged_partial_division_of {a..b}" "d fine p" |
|
4320 shows "norm(setsum (\<lambda>(x,k). content k *\<^sub>R f x - integral k f) p) \<le> e" (is "?x \<le> e") |
|
4321 proof- { presume "\<And>k. 0<k \<Longrightarrow> ?x \<le> e + k" thus ?thesis by arith } |
|
4322 fix k::real assume k:"k>0" note p' = tagged_partial_division_ofD[OF p(1)] |
|
4323 have "\<Union>snd ` p \<subseteq> {a..b}" using p'(3) by fastsimp |
|
4324 note partial_division_of_tagged_division[OF p(1)] this |
|
4325 from partial_division_extend_interval[OF this] guess q . note q=this and q' = division_ofD[OF this(2)] |
|
4326 def r \<equiv> "q - snd ` p" have "snd ` p \<inter> r = {}" unfolding r_def by auto |
|
4327 have r:"finite r" using q' unfolding r_def by auto |
|
4328 |
|
4329 have "\<forall>i\<in>r. \<exists>p. p tagged_division_of i \<and> d fine p \<and> |
|
4330 norm(setsum (\<lambda>(x,j). content j *\<^sub>R f x) p - integral i f) < k / (real (card r) + 1)" |
|
4331 proof safe case goal1 hence i:"i \<in> q" unfolding r_def by auto |
|
4332 from q'(4)[OF this] guess u v apply-by(erule exE)+ note uv=this |
|
4333 have *:"k / (real (card r) + 1) > 0" apply(rule divide_pos_pos,rule k) by auto |
|
4334 have "f integrable_on {u..v}" apply(rule integrable_subinterval[OF assms(1)]) |
|
4335 using q'(2)[OF i] unfolding uv by auto |
|
4336 note integrable_integral[OF this, unfolded has_integral[of f]] |
|
4337 from this[rule_format,OF *] guess dd .. note dd=conjunctD2[OF this,rule_format] |
|
4338 note gauge_inter[OF `gauge d` dd(1)] from fine_division_exists[OF this,of u v] guess qq . |
|
4339 thus ?case apply(rule_tac x=qq in exI) using dd(2)[of qq] unfolding fine_inter uv by auto qed |
|
4340 from bchoice[OF this] guess qq .. note qq=this[rule_format] |
|
4341 |
|
4342 let ?p = "p \<union> \<Union>qq ` r" have "norm ((\<Sum>(x, k)\<in>?p. content k *\<^sub>R f x) - integral {a..b} f) < e" |
|
4343 apply(rule assms(4)[rule_format]) |
|
4344 proof show "d fine ?p" apply(rule fine_union,rule p) apply(rule fine_unions) using qq by auto |
|
4345 note * = tagged_partial_division_of_union_self[OF p(1)] |
|
4346 have "p \<union> \<Union>qq ` r tagged_division_of \<Union>snd ` p \<union> \<Union>r" |
|
4347 proof(rule tagged_division_union[OF * tagged_division_unions]) |
|
4348 show "finite r" by fact case goal2 thus ?case using qq by auto |
|
4349 next case goal3 thus ?case apply(rule,rule,rule) apply(rule q'(5)) unfolding r_def by auto |
|
4350 next case goal4 thus ?case apply(rule inter_interior_unions_intervals) apply(fact,rule) |
|
4351 apply(rule,rule q') defer apply(rule,subst Int_commute) |
|
4352 apply(rule inter_interior_unions_intervals) apply(rule finite_imageI,rule p',rule) defer |
|
4353 apply(rule,rule q') using q(1) p' unfolding r_def by auto qed |
|
4354 moreover have "\<Union>snd ` p \<union> \<Union>r = {a..b}" "{qq i |i. i \<in> r} = qq ` r" |
|
4355 unfolding Union_Un_distrib[THEN sym] r_def using q by auto |
|
4356 ultimately show "?p tagged_division_of {a..b}" by fastsimp qed |
|
4357 |
|
4358 hence "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>\<Union>qq ` r. content k *\<^sub>R f x) - |
|
4359 integral {a..b} f) < e" apply(subst setsum_Un_zero[THEN sym]) apply(rule p') prefer 3 |
|
4360 apply assumption apply rule apply(rule finite_imageI,rule r) apply safe apply(drule qq) |
|
4361 proof- fix x l k assume as:"(x,l)\<in>p" "(x,l)\<in>qq k" "k\<in>r" |
|
4362 note qq[OF this(3)] note tagged_division_ofD(3,4)[OF conjunct1[OF this] as(2)] |
|
4363 from this(2) guess u v apply-by(erule exE)+ note uv=this |
|
4364 have "l\<in>snd ` p" unfolding image_iff apply(rule_tac x="(x,l)" in bexI) using as by auto |
|
4365 hence "l\<in>q" "k\<in>q" "l\<noteq>k" using as(1,3) q(1) unfolding r_def by auto |
|
4366 note q'(5)[OF this] hence "interior l = {}" using subset_interior[OF `l \<subseteq> k`] by blast |
|
4367 thus "content l *\<^sub>R f x = 0" unfolding uv content_eq_0_interior[THEN sym] by auto qed auto |
|
4368 |
|
4369 hence "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + setsum (setsum (\<lambda>(x, k). content k *\<^sub>R f x)) |
|
4370 (qq ` r) - integral {a..b} f) < e" apply(subst(asm) setsum_UNION_zero) |
|
4371 prefer 4 apply assumption apply(rule finite_imageI,fact) |
|
4372 unfolding split_paired_all split_conv image_iff defer apply(erule bexE)+ |
|
4373 proof- fix x m k l T1 T2 assume "(x,m)\<in>T1" "(x,m)\<in>T2" "T1\<noteq>T2" "k\<in>r" "l\<in>r" "T1 = qq k" "T2 = qq l" |
|
4374 note as = this(1-5)[unfolded this(6-)] note kl = tagged_division_ofD(3,4)[OF qq[THEN conjunct1]] |
|
4375 from this(2)[OF as(4,1)] guess u v apply-by(erule exE)+ note uv=this |
|
4376 have *:"interior (k \<inter> l) = {}" unfolding interior_inter apply(rule q') |
|
4377 using as unfolding r_def by auto |
|
4378 have "interior m = {}" unfolding subset_empty[THEN sym] unfolding *[THEN sym] |
|
4379 apply(rule subset_interior) using kl(1)[OF as(4,1)] kl(1)[OF as(5,2)] by auto |
|
4380 thus "content m *\<^sub>R f x = 0" unfolding uv content_eq_0_interior[THEN sym] by auto |
|
4381 qed(insert qq, auto) |
|
4382 |
|
4383 hence **:"norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + setsum (setsum (\<lambda>(x, k). content k *\<^sub>R f x) \<circ> qq) r - |
|
4384 integral {a..b} f) < e" apply(subst(asm) setsum_reindex_nonzero) apply fact |
|
4385 apply(rule setsum_0',rule) unfolding split_paired_all split_conv defer apply assumption |
|
4386 proof- fix k l x m assume as:"k\<in>r" "l\<in>r" "k\<noteq>l" "qq k = qq l" "(x,m)\<in>qq k" |
|
4387 note tagged_division_ofD(6)[OF qq[THEN conjunct1]] from this[OF as(1)] this[OF as(2)] |
|
4388 show "content m *\<^sub>R f x = 0" using as(3) unfolding as by auto qed |
|
4389 |
|
4390 have *:"\<And>ir ip i cr cp. norm((cp + cr) - i) < e \<Longrightarrow> norm(cr - ir) < k \<Longrightarrow> |
|
4391 ip + ir = i \<Longrightarrow> norm(cp - ip) \<le> e + k" |
|
4392 proof- case goal1 thus ?case using norm_triangle_le[of "cp + cr - i" "- (cr - ir)"] |
|
4393 unfolding goal1(3)[THEN sym] norm_minus_cancel by(auto simp add:group_simps) qed |
|
4394 |
|
4395 have "?x = norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p. integral k f))" |
|
4396 unfolding split_def setsum_subtractf .. |
|
4397 also have "... \<le> e + k" apply(rule *[OF **, where ir="setsum (\<lambda>k. integral k f) r"]) |
|
4398 proof- case goal2 have *:"(\<Sum>(x, k)\<in>p. integral k f) = (\<Sum>k\<in>snd ` p. integral k f)" |
|
4399 apply(subst setsum_reindex_nonzero) apply fact |
|
4400 unfolding split_paired_all snd_conv split_def o_def |
|
4401 proof- fix x l y m assume as:"(x,l)\<in>p" "(y,m)\<in>p" "(x,l)\<noteq>(y,m)" "l = m" |
|
4402 from p'(4)[OF as(1)] guess u v apply-by(erule exE)+ note uv=this |
|
4403 show "integral l f = 0" unfolding uv apply(rule integral_unique) |
|
4404 apply(rule has_integral_null) unfolding content_eq_0_interior |
|
4405 using p'(5)[OF as(1-3)] unfolding uv as(4)[THEN sym] by auto |
|
4406 qed auto |
|
4407 show ?case unfolding integral_combine_division_topdown[OF assms(1) q(2)] * r_def |
|
4408 apply(rule setsum_Un_disjoint'[THEN sym]) using q(1) q'(1) p'(1) by auto |
|
4409 next case goal1 have *:"k * real (card r) / (1 + real (card r)) < k" using k by(auto simp add:field_simps) |
|
4410 show ?case apply(rule le_less_trans[of _ "setsum (\<lambda>x. k / (real (card r) + 1)) r"]) |
|
4411 unfolding setsum_subtractf[THEN sym] apply(rule setsum_norm_le,fact) |
|
4412 apply rule apply(drule qq) defer unfolding real_divide_def setsum_left_distrib[THEN sym] |
|
4413 unfolding real_divide_def[THEN sym] using * by(auto simp add:field_simps real_eq_of_nat) |
|
4414 qed finally show "?x \<le> e + k" . qed |
|
4415 |
|
4416 lemma henstock_lemma_part2: fixes f::"real^'m \<Rightarrow> real^'n" |
|
4417 assumes "f integrable_on {a..b}" "0 < e" "gauge d" |
|
4418 "\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow> norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - |
|
4419 integral({a..b}) f) < e" "p tagged_partial_division_of {a..b}" "d fine p" |
|
4420 shows "setsum (\<lambda>(x,k). norm(content k *\<^sub>R f x - integral k f)) p \<le> 2 * real (CARD('n)) * e" |
|
4421 unfolding split_def apply(rule vsum_norm_allsubsets_bound) defer |
|
4422 apply(rule henstock_lemma_part1[unfolded split_def,OF assms(1-3)]) |
|
4423 apply safe apply(rule assms[rule_format,unfolded split_def]) defer |
|
4424 apply(rule tagged_partial_division_subset,rule assms,assumption) |
|
4425 apply(rule fine_subset,assumption,rule assms) using assms(5) by auto |
|
4426 |
|
4427 lemma henstock_lemma: fixes f::"real^'m \<Rightarrow> real^'n" |
|
4428 assumes "f integrable_on {a..b}" "e>0" |
|
4429 obtains d where "gauge d" |
|
4430 "\<forall>p. p tagged_partial_division_of {a..b} \<and> d fine p |
|
4431 \<longrightarrow> setsum (\<lambda>(x,k). norm(content k *\<^sub>R f x - integral k f)) p < e" |
|
4432 proof- have *:"e / (2 * (real CARD('n) + 1)) > 0" apply(rule divide_pos_pos) using assms(2) by auto |
|
4433 from integrable_integral[OF assms(1),unfolded has_integral[of f],rule_format,OF this] |
|
4434 guess d .. note d = conjunctD2[OF this] show thesis apply(rule that,rule d) |
|
4435 proof safe case goal1 note * = henstock_lemma_part2[OF assms(1) * d this] |
|
4436 show ?case apply(rule le_less_trans[OF *]) using `e>0` by(auto simp add:field_simps) qed qed |
|
4437 |
|
4438 subsection {* monotone convergence (bounded interval first). *} |
|
4439 |
|
4440 lemma monotone_convergence_interval: fixes f::"nat \<Rightarrow> real^'n \<Rightarrow> real^1" |
|
4441 assumes "\<forall>k. (f k) integrable_on {a..b}" |
|
4442 "\<forall>k. \<forall>x\<in>{a..b}. dest_vec1(f k x) \<le> dest_vec1(f (Suc k) x)" |
|
4443 "\<forall>x\<in>{a..b}. ((\<lambda>k. f k x) ---> g x) sequentially" |
|
4444 "bounded {integral {a..b} (f k) | k . k \<in> UNIV}" |
|
4445 shows "g integrable_on {a..b} \<and> ((\<lambda>k. integral ({a..b}) (f k)) ---> integral ({a..b}) g) sequentially" |
|
4446 proof(case_tac[!] "content {a..b} = 0") assume as:"content {a..b} = 0" |
|
4447 show ?thesis using integrable_on_null[OF as] unfolding integral_null[OF as] using Lim_const by auto |
|
4448 next assume ab:"content {a..b} \<noteq> 0" |
|
4449 have fg:"\<forall>x\<in>{a..b}. \<forall> k. (f k x)$1 \<le> (g x)$1" |
|
4450 proof safe case goal1 note assms(3)[rule_format,OF this] |
|
4451 note * = Lim_component_ge[OF this trivial_limit_sequentially] |
|
4452 show ?case apply(rule *) unfolding eventually_sequentially |
|
4453 apply(rule_tac x=k in exI) apply- apply(rule transitive_stepwise_le) |
|
4454 using assms(2)[rule_format,OF goal1] by auto qed |
|
4455 have "\<exists>i. ((\<lambda>k. integral ({a..b}) (f k)) ---> i) sequentially" |
|
4456 apply(rule bounded_increasing_convergent) defer |
|
4457 apply rule apply(rule integral_component_le) apply safe |
|
4458 apply(rule assms(1-2)[rule_format])+ using assms(4) by auto |
|
4459 then guess i .. note i=this |
|
4460 have i':"\<And>k. dest_vec1(integral({a..b}) (f k)) \<le> dest_vec1 i" |
|
4461 apply(rule Lim_component_ge,rule i) apply(rule trivial_limit_sequentially) |
|
4462 unfolding eventually_sequentially apply(rule_tac x=k in exI) |
|
4463 apply(rule transitive_stepwise_le) prefer 3 apply(rule integral_dest_vec1_le) |
|
4464 apply(rule assms(1-2)[rule_format])+ using assms(2) by auto |
|
4465 |
|
4466 have "(g has_integral i) {a..b}" unfolding has_integral |
|
4467 proof safe case goal1 note e=this |
|
4468 hence "\<forall>k. (\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow> |
|
4469 norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f k x) - integral {a..b} (f k)) < e / 2 ^ (k + 2)))" |
|
4470 apply-apply(rule,rule assms(1)[unfolded has_integral_integral has_integral,rule_format]) |
|
4471 apply(rule divide_pos_pos) by auto |
|
4472 from choice[OF this] guess c .. note c=conjunctD2[OF this[rule_format],rule_format] |
|
4473 |
|
4474 have "\<exists>r. \<forall>k\<ge>r. 0 \<le> i$1 - dest_vec1(integral {a..b} (f k)) \<and> |
|
4475 i$1 - dest_vec1(integral {a..b} (f k)) < e / 4" |
|
4476 proof- case goal1 have "e/4 > 0" using e by auto |
|
4477 from i[unfolded Lim_sequentially,rule_format,OF this] guess r .. |
|
4478 thus ?case apply(rule_tac x=r in exI) apply rule |
|
4479 apply(erule_tac x=k in allE) |
|
4480 proof- case goal1 thus ?case using i'[of k] unfolding dist_real by auto qed qed |
|
4481 then guess r .. note r=conjunctD2[OF this[rule_format]] |
|
4482 |
|
4483 have "\<forall>x\<in>{a..b}. \<exists>n\<ge>r. \<forall>k\<ge>n. 0 \<le> (g x)$1 - (f k x)$1 \<and> |
|
4484 (g x)$1 - (f k x)$1 < e / (4 * content({a..b}))" |
|
4485 proof case goal1 have "e / (4 * content {a..b}) > 0" apply(rule divide_pos_pos,fact) |
|
4486 using ab content_pos_le[of a b] by auto |
|
4487 from assms(3)[rule_format,OF goal1,unfolded Lim_sequentially,rule_format,OF this] |
|
4488 guess n .. note n=this |
|
4489 thus ?case apply(rule_tac x="n + r" in exI) apply safe apply(erule_tac[2-3] x=k in allE) |
|
4490 unfolding dist_real using fg[rule_format,OF goal1] by(auto simp add:field_simps) qed |
|
4491 from bchoice[OF this] guess m .. note m=conjunctD2[OF this[rule_format],rule_format] |
|
4492 def d \<equiv> "\<lambda>x. c (m x) x" |
|
4493 |
|
4494 show ?case apply(rule_tac x=d in exI) |
|
4495 proof safe show "gauge d" using c(1) unfolding gauge_def d_def by auto |
|
4496 next fix p assume p:"p tagged_division_of {a..b}" "d fine p" |
|
4497 note p'=tagged_division_ofD[OF p(1)] |
|
4498 have "\<exists>a. \<forall>x\<in>p. m (fst x) \<le> a" by(rule upper_bound_finite_set,fact) |
|
4499 then guess s .. note s=this |
|
4500 have *:"\<forall>a b c d. norm(a - b) \<le> e / 4 \<and> norm(b - c) < e / 2 \<and> |
|
4501 norm(c - d) < e / 4 \<longrightarrow> norm(a - d) < e" |
|
4502 proof safe case goal1 thus ?case using norm_triangle_lt[of "a - b" "b - c" "3* e/4"] |
|
4503 norm_triangle_lt[of "a - b + (b - c)" "c - d" e] unfolding norm_minus_cancel |
|
4504 by(auto simp add:group_simps) qed |
|
4505 show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - i) < e" apply(rule *[rule_format,where |
|
4506 b="\<Sum>(x, k)\<in>p. content k *\<^sub>R f (m x) x" and c="\<Sum>(x, k)\<in>p. integral k (f (m x))"]) |
|
4507 proof safe case goal1 |
|
4508 show ?case apply(rule order_trans[of _ "\<Sum>(x, k)\<in>p. content k * (e / (4 * content {a..b}))"]) |
|
4509 unfolding setsum_subtractf[THEN sym] apply(rule order_trans,rule setsum_norm[OF p'(1)]) |
|
4510 apply(rule setsum_mono) unfolding split_paired_all split_conv |
|
4511 unfolding split_def setsum_left_distrib[THEN sym] scaleR.diff_right[THEN sym] |
|
4512 unfolding additive_content_tagged_division[OF p(1), unfolded split_def] |
|
4513 proof- fix x k assume xk:"(x,k) \<in> p" hence x:"x\<in>{a..b}" using p'(2-3)[OF xk] by auto |
|
4514 from p'(4)[OF xk] guess u v apply-by(erule exE)+ note uv=this |
|
4515 show " norm (content k *\<^sub>R (g x - f (m x) x)) \<le> content k * (e / (4 * content {a..b}))" |
|
4516 unfolding norm_scaleR uv unfolding abs_of_nonneg[OF content_pos_le] |
|
4517 apply(rule mult_left_mono) unfolding norm_real using m(2)[OF x,of "m x"] by auto |
|
4518 qed(insert ab,auto) |
|
4519 |
|
4520 next case goal2 show ?case apply(rule le_less_trans[of _ "norm (\<Sum>j = 0..s. |
|
4521 \<Sum>(x, k)\<in>{xk\<in>p. m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x)))"]) |
|
4522 apply(subst setsum_group) apply fact apply(rule finite_atLeastAtMost) defer |
|
4523 apply(subst split_def)+ unfolding setsum_subtractf apply rule |
|
4524 proof- show "norm (\<Sum>j = 0..s. \<Sum>(x, k)\<in>{xk \<in> p. |
|
4525 m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x))) < e / 2" |
|
4526 apply(rule le_less_trans[of _ "setsum (\<lambda>i. e / 2^(i+2)) {0..s}"]) |
|
4527 apply(rule setsum_norm_le[OF finite_atLeastAtMost]) |
|
4528 proof show "(\<Sum>i = 0..s. e / 2 ^ (i + 2)) < e / 2" |
|
4529 unfolding power_add real_divide_def inverse_mult_distrib |
|
4530 unfolding setsum_right_distrib[THEN sym] setsum_left_distrib[THEN sym] |
|
4531 unfolding power_inverse sum_gp apply(rule mult_strict_left_mono[OF _ e]) |
|
4532 unfolding power2_eq_square by auto |
|
4533 fix t assume "t\<in>{0..s}" |
|
4534 show "norm (\<Sum>(x, k)\<in>{xk \<in> p. m (fst xk) = t}. content k *\<^sub>R f (m x) x - |
|
4535 integral k (f (m x))) \<le> e / 2 ^ (t + 2)"apply(rule order_trans[of _ |
|
4536 "norm(setsum (\<lambda>(x,k). content k *\<^sub>R f t x - integral k (f t)) {xk \<in> p. m (fst xk) = t})"]) |
|
4537 apply(rule eq_refl) apply(rule arg_cong[where f=norm]) apply(rule setsum_cong2) defer |
|
4538 apply(rule henstock_lemma_part1) apply(rule assms(1)[rule_format]) |
|
4539 apply(rule divide_pos_pos,rule e) defer apply safe apply(rule c)+ |
|
4540 apply rule apply assumption+ apply(rule tagged_partial_division_subset[of p]) |
|
4541 apply(rule p(1)[unfolded tagged_division_of_def,THEN conjunct1]) defer |
|
4542 unfolding fine_def apply safe apply(drule p(2)[unfolded fine_def,rule_format]) |
|
4543 unfolding d_def by auto qed |
|
4544 qed(insert s, auto) |
|
4545 |
|
4546 next case goal3 |
|
4547 note comb = integral_combine_tagged_division_topdown[OF assms(1)[rule_format] p(1)] |
|
4548 have *:"\<And>sr sx ss ks kr::real^1. kr = sr \<longrightarrow> ks = ss \<longrightarrow> ks \<le> i \<and> sr \<le> sx \<and> sx \<le> ss \<and> 0 \<le> i$1 - kr$1 |
|
4549 \<and> i$1 - kr$1 < e/4 \<longrightarrow> abs(sx$1 - i$1) < e/4" unfolding Cart_eq forall_1 vector_le_def by arith |
|
4550 show ?case unfolding norm_real Cart_nth.diff apply(rule *[rule_format],safe) |
|
4551 apply(rule comb[of r],rule comb[of s]) unfolding vector_le_def forall_1 setsum_component |
|
4552 apply(rule i') apply(rule_tac[1-2] setsum_mono) unfolding split_paired_all split_conv |
|
4553 apply(rule_tac[1-2] integral_component_le[OF ]) |
|
4554 proof safe show "0 \<le> i$1 - (integral {a..b} (f r))$1" using r(1) by auto |
|
4555 show "i$1 - (integral {a..b} (f r))$1 < e / 4" using r(2) by auto |
|
4556 fix x k assume xk:"(x,k)\<in>p" from p'(4)[OF this] guess u v apply-by(erule exE)+ note uv=this |
|
4557 show "f r integrable_on k" "f s integrable_on k" "f (m x) integrable_on k" "f (m x) integrable_on k" |
|
4558 unfolding uv apply(rule_tac[!] integrable_on_subinterval[OF assms(1)[rule_format]]) |
|
4559 using p'(3)[OF xk] unfolding uv by auto |
|
4560 fix y assume "y\<in>k" hence "y\<in>{a..b}" using p'(3)[OF xk] by auto |
|
4561 hence *:"\<And>m. \<forall>n\<ge>m. (f m y)$1 \<le> (f n y)$1" apply-apply(rule transitive_stepwise_le) using assms(2) by auto |
|
4562 show "(f r y)$1 \<le> (f (m x) y)$1" "(f (m x) y)$1 \<le> (f s y)$1" |
|
4563 apply(rule_tac[!] *[rule_format]) using s[rule_format,OF xk] m(1)[of x] p'(2-3)[OF xk] by auto |
|
4564 qed qed qed qed note * = this |
|
4565 |
|
4566 have "integral {a..b} g = i" apply(rule integral_unique) using * . |
|
4567 thus ?thesis using i * by auto qed |
|
4568 |
|
4569 lemma monotone_convergence_increasing: fixes f::"nat \<Rightarrow> real^'n \<Rightarrow> real^1" |
|
4570 assumes "\<forall>k. (f k) integrable_on s" "\<forall>k. \<forall>x\<in>s. (f k x)$1 \<le> (f (Suc k) x)$1" |
|
4571 "\<forall>x\<in>s. ((\<lambda>k. f k x) ---> g x) sequentially" "bounded {integral s (f k)| k. True}" |
|
4572 shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially" |
|
4573 proof- have lem:"\<And>f::nat \<Rightarrow> real^'n \<Rightarrow> real^1. \<And> g s. \<forall>k.\<forall>x\<in>s. 0\<le>dest_vec1 (f k x) \<Longrightarrow> \<forall>k. (f k) integrable_on s \<Longrightarrow> |
|
4574 \<forall>k. \<forall>x\<in>s. (f k x)$1 \<le> (f (Suc k) x)$1 \<Longrightarrow> \<forall>x\<in>s. ((\<lambda>k. f k x) ---> g x) sequentially \<Longrightarrow> |
|
4575 bounded {integral s (f k)| k. True} \<Longrightarrow> g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially" |
|
4576 proof- case goal1 note assms=this[rule_format] |
|
4577 have "\<forall>x\<in>s. \<forall>k. dest_vec1(f k x) \<le> dest_vec1(g x)" apply safe apply(rule Lim_component_ge) |
|
4578 apply(rule goal1(4)[rule_format],assumption) apply(rule trivial_limit_sequentially) |
|
4579 unfolding eventually_sequentially apply(rule_tac x=k in exI) |
|
4580 apply(rule transitive_stepwise_le) using goal1(3) by auto note fg=this[rule_format] |
|
4581 |
|
4582 have "\<exists>i. ((\<lambda>k. integral s (f k)) ---> i) sequentially" apply(rule bounded_increasing_convergent) |
|
4583 apply(rule goal1(5)) apply(rule,rule integral_component_le) apply(rule goal1(2)[rule_format])+ |
|
4584 using goal1(3) by auto then guess i .. note i=this |
|
4585 have "\<And>k. \<forall>x\<in>s. \<forall>n\<ge>k. f k x \<le> f n x" apply(rule,rule transitive_stepwise_le) using goal1(3) by auto |
|
4586 hence i':"\<forall>k. (integral s (f k))$1 \<le> i$1" apply-apply(rule,rule Lim_component_ge) |
|
4587 apply(rule i,rule trivial_limit_sequentially) unfolding eventually_sequentially |
|
4588 apply(rule_tac x=k in exI,safe) apply(rule integral_dest_vec1_le) |
|
4589 apply(rule goal1(2)[rule_format])+ by auto |
|
4590 |
|
4591 note int = assms(2)[unfolded integrable_alt[of _ s],THEN conjunct1,rule_format] |
|
4592 have ifif:"\<And>k t. (\<lambda>x. if x \<in> t then if x \<in> s then f k x else 0 else 0) = |
|
4593 (\<lambda>x. if x \<in> t\<inter>s then f k x else 0)" apply(rule ext) by auto |
|
4594 have int':"\<And>k a b. f k integrable_on {a..b} \<inter> s" apply(subst integrable_restrict_univ[THEN sym]) |
|
4595 apply(subst ifif[THEN sym]) apply(subst integrable_restrict_univ) using int . |
|
4596 have "\<And>a b. (\<lambda>x. if x \<in> s then g x else 0) integrable_on {a..b} \<and> |
|
4597 ((\<lambda>k. integral {a..b} (\<lambda>x. if x \<in> s then f k x else 0)) ---> |
|
4598 integral {a..b} (\<lambda>x. if x \<in> s then g x else 0)) sequentially" |
|
4599 proof(rule monotone_convergence_interval,safe) |
|
4600 case goal1 show ?case using int . |
|
4601 next case goal2 thus ?case apply-apply(cases "x\<in>s") using assms(3) by auto |
|
4602 next case goal3 thus ?case apply-apply(cases "x\<in>s") using assms(4) by auto |
|
4603 next case goal4 note * = integral_dest_vec1_nonneg[unfolded vector_le_def forall_1 zero_index] |
|
4604 have "\<And>k. norm (integral {a..b} (\<lambda>x. if x \<in> s then f k x else 0)) \<le> norm (integral s (f k))" |
|
4605 unfolding norm_real apply(subst abs_of_nonneg) apply(rule *[OF int]) |
|
4606 apply(safe,case_tac "x\<in>s") apply(drule assms(1)) prefer 3 |
|
4607 apply(subst abs_of_nonneg) apply(rule *[OF assms(2) goal1(1)[THEN spec]]) |
|
4608 apply(subst integral_restrict_univ[THEN sym,OF int]) |
|
4609 unfolding ifif unfolding integral_restrict_univ[OF int'] |
|
4610 apply(rule integral_subset_component_le[OF _ int' assms(2)]) using assms(1) by auto |
|
4611 thus ?case using assms(5) unfolding bounded_iff apply safe |
|
4612 apply(rule_tac x=aa in exI,safe) apply(erule_tac x="integral s (f k)" in ballE) |
|
4613 apply(rule order_trans) apply assumption by auto qed note g = conjunctD2[OF this] |
|
4614 |
|
4615 have "(g has_integral i) s" unfolding has_integral_alt' apply safe apply(rule g(1)) |
|
4616 proof- case goal1 hence "e/4>0" by auto |
|
4617 from i[unfolded Lim_sequentially,rule_format,OF this] guess N .. note N=this |
|
4618 note assms(2)[of N,unfolded has_integral_integral has_integral_alt'[of "f N"]] |
|
4619 from this[THEN conjunct2,rule_format,OF `e/4>0`] guess B .. note B=conjunctD2[OF this] |
|
4620 show ?case apply(rule,rule,rule B,safe) |
|
4621 proof- fix a b::"real^'n" assume ab:"ball 0 B \<subseteq> {a..b}" |
|
4622 from `e>0` have "e/2>0" by auto |
|
4623 from g(2)[unfolded Lim_sequentially,of a b,rule_format,OF this] guess M .. note M=this |
|
4624 have **:"norm (integral {a..b} (\<lambda>x. if x \<in> s then f N x else 0) - i) < e/2" |
|
4625 apply(rule norm_triangle_half_l) using B(2)[rule_format,OF ab] N[rule_format,of N] |
|
4626 unfolding vector_dist_norm apply-defer apply(subst norm_minus_commute) by auto |
|
4627 have *:"\<And>f1 f2 g. abs(f1 - i$1) < e / 2 \<longrightarrow> abs(f2 - g) < e / 2 \<longrightarrow> f1 \<le> f2 \<longrightarrow> f2 \<le> i$1 |
|
4628 \<longrightarrow> abs(g - i$1) < e" by arith |
|
4629 show "norm (integral {a..b} (\<lambda>x. if x \<in> s then g x else 0) - i) < e" |
|
4630 unfolding norm_real Cart_simps apply(rule *[rule_format]) |
|
4631 apply(rule **[unfolded norm_real Cart_simps]) |
|
4632 apply(rule M[rule_format,of "M + N",unfolded dist_real]) apply(rule le_add1) |
|
4633 apply(rule integral_component_le[OF int int]) defer |
|
4634 apply(rule order_trans[OF _ i'[rule_format,of "M + N"]]) |
|
4635 proof safe case goal2 have "\<And>m. x\<in>s \<Longrightarrow> \<forall>n\<ge>m. (f m x)$1 \<le> (f n x)$1" |
|
4636 apply(rule transitive_stepwise_le) using assms(3) by auto thus ?case by auto |
|
4637 next case goal1 show ?case apply(subst integral_restrict_univ[THEN sym,OF int]) |
|
4638 unfolding ifif integral_restrict_univ[OF int'] |
|
4639 apply(rule integral_subset_component_le[OF _ int']) using assms by auto |
|
4640 qed qed qed |
|
4641 thus ?case apply safe defer apply(drule integral_unique) using i by auto qed |
|
4642 |
|
4643 have sub:"\<And>k. integral s (\<lambda>x. f k x - f 0 x) = integral s (f k) - integral s (f 0)" |
|
4644 apply(subst integral_sub) apply(rule assms(1)[rule_format])+ by rule |
|
4645 have "\<And>x m. x\<in>s \<Longrightarrow> \<forall>n\<ge>m. dest_vec1 (f m x) \<le> dest_vec1 (f n x)" apply(rule transitive_stepwise_le) |
|
4646 using assms(2) by auto note * = this[rule_format] |
|
4647 have "(\<lambda>x. g x - f 0 x) integrable_on s \<and>((\<lambda>k. integral s (\<lambda>x. f (Suc k) x - f 0 x)) ---> |
|
4648 integral s (\<lambda>x. g x - f 0 x)) sequentially" apply(rule lem,safe) |
|
4649 proof- case goal1 thus ?case using *[of x 0 "Suc k"] by auto |
|
4650 next case goal2 thus ?case apply(rule integrable_sub) using assms(1) by auto |
|
4651 next case goal3 thus ?case using *[of x "Suc k" "Suc (Suc k)"] by auto |
|
4652 next case goal4 thus ?case apply-apply(rule Lim_sub) |
|
4653 using seq_offset[OF assms(3)[rule_format],of x 1] by auto |
|
4654 next case goal5 thus ?case using assms(4) unfolding bounded_iff |
|
4655 apply safe apply(rule_tac x="a + norm (integral s (\<lambda>x. f 0 x))" in exI) |
|
4656 apply safe apply(erule_tac x="integral s (\<lambda>x. f (Suc k) x)" in ballE) unfolding sub |
|
4657 apply(rule order_trans[OF norm_triangle_ineq4]) by auto qed |
|
4658 note conjunctD2[OF this] note Lim_add[OF this(2) Lim_const[of "integral s (f 0)"]] |
|
4659 integrable_add[OF this(1) assms(1)[rule_format,of 0]] |
|
4660 thus ?thesis unfolding sub apply-apply rule defer apply(subst(asm) integral_sub) |
|
4661 using assms(1) apply auto apply(rule seq_offset_rev[where k=1]) by auto qed |
|
4662 |
|
4663 lemma monotone_convergence_decreasing: fixes f::"nat \<Rightarrow> real^'n \<Rightarrow> real^1" |
|
4664 assumes "\<forall>k. (f k) integrable_on s" "\<forall>k. \<forall>x\<in>s. (f (Suc k) x)$1 \<le> (f k x)$1" |
|
4665 "\<forall>x\<in>s. ((\<lambda>k. f k x) ---> g x) sequentially" "bounded {integral s (f k)| k. True}" |
|
4666 shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially" |
|
4667 proof- note assm = assms[rule_format] |
|
4668 have *:"{integral s (\<lambda>x. - f k x) |k. True} = op *\<^sub>R -1 ` {integral s (f k)| k. True}" |
|
4669 apply safe unfolding image_iff apply(rule_tac x="integral s (f k)" in bexI) prefer 3 |
|
4670 apply(rule_tac x=k in exI) unfolding integral_neg[OF assm(1)] by auto |
|
4671 have "(\<lambda>x. - g x) integrable_on s \<and> ((\<lambda>k. integral s (\<lambda>x. - f k x)) |
|
4672 ---> integral s (\<lambda>x. - g x)) sequentially" apply(rule monotone_convergence_increasing) |
|
4673 apply(safe,rule integrable_neg) apply(rule assm) defer apply(rule Lim_neg) |
|
4674 apply(rule assm,assumption) unfolding * apply(rule bounded_scaling) using assm by auto |
|
4675 note * = conjunctD2[OF this] |
|
4676 show ?thesis apply rule using integrable_neg[OF *(1)] defer |
|
4677 using Lim_neg[OF *(2)] apply- unfolding integral_neg[OF assm(1)] |
|
4678 unfolding integral_neg[OF *(1),THEN sym] by auto qed |
|
4679 |
|
4680 lemma monotone_convergence_increasing_real: fixes f::"nat \<Rightarrow> real^'n \<Rightarrow> real" |
|
4681 assumes "\<forall>k. (f k) integrable_on s" "\<forall>k. \<forall>x\<in>s. (f (Suc k) x) \<ge> (f k x)" |
|
4682 "\<forall>x\<in>s. ((\<lambda>k. f k x) ---> g x) sequentially" "bounded {integral s (f k)| k. True}" |
|
4683 shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially" |
|
4684 proof- have *:"{integral s (\<lambda>x. vec1 (f k x)) |k. True} = vec1 ` {integral s (f k) |k. True}" |
|
4685 unfolding integral_trans[OF assms(1)[rule_format]] by auto |
|
4686 have "vec1 \<circ> g integrable_on s \<and> ((\<lambda>k. integral s (vec1 \<circ> f k)) ---> integral s (vec1 \<circ> g)) sequentially" |
|
4687 apply(rule monotone_convergence_increasing) unfolding o_def integrable_on_trans |
|
4688 unfolding vec1_dest_vec1 apply(rule assms)+ unfolding Lim_trans unfolding * using assms(3,4) by auto |
|
4689 thus ?thesis unfolding o_def unfolding integral_trans[OF assms(1)[rule_format]] by auto qed |
|
4690 |
|
4691 lemma monotone_convergence_decreasing_real: fixes f::"nat \<Rightarrow> real^'n \<Rightarrow> real" |
|
4692 assumes "\<forall>k. (f k) integrable_on s" "\<forall>k. \<forall>x\<in>s. (f (Suc k) x) \<le> (f k x)" |
|
4693 "\<forall>x\<in>s. ((\<lambda>k. f k x) ---> g x) sequentially" "bounded {integral s (f k)| k. True}" |
|
4694 shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially" |
|
4695 proof- have *:"{integral s (\<lambda>x. vec1 (f k x)) |k. True} = vec1 ` {integral s (f k) |k. True}" |
|
4696 unfolding integral_trans[OF assms(1)[rule_format]] by auto |
|
4697 have "vec1 \<circ> g integrable_on s \<and> ((\<lambda>k. integral s (vec1 \<circ> f k)) ---> integral s (vec1 \<circ> g)) sequentially" |
|
4698 apply(rule monotone_convergence_decreasing) unfolding o_def integrable_on_trans |
|
4699 unfolding vec1_dest_vec1 apply(rule assms)+ unfolding Lim_trans unfolding * using assms(3,4) by auto |
|
4700 thus ?thesis unfolding o_def unfolding integral_trans[OF assms(1)[rule_format]] by auto qed |
|
4701 |
|
4702 subsection {* absolute integrability (this is the same as Lebesgue integrability). *} |
|
4703 |
|
4704 definition absolutely_integrable_on (infixr "absolutely'_integrable'_on" 46) where |
|
4705 "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s \<and> (\<lambda>x. (norm(f x))) integrable_on s" |
|
4706 |
|
4707 lemma absolutely_integrable_onI[intro?]: |
|
4708 "f integrable_on s \<Longrightarrow> (\<lambda>x. (norm(f x))) integrable_on s \<Longrightarrow> f absolutely_integrable_on s" |
|
4709 unfolding absolutely_integrable_on_def by auto |
|
4710 |
|
4711 lemma absolutely_integrable_onD[dest]: assumes "f absolutely_integrable_on s" |
|
4712 shows "f integrable_on s" "(\<lambda>x. (norm(f x))) integrable_on s" |
|
4713 using assms unfolding absolutely_integrable_on_def by auto |
|
4714 |
|
4715 lemma absolutely_integrable_on_trans[simp]: fixes f::"real^'n \<Rightarrow> real" shows |
|
4716 "(vec1 o f) absolutely_integrable_on s \<longleftrightarrow> f absolutely_integrable_on s" |
|
4717 unfolding absolutely_integrable_on_def o_def by auto |
|
4718 |
|
4719 lemma integral_norm_bound_integral: fixes f::"real^'n \<Rightarrow> 'a::banach" |
|
4720 assumes "f integrable_on s" "g integrable_on s" "\<forall>x\<in>s. norm(f x) \<le> g x" |
|
4721 shows "norm(integral s f) \<le> (integral s g)" |
|
4722 proof- have *:"\<And>x y. (\<forall>e::real. 0 < e \<longrightarrow> x < y + e) \<longrightarrow> x \<le> y" apply(safe,rule ccontr) |
|
4723 apply(erule_tac x="x - y" in allE) by auto |
|
4724 have "\<And>e sg dsa dia ig. norm(sg) \<le> dsa \<longrightarrow> abs(dsa - dia) < e / 2 \<longrightarrow> norm(sg - ig) < e / 2 |
|
4725 \<longrightarrow> norm(ig) < dia + e" |
|
4726 proof safe case goal1 show ?case apply(rule le_less_trans[OF norm_triangle_sub[of ig sg]]) |
|
4727 apply(subst real_sum_of_halves[of e,THEN sym]) unfolding class_semiring.add_a |
|
4728 apply(rule add_le_less_mono) defer apply(subst norm_minus_commute,rule goal1) |
|
4729 apply(rule order_trans[OF goal1(1)]) using goal1(2) by arith |
|
4730 qed note norm=this[rule_format] |
|
4731 have lem:"\<And>f::real^'n \<Rightarrow> 'a. \<And> g a b. f integrable_on {a..b} \<Longrightarrow> g integrable_on {a..b} \<Longrightarrow> |
|
4732 \<forall>x\<in>{a..b}. norm(f x) \<le> (g x) \<Longrightarrow> norm(integral({a..b}) f) \<le> (integral({a..b}) g)" |
|
4733 proof(rule *[rule_format]) case goal1 hence *:"e/2>0" by auto |
|
4734 from integrable_integral[OF goal1(1),unfolded has_integral[of f],rule_format,OF *] |
|
4735 guess d1 .. note d1 = conjunctD2[OF this,rule_format] |
|
4736 from integrable_integral[OF goal1(2),unfolded has_integral[of g],rule_format,OF *] |
|
4737 guess d2 .. note d2 = conjunctD2[OF this,rule_format] |
|
4738 note gauge_inter[OF d1(1) d2(1)] |
|
4739 from fine_division_exists[OF this, of a b] guess p . note p=this |
|
4740 show ?case apply(rule norm) defer |
|
4741 apply(rule d2(2)[OF conjI[OF p(1)],unfolded real_norm_def]) defer |
|
4742 apply(rule d1(2)[OF conjI[OF p(1)]]) defer apply(rule setsum_norm_le) |
|
4743 proof safe fix x k assume "(x,k)\<in>p" note as = tagged_division_ofD(2-4)[OF p(1) this] |
|
4744 from this(3) guess u v apply-by(erule exE)+ note uv=this |
|
4745 show "norm (content k *\<^sub>R f x) \<le> content k *\<^sub>R g x" unfolding uv norm_scaleR |
|
4746 unfolding abs_of_nonneg[OF content_pos_le] real_scaleR_def |
|
4747 apply(rule mult_left_mono) using goal1(3) as by auto |
|
4748 qed(insert p[unfolded fine_inter],auto) qed |
|
4749 |
|
4750 { presume "\<And>e. 0 < e \<Longrightarrow> norm (integral s f) < integral s g + e" |
|
4751 thus ?thesis apply-apply(rule *[rule_format]) by auto } |
|
4752 fix e::real assume "e>0" hence e:"e/2 > 0" by auto |
|
4753 note assms(1)[unfolded integrable_alt[of f]] note f=this[THEN conjunct1,rule_format] |
|
4754 note assms(2)[unfolded integrable_alt[of g]] note g=this[THEN conjunct1,rule_format] |
|
4755 from integrable_integral[OF assms(1),unfolded has_integral'[of f],rule_format,OF e] |
|
4756 guess B1 .. note B1=conjunctD2[OF this[rule_format],rule_format] |
|
4757 from integrable_integral[OF assms(2),unfolded has_integral'[of g],rule_format,OF e] |
|
4758 guess B2 .. note B2=conjunctD2[OF this[rule_format],rule_format] |
|
4759 from bounded_subset_closed_interval[OF bounded_ball, of "0::real^'n" "max B1 B2"] |
|
4760 guess a b apply-by(erule exE)+ note ab=this[unfolded ball_max_Un] |
|
4761 |
|
4762 have "ball 0 B1 \<subseteq> {a..b}" using ab by auto |
|
4763 from B1(2)[OF this] guess z .. note z=conjunctD2[OF this] |
|
4764 have "ball 0 B2 \<subseteq> {a..b}" using ab by auto |
|
4765 from B2(2)[OF this] guess w .. note w=conjunctD2[OF this] |
|
4766 |
|
4767 show "norm (integral s f) < integral s g + e" apply(rule norm) |
|
4768 apply(rule lem[OF f g, of a b]) unfolding integral_unique[OF z(1)] integral_unique[OF w(1)] |
|
4769 defer apply(rule w(2)[unfolded real_norm_def],rule z(2)) |
|
4770 apply safe apply(case_tac "x\<in>s") unfolding if_P apply(rule assms(3)[rule_format]) by auto qed |
|
4771 |
|
4772 lemma integral_norm_bound_integral_component: fixes f::"real^'n \<Rightarrow> 'a::banach" |
|
4773 assumes "f integrable_on s" "g integrable_on s" "\<forall>x\<in>s. norm(f x) \<le> (g x)$k" |
|
4774 shows "norm(integral s f) \<le> (integral s g)$k" |
|
4775 proof- have "norm (integral s f) \<le> integral s ((\<lambda>x. x $ k) o g)" |
|
4776 apply(rule integral_norm_bound_integral[OF assms(1)]) |
|
4777 apply(rule integrable_linear[OF assms(2)],rule) |
|
4778 unfolding o_def by(rule assms) |
|
4779 thus ?thesis unfolding o_def integral_component_eq[OF assms(2)] . qed |
|
4780 |
|
4781 lemma has_integral_norm_bound_integral_component: fixes f::"real^'n \<Rightarrow> 'a::banach" |
|
4782 assumes "(f has_integral i) s" "(g has_integral j) s" "\<forall>x\<in>s. norm(f x) \<le> (g x)$k" |
|
4783 shows "norm(i) \<le> j$k" using integral_norm_bound_integral_component[of f s g k] |
|
4784 unfolding integral_unique[OF assms(1)] integral_unique[OF assms(2)] |
|
4785 using assms by auto |
|
4786 |
|
4787 lemma absolutely_integrable_le: fixes f::"real^'n \<Rightarrow> 'a::banach" |
|
4788 assumes "f absolutely_integrable_on s" |
|
4789 shows "norm(integral s f) \<le> integral s (\<lambda>x. norm(f x))" |
|
4790 apply(rule integral_norm_bound_integral) using assms by auto |
|
4791 |
|
4792 lemma absolutely_integrable_0[intro]: "(\<lambda>x. 0) absolutely_integrable_on s" |
|
4793 unfolding absolutely_integrable_on_def by auto |
|
4794 |
|
4795 lemma absolutely_integrable_cmul[intro]: |
|
4796 "f absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. c *\<^sub>R f x) absolutely_integrable_on s" |
|
4797 unfolding absolutely_integrable_on_def using integrable_cmul[of f s c] |
|
4798 using integrable_cmul[of "\<lambda>x. norm (f x)" s "abs c"] by auto |
|
4799 |
|
4800 lemma absolutely_integrable_neg[intro]: |
|
4801 "f absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. -f(x)) absolutely_integrable_on s" |
|
4802 apply(drule absolutely_integrable_cmul[where c="-1"]) by auto |
|
4803 |
|
4804 lemma absolutely_integrable_norm[intro]: |
|
4805 "f absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. norm(f x)) absolutely_integrable_on s" |
|
4806 unfolding absolutely_integrable_on_def by auto |
|
4807 |
|
4808 lemma absolutely_integrable_abs[intro]: |
|
4809 "f absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. abs(f x::real)) absolutely_integrable_on s" |
|
4810 apply(drule absolutely_integrable_norm) unfolding real_norm_def . |
|
4811 |
|
4812 lemma absolutely_integrable_on_subinterval: fixes f::"real^'n \<Rightarrow> 'a::banach" shows |
|
4813 "f absolutely_integrable_on s \<Longrightarrow> {a..b} \<subseteq> s \<Longrightarrow> f absolutely_integrable_on {a..b}" |
|
4814 unfolding absolutely_integrable_on_def by(meson integrable_on_subinterval) |
|
4815 |
|
4816 lemma absolutely_integrable_bounded_variation: fixes f::"real^'n \<Rightarrow> 'a::banach" |
|
4817 assumes "f absolutely_integrable_on UNIV" |
|
4818 obtains B where "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B" |
|
4819 apply(rule that[of "integral UNIV (\<lambda>x. norm (f x))"]) |
|
4820 proof safe case goal1 note d = division_ofD[OF this(2)] |
|
4821 have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>i\<in>d. integral i (\<lambda>x. norm (f x)))" |
|
4822 apply(rule setsum_mono,rule absolutely_integrable_le) apply(drule d(4),safe) |
|
4823 apply(rule absolutely_integrable_on_subinterval[OF assms]) by auto |
|
4824 also have "... \<le> integral (\<Union>d) (\<lambda>x. norm (f x))" |
|
4825 apply(subst integral_combine_division_topdown[OF _ goal1(2)]) |
|
4826 using integrable_on_subdivision[OF goal1(2)] using assms by auto |
|
4827 also have "... \<le> integral UNIV (\<lambda>x. norm (f x))" |
|
4828 apply(rule integral_subset_le) |
|
4829 using integrable_on_subdivision[OF goal1(2)] using assms by auto |
|
4830 finally show ?case . qed |
|
4831 |
|
4832 lemma helplemma: |
|
4833 assumes "setsum (\<lambda>x. norm(f x - g x)) s < e" "finite s" |
|
4834 shows "abs(setsum (\<lambda>x. norm(f x)) s - setsum (\<lambda>x. norm(g x)) s) < e" |
|
4835 unfolding setsum_subtractf[THEN sym] apply(rule le_less_trans[OF setsum_abs]) |
|
4836 apply(rule le_less_trans[OF _ assms(1)]) apply(rule setsum_mono) |
|
4837 using norm_triangle_ineq3 . |
|
4838 |
|
4839 lemma bounded_variation_absolutely_integrable_interval: |
|
4840 fixes f::"real^'n \<Rightarrow> real^'m" assumes "f integrable_on {a..b}" |
|
4841 "\<forall>d. d division_of {a..b} \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B" |
|
4842 shows "f absolutely_integrable_on {a..b}" |
|
4843 proof- let ?S = "(\<lambda>d. setsum (\<lambda>k. norm(integral k f)) d) ` {d. d division_of {a..b} }" def i \<equiv> "Sup ?S" |
|
4844 have i:"isLub UNIV ?S i" unfolding i_def apply(rule Sup) |
|
4845 apply(rule elementary_interval) defer apply(rule_tac x=B in exI) |
|
4846 apply(rule setleI) using assms(2) by auto |
|
4847 show ?thesis apply(rule,rule assms) apply rule apply(subst has_integral[of _ i]) |
|
4848 proof safe case goal1 hence "i - e / 2 \<notin> Collect (isUb UNIV (setsum (\<lambda>k. norm (integral k f)) ` |
|
4849 {d. d division_of {a..b}}))" using isLub_ubs[OF i,rule_format] |
|
4850 unfolding setge_def ubs_def by auto |
|
4851 hence " \<exists>y. y division_of {a..b} \<and> i - e / 2 < (\<Sum>k\<in>y. norm (integral k f))" |
|
4852 unfolding mem_Collect_eq isUb_def setle_def by simp then guess d .. note d=conjunctD2[OF this] |
|
4853 note d' = division_ofD[OF this(1)] |
|
4854 |
|
4855 have "\<forall>x. \<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}" |
|
4856 proof case goal1 have "\<exists>da>0. \<forall>xa\<in>\<Union>{i \<in> d. x \<notin> i}. da \<le> dist x xa" |
|
4857 apply(rule separate_point_closed) apply(rule closed_Union) |
|
4858 apply(rule finite_subset[OF _ d'(1)]) apply safe apply(drule d'(4)) by auto |
|
4859 thus ?case apply safe apply(rule_tac x=da in exI,safe) |
|
4860 apply(erule_tac x=xa in ballE) by auto |
|
4861 qed from choice[OF this] guess k .. note k=conjunctD2[OF this[rule_format],rule_format] |
|
4862 |
|
4863 have "e/2 > 0" using goal1 by auto |
|
4864 from henstock_lemma[OF assms(1) this] guess g . note g=this[rule_format] |
|
4865 let ?g = "\<lambda>x. g x \<inter> ball x (k x)" |
|
4866 show ?case apply(rule_tac x="?g" in exI) apply safe |
|
4867 proof- show "gauge ?g" using g(1) unfolding gauge_def using k(1) by auto |
|
4868 fix p assume "p tagged_division_of {a..b}" "?g fine p" |
|
4869 note p = this(1) conjunctD2[OF this(2)[unfolded fine_inter]] |
|
4870 note p' = tagged_division_ofD[OF p(1)] |
|
4871 def p' \<equiv> "{(x,k) | x k. \<exists>i l. x \<in> i \<and> i \<in> d \<and> (x,l) \<in> p \<and> k = i \<inter> l}" |
|
4872 have gp':"g fine p'" using p(2) unfolding p'_def fine_def by auto |
|
4873 have p'':"p' tagged_division_of {a..b}" apply(rule tagged_division_ofI) |
|
4874 proof- show "finite p'" apply(rule finite_subset[of _ "(\<lambda>(k,(x,l)). (x,k \<inter> l)) |
|
4875 ` {(k,xl) | k xl. k \<in> d \<and> xl \<in> p}"]) unfolding p'_def |
|
4876 defer apply(rule finite_imageI,rule finite_product_dependent[OF d'(1) p'(1)]) |
|
4877 apply safe unfolding image_iff apply(rule_tac x="(i,x,l)" in bexI) by auto |
|
4878 fix x k assume "(x,k)\<in>p'" |
|
4879 hence "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l" unfolding p'_def by auto |
|
4880 then guess i l apply-by(erule exE)+ note il=conjunctD4[OF this] |
|
4881 show "x\<in>k" "k\<subseteq>{a..b}" using p'(2-3)[OF il(3)] il by auto |
|
4882 show "\<exists>a b. k = {a..b}" unfolding il using p'(4)[OF il(3)] d'(4)[OF il(2)] |
|
4883 apply safe unfolding inter_interval by auto |
|
4884 next fix x1 k1 assume "(x1,k1)\<in>p'" |
|
4885 hence "\<exists>i l. x1 \<in> i \<and> i \<in> d \<and> (x1, l) \<in> p \<and> k1 = i \<inter> l" unfolding p'_def by auto |
|
4886 then guess i1 l1 apply-by(erule exE)+ note il1=conjunctD4[OF this] |
|
4887 fix x2 k2 assume "(x2,k2)\<in>p'" |
|
4888 hence "\<exists>i l. x2 \<in> i \<and> i \<in> d \<and> (x2, l) \<in> p \<and> k2 = i \<inter> l" unfolding p'_def by auto |
|
4889 then guess i2 l2 apply-by(erule exE)+ note il2=conjunctD4[OF this] |
|
4890 assume "(x1, k1) \<noteq> (x2, k2)" |
|
4891 hence "interior(i1) \<inter> interior(i2) = {} \<or> interior(l1) \<inter> interior(l2) = {}" |
|
4892 using d'(5)[OF il1(2) il2(2)] p'(5)[OF il1(3) il2(3)] unfolding il1 il2 by auto |
|
4893 thus "interior k1 \<inter> interior k2 = {}" unfolding il1 il2 by auto |
|
4894 next have *:"\<forall>(x, X) \<in> p'. X \<subseteq> {a..b}" unfolding p'_def using d' by auto |
|
4895 show "\<Union>{k. \<exists>x. (x, k) \<in> p'} = {a..b}" apply rule apply(rule Union_least) |
|
4896 unfolding mem_Collect_eq apply(erule exE) apply(drule *[rule_format]) apply safe |
|
4897 proof- fix y assume y:"y\<in>{a..b}" |
|
4898 hence "\<exists>x l. (x, l) \<in> p \<and> y\<in>l" unfolding p'(6)[THEN sym] by auto |
|
4899 then guess x l apply-by(erule exE)+ note xl=conjunctD2[OF this] |
|
4900 hence "\<exists>k. k\<in>d \<and> y\<in>k" using y unfolding d'(6)[THEN sym] by auto |
|
4901 then guess i .. note i = conjunctD2[OF this] |
|
4902 have "x\<in>i" using fineD[OF p(3) xl(1)] using k(2)[OF i(1), of x] using i(2) xl(2) by auto |
|
4903 thus "y\<in>\<Union>{k. \<exists>x. (x, k) \<in> p'}" unfolding p'_def Union_iff apply(rule_tac x="i \<inter> l" in bexI) |
|
4904 defer unfolding mem_Collect_eq apply(rule_tac x=x in exI)+ apply(rule_tac x="i\<inter>l" in exI) |
|
4905 apply safe apply(rule_tac x=i in exI) apply(rule_tac x=l in exI) using i xl by auto |
|
4906 qed qed |
|
4907 |
|
4908 hence "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x - integral k f)) < e / 2" |
|
4909 apply-apply(rule g(2)[rule_format]) unfolding tagged_division_of_def apply safe using gp' . |
|
4910 hence **:" \<bar>(\<Sum>(x,k)\<in>p'. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p'. norm (integral k f))\<bar> < e / 2" |
|
4911 unfolding split_def apply(rule helplemma) using p'' by auto |
|
4912 |
|
4913 have p'alt:"p' = {(x,(i \<inter> l)) | x i l. (x,l) \<in> p \<and> i \<in> d \<and> ~(i \<inter> l = {})}" |
|
4914 proof safe case goal2 |
|
4915 have "x\<in>i" using fineD[OF p(3) goal2(1)] k(2)[OF goal2(2), of x] goal2(4-) by auto |
|
4916 hence "(x, i \<inter> l) \<in> p'" unfolding p'_def apply safe |
|
4917 apply(rule_tac x=x in exI,rule_tac x="i\<inter>l" in exI) apply safe using goal2 by auto |
|
4918 thus ?case using goal2(3) by auto |
|
4919 next fix x k assume "(x,k)\<in>p'" |
|
4920 hence "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l" unfolding p'_def by auto |
|
4921 then guess i l apply-by(erule exE)+ note il=conjunctD4[OF this] |
|
4922 thus "\<exists>y i l. (x, k) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}" |
|
4923 apply(rule_tac x=x in exI,rule_tac x=i in exI,rule_tac x=l in exI) |
|
4924 using p'(2)[OF il(3)] by auto |
|
4925 qed |
|
4926 have sum_p':"(\<Sum>(x, k)\<in>p'. norm (integral k f)) = (\<Sum>k\<in>snd ` p'. norm (integral k f))" |
|
4927 apply(subst setsum_over_tagged_division_lemma[OF p'',of "\<lambda>k. norm (integral k f)"]) |
|
4928 unfolding norm_eq_zero apply(rule integral_null,assumption) .. |
|
4929 note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]] |
|
4930 |
|
4931 have *:"\<And>sni sni' sf sf'. abs(sf' - sni') < e / 2 \<longrightarrow> i - e / 2 < sni \<and> sni' \<le> i \<and> |
|
4932 sni \<le> sni' \<and> sf' = sf \<longrightarrow> abs(sf - i) < e" by arith |
|
4933 show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - i) < e" |
|
4934 unfolding real_norm_def apply(rule *[rule_format,OF **],safe) apply(rule d(2)) |
|
4935 proof- case goal1 show ?case unfolding sum_p' |
|
4936 apply(rule isLubD2[OF i]) using division_of_tagged_division[OF p''] by auto |
|
4937 next case goal2 have *:"{k \<inter> l | k l. k \<in> d \<and> l \<in> snd ` p} = |
|
4938 (\<lambda>(k,l). k \<inter> l) ` {(k,l)|k l. k \<in> d \<and> l \<in> snd ` p}" by auto |
|
4939 have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>i\<in>d. \<Sum>l\<in>snd ` p. norm (integral (i \<inter> l) f))" |
|
4940 proof(rule setsum_mono) case goal1 note k=this |
|
4941 from d'(4)[OF this] guess u v apply-by(erule exE)+ note uv=this |
|
4942 def d' \<equiv> "{{u..v} \<inter> l |l. l \<in> snd ` p \<and> ~({u..v} \<inter> l = {})}" note uvab = d'(2)[OF k[unfolded uv]] |
|
4943 have "d' division_of {u..v}" apply(subst d'_def) apply(rule division_inter_1) |
|
4944 apply(rule division_of_tagged_division[OF p(1)]) using uvab . |
|
4945 hence "norm (integral k f) \<le> setsum (\<lambda>k. norm (integral k f)) d'" |
|
4946 unfolding uv apply(subst integral_combine_division_topdown[of _ _ d']) |
|
4947 apply(rule integrable_on_subinterval[OF assms(1) uvab]) apply assumption |
|
4948 apply(rule setsum_norm_le) by auto |
|
4949 also have "... = (\<Sum>k\<in>{k \<inter> l |l. l \<in> snd ` p}. norm (integral k f))" |
|
4950 apply(rule setsum_mono_zero_left) apply(subst simple_image) |
|
4951 apply(rule finite_imageI)+ apply fact unfolding d'_def uv apply blast |
|
4952 proof case goal1 hence "i \<in> {{u..v} \<inter> l |l. l \<in> snd ` p}" by auto |
|
4953 from this[unfolded mem_Collect_eq] guess l .. note l=this |
|
4954 hence "{u..v} \<inter> l = {}" using goal1 by auto thus ?case using l by auto |
|
4955 qed also have "... = (\<Sum>l\<in>snd ` p. norm (integral (k \<inter> l) f))" unfolding simple_image |
|
4956 apply(rule setsum_reindex_nonzero[unfolded o_def])apply(rule finite_imageI,rule p') |
|
4957 proof- case goal1 have "interior (k \<inter> l) \<subseteq> interior (l \<inter> y)" apply(subst(2) interior_inter) |
|
4958 apply(rule Int_greatest) defer apply(subst goal1(4)) by auto |
|
4959 hence *:"interior (k \<inter> l) = {}" using snd_p(5)[OF goal1(1-3)] by auto |
|
4960 from d'(4)[OF k] snd_p(4)[OF goal1(1)] guess u1 v1 u2 v2 apply-by(erule exE)+ note uv=this |
|
4961 show ?case using * unfolding uv inter_interval content_eq_0_interior[THEN sym] by auto |
|
4962 qed finally show ?case . |
|
4963 qed also have "... = (\<Sum>(i,l)\<in>{(i, l) |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral (i\<inter>l) f))" |
|
4964 apply(subst sum_sum_product[THEN sym],fact) using p'(1) by auto |
|
4965 also have "... = (\<Sum>x\<in>{(i, l) |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral (split op \<inter> x) f))" |
|
4966 unfolding split_def .. |
|
4967 also have "... = (\<Sum>k\<in>{i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral k f))" |
|
4968 unfolding * apply(rule setsum_reindex_nonzero[THEN sym,unfolded o_def]) |
|
4969 apply(rule finite_product_dependent) apply(fact,rule finite_imageI,rule p') |
|
4970 unfolding split_paired_all mem_Collect_eq split_conv o_def |
|
4971 proof- note * = division_ofD(4,5)[OF division_of_tagged_division,OF p(1)] |
|
4972 fix l1 l2 k1 k2 assume as:"(l1, k1) \<noteq> (l2, k2)" "l1 \<inter> k1 = l2 \<inter> k2" |
|
4973 "\<exists>i l. (l1, k1) = (i, l) \<and> i \<in> d \<and> l \<in> snd ` p" |
|
4974 "\<exists>i l. (l2, k2) = (i, l) \<and> i \<in> d \<and> l \<in> snd ` p" |
|
4975 hence "l1 \<in> d" "k1 \<in> snd ` p" by auto from d'(4)[OF this(1)] *(1)[OF this(2)] |
|
4976 guess u1 v1 u2 v2 apply-by(erule exE)+ note uv=this |
|
4977 have "l1 \<noteq> l2 \<or> k1 \<noteq> k2" using as by auto |
|
4978 hence "(interior(k1) \<inter> interior(k2) = {} \<or> interior(l1) \<inter> interior(l2) = {})" apply- |
|
4979 apply(erule disjE) apply(rule disjI2) apply(rule d'(5)) prefer 4 apply(rule disjI1) |
|
4980 apply(rule *) using as by auto |
|
4981 moreover have "interior(l1 \<inter> k1) = interior(l2 \<inter> k2)" using as(2) by auto |
|
4982 ultimately have "interior(l1 \<inter> k1) = {}" by auto |
|
4983 thus "norm (integral (l1 \<inter> k1) f) = 0" unfolding uv inter_interval |
|
4984 unfolding content_eq_0_interior[THEN sym] by auto |
|
4985 qed also have "... = (\<Sum>(x, k)\<in>p'. norm (integral k f))" unfolding sum_p' |
|
4986 apply(rule setsum_mono_zero_right) apply(subst *) |
|
4987 apply(rule finite_imageI[OF finite_product_dependent]) apply fact |
|
4988 apply(rule finite_imageI[OF p'(1)]) apply safe |
|
4989 proof- case goal2 have "ia \<inter> b = {}" using goal2 unfolding p'alt image_iff Bex_def not_ex |
|
4990 apply(erule_tac x="(a,ia\<inter>b)" in allE) by auto thus ?case by auto |
|
4991 next case goal1 thus ?case unfolding p'_def apply safe |
|
4992 apply(rule_tac x=i in exI,rule_tac x=l in exI) unfolding snd_conv image_iff |
|
4993 apply safe apply(rule_tac x="(a,l)" in bexI) by auto |
|
4994 qed finally show ?case . |
|
4995 |
|
4996 next case goal3 |
|
4997 let ?S = "{(x, i \<inter> l) |x i l. (x, l) \<in> p \<and> i \<in> d}" |
|
4998 have Sigma_alt:"\<And>s t. s \<times> t = {(i, j) |i j. i \<in> s \<and> j \<in> t}" by auto |
|
4999 have *:"?S = (\<lambda>(xl,i). (fst xl, snd xl \<inter> i)) ` (p \<times> d)" (*{(xl,i)|xl i. xl\<in>p \<and> i\<in>d}"**) |
|
5000 apply safe unfolding image_iff apply(rule_tac x="((x,l),i)" in bexI) by auto |
|
5001 note pdfin = finite_cartesian_product[OF p'(1) d'(1)] |
|
5002 have "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x)) = (\<Sum>(x, k)\<in>?S. \<bar>content k\<bar> * norm (f x))" |
|
5003 unfolding norm_scaleR apply(rule setsum_mono_zero_left) |
|
5004 apply(subst *, rule finite_imageI) apply fact unfolding p'alt apply blast |
|
5005 apply safe apply(rule_tac x=x in exI,rule_tac x=i in exI,rule_tac x=l in exI) by auto |
|
5006 also have "... = (\<Sum>((x,l),i)\<in>p \<times> d. \<bar>content (l \<inter> i)\<bar> * norm (f x))" unfolding * |
|
5007 apply(subst setsum_reindex_nonzero,fact) unfolding split_paired_all |
|
5008 unfolding o_def split_def snd_conv fst_conv mem_Sigma_iff Pair_eq apply(erule_tac conjE)+ |
|
5009 proof- fix x1 l1 k1 x2 l2 k2 assume as:"(x1,l1)\<in>p" "(x2,l2)\<in>p" "k1\<in>d" "k2\<in>d" |
|
5010 "x1 = x2" "l1 \<inter> k1 = l2 \<inter> k2" "\<not> ((x1 = x2 \<and> l1 = l2) \<and> k1 = k2)" |
|
5011 from d'(4)[OF as(3)] p'(4)[OF as(1)] guess u1 v1 u2 v2 apply-by(erule exE)+ note uv=this |
|
5012 from as have "l1 \<noteq> l2 \<or> k1 \<noteq> k2" by auto |
|
5013 hence "(interior(k1) \<inter> interior(k2) = {} \<or> interior(l1) \<inter> interior(l2) = {})" |
|
5014 apply-apply(erule disjE) apply(rule disjI2) defer apply(rule disjI1) |
|
5015 apply(rule d'(5)[OF as(3-4)],assumption) apply(rule p'(5)[OF as(1-2)]) by auto |
|
5016 moreover have "interior(l1 \<inter> k1) = interior(l2 \<inter> k2)" unfolding as .. |
|
5017 ultimately have "interior (l1 \<inter> k1) = {}" by auto |
|
5018 thus "\<bar>content (l1 \<inter> k1)\<bar> * norm (f x1) = 0" unfolding uv inter_interval |
|
5019 unfolding content_eq_0_interior[THEN sym] by auto |
|
5020 qed safe also have "... = (\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x))" unfolding Sigma_alt |
|
5021 apply(subst sum_sum_product[THEN sym]) apply(rule p', rule,rule d') |
|
5022 apply(rule setsum_cong2) unfolding split_paired_all split_conv |
|
5023 proof- fix x l assume as:"(x,l)\<in>p" |
|
5024 note xl = p'(2-4)[OF this] from this(3) guess u v apply-by(erule exE)+ note uv=this |
|
5025 have "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar>) = (\<Sum>k\<in>d. content (k \<inter> {u..v}))" |
|
5026 apply(rule setsum_cong2) apply(drule d'(4),safe) apply(subst Int_commute) |
|
5027 unfolding inter_interval uv apply(subst abs_of_nonneg) by auto |
|
5028 also have "... = setsum content {k\<inter>{u..v}| k. k\<in>d}" unfolding simple_image |
|
5029 apply(rule setsum_reindex_nonzero[unfolded o_def,THEN sym]) apply(rule d') |
|
5030 proof- case goal1 from d'(4)[OF this(1)] d'(4)[OF this(2)] |
|
5031 guess u1 v1 u2 v2 apply- by(erule exE)+ note uv=this |
|
5032 have "{} = interior ((k \<inter> y) \<inter> {u..v})" apply(subst interior_inter) |
|
5033 using d'(5)[OF goal1(1-3)] by auto |
|
5034 also have "... = interior (y \<inter> (k \<inter> {u..v}))" by auto |
|
5035 also have "... = interior (k \<inter> {u..v})" unfolding goal1(4) by auto |
|
5036 finally show ?case unfolding uv inter_interval content_eq_0_interior .. |
|
5037 qed also have "... = setsum content {{u..v} \<inter> k |k. k \<in> d \<and> ~({u..v} \<inter> k = {})}" |
|
5038 apply(rule setsum_mono_zero_right) unfolding simple_image |
|
5039 apply(rule finite_imageI,rule d') apply blast apply safe |
|
5040 apply(rule_tac x=k in exI) |
|
5041 proof- case goal1 from d'(4)[OF this(1)] guess a b apply-by(erule exE)+ note ab=this |
|
5042 have "interior (k \<inter> {u..v}) \<noteq> {}" using goal1(2) |
|
5043 unfolding ab inter_interval content_eq_0_interior by auto |
|
5044 thus ?case using goal1(1) using interior_subset[of "k \<inter> {u..v}"] by auto |
|
5045 qed finally show "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar> * norm (f x)) = content l *\<^sub>R norm (f x)" |
|
5046 unfolding setsum_left_distrib[THEN sym] real_scaleR_def apply - |
|
5047 apply(subst(asm) additive_content_division[OF division_inter_1[OF d(1)]]) |
|
5048 using xl(2)[unfolded uv] unfolding uv by auto |
|
5049 qed finally show ?case . |
|
5050 qed qed qed qed |
|
5051 |
|
5052 lemma bounded_variation_absolutely_integrable: fixes f::"real^'n \<Rightarrow> real^'m" |
|
5053 assumes "f integrable_on UNIV" "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B" |
|
5054 shows "f absolutely_integrable_on UNIV" |
|
5055 proof(rule absolutely_integrable_onI,fact,rule) |
|
5056 let ?S = "(\<lambda>d. setsum (\<lambda>k. norm(integral k f)) d) ` {d. d division_of (\<Union>d)}" def i \<equiv> "Sup ?S" |
|
5057 have i:"isLub UNIV ?S i" unfolding i_def apply(rule Sup) |
|
5058 apply(rule elementary_interval) defer apply(rule_tac x=B in exI) |
|
5059 apply(rule setleI) using assms(2) by auto |
|
5060 have f_int:"\<And>a b. f absolutely_integrable_on {a..b}" |
|
5061 apply(rule bounded_variation_absolutely_integrable_interval[where B=B]) |
|
5062 apply(rule integrable_on_subinterval[OF assms(1)]) defer apply safe |
|
5063 apply(rule assms(2)[rule_format]) by auto |
|
5064 show "((\<lambda>x. norm (f x)) has_integral i) UNIV" apply(subst has_integral_alt',safe) |
|
5065 proof- case goal1 show ?case using f_int[of a b] by auto |
|
5066 next case goal2 have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> i - e" |
|
5067 proof(rule ccontr) case goal1 hence "i \<le> i - e" apply- |
|
5068 apply(rule isLub_le_isUb[OF i]) apply(rule isUbI) unfolding setle_def by auto |
|
5069 thus False using goal2 by auto |
|
5070 qed then guess K .. note * = this[unfolded image_iff not_le] |
|
5071 from this(1) guess d .. note this[unfolded mem_Collect_eq] |
|
5072 note d = this(1) *(2)[unfolded this(2)] note d'=division_ofD[OF this(1)] |
|
5073 have "bounded (\<Union>d)" by(rule elementary_bounded,fact) |
|
5074 from this[unfolded bounded_pos] guess K .. note K=conjunctD2[OF this] |
|
5075 show ?case apply(rule_tac x="K + 1" in exI,safe) |
|
5076 proof- fix a b assume ab:"ball 0 (K + 1) \<subseteq> {a..b::real^'n}" |
|
5077 have *:"\<forall>s s1. i - e < s1 \<and> s1 \<le> s \<and> s < i + e \<longrightarrow> abs(s - i) < (e::real)" by arith |
|
5078 show "norm (integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - i) < e" |
|
5079 unfolding real_norm_def apply(rule *[rule_format],safe) apply(rule d(2)) |
|
5080 proof- case goal1 have "(\<Sum>k\<in>d. norm (integral k f)) \<le> setsum (\<lambda>k. integral k (\<lambda>x. norm (f x))) d" |
|
5081 apply(rule setsum_mono) apply(rule absolutely_integrable_le) |
|
5082 apply(drule d'(4),safe) by(rule f_int) |
|
5083 also have "... = integral (\<Union>d) (\<lambda>x. norm(f x))" |
|
5084 apply(rule integral_combine_division_bottomup[THEN sym]) |
|
5085 apply(rule d) unfolding forall_in_division[OF d(1)] using f_int by auto |
|
5086 also have "... \<le> integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0)" |
|
5087 proof- case goal1 have "\<Union>d \<subseteq> {a..b}" apply rule apply(drule K(2)[rule_format]) |
|
5088 apply(rule ab[unfolded subset_eq,rule_format]) by(auto simp add:dist_norm) |
|
5089 thus ?case apply- apply(subst if_P,rule) apply(rule integral_subset_le) defer |
|
5090 apply(rule integrable_on_subdivision[of _ _ _ "{a..b}"]) |
|
5091 apply(rule d) using f_int[of a b] by auto |
|
5092 qed finally show ?case . |
|
5093 |
|
5094 next note f = absolutely_integrable_onD[OF f_int[of a b]] |
|
5095 note * = this(2)[unfolded has_integral_integral has_integral[of "\<lambda>x. norm (f x)"],rule_format] |
|
5096 have "e/2>0" using `e>0` by auto from *[OF this] guess d1 .. note d1=conjunctD2[OF this] |
|
5097 from henstock_lemma[OF f(1) `e/2>0`] guess d2 . note d2=this |
|
5098 from fine_division_exists[OF gauge_inter[OF d1(1) d2(1)], of a b] guess p . |
|
5099 note p=this(1) conjunctD2[OF this(2)[unfolded fine_inter]] |
|
5100 have *:"\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> i \<longrightarrow> abs(sf - si) < e / 2 |
|
5101 \<longrightarrow> abs(sf' - di) < e / 2 \<longrightarrow> di < i + e" by arith |
|
5102 show "integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < i + e" apply(subst if_P,rule) |
|
5103 proof(rule *[rule_format]) |
|
5104 show "\<bar>(\<Sum>(x,k)\<in>p. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p. norm (integral k f))\<bar> < e / 2" |
|
5105 unfolding split_def apply(rule helplemma) using d2(2)[rule_format,of p] |
|
5106 using p(1,3) unfolding tagged_division_of_def split_def by auto |
|
5107 show "abs ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - integral {a..b} (\<lambda>x. norm(f x))) < e / 2" |
|
5108 using d1(2)[rule_format,OF conjI[OF p(1,2)]] unfolding real_norm_def . |
|
5109 show "(\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) = (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x))" |
|
5110 apply(rule setsum_cong2) unfolding split_paired_all split_conv |
|
5111 apply(drule tagged_division_ofD(4)[OF p(1)]) unfolding norm_scaleR |
|
5112 apply(subst abs_of_nonneg) by auto |
|
5113 show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> i" |
|
5114 apply(subst setsum_over_tagged_division_lemma[OF p(1)]) defer apply(rule isLubD2[OF i]) |
|
5115 unfolding image_iff apply(rule_tac x="snd ` p" in bexI) unfolding mem_Collect_eq defer |
|
5116 apply(rule partial_division_of_tagged_division[of _ "{a..b}"]) |
|
5117 using p(1) unfolding tagged_division_of_def by auto |
|
5118 qed qed qed(insert K,auto) qed qed |
|
5119 |
|
5120 lemma absolutely_integrable_restrict_univ: |
|
5121 "(\<lambda>x. if x \<in> s then f x else (0::'a::banach)) absolutely_integrable_on UNIV \<longleftrightarrow> f absolutely_integrable_on s" |
|
5122 unfolding absolutely_integrable_on_def if_distrib norm_zero integrable_restrict_univ .. |
|
5123 |
|
5124 lemma absolutely_integrable_add[intro]: fixes f g::"real^'n \<Rightarrow> real^'m" |
|
5125 assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s" |
|
5126 shows "(\<lambda>x. f(x) + g(x)) absolutely_integrable_on s" |
|
5127 proof- let ?P = "\<And>f g::real^'n \<Rightarrow> real^'m. f absolutely_integrable_on UNIV \<Longrightarrow> |
|
5128 g absolutely_integrable_on UNIV \<Longrightarrow> (\<lambda>x. f(x) + g(x)) absolutely_integrable_on UNIV" |
|
5129 { presume as:"PROP ?P" note a = absolutely_integrable_restrict_univ[THEN sym] |
|
5130 have *:"\<And>x. (if x \<in> s then f x else 0) + (if x \<in> s then g x else 0) |
|
5131 = (if x \<in> s then f x + g x else 0)" by auto |
|
5132 show ?thesis apply(subst a) using as[OF assms[unfolded a[of f] a[of g]]] unfolding * . } |
|
5133 fix f g::"real^'n \<Rightarrow> real^'m" assume assms:"f absolutely_integrable_on UNIV" |
|
5134 "g absolutely_integrable_on UNIV" |
|
5135 note absolutely_integrable_bounded_variation |
|
5136 from this[OF assms(1)] this[OF assms(2)] guess B1 B2 . note B=this[rule_format] |
|
5137 show "(\<lambda>x. f(x) + g(x)) absolutely_integrable_on UNIV" |
|
5138 apply(rule bounded_variation_absolutely_integrable[of _ "B1+B2"]) |
|
5139 apply(rule integrable_add) prefer 3 |
|
5140 proof safe case goal1 have "\<And>k. k \<in> d \<Longrightarrow> f integrable_on k \<and> g integrable_on k" |
|
5141 apply(drule division_ofD(4)[OF goal1]) apply safe |
|
5142 apply(rule_tac[!] integrable_on_subinterval[of _ UNIV]) using assms by auto |
|
5143 hence "(\<Sum>k\<in>d. norm (integral k (\<lambda>x. f x + g x))) \<le> |
|
5144 (\<Sum>k\<in>d. norm (integral k f)) + (\<Sum>k\<in>d. norm (integral k g))" apply- |
|
5145 unfolding setsum_addf[THEN sym] apply(rule setsum_mono) |
|
5146 apply(subst integral_add) prefer 3 apply(rule norm_triangle_ineq) by auto |
|
5147 also have "... \<le> B1 + B2" using B(1)[OF goal1] B(2)[OF goal1] by auto |
|
5148 finally show ?case . |
|
5149 qed(insert assms,auto) qed |
|
5150 |
|
5151 lemma absolutely_integrable_sub[intro]: fixes f g::"real^'n \<Rightarrow> real^'m" |
|
5152 assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s" |
|
5153 shows "(\<lambda>x. f(x) - g(x)) absolutely_integrable_on s" |
|
5154 using absolutely_integrable_add[OF assms(1) absolutely_integrable_neg[OF assms(2)]] |
|
5155 unfolding group_simps . |
|
5156 |
|
5157 lemma absolutely_integrable_linear: fixes f::"real^'m \<Rightarrow> real^'n" and h::"real^'n \<Rightarrow> real^'p" |
|
5158 assumes "f absolutely_integrable_on s" "bounded_linear h" |
|
5159 shows "(h o f) absolutely_integrable_on s" |
|
5160 proof- { presume as:"\<And>f::real^'m \<Rightarrow> real^'n. \<And>h::real^'n \<Rightarrow> real^'p. |
|
5161 f absolutely_integrable_on UNIV \<Longrightarrow> bounded_linear h \<Longrightarrow> |
|
5162 (h o f) absolutely_integrable_on UNIV" note a = absolutely_integrable_restrict_univ[THEN sym] |
|
5163 show ?thesis apply(subst a) using as[OF assms[unfolded a[of f] a[of g]]] |
|
5164 unfolding o_def if_distrib linear_simps[OF assms(2)] . } |
|
5165 fix f::"real^'m \<Rightarrow> real^'n" and h::"real^'n \<Rightarrow> real^'p" |
|
5166 assume assms:"f absolutely_integrable_on UNIV" "bounded_linear h" |
|
5167 from absolutely_integrable_bounded_variation[OF assms(1)] guess B . note B=this |
|
5168 from bounded_linear.pos_bounded[OF assms(2)] guess b .. note b=conjunctD2[OF this] |
|
5169 show "(h o f) absolutely_integrable_on UNIV" |
|
5170 apply(rule bounded_variation_absolutely_integrable[of _ "B * b"]) |
|
5171 apply(rule integrable_linear[OF _ assms(2)]) |
|
5172 proof safe case goal2 |
|
5173 have "(\<Sum>k\<in>d. norm (integral k (h \<circ> f))) \<le> setsum (\<lambda>k. norm(integral k f)) d * b" |
|
5174 unfolding setsum_left_distrib apply(rule setsum_mono) |
|
5175 proof- case goal1 from division_ofD(4)[OF goal2 this] |
|
5176 guess u v apply-by(erule exE)+ note uv=this |
|
5177 have *:"f integrable_on k" unfolding uv apply(rule integrable_on_subinterval[of _ UNIV]) |
|
5178 using assms by auto note this[unfolded has_integral_integral] |
|
5179 note has_integral_linear[OF this assms(2)] integrable_linear[OF * assms(2)] |
|
5180 note * = has_integral_unique[OF this(2)[unfolded has_integral_integral] this(1)] |
|
5181 show ?case unfolding * using b by auto |
|
5182 qed also have "... \<le> B * b" apply(rule mult_right_mono) using B goal2 b by auto |
|
5183 finally show ?case . |
|
5184 qed(insert assms,auto) qed |
|
5185 |
|
5186 lemma absolutely_integrable_setsum: fixes f::"'a \<Rightarrow> real^'n \<Rightarrow> real^'m" |
|
5187 assumes "finite t" "\<And>a. a \<in> t \<Longrightarrow> (f a) absolutely_integrable_on s" |
|
5188 shows "(\<lambda>x. setsum (\<lambda>a. f a x) t) absolutely_integrable_on s" |
|
5189 using assms(1,2) apply induct defer apply(subst setsum.insert) apply assumption+ by(rule,auto) |
|
5190 |
|
5191 lemma absolutely_integrable_vector_abs: |
|
5192 assumes "f absolutely_integrable_on s" |
|
5193 shows "(\<lambda>x. (\<chi> i. abs(f x$i))::real^'n) absolutely_integrable_on s" |
|
5194 proof- have *:"\<And>x. ((\<chi> i. abs(f x$i))::real^'n) = (setsum (\<lambda>i. |
|
5195 (((\<lambda>y. (\<chi> j. if j = i then y$1 else 0)) o |
|
5196 (vec1 o ((\<lambda>x. (norm((\<chi> j. if j = i then x$i else 0)::real^'n))) o f))) x)) UNIV)" |
|
5197 unfolding Cart_eq setsum_component Cart_lambda_beta |
|
5198 proof case goal1 have *:"\<And>i xa. ((if i = xa then f x $ xa else 0) \<bullet> (if i = xa then f x $ xa else 0)) = |
|
5199 (if i = xa then (f x $ xa) * (f x $ xa) else 0)" by auto |
|
5200 have "\<bar>f x $ i\<bar> = (setsum (\<lambda>k. if k = i then abs ((f x)$i) else 0) UNIV)" |
|
5201 unfolding setsum_delta[OF finite_UNIV] by auto |
|
5202 also have "... = (\<Sum>xa\<in>UNIV. ((\<lambda>y. \<chi> j. if j = xa then dest_vec1 y else 0) \<circ> |
|
5203 (\<lambda>x. vec1 (norm (\<chi> j. if j = xa then x $ xa else 0))) \<circ> f) x $ i)" |
|
5204 unfolding norm_eq_sqrt_inner inner_vector_def Cart_lambda_beta o_def * |
|
5205 apply(rule setsum_cong2) unfolding setsum_delta[OF finite_UNIV] by auto |
|
5206 finally show ?case unfolding o_def . qed |
|
5207 show ?thesis unfolding * apply(rule absolutely_integrable_setsum) apply(rule finite_UNIV) |
|
5208 apply(rule absolutely_integrable_linear) |
|
5209 unfolding absolutely_integrable_on_trans unfolding o_def apply(rule absolutely_integrable_norm) |
|
5210 apply(rule absolutely_integrable_linear[OF assms,unfolded o_def]) unfolding linear_linear |
|
5211 apply(rule_tac[!] linearI) unfolding Cart_eq by auto |
|
5212 qed |
|
5213 |
|
5214 lemma absolutely_integrable_max: fixes f::"real^'m \<Rightarrow> real^'n" |
|
5215 assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s" |
|
5216 shows "(\<lambda>x. (\<chi> i. max (f(x)$i) (g(x)$i))::real^'n) absolutely_integrable_on s" |
|
5217 proof- have *:"\<And>x. (1 / 2) *\<^sub>R ((\<chi> i. \<bar>(f x - g x) $ i\<bar>) + (f x + g x)) = (\<chi> i. max (f(x)$i) (g(x)$i))" |
|
5218 unfolding Cart_eq by auto |
|
5219 note absolutely_integrable_sub[OF assms] absolutely_integrable_add[OF assms] |
|
5220 note absolutely_integrable_vector_abs[OF this(1)] this(2) |
|
5221 note absolutely_integrable_add[OF this] note absolutely_integrable_cmul[OF this,of "1/2"] |
|
5222 thus ?thesis unfolding * . qed |
|
5223 |
|
5224 lemma absolutely_integrable_max_real: fixes f::"real^'m \<Rightarrow> real" |
|
5225 assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s" |
|
5226 shows "(\<lambda>x. max (f x) (g x)) absolutely_integrable_on s" |
|
5227 proof- have *:"(\<lambda>x. \<chi> i. max ((vec1 \<circ> f) x $ i) ((vec1 \<circ> g) x $ i)) = vec1 o (\<lambda>x. max (f x) (g x))" |
|
5228 apply rule unfolding Cart_eq by auto note absolutely_integrable_max[of "vec1 o f" s "vec1 o g"] |
|
5229 note this[unfolded absolutely_integrable_on_trans,OF assms] |
|
5230 thus ?thesis unfolding * by auto qed |
|
5231 |
|
5232 lemma absolutely_integrable_min: fixes f::"real^'m \<Rightarrow> real^'n" |
|
5233 assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s" |
|
5234 shows "(\<lambda>x. (\<chi> i. min (f(x)$i) (g(x)$i))::real^'n) absolutely_integrable_on s" |
|
5235 proof- have *:"\<And>x. (1 / 2) *\<^sub>R ((f x + g x) - (\<chi> i. \<bar>(f x - g x) $ i\<bar>)) = (\<chi> i. min (f(x)$i) (g(x)$i))" |
|
5236 unfolding Cart_eq by auto |
|
5237 note absolutely_integrable_add[OF assms] absolutely_integrable_sub[OF assms] |
|
5238 note this(1) absolutely_integrable_vector_abs[OF this(2)] |
|
5239 note absolutely_integrable_sub[OF this] note absolutely_integrable_cmul[OF this,of "1/2"] |
|
5240 thus ?thesis unfolding * . qed |
|
5241 |
|
5242 lemma absolutely_integrable_min_real: fixes f::"real^'m \<Rightarrow> real" |
|
5243 assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s" |
|
5244 shows "(\<lambda>x. min (f x) (g x)) absolutely_integrable_on s" |
|
5245 proof- have *:"(\<lambda>x. \<chi> i. min ((vec1 \<circ> f) x $ i) ((vec1 \<circ> g) x $ i)) = vec1 o (\<lambda>x. min (f x) (g x))" |
|
5246 apply rule unfolding Cart_eq by auto note absolutely_integrable_min[of "vec1 o f" s "vec1 o g"] |
|
5247 note this[unfolded absolutely_integrable_on_trans,OF assms] |
|
5248 thus ?thesis unfolding * by auto qed |
|
5249 |
|
5250 lemma absolutely_integrable_abs_eq: fixes f::"real^'n \<Rightarrow> real^'m" |
|
5251 shows "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s \<and> |
|
5252 (\<lambda>x. (\<chi> i. abs(f x$i))::real^'m) integrable_on s" (is "?l = ?r") |
|
5253 proof assume ?l thus ?r apply-apply rule defer |
|
5254 apply(drule absolutely_integrable_vector_abs) by auto |
|
5255 next assume ?r { presume lem:"\<And>f::real^'n \<Rightarrow> real^'m. f integrable_on UNIV \<Longrightarrow> |
|
5256 (\<lambda>x. (\<chi> i. abs(f(x)$i))::real^'m) integrable_on UNIV \<Longrightarrow> f absolutely_integrable_on UNIV" |
|
5257 have *:"\<And>x. (\<chi> i. \<bar>(if x \<in> s then f x else 0) $ i\<bar>) = (if x\<in>s then (\<chi> i. \<bar>f x $ i\<bar>) else 0)" |
|
5258 unfolding Cart_eq by auto |
|
5259 show ?l apply(subst absolutely_integrable_restrict_univ[THEN sym]) apply(rule lem) |
|
5260 unfolding integrable_restrict_univ * using `?r` by auto } |
|
5261 fix f::"real^'n \<Rightarrow> real^'m" assume assms:"f integrable_on UNIV" |
|
5262 "(\<lambda>x. (\<chi> i. abs(f(x)$i))::real^'m) integrable_on UNIV" |
|
5263 let ?B = "setsum (\<lambda>i. integral UNIV (\<lambda>x. (\<chi> j. abs(f x$j)) ::real^'m) $ i) UNIV" |
|
5264 show "f absolutely_integrable_on UNIV" |
|
5265 apply(rule bounded_variation_absolutely_integrable[OF assms(1), where B="?B"],safe) |
|
5266 proof- case goal1 note d=this and d'=division_ofD[OF this] |
|
5267 have "(\<Sum>k\<in>d. norm (integral k f)) \<le> |
|
5268 (\<Sum>k\<in>d. setsum (op $ (integral k (\<lambda>x. \<chi> j. \<bar>f x $ j\<bar>))) UNIV)" apply(rule setsum_mono) |
|
5269 apply(rule order_trans[OF norm_le_l1],rule setsum_mono) |
|
5270 proof- fix k and i::'m assume "k\<in>d" |
|
5271 from d'(4)[OF this] guess a b apply-by(erule exE)+ note ab=this |
|
5272 show "\<bar>integral k f $ i\<bar> \<le> integral k (\<lambda>x. \<chi> j. \<bar>f x $ j\<bar>) $ i" apply(rule abs_leI) |
|
5273 unfolding vector_uminus_component[THEN sym] defer apply(subst integral_neg[THEN sym]) |
|
5274 defer apply(rule_tac[1-2] integral_component_le) apply(rule integrable_neg) |
|
5275 using integrable_on_subinterval[OF assms(1),of a b] |
|
5276 integrable_on_subinterval[OF assms(2),of a b] unfolding ab by auto |
|
5277 qed also have "... \<le> setsum (op $ (integral UNIV (\<lambda>x. \<chi> j. \<bar>f x $ j\<bar>))) UNIV" |
|
5278 apply(subst setsum_commute,rule setsum_mono) |
|
5279 proof- case goal1 have *:"(\<lambda>x. \<chi> j. \<bar>f x $ j\<bar>) integrable_on \<Union>d" |
|
5280 using integrable_on_subdivision[OF d assms(2)] by auto |
|
5281 have "(\<Sum>i\<in>d. integral i (\<lambda>x. \<chi> j. \<bar>f x $ j\<bar>) $ j) |
|
5282 = integral (\<Union>d) (\<lambda>x. (\<chi> j. abs(f x$j)) ::real^'m) $ j" |
|
5283 unfolding setsum_component[THEN sym] |
|
5284 apply(subst integral_combine_division_topdown[THEN sym,OF * d]) by auto |
|
5285 also have "... \<le> integral UNIV (\<lambda>x. \<chi> j. \<bar>f x $ j\<bar>) $ j" |
|
5286 apply(rule integral_subset_component_le) using assms * by auto |
|
5287 finally show ?case . |
|
5288 qed finally show ?case . qed qed |
|
5289 |
|
5290 lemma nonnegative_absolutely_integrable: fixes f::"real^'n \<Rightarrow> real^'m" |
|
5291 assumes "\<forall>x\<in>s. \<forall>i. 0 \<le> f(x)$i" "f integrable_on s" |
|
5292 shows "f absolutely_integrable_on s" |
|
5293 unfolding absolutely_integrable_abs_eq apply rule defer |
|
5294 apply(rule integrable_eq[of _ f]) unfolding Cart_eq using assms by auto |
|
5295 |
|
5296 lemma absolutely_integrable_integrable_bound: fixes f::"real^'n \<Rightarrow> real^'m" |
|
5297 assumes "\<forall>x\<in>s. norm(f x) \<le> g x" "f integrable_on s" "g integrable_on s" |
|
5298 shows "f absolutely_integrable_on s" |
|
5299 proof- { presume *:"\<And>f::real^'n \<Rightarrow> real^'m. \<And> g. \<forall>x. norm(f x) \<le> g x \<Longrightarrow> f integrable_on UNIV |
|
5300 \<Longrightarrow> g integrable_on UNIV \<Longrightarrow> f absolutely_integrable_on UNIV" |
|
5301 show ?thesis apply(subst absolutely_integrable_restrict_univ[THEN sym]) |
|
5302 apply(rule *[of _ "\<lambda>x. if x\<in>s then g x else 0"]) |
|
5303 using assms unfolding integrable_restrict_univ by auto } |
|
5304 fix g and f :: "real^'n \<Rightarrow> real^'m" |
|
5305 assume assms:"\<forall>x. norm(f x) \<le> g x" "f integrable_on UNIV" "g integrable_on UNIV" |
|
5306 show "f absolutely_integrable_on UNIV" |
|
5307 apply(rule bounded_variation_absolutely_integrable[OF assms(2),where B="integral UNIV g"]) |
|
5308 proof safe case goal1 note d=this and d'=division_ofD[OF this] |
|
5309 have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>k\<in>d. integral k g)" |
|
5310 apply(rule setsum_mono) apply(rule integral_norm_bound_integral) apply(drule_tac[!] d'(4),safe) |
|
5311 apply(rule_tac[1-2] integrable_on_subinterval) using assms by auto |
|
5312 also have "... = integral (\<Union>d) g" apply(rule integral_combine_division_bottomup[THEN sym]) |
|
5313 apply(rule d,safe) apply(drule d'(4),safe) |
|
5314 apply(rule integrable_on_subinterval[OF assms(3)]) by auto |
|
5315 also have "... \<le> integral UNIV g" apply(rule integral_subset_le) defer |
|
5316 apply(rule integrable_on_subdivision[OF d,of _ UNIV]) prefer 4 |
|
5317 apply(rule,rule_tac y="norm (f x)" in order_trans) using assms by auto |
|
5318 finally show ?case . qed qed |
|
5319 |
|
5320 lemma absolutely_integrable_integrable_bound_real: fixes f::"real^'n \<Rightarrow> real" |
|
5321 assumes "\<forall>x\<in>s. norm(f x) \<le> g x" "f integrable_on s" "g integrable_on s" |
|
5322 shows "f absolutely_integrable_on s" |
|
5323 apply(subst absolutely_integrable_on_trans[THEN sym]) |
|
5324 apply(rule absolutely_integrable_integrable_bound[where g=g]) |
|
5325 using assms unfolding o_def by auto |
|
5326 |
|
5327 lemma absolutely_integrable_absolutely_integrable_bound: |
|
5328 fixes f::"real^'n \<Rightarrow> real^'m" and g::"real^'n \<Rightarrow> real^'p" |
|
5329 assumes "\<forall>x\<in>s. norm(f x) \<le> norm(g x)" "f integrable_on s" "g absolutely_integrable_on s" |
|
5330 shows "f absolutely_integrable_on s" |
|
5331 apply(rule absolutely_integrable_integrable_bound[of s f "\<lambda>x. norm (g x)"]) |
|
5332 using assms by auto |
|
5333 |
|
5334 lemma absolutely_integrable_inf_real: |
|
5335 assumes "finite k" "k \<noteq> {}" |
|
5336 "\<forall>i\<in>k. (\<lambda>x. (fs x i)::real) absolutely_integrable_on s" |
|
5337 shows "(\<lambda>x. (Inf ((fs x) ` k))) absolutely_integrable_on s" using assms |
|
5338 proof induct case (insert a k) let ?P = " (\<lambda>x. if fs x ` k = {} then fs x a |
|
5339 else min (fs x a) (Inf (fs x ` k))) absolutely_integrable_on s" |
|
5340 show ?case unfolding image_insert |
|
5341 apply(subst Inf_insert_finite) apply(rule finite_imageI[OF insert(1)]) |
|
5342 proof(cases "k={}") case True |
|
5343 thus ?P apply(subst if_P) defer apply(rule insert(5)[rule_format]) by auto |
|
5344 next case False thus ?P apply(subst if_not_P) defer |
|
5345 apply(rule absolutely_integrable_min_real) |
|
5346 defer apply(rule insert(3)[OF False]) using insert(5) by auto |
|
5347 qed qed auto |
|
5348 |
|
5349 lemma absolutely_integrable_sup_real: |
|
5350 assumes "finite k" "k \<noteq> {}" |
|
5351 "\<forall>i\<in>k. (\<lambda>x. (fs x i)::real) absolutely_integrable_on s" |
|
5352 shows "(\<lambda>x. (Sup ((fs x) ` k))) absolutely_integrable_on s" using assms |
|
5353 proof induct case (insert a k) let ?P = " (\<lambda>x. if fs x ` k = {} then fs x a |
|
5354 else max (fs x a) (Sup (fs x ` k))) absolutely_integrable_on s" |
|
5355 show ?case unfolding image_insert |
|
5356 apply(subst Sup_insert_finite) apply(rule finite_imageI[OF insert(1)]) |
|
5357 proof(cases "k={}") case True |
|
5358 thus ?P apply(subst if_P) defer apply(rule insert(5)[rule_format]) by auto |
|
5359 next case False thus ?P apply(subst if_not_P) defer |
|
5360 apply(rule absolutely_integrable_max_real) |
|
5361 defer apply(rule insert(3)[OF False]) using insert(5) by auto |
|
5362 qed qed auto |
|
5363 |
|
5364 subsection {* Dominated convergence. *} |
|
5365 |
|
5366 lemma dominated_convergence: fixes f::"nat \<Rightarrow> real^'n \<Rightarrow> real" |
|
5367 assumes "\<And>k. (f k) integrable_on s" "h integrable_on s" |
|
5368 "\<And>k. \<forall>x \<in> s. norm(f k x) \<le> (h x)" |
|
5369 "\<forall>x \<in> s. ((\<lambda>k. f k x) ---> g x) sequentially" |
|
5370 shows "g integrable_on s" "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially" |
|
5371 proof- have "\<And>m. (\<lambda>x. Inf {f j x |j. m \<le> j}) integrable_on s \<and> |
|
5372 ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) ---> |
|
5373 integral s (\<lambda>x. Inf {f j x |j. m \<le> j}))sequentially" |
|
5374 proof(rule monotone_convergence_decreasing_real,safe) fix m::nat |
|
5375 show "bounded {integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) |k. True}" |
|
5376 unfolding bounded_iff apply(rule_tac x="integral s h" in exI) |
|
5377 proof safe fix k::nat |
|
5378 show "norm (integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) \<le> integral s h" |
|
5379 apply(rule integral_norm_bound_integral) unfolding simple_image |
|
5380 apply(rule absolutely_integrable_onD) apply(rule absolutely_integrable_inf_real) |
|
5381 prefer 5 unfolding real_norm_def apply(rule) apply(rule Inf_abs_ge) |
|
5382 prefer 5 apply rule apply(rule_tac g=h in absolutely_integrable_integrable_bound_real) |
|
5383 using assms unfolding real_norm_def by auto |
|
5384 qed fix k::nat show "(\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) integrable_on s" |
|
5385 unfolding simple_image apply(rule absolutely_integrable_onD) |
|
5386 apply(rule absolutely_integrable_inf_real) prefer 3 |
|
5387 using absolutely_integrable_integrable_bound_real[OF assms(3,1,2)] by auto |
|
5388 fix x assume x:"x\<in>s" show "Inf {f j x |j. j \<in> {m..m + Suc k}} |
|
5389 \<le> Inf {f j x |j. j \<in> {m..m + k}}" apply(rule Inf_ge) unfolding setge_def |
|
5390 defer apply rule apply(subst Inf_finite_le_iff) prefer 3 |
|
5391 apply(rule_tac x=xa in bexI) by auto |
|
5392 let ?S = "{f j x| j. m \<le> j}" def i \<equiv> "Inf ?S" |
|
5393 show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) ---> i) sequentially" |
|
5394 unfolding Lim_sequentially |
|
5395 proof safe case goal1 note e=this have i:"isGlb UNIV ?S i" unfolding i_def apply(rule Inf) |
|
5396 defer apply(rule_tac x="- h x - 1" in exI) unfolding setge_def |
|
5397 proof safe case goal1 thus ?case using assms(3)[rule_format,OF x, of j] by auto |
|
5398 qed auto |
|
5399 |
|
5400 have "\<exists>y\<in>?S. \<not> y \<ge> i + e" |
|
5401 proof(rule ccontr) case goal1 hence "i \<ge> i + e" apply- |
|
5402 apply(rule isGlb_le_isLb[OF i]) apply(rule isLbI) unfolding setge_def by fastsimp+ |
|
5403 thus False using e by auto |
|
5404 qed then guess y .. note y=this[unfolded not_le] |
|
5405 from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this] |
|
5406 |
|
5407 show ?case apply(rule_tac x=N in exI) |
|
5408 proof safe case goal1 |
|
5409 have *:"\<And>y ix. y < i + e \<longrightarrow> i \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - i) < e" by arith |
|
5410 show ?case unfolding dist_real_def apply(rule *[rule_format,OF y(2)]) |
|
5411 unfolding i_def apply(rule real_le_inf_subset) prefer 3 |
|
5412 apply(rule,rule isGlbD1[OF i]) prefer 3 apply(subst Inf_finite_le_iff) |
|
5413 prefer 3 apply(rule_tac x=y in bexI) using N goal1 by auto |
|
5414 qed qed qed note dec1 = conjunctD2[OF this] |
|
5415 |
|
5416 have "\<And>m. (\<lambda>x. Sup {f j x |j. m \<le> j}) integrable_on s \<and> |
|
5417 ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}})) ---> |
|
5418 integral s (\<lambda>x. Sup {f j x |j. m \<le> j})) sequentially" |
|
5419 proof(rule monotone_convergence_increasing_real,safe) fix m::nat |
|
5420 show "bounded {integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) |k. True}" |
|
5421 unfolding bounded_iff apply(rule_tac x="integral s h" in exI) |
|
5422 proof safe fix k::nat |
|
5423 show "norm (integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}})) \<le> integral s h" |
|
5424 apply(rule integral_norm_bound_integral) unfolding simple_image |
|
5425 apply(rule absolutely_integrable_onD) apply(rule absolutely_integrable_sup_real) |
|
5426 prefer 5 unfolding real_norm_def apply(rule) apply(rule Sup_abs_le) |
|
5427 prefer 5 apply rule apply(rule_tac g=h in absolutely_integrable_integrable_bound_real) |
|
5428 using assms unfolding real_norm_def by auto |
|
5429 qed fix k::nat show "(\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) integrable_on s" |
|
5430 unfolding simple_image apply(rule absolutely_integrable_onD) |
|
5431 apply(rule absolutely_integrable_sup_real) prefer 3 |
|
5432 using absolutely_integrable_integrable_bound_real[OF assms(3,1,2)] by auto |
|
5433 fix x assume x:"x\<in>s" show "Sup {f j x |j. j \<in> {m..m + Suc k}} |
|
5434 \<ge> Sup {f j x |j. j \<in> {m..m + k}}" apply(rule Sup_le) unfolding setle_def |
|
5435 defer apply rule apply(subst Sup_finite_ge_iff) prefer 3 apply(rule_tac x=y in bexI) by auto |
|
5436 let ?S = "{f j x| j. m \<le> j}" def i \<equiv> "Sup ?S" |
|
5437 show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) ---> i) sequentially" |
|
5438 unfolding Lim_sequentially |
|
5439 proof safe case goal1 note e=this have i:"isLub UNIV ?S i" unfolding i_def apply(rule Sup) |
|
5440 defer apply(rule_tac x="h x" in exI) unfolding setle_def |
|
5441 proof safe case goal1 thus ?case using assms(3)[rule_format,OF x, of j] by auto |
|
5442 qed auto |
|
5443 |
|
5444 have "\<exists>y\<in>?S. \<not> y \<le> i - e" |
|
5445 proof(rule ccontr) case goal1 hence "i \<le> i - e" apply- |
|
5446 apply(rule isLub_le_isUb[OF i]) apply(rule isUbI) unfolding setle_def by fastsimp+ |
|
5447 thus False using e by auto |
|
5448 qed then guess y .. note y=this[unfolded not_le] |
|
5449 from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this] |
|
5450 |
|
5451 show ?case apply(rule_tac x=N in exI) |
|
5452 proof safe case goal1 |
|
5453 have *:"\<And>y ix. i - e < y \<longrightarrow> ix \<le> i \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - i) < e" by arith |
|
5454 show ?case unfolding dist_real_def apply(rule *[rule_format,OF y(2)]) |
|
5455 unfolding i_def apply(rule real_ge_sup_subset) prefer 3 |
|
5456 apply(rule,rule isLubD1[OF i]) prefer 3 apply(subst Sup_finite_ge_iff) |
|
5457 prefer 3 apply(rule_tac x=y in bexI) using N goal1 by auto |
|
5458 qed qed qed note inc1 = conjunctD2[OF this] |
|
5459 |
|
5460 have "g integrable_on s \<and> ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. k \<le> j})) ---> integral s g) sequentially" |
|
5461 apply(rule monotone_convergence_increasing_real,safe) apply fact |
|
5462 proof- show "bounded {integral s (\<lambda>x. Inf {f j x |j. k \<le> j}) |k. True}" |
|
5463 unfolding bounded_iff apply(rule_tac x="integral s h" in exI) |
|
5464 proof safe fix k::nat |
|
5465 show "norm (integral s (\<lambda>x. Inf {f j x |j. k \<le> j})) \<le> integral s h" |
|
5466 apply(rule integral_norm_bound_integral) apply fact+ |
|
5467 unfolding real_norm_def apply(rule) apply(rule Inf_abs_ge) using assms(3) by auto |
|
5468 qed fix k::nat and x assume x:"x\<in>s" |
|
5469 |
|
5470 have *:"\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto |
|
5471 show "Inf {f j x |j. k \<le> j} \<le> Inf {f j x |j. Suc k \<le> j}" apply- |
|
5472 apply(rule real_le_inf_subset) prefer 3 unfolding setge_def |
|
5473 apply(rule_tac x="- h x" in exI) apply safe apply(rule *) |
|
5474 using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto |
|
5475 show "((\<lambda>k. Inf {f j x |j. k \<le> j}) ---> g x) sequentially" unfolding Lim_sequentially |
|
5476 proof safe case goal1 hence "0<e/2" by auto |
|
5477 from assms(4)[unfolded Lim_sequentially,rule_format,OF x this] guess N .. note N=this |
|
5478 show ?case apply(rule_tac x=N in exI,safe) unfolding dist_real_def |
|
5479 apply(rule le_less_trans[of _ "e/2"]) apply(rule Inf_asclose) apply safe |
|
5480 defer apply(rule less_imp_le) using N goal1 unfolding dist_real_def by auto |
|
5481 qed qed note inc2 = conjunctD2[OF this] |
|
5482 |
|
5483 have "g integrable_on s \<and> ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) ---> integral s g) sequentially" |
|
5484 apply(rule monotone_convergence_decreasing_real,safe) apply fact |
|
5485 proof- show "bounded {integral s (\<lambda>x. Sup {f j x |j. k \<le> j}) |k. True}" |
|
5486 unfolding bounded_iff apply(rule_tac x="integral s h" in exI) |
|
5487 proof safe fix k::nat |
|
5488 show "norm (integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) \<le> integral s h" |
|
5489 apply(rule integral_norm_bound_integral) apply fact+ |
|
5490 unfolding real_norm_def apply(rule) apply(rule Sup_abs_le) using assms(3) by auto |
|
5491 qed fix k::nat and x assume x:"x\<in>s" |
|
5492 |
|
5493 show "Sup {f j x |j. k \<le> j} \<ge> Sup {f j x |j. Suc k \<le> j}" apply- |
|
5494 apply(rule real_ge_sup_subset) prefer 3 unfolding setle_def |
|
5495 apply(rule_tac x="h x" in exI) apply safe |
|
5496 using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto |
|
5497 show "((\<lambda>k. Sup {f j x |j. k \<le> j}) ---> g x) sequentially" unfolding Lim_sequentially |
|
5498 proof safe case goal1 hence "0<e/2" by auto |
|
5499 from assms(4)[unfolded Lim_sequentially,rule_format,OF x this] guess N .. note N=this |
|
5500 show ?case apply(rule_tac x=N in exI,safe) unfolding dist_real_def |
|
5501 apply(rule le_less_trans[of _ "e/2"]) apply(rule Sup_asclose) apply safe |
|
5502 defer apply(rule less_imp_le) using N goal1 unfolding dist_real_def by auto |
|
5503 qed qed note dec2 = conjunctD2[OF this] |
|
5504 |
|
5505 show "g integrable_on s" by fact |
|
5506 show "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially" unfolding Lim_sequentially |
|
5507 proof safe case goal1 |
|
5508 from inc2(2)[unfolded Lim_sequentially,rule_format,OF goal1] guess N1 .. note N1=this[unfolded dist_real_def] |
|
5509 from dec2(2)[unfolded Lim_sequentially,rule_format,OF goal1] guess N2 .. note N2=this[unfolded dist_real_def] |
|
5510 show ?case apply(rule_tac x="N1+N2" in exI,safe) |
|
5511 proof- fix n assume n:"n \<ge> N1 + N2" |
|
5512 have *:"\<And>i0 i i1 g. \<bar>i0 - g\<bar> < e \<longrightarrow> \<bar>i1 - g\<bar> < e \<longrightarrow> i0 \<le> i \<longrightarrow> i \<le> i1 \<longrightarrow> \<bar>i - g\<bar> < e" by arith |
|
5513 show "dist (integral s (f n)) (integral s g) < e" unfolding dist_real_def |
|
5514 apply(rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n]) |
|
5515 proof- show "integral s (\<lambda>x. Inf {f j x |j. n \<le> j}) \<le> integral s (f n)" |
|
5516 proof(rule integral_le[OF dec1(1) assms(1)],safe) |
|
5517 fix x assume x:"x \<in> s" have *:"\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto |
|
5518 show "Inf {f j x |j. n \<le> j} \<le> f n x" apply(rule Inf_lower[where z="- h x"]) defer |
|
5519 apply(rule *) using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto |
|
5520 qed show "integral s (f n) \<le> integral s (\<lambda>x. Sup {f j x |j. n \<le> j})" |
|
5521 proof(rule integral_le[OF assms(1) inc1(1)],safe) |
|
5522 fix x assume x:"x \<in> s" |
|
5523 show "f n x \<le> Sup {f j x |j. n \<le> j}" apply(rule Sup_upper[where z="h x"]) defer |
|
5524 using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto |
|
5525 qed qed(insert n,auto) qed qed qed |
3912 |
5526 |
3913 declare [[smt_certificates=""]] |
5527 declare [[smt_certificates=""]] |
3914 |
5528 |
3915 end |
5529 end |