Theory HOL-Library.Indicator_Function

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

section ‹Indicator Function›

theory Indicator_Function
imports Complex_Main Disjoint_Sets
begin

definition "indicator S x = of_bool (x  S)"

text‹Type constrained version›
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 mult_indicator_cong:
  fixes f g :: "_  'a :: semiring_1"
  shows "(x. x  A  f x = g x)  indicator A x * f x = indicator A x * g x"
  by (auto simp: indicator_def)
  
lemma  
  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 
    (x  A. indicator (B x) (g x) *R f x) = (x  {xA. g x  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,zero_neq_one})  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 incseq A, of i "n + i" for n] x  A i 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<k. A i) x :: 'a::{topological_space,zero_neq_one})  indicator (i. A i) x"
proof -
  have "(λk. indicator (i<k. A i) x::'a)  indicator (k. i<k. A i) x"
    by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def intro: less_le_trans)
  also have "(k. i<k. A i) = (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,zero_neq_one})  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 decseq A, of i "n + i" for n] x  A i 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<k. A i) x :: 'a::{topological_space,zero_neq_one})  indicator (i. A i) x"
proof -
  have "(λk. indicator (i<k. A i) x::'a)  indicator (k. i<k. A i) x"
    by (intro LIMSEQ_indicator_decseq) (auto simp: decseq_def intro: less_le_trans)
  also have "(k. i<k. A i) = (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_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 *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 ‹
  The indicator function of the union of a disjoint family of sets is the
  sum over all the individual indicators.
›

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

end