author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 35292  e4a431b6d9b7 
permissions  rwrr 
35292
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

1 
header{*Integration on real intervals*} 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

2 

e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

3 
theory Real_Integration 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

4 
imports Integration 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

5 
begin 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

6 

e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

7 
text{*We follow John Harrison in formalizing the Gauge integral.*} 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

8 

e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

9 
definition Integral :: "real set \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool" where 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

10 
"Integral s f k = (f o dest_vec1 has_integral k) (vec1 ` s)" 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

11 

e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

12 
lemmas integral_unfold = Integral_def split_conv o_def vec1_interval 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

13 

e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

14 
lemma Integral_unique: 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

15 
"[ Integral{a..b} f k1; Integral{a..b} f k2 ] ==> k1 = k2" 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

16 
unfolding integral_unfold apply(rule has_integral_unique) by assumption+ 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

17 

e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

18 
lemma Integral_zero [simp]: "Integral{a..a} f 0" 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

19 
unfolding integral_unfold by auto 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

20 

e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

21 
lemma Integral_eq_diff_bounds: assumes "a \<le> b" shows "Integral{a..b} (%x. 1) (b  a)" 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

22 
unfolding integral_unfold using has_integral_const[of "1::real" "vec1 a" "vec1 b"] 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

23 
unfolding content_1'[OF assms] by auto 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

24 

e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

25 
lemma Integral_mult_const: assumes "a \<le> b" shows "Integral{a..b} (%x. c) (c*(b  a))" 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

26 
unfolding integral_unfold using has_integral_const[of "c::real" "vec1 a" "vec1 b"] 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

27 
unfolding content_1'[OF assms] by(auto simp add:field_simps) 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

28 

e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

29 
lemma Integral_mult: assumes "Integral{a..b} f k" shows "Integral{a..b} (%x. c * f x) (c * k)" 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

30 
using assms unfolding integral_unfold apply(drule_tac has_integral_cmul[where c=c]) by auto 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

31 

e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

32 
lemma Integral_add: 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

33 
assumes "Integral {a..b} f x1" "Integral {b..c} f x2" "a \<le> b" and "b \<le> c" 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

34 
shows "Integral {a..c} f (x1 + x2)" 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

35 
using assms unfolding integral_unfold apply 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

36 
apply(rule has_integral_combine[of "vec1 a" "vec1 b" "vec1 c"]) by auto 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

37 

e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

38 
lemma FTC1: assumes "a \<le> b" "\<forall>x. a \<le> x & x \<le> b > DERIV f x :> f'(x)" 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

39 
shows "Integral{a..b} f' (f(b)  f(a))" 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

40 
proofnote fundamental_theorem_of_calculus[OF assms(1), of"f o dest_vec1" "f' o dest_vec1"] 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

41 
note * = this[unfolded o_def vec1_dest_vec1] 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

42 
have **:"\<And>x. (\<lambda>xa\<Colon>real. xa * f' x) = op * (f' x)" apply(rule ext) by(auto simp add:field_simps) 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

43 
show ?thesis unfolding integral_unfold apply(rule *) 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

44 
using assms(2) unfolding DERIV_conv_has_derivative has_vector_derivative_def 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

45 
apply safe apply(rule has_derivative_at_within) by(auto simp add:**) qed 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

46 

e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

47 
lemma Integral_subst: "[ Integral{a..b} f k1; k2=k1 ] ==> Integral{a..b} f k2" 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

48 
by simp 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

49 

e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

50 
subsection {* Additivity Theorem of Gauge Integral *} 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

51 

e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

52 
text{* Bartle/Sherbert: Theorem 10.1.5 p. 278 *} 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

53 
lemma Integral_add_fun: "[ Integral{a..b} f k1; Integral{a..b} g k2 ] ==> Integral{a..b} (%x. f x + g x) (k1 + k2)" 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

54 
unfolding integral_unfold apply(rule has_integral_add) by assumption+ 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

55 

e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

56 
lemma norm_vec1'[simp]:"norm (vec1 x) = norm x" 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

57 
using norm_vector_1[of "vec1 x"] by auto 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

58 

e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

59 
lemma Integral_le: assumes "a \<le> b" "\<forall>x. a \<le> x & x \<le> b > f(x) \<le> g(x)" "Integral{a..b} f k1" "Integral{a..b} g k2" shows "k1 \<le> k2" 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

60 
proof note assms(34)[unfolded integral_unfold] note has_integral_vec1[OF this(1)] has_integral_vec1[OF this(2)] 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

61 
note has_integral_component_le[OF this,of 1] thus ?thesis using assms(2) by auto qed 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

62 

e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

63 
lemma monotonic_anti_derivative: 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

64 
fixes f g :: "real => real" shows 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

65 
"[ a \<le> b; \<forall>c. a \<le> c & c \<le> b > f' c \<le> g' c; 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

66 
\<forall>x. DERIV f x :> f' x; \<forall>x. DERIV g x :> g' x ] 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

67 
==> f b  f a \<le> g b  g a" 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

68 
apply (rule Integral_le, assumption) 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

69 
apply (auto intro: FTC1) 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

70 
done 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

71 

e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
diff
changeset

72 
end 