src/HOL/Multivariate_Analysis/Integration.thy
 changeset 37665 579258a77fec parent 37489 44e42d392c6e child 38656 d5d342611edb
```     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu Jul 01 09:01:09 2010 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Jul 01 11:48:42 2010 +0200
1.3 @@ -4,7 +4,7 @@
1.4      Translation from HOL light: Robert Himmelmann, TU Muenchen *)
1.5
1.6  theory Integration
1.7 -  imports Derivative "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
1.8 +  imports Derivative "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Indicator_Function
1.9  begin
1.10
1.11  declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.certs"]]
1.12 @@ -2468,22 +2468,7 @@
1.13
1.14  subsection {* Negligible sets. *}
1.15
1.16 -definition "indicator s \<equiv> (\<lambda>x. if x \<in> s then 1 else (0::real))"
1.17 -
1.18 -lemma dest_vec1_indicator:
1.19 - "indicator s x = (if x \<in> s then 1 else 0)" unfolding indicator_def by auto
1.20 -
1.21 -lemma indicator_pos_le[intro]: "0 \<le> (indicator s x)" unfolding indicator_def by auto
1.22 -
1.23 -lemma indicator_le_1[intro]: "(indicator s x) \<le> 1" unfolding indicator_def by auto
1.24 -
1.25 -lemma dest_vec1_indicator_abs_le_1: "abs(indicator s x) \<le> 1"
1.26 -  unfolding indicator_def by auto
1.27 -
1.28 -definition "negligible (s::(_::ordered_euclidean_space) set) \<equiv> (\<forall>a b. ((indicator s) has_integral 0) {a..b})"
1.29 -
1.30 -lemma indicator_simps[simp]:"x\<in>s \<Longrightarrow> indicator s x = 1" "x\<notin>s \<Longrightarrow> indicator s x = 0"
1.31 -  unfolding indicator_def by auto
1.32 +definition "negligible (s::('a::ordered_euclidean_space) set) \<equiv> (\<forall>a b. ((indicator s :: 'a\<Rightarrow>real) has_integral 0) {a..b})"
1.33
1.34  subsection {* Negligibility of hyperplane. *}
1.35
1.36 @@ -2543,7 +2528,9 @@
1.37  lemma negligible_standard_hyperplane[intro]: fixes type::"'a::ordered_euclidean_space" assumes k:"k<DIM('a)"
1.38    shows "negligible {x::'a. x\$\$k = (c::real)}"
1.39    unfolding negligible_def has_integral apply(rule,rule,rule,rule)
1.40 -proof- case goal1 from content_doublesplit[OF this k,of a b c] guess d . note d=this let ?i = "indicator {x::'a. x\$\$k = c}"
1.41 +proof-
1.42 +  case goal1 from content_doublesplit[OF this k,of a b c] guess d . note d=this
1.43 +  let ?i = "indicator {x::'a. x\$\$k = c} :: 'a\<Rightarrow>real"
1.44    show ?case apply(rule_tac x="\<lambda>x. ball x d" in exI) apply(rule,rule gauge_ball,rule d)
1.45    proof(rule,rule) fix p assume p:"p tagged_division_of {a..b} \<and> (\<lambda>x. ball x d) fine p"
1.46      have *:"(\<Sum>(x, ka)\<in>p. content ka *\<^sub>R ?i x) = (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. abs(x\$\$k - c) \<le> d}) *\<^sub>R ?i x)"
1.47 @@ -2684,13 +2671,13 @@
1.48        have "\<forall>i. \<exists>q. q tagged_division_of {a..b} \<and> (d i) fine q \<and> (\<forall>(x, k)\<in>p. k \<subseteq> (d i) x \<longrightarrow> (x, k) \<in> q)"
1.49          apply(rule,rule tagged_division_finer[OF as(1) d(1)]) by auto
1.50        from choice[OF this] guess q .. note q=conjunctD3[OF this[rule_format]]
1.51 -      have *:"\<And>i. (\<Sum>(x, k)\<in>q i. content k *\<^sub>R indicator s x) \<ge> 0" apply(rule setsum_nonneg,safe)
1.52 +      have *:"\<And>i. (\<Sum>(x, k)\<in>q i. content k *\<^sub>R indicator s x) \<ge> (0::real)" apply(rule setsum_nonneg,safe)
1.53          unfolding real_scaleR_def apply(rule mult_nonneg_nonneg) apply(drule tagged_division_ofD(4)[OF q(1)]) by auto
1.54        have **:"\<And>f g s t. finite s \<Longrightarrow> finite t \<Longrightarrow> (\<forall>(x,y) \<in> t. (0::real) \<le> g(x,y)) \<Longrightarrow> (\<forall>y\<in>s. \<exists>x. (x,y) \<in> t \<and> f(y) \<le> g(x,y)) \<Longrightarrow> setsum f s \<le> setsum g t"
1.55        proof- case goal1 thus ?case apply-apply(rule setsum_le_included[of s t g snd f]) prefer 4
1.56            apply safe apply(erule_tac x=x in ballE) apply(erule exE) apply(rule_tac x="(xa,x)" in bexI) by auto qed
1.57        have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) \<le> setsum (\<lambda>i. (real i + 1) *
1.58 -                     norm(setsum (\<lambda>(x,k). content k *\<^sub>R indicator s x) (q i))) {0..N+1}"
1.59 +                     norm(setsum (\<lambda>(x,k). content k *\<^sub>R indicator s x :: real) (q i))) {0..N+1}"
1.60          unfolding real_norm_def setsum_right_distrib abs_of_nonneg[OF *] diff_0_right
1.61          apply(rule order_trans,rule setsum_norm) defer apply(subst sum_sum_product) prefer 3
1.62        proof(rule **,safe) show "finite {(i, j) |i j. i \<in> {0..N + 1} \<and> j \<in> q i}" apply(rule finite_product_dependent) using q by auto
1.63 @@ -2780,14 +2767,14 @@
1.64  lemma negligible_unions[intro]: assumes "finite s" "\<forall>t\<in>s. negligible t" shows "negligible(\<Union>s)"
1.65    using assms by(induct,auto)
1.66
1.67 -lemma negligible:  "negligible s \<longleftrightarrow> (\<forall>t::('a::ordered_euclidean_space) set. (indicator s has_integral 0) t)"
1.68 +lemma negligible:  "negligible s \<longleftrightarrow> (\<forall>t::('a::ordered_euclidean_space) set. ((indicator s::'a\<Rightarrow>real) has_integral 0) t)"
1.69    apply safe defer apply(subst negligible_def)
1.70  proof- fix t::"'a set" assume as:"negligible s"
1.71    have *:"(\<lambda>x. if x \<in> s \<inter> t then 1 else 0) = (\<lambda>x. if x\<in>t then if x\<in>s then 1 else 0 else 0)" by(rule ext,auto)
1.72 -  show "(indicator s has_integral 0) t" apply(subst has_integral_alt)
1.73 +  show "((indicator s::'a\<Rightarrow>real) has_integral 0) t" apply(subst has_integral_alt)
1.74      apply(cases,subst if_P,assumption) unfolding if_not_P apply(safe,rule as[unfolded negligible_def,rule_format])
1.75      apply(rule_tac x=1 in exI) apply(safe,rule zero_less_one) apply(rule_tac x=0 in exI)
1.76 -    using negligible_subset[OF as,of "s \<inter> t"] unfolding negligible_def indicator_def unfolding * by auto qed auto
1.77 +    using negligible_subset[OF as,of "s \<inter> t"] unfolding negligible_def indicator_def_raw unfolding * by auto qed auto
1.78
1.79  subsection {* Finite case of the spike theorem is quite commonly needed. *}
1.80
```