src/HOL/Multivariate_Analysis/Real_Integration.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 35292 e4a431b6d9b7
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35292
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
     1
header{*Integration on real intervals*}
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
     2
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
     3
theory Real_Integration
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
     4
imports Integration
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
     5
begin
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
     6
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
     7
text{*We follow John Harrison in formalizing the Gauge integral.*}
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
     8
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
     9
definition Integral :: "real set \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool" where
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    10
  "Integral s f k = (f o dest_vec1 has_integral k) (vec1 ` s)"
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    11
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    12
lemmas integral_unfold = Integral_def split_conv o_def vec1_interval
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    13
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    14
lemma Integral_unique:
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    15
    "[| Integral{a..b} f k1; Integral{a..b} f k2 |] ==> k1 = k2"
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    16
  unfolding integral_unfold apply(rule has_integral_unique) by assumption+
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    17
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    18
lemma Integral_zero [simp]: "Integral{a..a} f 0"
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    19
  unfolding integral_unfold by auto
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    20
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/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 Multivariate-Analysis/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 Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    23
  unfolding content_1'[OF assms] by auto
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    24
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/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 Multivariate-Analysis/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 Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    27
  unfolding content_1'[OF assms] by(auto simp add:field_simps)
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    28
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/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 Multivariate-Analysis/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 Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    31
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    32
lemma Integral_add:
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/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 Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    34
  shows "Integral {a..c} f (x1 + x2)"
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    35
  using assms unfolding integral_unfold apply-
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/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 Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    37
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/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 Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    39
  shows "Integral{a..b} f' (f(b) - f(a))"
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    40
proof-note fundamental_theorem_of_calculus[OF assms(1), of"f o dest_vec1" "f' o dest_vec1"]
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    41
  note * = this[unfolded o_def vec1_dest_vec1]
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/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 Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    43
  show ?thesis unfolding integral_unfold apply(rule *)
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    44
    using assms(2) unfolding DERIV_conv_has_derivative has_vector_derivative_def
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    45
    apply safe apply(rule has_derivative_at_within) by(auto simp add:**) qed
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    46
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/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 Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    48
by simp
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    49
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    50
subsection {* Additivity Theorem of Gauge Integral *}
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    51
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    52
text{* Bartle/Sherbert: Theorem 10.1.5 p. 278 *}
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/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 Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    54
  unfolding integral_unfold apply(rule has_integral_add) by assumption+
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    55
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    56
lemma norm_vec1'[simp]:"norm (vec1 x) = norm x"
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    57
  using norm_vector_1[of "vec1 x"] by auto
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    58
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/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 Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    60
proof- note assms(3-4)[unfolded integral_unfold] note has_integral_vec1[OF this(1)] has_integral_vec1[OF this(2)]
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/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 Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    62
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    63
lemma monotonic_anti_derivative:
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    64
  fixes f g :: "real => real" shows
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/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 Multivariate-Analysis/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 Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    67
      ==> f b - f a \<le> g b - g a"
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    68
apply (rule Integral_le, assumption)
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    69
apply (auto intro: FTC1)
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    70
done
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    71
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
diff changeset
    72
end