Add theory for indicator function.
authorhoelzl
Thu Jul 01 11:48:42 2010 +0200 (2010-07-01)
changeset 37665579258a77fec
parent 37664 2946b8f057df
child 37666 e31fd427c285
Add theory for indicator function.
src/HOL/IsaMakefile
src/HOL/Library/Indicator_Function.thy
src/HOL/Library/Library.thy
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Integration.thy
     1.1 --- a/src/HOL/IsaMakefile	Thu Jul 01 09:01:09 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu Jul 01 11:48:42 2010 +0200
     1.3 @@ -406,7 +406,8 @@
     1.4    Library/Float.thy Library/Formal_Power_Series.thy			\
     1.5    Library/Fraction_Field.thy Library/FrechetDeriv.thy Library/Fset.thy	\
     1.6    Library/FuncSet.thy Library/Fundamental_Theorem_Algebra.thy		\
     1.7 -  Library/Glbs.thy Library/Infinite_Set.thy Library/Inner_Product.thy	\
     1.8 +  Library/Glbs.thy Library/Indicator_Function.thy			\
     1.9 +  Library/Infinite_Set.thy Library/Inner_Product.thy			\
    1.10    Library/HOL_Library_ROOT.ML Library/Kleene_Algebra.thy		\
    1.11    Library/LaTeXsugar.thy Library/Lattice_Algebras.thy			\
    1.12    Library/Lattice_Syntax.thy Library/Library.thy			\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Indicator_Function.thy	Thu Jul 01 11:48:42 2010 +0200
     2.3 @@ -0,0 +1,58 @@
     2.4 +(*  Title:      HOL/Library/Indicator_Function.thy
     2.5 +    Author:     Johannes Hoelzl (TU Muenchen)
     2.6 +*)
     2.7 +
     2.8 +header {* Indicator Function *}
     2.9 +
    2.10 +theory Indicator_Function
    2.11 +imports Main
    2.12 +begin
    2.13 +
    2.14 +definition "indicator S x = (if x \<in> S then 1 else 0)"
    2.15 +
    2.16 +lemma indicator_simps[simp]:
    2.17 +  "x \<in> S \<Longrightarrow> indicator S x = 1"
    2.18 +  "x \<notin> S \<Longrightarrow> indicator S x = 0"
    2.19 +  unfolding indicator_def by auto
    2.20 +
    2.21 +lemma
    2.22 +  shows indicator_pos_le[intro, simp]: "(0::'a::linordered_semidom) \<le> indicator S x"
    2.23 +  and indicator_le_1[intro, simp]: "indicator S x \<le> (1::'a::linordered_semidom)"
    2.24 +  and indicator_abs_le_1: "\<bar>indicator S x\<bar> \<le> (1::'a::linordered_idom)"
    2.25 +  unfolding indicator_def by auto
    2.26 +
    2.27 +lemma split_indicator:
    2.28 +  "P (indicator S x) \<longleftrightarrow> ((x \<in> S \<longrightarrow> P 1) \<and> (x \<notin> S \<longrightarrow> P 0))"
    2.29 +  unfolding indicator_def by auto
    2.30 +
    2.31 +lemma
    2.32 +  shows indicator_inter_arith: "indicator (A \<inter> B) x = indicator A x * (indicator B x::'a::semiring_1)"
    2.33 +  and indicator_union_arith: "indicator (A \<union> B) x =  indicator A x + indicator B x - indicator A x * (indicator B x::'a::ring_1)"
    2.34 +  and indicator_inter_min: "indicator (A \<inter> B) x = min (indicator A x) (indicator B x::'a::linordered_semidom)"
    2.35 +  and indicator_union_max: "indicator (A \<union> B) x = max (indicator A x) (indicator B x::'a::linordered_semidom)"
    2.36 +  and indicator_compl: "indicator (- A) x = 1 - (indicator A x::'a::ring_1)"
    2.37 +  and indicator_diff: "indicator (A - B) x = indicator A x * (1 - indicator B x::'a::ring_1)"
    2.38 +  unfolding indicator_def by (auto simp: min_def max_def)
    2.39 +
    2.40 +lemma
    2.41 +  shows indicator_times: "indicator (A \<times> B) x = indicator A (fst x) * (indicator B (snd x)::'a::semiring_1)"
    2.42 +  unfolding indicator_def by (cases x) auto
    2.43 +
    2.44 +lemma
    2.45 +  shows indicator_sum: "indicator (A <+> B) x = (case x of Inl x \<Rightarrow> indicator A x | Inr x \<Rightarrow> indicator B x)"
    2.46 +  unfolding indicator_def by (cases x) auto
    2.47 +
    2.48 +lemma
    2.49 +  fixes f :: "'a \<Rightarrow> 'b::semiring_1" assumes "finite A"
    2.50 +  shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)"
    2.51 +  and setsum_indicator_mult[simp]: "(\<Sum>x \<in> A. indicator B x * f x) = (\<Sum>x \<in> A \<inter> B. f x)"
    2.52 +  unfolding indicator_def
    2.53 +  using assms by (auto intro!: setsum_mono_zero_cong_right split: split_if_asm)
    2.54 +
    2.55 +lemma setsum_indicator_eq_card:
    2.56 +  assumes "finite A"
    2.57 +  shows "(SUM x : A. indicator B x) = card (A Int B)"
    2.58 +  using setsum_mult_indicator[OF assms, of "%x. 1::nat"]
    2.59 +  unfolding card_eq_setsum by simp
    2.60 +
    2.61 +end
    2.62 \ No newline at end of file
     3.1 --- a/src/HOL/Library/Library.thy	Thu Jul 01 09:01:09 2010 +0200
     3.2 +++ b/src/HOL/Library/Library.thy	Thu Jul 01 11:48:42 2010 +0200
     3.3 @@ -27,6 +27,7 @@
     3.4    Fset
     3.5    FuncSet
     3.6    Fundamental_Theorem_Algebra
     3.7 +  Indicator_Function
     3.8    Infinite_Set
     3.9    Inner_Product
    3.10    Lattice_Algebras
     4.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Jul 01 09:01:09 2010 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Jul 01 11:48:42 2010 +0200
     4.3 @@ -179,9 +179,6 @@
     4.4  
     4.5  subsection{* Basic componentwise operations on vectors. *}
     4.6  
     4.7 -lemma dimindex_ge_1:"CARD(_::finite) \<ge> 1"
     4.8 -  using one_le_card_finite by auto
     4.9 -
    4.10  instantiation cart :: (times,finite) times
    4.11  begin
    4.12    definition vector_mult_def : "op * \<equiv> (\<lambda> x y.  (\<chi> i. (x$i) * (y$i)))"
     5.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu Jul 01 09:01:09 2010 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Jul 01 11:48:42 2010 +0200
     5.3 @@ -4,7 +4,7 @@
     5.4      Translation from HOL light: Robert Himmelmann, TU Muenchen *)
     5.5  
     5.6  theory Integration
     5.7 -  imports Derivative "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
     5.8 +  imports Derivative "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Indicator_Function
     5.9  begin
    5.10  
    5.11  declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.certs"]]
    5.12 @@ -2468,22 +2468,7 @@
    5.13  
    5.14  subsection {* Negligible sets. *}
    5.15  
    5.16 -definition "indicator s \<equiv> (\<lambda>x. if x \<in> s then 1 else (0::real))"
    5.17 -
    5.18 -lemma dest_vec1_indicator:
    5.19 - "indicator s x = (if x \<in> s then 1 else 0)" unfolding indicator_def by auto
    5.20 -
    5.21 -lemma indicator_pos_le[intro]: "0 \<le> (indicator s x)" unfolding indicator_def by auto
    5.22 -
    5.23 -lemma indicator_le_1[intro]: "(indicator s x) \<le> 1" unfolding indicator_def by auto
    5.24 -
    5.25 -lemma dest_vec1_indicator_abs_le_1: "abs(indicator s x) \<le> 1"
    5.26 -  unfolding indicator_def by auto
    5.27 -
    5.28 -definition "negligible (s::(_::ordered_euclidean_space) set) \<equiv> (\<forall>a b. ((indicator s) has_integral 0) {a..b})"
    5.29 -
    5.30 -lemma indicator_simps[simp]:"x\<in>s \<Longrightarrow> indicator s x = 1" "x\<notin>s \<Longrightarrow> indicator s x = 0"
    5.31 -  unfolding indicator_def by auto
    5.32 +definition "negligible (s::('a::ordered_euclidean_space) set) \<equiv> (\<forall>a b. ((indicator s :: 'a\<Rightarrow>real) has_integral 0) {a..b})"
    5.33  
    5.34  subsection {* Negligibility of hyperplane. *}
    5.35  
    5.36 @@ -2543,7 +2528,9 @@
    5.37  lemma negligible_standard_hyperplane[intro]: fixes type::"'a::ordered_euclidean_space" assumes k:"k<DIM('a)"
    5.38    shows "negligible {x::'a. x$$k = (c::real)}" 
    5.39    unfolding negligible_def has_integral apply(rule,rule,rule,rule)
    5.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}"
    5.41 +proof-
    5.42 +  case goal1 from content_doublesplit[OF this k,of a b c] guess d . note d=this
    5.43 +  let ?i = "indicator {x::'a. x$$k = c} :: 'a\<Rightarrow>real"
    5.44    show ?case apply(rule_tac x="\<lambda>x. ball x d" in exI) apply(rule,rule gauge_ball,rule d)
    5.45    proof(rule,rule) fix p assume p:"p tagged_division_of {a..b} \<and> (\<lambda>x. ball x d) fine p"
    5.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)"
    5.47 @@ -2684,13 +2671,13 @@
    5.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)"
    5.49          apply(rule,rule tagged_division_finer[OF as(1) d(1)]) by auto
    5.50        from choice[OF this] guess q .. note q=conjunctD3[OF this[rule_format]]
    5.51 -      have *:"\<And>i. (\<Sum>(x, k)\<in>q i. content k *\<^sub>R indicator s x) \<ge> 0" apply(rule setsum_nonneg,safe) 
    5.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) 
    5.53          unfolding real_scaleR_def apply(rule mult_nonneg_nonneg) apply(drule tagged_division_ofD(4)[OF q(1)]) by auto
    5.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"
    5.55        proof- case goal1 thus ?case apply-apply(rule setsum_le_included[of s t g snd f]) prefer 4
    5.56            apply safe apply(erule_tac x=x in ballE) apply(erule exE) apply(rule_tac x="(xa,x)" in bexI) by auto qed
    5.57        have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) \<le> setsum (\<lambda>i. (real i + 1) *
    5.58 -                     norm(setsum (\<lambda>(x,k). content k *\<^sub>R indicator s x) (q i))) {0..N+1}"
    5.59 +                     norm(setsum (\<lambda>(x,k). content k *\<^sub>R indicator s x :: real) (q i))) {0..N+1}"
    5.60          unfolding real_norm_def setsum_right_distrib abs_of_nonneg[OF *] diff_0_right
    5.61          apply(rule order_trans,rule setsum_norm) defer apply(subst sum_sum_product) prefer 3 
    5.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
    5.63 @@ -2780,14 +2767,14 @@
    5.64  lemma negligible_unions[intro]: assumes "finite s" "\<forall>t\<in>s. negligible t" shows "negligible(\<Union>s)"
    5.65    using assms by(induct,auto) 
    5.66  
    5.67 -lemma negligible:  "negligible s \<longleftrightarrow> (\<forall>t::('a::ordered_euclidean_space) set. (indicator s has_integral 0) t)"
    5.68 +lemma negligible:  "negligible s \<longleftrightarrow> (\<forall>t::('a::ordered_euclidean_space) set. ((indicator s::'a\<Rightarrow>real) has_integral 0) t)"
    5.69    apply safe defer apply(subst negligible_def)
    5.70  proof- fix t::"'a set" assume as:"negligible s"
    5.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)  
    5.72 -  show "(indicator s has_integral 0) t" apply(subst has_integral_alt)
    5.73 +  show "((indicator s::'a\<Rightarrow>real) has_integral 0) t" apply(subst has_integral_alt)
    5.74      apply(cases,subst if_P,assumption) unfolding if_not_P apply(safe,rule as[unfolded negligible_def,rule_format])
    5.75      apply(rule_tac x=1 in exI) apply(safe,rule zero_less_one) apply(rule_tac x=0 in exI)
    5.76 -    using negligible_subset[OF as,of "s \<inter> t"] unfolding negligible_def indicator_def unfolding * by auto qed auto
    5.77 +    using negligible_subset[OF as,of "s \<inter> t"] unfolding negligible_def indicator_def_raw unfolding * by auto qed auto
    5.78  
    5.79  subsection {* Finite case of the spike theorem is quite commonly needed. *}
    5.80