Theory Confine

section‹Confining a series to a set›

theory Confine
  imports Complex_Main
begin

definition confine :: "('a ⇒ 'b::zero) ⇒ 'a set ⇒ 'a ⇒ 'b"
  where "confine f A = (λx. if x ∈ A then f x else 0)"

lemma confine_UNIV [simp]: "confine f UNIV = f"
  by (simp add: confine_def)

lemma sum_confine_eq_Int:
  assumes "finite I"
  shows "sum (confine f A) I = (∑i ∈ I ∩ A. f i)"
proof -
  have "sum f(I ∩ A) = (∑a∈I. if a ∈ A then f a else 0)"
    using assms sum.inter_restrict by blast
  then show ?thesis
    by (auto simp: confine_def)
qed

lemma sums_confine_add:
  fixes f :: "nat ⇒ 'a::real_normed_vector"
  assumes "confine f N sums a" "confine g N sums b"
  shows "confine (λi. f i + g i) N sums (a+b)"
proof -
  have "⋀n. (if n ∈ N then f n + g n else 0) = (if n ∈ N then f n else 0) + (if n ∈ N then g n else 0)"
    by simp
  then show ?thesis
    using sums_add [of "confine f N" a "confine g N" b] assms
    by (simp add: confine_def)
qed

lemma sums_confine_minus:
  fixes f :: "nat ⇒ 'a::real_normed_vector"
  shows "confine f N sums a ⟹ confine (uminus ∘ f) N sums (-a)"
     using sums_minus [of "confine f N" a]
     by (simp add: confine_def if_distrib [of uminus] cong: if_cong)

lemma sums_confine_mult:
  fixes f :: "nat ⇒ 'a::real_normed_algebra"
  shows "confine f N sums a ⟹ confine (λn. c * f n) N sums (c * a)"
     using sums_mult [of "confine f N" a c]
     by (simp add: confine_def if_distrib [of "(*)c"] cong: if_cong)

lemma sums_confine_divide:
  fixes f :: "nat ⇒ 'a::real_normed_field"
  shows "confine f N sums a ⟹ confine (λn. f n / c) N sums (a/c)"
     using sums_divide [of "confine f N" a c]
     by (simp add: confine_def if_distrib [of "λx. x/c"] cong: if_cong)

lemma sums_confine_divide_iff:
  fixes f :: "nat ⇒ 'a::real_normed_field"
  assumes "c ≠ 0"
  shows "confine (λn. f n / c) N sums (a/c) ⟷ confine f N sums a"
proof
  show "confine f N sums a"
    if "confine (λn. f n / c) N sums (a / c)"
    using sums_confine_mult [OF that, of c] assms by simp
qed (auto simp: sums_confine_divide)

lemma sums_confine:
  fixes f :: "nat ⇒ 'a::real_normed_vector"
  shows "confine f N sums l ⟷ ((λn. ∑i ∈ {..<n} ∩ N. f i) ⇢ l)"
  by (simp add: sums_def atLeast0LessThan confine_def sum.inter_restrict)

lemma sums_confine_le:
  fixes f :: "nat ⇒ 'a::real_normed_vector"
  shows "confine f N sums l ⟷ ((λn. ∑i ∈ {..n} ∩ N. f i) ⇢ l)"
  by (simp add: sums_def_le atLeast0AtMost confine_def sum.inter_restrict)

end