Theory Indicator_Function

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

header {* Indicator Function *}

theory Indicator_Function
imports Complex_Main
begin

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

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::_::zero_neq_one) <-> x ∉ A"
  by (auto simp: indicator_def)

lemma indicator_eq_1_iff: "indicator A x = (1::_::zero_neq_one) <-> x ∈ A"
  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
  fixes f :: "'a => 'b::semiring_1" assumes "finite A"
  shows setsum_mult_indicator[simp]: "(∑x ∈ A. f x * indicator B x) = (∑x ∈ A ∩ B. f x)"
  and setsum_indicator_mult[simp]: "(∑x ∈ A. indicator B x * f x) = (∑x ∈ A ∩ B. f x)"
  unfolding indicator_def
  using assms by (auto intro!: setsum.mono_neutral_cong_right split: split_if_asm)

lemma setsum_indicator_eq_card:
  assumes "finite A"
  shows "(SUM x : A. indicator B x) = card (A Int B)"
  using setsum_mult_indicator[OF assms, of "%x. 1::nat"]
  unfolding card_eq_setsum by simp

lemma setsum_indicator_scaleR[simp]:
  "finite A ==>
    (∑x ∈ A. indicator (B x) (g x) *R f x) = (∑x ∈ {x∈A. g x ∈ B x}. f x::'a::real_vector)"
  using assms by (auto intro!: setsum.mono_neutral_cong_right split: split_if_asm simp: indicator_def)

lemma LIMSEQ_indicator_incseq:
  assumes "incseq A"
  shows "(λi. indicator (A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Union>i. A i) x"
proof cases
  assume "∃i. x ∈ A i"
  then obtain i where "x ∈ A i"
    by auto
  then have 
    "!!n. (indicator (A (n + i)) x :: 'a) = 1"
    "(indicator (\<Union> i. A i) x :: 'a) = 1"
    using incseqD[OF `incseq A`, of i "n + i" for n] `x ∈ A i` by (auto simp: indicator_def)
  then show ?thesis
    by (rule_tac LIMSEQ_offset[of _ i]) (simp add: tendsto_const)
qed (auto simp: indicator_def tendsto_const)

lemma LIMSEQ_indicator_UN:
  "(λk. indicator (\<Union> i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Union>i. A i) x"
proof -
  have "(λk. indicator (\<Union> i<k. A i) x::'a) ----> indicator (\<Union>k. \<Union> i<k. A i) x"
    by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def intro: less_le_trans)
  also have "(\<Union>k. \<Union> i<k. A i) = (\<Union>i. 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 (\<Inter>i. A i) x"
proof cases
  assume "∃i. x ∉ A i"
  then obtain i where "x ∉ A i"
    by auto
  then have 
    "!!n. (indicator (A (n + i)) x :: 'a) = 0"
    "(indicator (\<Inter>i. A i) x :: 'a) = 0"
    using decseqD[OF `decseq A`, of i "n + i" for n] `x ∉ A i` by (auto simp: indicator_def)
  then show ?thesis
    by (rule_tac LIMSEQ_offset[of _ i]) (simp add: tendsto_const)
qed (auto simp: indicator_def tendsto_const)

lemma LIMSEQ_indicator_INT:
  "(λk. indicator (\<Inter>i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Inter>i. A i) x"
proof -
  have "(λk. indicator (\<Inter>i<k. A i) x::'a) ----> indicator (\<Inter>k. \<Inter>i<k. A i) x"
    by (intro LIMSEQ_indicator_decseq) (auto simp: decseq_def intro: less_le_trans)
  also have "(\<Inter>k. \<Inter> i<k. A i) = (\<Inter>i. 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_sums: 
  assumes "!!i j. i ≠ j ==> A i ∩ A j = {}"
  shows "(λi. indicator (A i) x::real) sums indicator (\<Union>i. A i) x"
proof cases
  assume "∃i. x ∈ A i"
  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 (\<Union>i. A i) x"
    using i by (auto split: split_indicator)
  finally show ?thesis .
qed simp

end