Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Indicator_Function.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Library/Indicator_Function.thy
    Author:     Johannes Hoelzl (TU Muenchen)
*)

section \<open>Indicator Function\<close>

theory Indicator_Function
imports Complex_Main Disjoint_Sets
begin

definition "indicator S x = (if x \ S then 1 else 0)"

text\<open>Type constrained version\<close>
abbreviation indicat_real :: "'a set \ 'a \ real" where "indicat_real S \ indicator S"

lemma indicator_simps[simp]:
  "x \ S \ indicator S x = 1"
  "x \ S \ indicator S x = 0"
  unfolding indicator_def by auto

lemma indicator_pos_le[intro, simp]: "(0::'a::linordered_semidom) \ indicator S x"
  and indicator_le_1[intro, simp]: "indicator S x \ (1::'a::linordered_semidom)"
  unfolding indicator_def by auto

lemma indicator_abs_le_1: "\indicator S x\ \ (1::'a::linordered_idom)"
  unfolding indicator_def by auto

lemma indicator_eq_0_iff: "indicator A x = (0::'a::zero_neq_one) \ x \ A"
  by (auto simp: indicator_def)

lemma indicator_eq_1_iff: "indicator A x = (1::'a::zero_neq_one) \ x \ A"
  by (auto simp: indicator_def)

lemma indicator_UNIV [simp]: "indicator UNIV = (\x. 1)"
  by auto

lemma indicator_leI:
  "(x \ A \ y \ B) \ (indicator A x :: 'a::linordered_nonzero_semiring) \ indicator B y"
  by (auto simp: indicator_def)

lemma split_indicator: "P (indicator S x) \ ((x \ S \ P 1) \ (x \ S \ P 0))"
  unfolding indicator_def by auto

lemma split_indicator_asm: "P (indicator S x) \ (\ (x \ S \ \ P 1 \ x \ S \ \ P 0))"
  unfolding indicator_def by auto

lemma indicator_inter_arith: "indicator (A \ B) x = indicator A x * (indicator B x::'a::semiring_1)"
  unfolding indicator_def by (auto simp: min_def max_def)

lemma indicator_union_arith:
  "indicator (A \ B) x = indicator A x + indicator B x - indicator A x * (indicator B x :: 'a::ring_1)"
  unfolding indicator_def by (auto simp: min_def max_def)

lemma indicator_inter_min: "indicator (A \ B) x = min (indicator A x) (indicator B x::'a::linordered_semidom)"
  and indicator_union_max: "indicator (A \ B) x = max (indicator A x) (indicator B x::'a::linordered_semidom)"
  unfolding indicator_def by (auto simp: min_def max_def)

lemma indicator_disj_union:
  "A \ B = {} \ indicator (A \ B) x = (indicator A x + indicator B x :: 'a::linordered_semidom)"
  by (auto split: split_indicator)

lemma indicator_compl: "indicator (- A) x = 1 - (indicator A x :: 'a::ring_1)"
  and indicator_diff: "indicator (A - B) x = indicator A x * (1 - indicator B x ::'a::ring_1)"
  unfolding indicator_def by (auto simp: min_def max_def)

lemma indicator_times:
  "indicator (A \ B) x = indicator A (fst x) * (indicator B (snd x) :: 'a::semiring_1)"
  unfolding indicator_def by (cases x) auto

lemma indicator_sum:
  "indicator (A <+> B) x = (case x of Inl x \ indicator A x | Inr x \ indicator B x)"
  unfolding indicator_def by (cases x) auto

lemma indicator_image: "inj f \ indicator (f ` X) (f x) = (indicator X x::_::zero_neq_one)"
  by (auto simp: indicator_def inj_def)

lemma indicator_vimage: "indicator (f -` A) x = indicator A (f x)"
  by (auto split: split_indicator)

lemma  (* FIXME unnamed!? *)
  fixes f :: "'a \ 'b::semiring_1"
  assumes "finite A"
  shows sum_mult_indicator[simp]: "(\x \ A. f x * indicator B x) = (\x \ A \ B. f x)"
    and sum_indicator_mult[simp]: "(\x \ A. indicator B x * f x) = (\x \ A \ B. f x)"
  unfolding indicator_def
  using assms by (auto intro!: sum.mono_neutral_cong_right split: if_split_asm)

lemma sum_indicator_eq_card:
  assumes "finite A"
  shows "(\x \ A. indicator B x) = card (A Int B)"
  using sum_mult_indicator [OF assms, of "\x. 1::nat"]
  unfolding card_eq_sum by simp

