Theory PNT_Subsummable

theory PNT_Subsummable
imports
  "PNT_Remainder_Library"
begin
unbundle pnt_syntax

definition has_subsum where "has_subsum f S x ≡ (λn. if n ∈ S then f n else 0) sums x"
definition subsum where "subsum f S ≡ ∑n. if n ∈ S then f n else 0"
definition subsummable (infix ‹subsummable› 50)
  where "f subsummable S ≡ summable (λn. if n ∈ S then f n else 0)"

syntax "_subsum" :: "pttrn ⇒ nat set ⇒ 'a ⇒ 'a"
  (‹(2∑`_ ∈ (_)./ _)› [0, 0, 10] 10)
syntax_consts "_subsum" == subsum
translations
  "∑` x∈S. t" => "CONST subsum (λx. t) S"

syntax "_subsum_prop" :: "pttrn ⇒ bool ⇒ 'a ⇒ 'a"
  (‹(2∑`_ | (_)./ _)› [0, 0, 10] 10)
syntax_consts "_subsum_prop" == subsum
translations
  "∑` x|P. t" => "CONST subsum (λx. t) {x. P}"

syntax "_subsum_ge" :: "pttrn ⇒ nat ⇒ 'a ⇒ 'a"
  (‹(2∑`_ ≥ _./ _)› [0, 0, 10] 10)
syntax_consts "_subsum_ge" == subsum
translations
  "∑` x≥n. t" => "CONST subsum (λx. t) {n..}"

lemma has_subsum_finite:
  "finite F ⟹ has_subsum f F (sum f F)"
  unfolding has_subsum_def by (rule sums_If_finite_set)

lemma has_subsum_If_finite_set:
  assumes "finite F"
  shows "has_subsum (λn. if n ∈ F then f n else 0) A (sum f (F ∩ A))"
proof -
  have "F ∩ A = {x. x ∈ A ∧ x ∈ F}" by auto
  thus ?thesis unfolding has_subsum_def using assms
    by (auto simp add: if_if_eq_conj intro!: sums_If_finite)
qed

lemma has_subsum_If_finite:
  assumes "finite {n ∈ A. p n}"
  shows "has_subsum (λn. if p n then f n else 0) A (sum f {n ∈ A. p n})"
unfolding has_subsum_def using assms
  by (auto simp add: if_if_eq_conj intro!: sums_If_finite)

lemma has_subsum_univ:
  "f sums v ⟹ has_subsum f UNIV v" 
  unfolding has_subsum_def by auto

lemma subsumI:
  fixes f :: "nat ⇒ 'a :: {t2_space, comm_monoid_add}"
  shows "has_subsum f A x ⟹ x = subsum f A"
  unfolding has_subsum_def subsum_def by (intro sums_unique)

lemma has_subsum_summable:
  "has_subsum f A x ⟹ f subsummable A"
  unfolding has_subsum_def subsummable_def by (rule sums_summable)

lemma subsummable_sums:
  fixes f :: "nat ⇒ 'a :: {comm_monoid_add, t2_space}"
  shows "f subsummable S ⟹ has_subsum f S (subsum f S)"
  unfolding subsummable_def has_subsum_def subsum_def by (intro summable_sums)

lemma has_subsum_diff_finite:
  fixes S :: "'a :: {topological_ab_group_add, t2_space}"
  assumes "finite F" "has_subsum f A S" "F ⊆ A"
  shows "has_subsum f (A - F) (S - sum f F)"
proof -
  define p where "p n ≡ if n ∈ F then 0 else (if n ∈ A then f n else 0)" for n
  define q where "q n ≡ if n ∈ A - F then f n else 0" for n
  have "F ∩ A = F" using assms(3) by auto
  hence "p sums (S - sum f F)"
    using assms unfolding p_def has_subsum_def
    by (auto intro: sums_If_finite_set' [where ?S = S]
             simp: sum_negf sum.inter_restrict [symmetric])
  moreover have "p = q" unfolding p_def q_def by auto
  finally show ?thesis unfolding q_def has_subsum_def by auto
qed

lemma subsum_split:
  fixes f :: "nat ⇒ 'a :: {topological_ab_group_add, t2_space}"
  assumes "f subsummable A" "finite F" "F ⊆ A"
  shows "subsum f A = sum f F + subsum f (A - F)"
proof -
  from assms(1) have "has_subsum f A (subsum f A)" by (intro subsummable_sums)
  hence "has_subsum f (A - F) (subsum f A - sum f F)"
    using assms by (intro has_subsum_diff_finite)
  hence "subsum f A - sum f F = subsum f (A - F)" by (rule subsumI)
  thus ?thesis by (auto simp add: algebra_simps)
qed

lemma has_subsum_zero [simp]: "has_subsum (λn. 0) A 0" unfolding has_subsum_def by auto
lemma zero_subsummable [simp]: "(λn. 0) subsummable A" unfolding subsummable_def by auto
lemma zero_subsum [simp]: "(∑`n∈A. 0 :: 'a :: {comm_monoid_add, t2_space}) = 0" unfolding subsum_def by auto

lemma has_subsum_minus:
  fixes f :: "nat ⇒ 'a :: real_normed_vector"
  assumes "has_subsum f A a" "has_subsum g A b"
  shows "has_subsum (λn. f n - g n) A (a - b)"
proof -
  define p where "p n = (if n ∈ A then f n else 0)" for n
  define q where "q n = (if n ∈ A then g n else 0)" for n
  have "(λn. p n - q n) sums (a - b)"
    using assms unfolding p_def q_def has_subsum_def by (intro sums_diff)
  moreover have "(if n ∈ A then f n - g n else 0) = p n - q n" for n
    unfolding p_def q_def by auto
  ultimately show ?thesis unfolding has_subsum_def by auto
qed

lemma subsum_minus:
  assumes "f subsummable A" "g subsummable A"
  shows "subsum f A - subsum g A = (∑`n∈A. f n - g n :: 'a :: real_normed_vector)"
  by (intro subsumI has_subsum_minus subsummable_sums assms)

lemma subsummable_minus:
  assumes "f subsummable A" "g subsummable A"
  shows "(λn. f n - g n :: 'a :: real_normed_vector) subsummable A"
  by (auto intro: has_subsum_summable has_subsum_minus subsummable_sums assms)

lemma has_subsum_uminus:
  assumes "has_subsum f A a"
  shows "has_subsum (λn. - f n :: 'a :: real_normed_vector) A (- a)"
proof -
  have "has_subsum (λn. 0 - f n) A (0 - a)"
    by (intro has_subsum_minus) (use assms in auto)
  thus ?thesis by auto
qed

lemma subsum_uminus:
  "f subsummable A ⟹ - subsum f A = (∑`n∈A. - f n :: 'a :: real_normed_vector)"
  by (intro subsumI has_subsum_uminus subsummable_sums)

lemma subsummable_uminus:
  "f subsummable A ⟹ (λn. - f n :: 'a :: real_normed_vector) subsummable A"
  by (auto intro: has_subsum_summable has_subsum_uminus subsummable_sums)

lemma has_subsum_add:
  fixes f :: "nat ⇒ 'a :: real_normed_vector"
  assumes "has_subsum f A a" "has_subsum g A b"
  shows "has_subsum (λn. f n + g n) A (a + b)"
proof -
  have "has_subsum (λn. f n - - g n) A (a - - b)"
    by (intro has_subsum_minus has_subsum_uminus assms)
  thus ?thesis by auto
qed

lemma subsum_add:
  assumes "f subsummable A" "g subsummable A"
  shows "subsum f A + subsum g A = (∑`n∈A. f n + g n :: 'a :: real_normed_vector)"
  by (intro subsumI has_subsum_add subsummable_sums assms)

lemma subsummable_add:
  assumes "f subsummable A" "g subsummable A"
  shows "(λn. f n + g n :: 'a :: real_normed_vector) subsummable A"
  by (auto intro: has_subsum_summable has_subsum_add subsummable_sums assms)

lemma subsum_cong:
  "(⋀x. x ∈ A ⟹ f x = g x) ⟹ subsum f A = subsum g A"
  unfolding subsum_def by (intro suminf_cong) auto

lemma subsummable_cong:
  fixes f :: "nat ⇒ 'a :: real_normed_vector"
  shows "(⋀x. x ∈ A ⟹ f x = g x) ⟹ (f subsummable A) = (g subsummable A)"
  unfolding subsummable_def by (intro summable_cong) auto

lemma subsum_norm_bound:
  fixes f :: "nat ⇒ 'a :: banach"
  assumes "g subsummable A" "⋀n. n ∈ A ⟹ ∥f n∥ ≤ g n"
  shows "∥subsum f A∥ ≤ subsum g A"
  using assms unfolding subsummable_def subsum_def
  by (intro suminf_norm_bound) auto

lemma eval_fds_subsum:
  fixes f :: "'a :: {nat_power, banach, real_normed_field} fds"
  assumes "fds_converges f s"
  shows "has_subsum (λn. fds_nth f n / nat_power n s) {1..} (eval_fds f s)"
proof -
  let ?f = "λn. fds_nth f n / nat_power n s"
  let ?v = "eval_fds f s"
  have "has_subsum (λn. ?f n) UNIV ?v"
    by (intro has_subsum_univ fds_converges_iff [THEN iffD1] assms)
  hence "has_subsum ?f (UNIV - {0}) (?v - sum ?f {0})"
    by (intro has_subsum_diff_finite) auto
  moreover have "UNIV - {0 :: nat} = {1..}" by auto
  ultimately show ?thesis by auto
qed

lemma fds_abs_subsummable:
  fixes f :: "'a :: {nat_power, banach, real_normed_field} fds"
  assumes "fds_abs_converges f s"
  shows "(λn. ∥fds_nth f n / nat_power n s∥) subsummable {1..}"
proof -
  have "summable (λn. ∥fds_nth f n / nat_power n s∥)"
    by (subst fds_abs_converges_def [symmetric]) (rule assms)
  moreover have "∥fds_nth f n / nat_power n s∥ = 0" when "¬ 1 ≤ n" for n
  proof -
    have "n = 0" using that by auto
    thus ?thesis by auto
  qed
  hence "(λn. if 1 ≤ n then ∥fds_nth f n / nat_power n s∥ else 0)
       = (λn. ∥fds_nth f n / nat_power n s∥)" by auto
  ultimately show ?thesis unfolding subsummable_def by auto
qed

lemma subsum_mult2:
  fixes f :: "nat ⇒ 'a :: real_normed_algebra"
  shows "f subsummable A ⟹ (∑`x∈A. f x * c) = subsum f A * c"
unfolding subsum_def subsummable_def
  by (subst suminf_mult2) (auto intro: suminf_cong)

lemma subsummable_mult2:
  fixes f :: "nat ⇒ 'a :: real_normed_algebra"
  assumes "f subsummable A"
  shows "(λx. f x * c) subsummable A"
proof -
  have "summable (λn. (if n ∈ A then f n else 0) * c)" (is ?P)
    using assms unfolding subsummable_def by (intro summable_mult2)
  moreover have "?P = ?thesis"
    unfolding subsummable_def by (rule summable_cong) auto
  ultimately show ?thesis by auto
qed

lemma subsum_ge_limit:
  "lim (λN. ∑n = m..N. f n) = (∑`n ≥ m. f n)"
proof -
  define g where "g n ≡ if n ∈ {m..} then f n else 0" for n
  have "(∑n. g n) = lim (λN. ∑n<N. g n)" by (rule suminf_eq_lim)
  also have "… = lim (λN. ∑n<N + 1. g n)"
    unfolding lim_def using LIMSEQ_ignore_initial_segment LIMSEQ_offset
    by (intro The_cong iffI) blast
  also have "… = lim (λN. ∑n = m..N. f n)"
  proof -
    have "{x. x < N + 1 ∧ m ≤ x} = {m..N}" for N by auto
    thus ?thesis unfolding g_def by (subst sum.inter_filter [symmetric]) auto
  qed
  finally show ?thesis unfolding subsum_def g_def by auto
qed

lemma has_subsum_ge_limit:
  fixes f :: "nat ⇒ 'a :: {t2_space, comm_monoid_add, topological_space}"
  assumes "((λN. ∑n = m..N. f n) ⤏ l) at_top"
  shows "has_subsum f {m..} l"
proof -
  define g where "g n ≡ if n ∈ {m..} then f n else 0" for n
  have "((λN. ∑n<N + 1. g n) ⤏ l) at_top"
  proof -
    have "{x. x < N + 1 ∧ m ≤ x} = {m..N}" for N by auto
    with assms show ?thesis
      unfolding g_def by (subst sum.inter_filter [symmetric]) auto
  qed
  hence "((λN. ∑n<N. g n) ⤏ l) at_top" by (rule LIMSEQ_offset)
  thus ?thesis unfolding has_subsum_def sums_def g_def by auto
qed

lemma eval_fds_complex:
  fixes f :: "complex fds"
  assumes "fds_converges f s"
  shows "has_subsum (λn. fds_nth f n / n nat_powr s) {1..} (eval_fds f s)"
proof -
  have "has_subsum (λn. fds_nth f n / nat_power n s) {1..} (eval_fds f s)"
    by (intro eval_fds_subsum assms)
  thus ?thesis unfolding nat_power_complex_def .
qed

lemma eval_fds_complex_subsum:
  fixes f :: "complex fds"
  assumes "fds_converges f s"
  shows "eval_fds f s = (∑`n ≥ 1. fds_nth f n / n nat_powr s)"
        "(λn. fds_nth f n / n nat_powr s) subsummable {1..}"
proof (goal_cases)
  case 1 show ?case by (intro subsumI eval_fds_complex assms)
  case 2 show ?case by (intro has_subsum_summable) (rule eval_fds_complex assms)+
qed

lemma has_sum_imp_has_subsum:
  fixes x :: "'a :: {comm_monoid_add, t2_space}"
  assumes "(f has_sum x) A"
  shows "has_subsum f A x"
proof -
  have "(∀⇩F x in at_top. sum f ({..<x} ∩ A) ∈ S)"
    when "open S" "x ∈ S" for S
  proof -
    have "∀S. open S ⟶ x ∈ S ⟶ (∀⇩F x in finite_subsets_at_top A. sum f x ∈ S)"
      using assms unfolding has_sum_def tendsto_def .
    hence "∀⇩F x in finite_subsets_at_top A. sum f x ∈ S" using that by auto
    then obtain X where hX: "finite X" "X ⊆ A"
      and hY: "⋀Y. finite Y ⟹ X ⊆ Y ⟹ Y ⊆ A ⟹ sum f Y ∈ S"
      unfolding eventually_finite_subsets_at_top by metis
    define n where "n ≡ Max X + 1"
    show ?thesis
    proof (subst eventually_sequentially, standard, safe)
      fix m assume Hm: "n ≤ m"
      moreover have "x ∈ X ⟹ x < n" for x
        unfolding n_def using Max_ge [OF hX(1), of x] by auto
      ultimately show "sum f ({..<m} ∩ A) ∈ S"
        using hX(2) by (intro hY, auto) (metis order.strict_trans2)
    qed
  qed
  thus ?thesis unfolding has_subsum_def sums_def tendsto_def
    by (simp add: sum.inter_restrict [symmetric])
qed

unbundle no pnt_syntax

end