lemma sum_indicator_scaleR[simp]:
  "finite A \
    (\<Sum>x \<in> A. indicator (B x) (g x) *\<^sub>R f x) = (\<Sum>x \<in> {x\<in>A. g x \<in> B x}. f x :: 'a::real_vector)"
  by (auto intro!: sum.mono_neutral_cong_right split: if_split_asm simp: indicator_def)

lemma LIMSEQ_indicator_incseq:
  assumes "incseq A"
  shows "(\i. indicator (A i) x :: 'a::{topological_space,one,zero}) \ indicator (\i. A i) x"
proof (cases "\i. x \ A i")
  case True
  then obtain i where "x \ A i"
    by auto
  then have *:
    "\n. (indicator (A (n + i)) x :: 'a) = 1"
    "(indicator (\i. A i) x :: 'a) = 1"
    using incseqD[OF \<open>incseq A\<close>, of i "n + i" for n] \<open>x \<in> A i\<close> by (auto simp: indicator_def)
  show ?thesis
    by (rule LIMSEQ_offset[of _ i]) (use * in simp)
next
  case False
  then show ?thesis by (simp add: indicator_def)
qed

lemma LIMSEQ_indicator_UN:
  "(\k. indicator (\i indicator (\i. A i) x"
proof -
  have "(\k. indicator (\i indicator (\k. \i
    by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def intro: less_le_trans)
  also have "(\k. \ii. A i)"
    by auto
  finally show ?thesis .
qed

lemma LIMSEQ_indicator_decseq:
  assumes "decseq A"
  shows "(\i. indicator (A i) x :: 'a::{topological_space,one,zero}) \ indicator (\i. A i) x"
proof (cases "\i. x \ A i")
  case True
  then obtain i where "x \ A i"
    by auto
  then have *:
    "\n. (indicator (A (n + i)) x :: 'a) = 0"
    "(indicator (\i. A i) x :: 'a) = 0"
    using decseqD[OF \<open>decseq A\<close>, of i "n + i" for n] \<open>x \<notin> A i\<close> by (auto simp: indicator_def)
  show ?thesis
    by (rule LIMSEQ_offset[of _ i]) (use * in simp)
next
  case False
  then show ?thesis by (simp add: indicator_def)
qed

lemma LIMSEQ_indicator_INT:
  "(\k. indicator (\i indicator (\i. A i) x"
proof -
  have "(\k. indicator (\i indicator (\k. \i
    by (intro LIMSEQ_indicator_decseq) (auto simp: decseq_def intro: less_le_trans)
  also have "(\k. \ii. A i)"
    by auto
  finally show ?thesis .
qed

lemma indicator_add:
  "A \ B = {} \ (indicator A x::_::monoid_add) + indicator B x = indicator (A \ B) x"
  unfolding indicator_def by auto

lemma of_real_indicator: "of_real (indicator A x) = indicator A x"
  by (simp split: split_indicator)

lemma real_of_nat_indicator: "real (indicator A x :: nat) = indicator A x"
  by (simp split: split_indicator)

lemma abs_indicator: "\indicator A x :: 'a::linordered_idom\ = indicator A x"
  by (simp split: split_indicator)

lemma mult_indicator_subset:
  "A \ B \ indicator A x * indicator B x = (indicator A x :: 'a::comm_semiring_1)"
  by (auto split: split_indicator simp: fun_eq_iff)

lemma indicator_times_eq_if:
  fixes f :: "'a \ 'b::comm_ring_1"
  shows "indicator S x * f x = (if x \ S then f x else 0)" "f x * indicator S x = (if x \ S then f x else 0)"
  by auto

lemma indicator_scaleR_eq_if:
  fixes f :: "'a \ 'b::real_vector"
  shows "indicator S x *\<^sub>R f x = (if x \ S then f x else 0)"
  by simp

lemma indicator_sums:
  assumes "\i j. i \ j \ A i \ A j = {}"
  shows "(\i. indicator (A i) x::real) sums indicator (\i. A i) x"
proof (cases "\i. x \ A i")
  case True
  then obtain i where i: "x \ A i" ..
  with assms have "(\i. indicator (A i) x::real) sums (\i\{i}. indicator (A i) x)"
    by (intro sums_finite) (auto split: split_indicator)
  also have "(\i\{i}. indicator (A i) x) = indicator (\i. A i) x"
    using i by (auto split: split_indicator)
  finally show ?thesis .
next
  case False
  then show ?thesis by simp
qed

text \<open>
  The indicator function of the union of a disjoint family of sets is the
  sum over all the individual indicators.
\<close>

lemma indicator_UN_disjoint:
  "finite A \ disjoint_family_on f A \ indicator (\(f ` A)) x = (\y\A. indicator (f y) x)"
  by (induct A rule: finite_induct)
    (auto simp: disjoint_family_on_def indicator_def split: if_splits)

end

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.