Theory Extended_Reals_Sums_Compl

theory Extended_Reals_Sums_Compl imports  
  "HOL-Analysis.Analysis" 
begin

lemma real_ereal_leq:
  fixes a::ereal and b::real
  assumes "real_of_ereal a ≤ b"
    and "a ≠ ∞"
  shows "a ≤ ereal b"
  by (metis (mono_tags, opaque_lifting) MInfty_eq_minfinity assms eq_iff ereal_eq_0(2) ereal_le_real_iff 
      ereal_less_eq(2) le_cases real_of_ereal.elims real_of_ereal.simps(1) zero_ereal_def) 

lemma ereal_sums_Pinfty:
  fixes f::"nat ⇒ ereal"
  assumes "f sums ∞"
    and "⋀n. ¦f n¦ ≠ ∞"
  shows "(λn. - f n) sums -∞" 
proof -
  define rf where "rf = (λn. real_of_ereal (f n))"
  have "⋀n. f n = ereal (rf n)" unfolding rf_def using assms by (simp add: ereal_real')
  define g where "g = (λn. (∑i ∈ {..< n}. rf i))"
  define gm where "gm = (λn. (∑i ∈ {..< n}. - rf i))"
  have "⋀n. gm n = - g n" unfolding g_def gm_def by (simp add: sum_negf)  
  hence "⋀n. ereal (gm n) = (∑i ∈ {..< n}.- f i)" using ‹⋀n. f n = ereal (rf n)›
    using gm_def by auto
  have "(λn. ereal (g n)) ⇢ ∞" using assms ‹⋀n. f n = ereal (rf n)› unfolding sums_def g_def 
    by simp
  have "∀M. ∃N. ∀n≥ N. (gm n) ≤ M" 
  proof
    fix M
    have "∃N. ∀n≥ N. ereal (-M) ≤ g n" using ‹g ⇢ ∞›  Lim_PInfty by simp
    from this obtain N where "∀n≥ N. ereal (-M) ≤ g n" by auto
    hence "∀n ≥ N. - (g n) ≤ M" by auto
    hence "∀n ≥ N. gm n ≤ M" using ‹⋀n. gm n = - g n› by simp
    thus "∃N. ∀n ≥ N. gm n ≤ M" by auto
  qed
  hence "(λn. ereal (gm n)) ⇢ -∞" by (simp add: Lim_MInfty)
  thus ?thesis  using ‹⋀n. ereal (gm n) = (∑i ∈ {..< n}.- f i)› unfolding sums_def by simp
qed

lemma ereal_sums_Minfty:
  fixes f::"nat ⇒ ereal"
  assumes "f sums -∞"
    and "⋀n. ¦f n¦ ≠ ∞"
  shows "(λn. - f n) sums ∞" 
proof -
  define rf where "rf = (λn. real_of_ereal (f n))"
  have "⋀n. f n = ereal (rf n)" unfolding rf_def using assms by (simp add: ereal_real')
  define g where "g = (λn. (∑i ∈ {..< n}. rf i))"
  define gm where "gm = (λn. (∑i ∈ {..< n}. - rf i))"
  have "⋀n. gm n = - g n" unfolding g_def gm_def by (simp add: sum_negf)  
  hence "⋀n. ereal (gm n) = (∑i ∈ {..< n}.- f i)" using ‹⋀n. f n = ereal (rf n)›
    using gm_def by auto
  have "(λn. ereal (g n)) ⇢ -∞" using assms ‹⋀n. f n = ereal (rf n)› unfolding sums_def g_def 
    by simp
  have "∀M. ∃N. ∀n≥ N. M ≤ (gm n)" 
  proof
    fix M
    have "∃N. ∀n≥ N. g n ≤ ereal (-M)" using ‹g ⇢ -∞›  Lim_MInfty by simp
    from this obtain N where "∀n≥ N. g n ≤ ereal (-M)" by auto
    hence "∀n ≥ N. M ≤ - (g n)" by auto
    hence "∀n ≥ N. M ≤ gm n" using ‹⋀n. gm n = - g n› by simp
    thus "∃N. ∀n ≥ N. M ≤ gm n" by auto
  qed
  hence "(λn. ereal (gm n)) ⇢ ∞" by (simp add: Lim_PInfty)
  thus ?thesis  using ‹⋀n. ereal (gm n) = (∑i ∈ {..< n}.- f i)› unfolding sums_def by simp
qed

lemma mem_sums_Pinfty:
  assumes "((f i)::ereal) = ∞"
  shows "f sums ∞" 
proof -
  define g where "g = (λn. (∑i ∈ {..< n}. f i))"
  have ginf: "∀ j ≥ Suc i. g j = ∞"
  proof (intro allI impI)
    fix j
    assume "Suc i ≤ j"
    hence "i < j" by simp
    hence "i ∈ {..< j}" by auto
    thus "g j = ∞" unfolding g_def using sum_Pinfty[of f "{..< j}"] assms by blast
  qed
  have "∀M. ∃N. ∀n≥ N. M ≤ (g n)" 
  proof
    fix M
    show "∃N. ∀n≥ N. M ≤ g n" using ginf by force
  qed
  hence "g ⇢ ∞" by (simp add: Lim_PInfty)
  thus ?thesis   unfolding sums_def g_def by simp
qed

lemma sum_Minfty:
  fixes f :: "nat ⇒ ereal"
  shows "⋀i. finite P ⟹ i ∈ P ⟹ f i = - ∞ ⟹ ∞ ∉ range f ⟹ sum f P = -∞"
proof -
  fix i 
  assume "finite P"
    and "i ∈ P" 
    and "f i = -∞"
    and "∞ ∉ range f"
  thus "sum f P = -∞"
  proof induct
    case empty
    then show ?case by simp
  next
    case (insert x F)
    then show ?case
      by (metis ereal_plus_eq_MInfty insert_iff rangeI sum.insert sum_Pinfty)
  qed
qed

lemma mem_sums_Minfty:
  assumes "((f i)::ereal) = -∞"
    and "∞ ∉ range f"
  shows "f sums -∞" 
proof -
  define g where "g = (λn. (∑i ∈ {..< n}. f i))"
  have ginf: "∀ j ≥ Suc i. g j = -∞"
  proof (intro allI impI)
    fix j
    assume "Suc i ≤ j"
    hence "i < j" by simp
    hence "i ∈ {..< j}" by auto
    thus "g j = -∞" unfolding g_def using sum_Minfty[of  "{..< j}"] assms by simp
  qed
  have "∀M. ∃N. ∀n≥ N. (g n) ≤ M" 
  proof
    fix M
    show "∃N. ∀n≥ N. g n ≤ M" using ginf by force
  qed
  hence "g ⇢ -∞" by (simp add: Lim_MInfty)
  thus ?thesis   unfolding sums_def g_def by simp
qed

lemma ereal_sums_not_infty:
  assumes "f sums (a::ereal)"
    and "¦a¦ ≠ ∞"
  shows "⋀n. ¦f n¦ ≠ ∞" 
proof (rule ccontr)
  fix n
  assume "¬¦f n¦ ≠ ∞"
  hence "¦f n¦ = ∞" by simp
  show False
  proof (cases "f n = ∞")
    case True
    hence "f sums ∞" using mem_sums_Pinfty by simp
    thus False using assms sums_unique2 by force
  next
    case False
    hence "f n = -∞" using ‹¦f n¦ = ∞› by blast
    show False
    proof (cases "∃i. f i = ∞")
      case True
      from this obtain i where "f i = ∞" by auto
      hence "f sums ∞" using mem_sums_Pinfty by simp
      thus False using assms sums_unique2 by force
    next
      case False
      hence "∀i. f i ≠ ∞" by simp
      hence "f sums -∞" using mem_sums_Minfty ‹f n = -∞›
        by (metis MInfty_eq_minfinity image_iff)
      thus False using assms sums_unique2 by force
    qed
  qed
qed

lemma ereal_sums_not_infty_minus:
  assumes "f sums (a::ereal)"
    and "¦a¦ ≠ ∞"
  shows "(λn. - f n) sums -a" 
proof -
  have "⋀n. ¦f n¦ ≠ ∞" using assms  ereal_sums_not_infty by simp
  define g where "g = (λn. real_of_ereal (f n))"
  have "⋀n. f n = ereal (g n)" using  ‹⋀n. ¦f n¦ ≠ ∞› by (simp add: ereal_real' g_def) 
  hence "⋀n. - f n = ereal (-g n)" by simp
  have "∃r. a = ereal (r)" using assms by auto
  from this obtain r where "a = ereal r" by auto
  hence "f sums (ereal r)" using assms by simp
  hence "(λn. ereal (g n)) sums (ereal r)" using ‹⋀n. f n = ereal (g n)› 
      sums_cong[of f "λn. ereal (g n)"] by simp
  hence "g sums r" by (simp add: sums_ereal) 
  hence "(λn. -g n) sums -r" using sums_minus[of g] by simp
  hence "(λn. ereal (- g n)) sums ereal (-r)" by (simp add: sums_ereal) 
  hence "(λn. - f n) sums (ereal (-r))" using ‹⋀n. - f n = ereal (-g n)›
      sums_cong[of f "λn. ereal (g n)"] by simp
  thus ?thesis using ‹a = ereal r› by simp
qed

lemma ereal_sums_minus:
  fixes f::"nat ⇒ ereal"
  assumes "f sums a"
    and "⋀n. ¦f n¦ ≠ ∞"
  shows "(λn. - f n) sums -a" 
proof (cases "¦a¦ = ∞")
  case False
  thus ?thesis using assms ereal_sums_not_infty_minus by simp
next
  case True
  hence "a = ∞ ∨ a = - ∞" by auto
  thus ?thesis using assms ereal_sums_Pinfty ereal_sums_Minfty by auto
qed

lemma sums_minus':
  fixes f::"nat ⇒ ereal"
  assumes "-∞ ∉ range f ∨ ∞ ∉ range f"
    and "f sums a"
  shows "(λn. - f n) sums (- a)"
proof (cases "∀n. ¦f n¦ ≠ ∞")
  case True
  thus ?thesis using ereal_sums_minus assms by simp
next
  case False
  have "∃n. ¦f n¦ = ∞" using False by simp
  from this obtain n where "¦f n¦ = ∞" by meson
  show ?thesis
  proof (cases "∞ ∈ range f")
    case True
    hence "∃j. f j = ∞" by (metis image_iff) 
    from this obtain j where "f j = ∞" by auto
    hence "a = ∞" using mem_sums_Pinfty assms(2) sums_unique2 by blast
    moreover have "-∞ ∉ range f" using assms True by simp
    ultimately show ?thesis using mem_sums_Minfty[of "λn. - f n"] assms ‹f j = ∞›
      using ereal_uminus_eq_reorder by fastforce
  next
    case False
    hence "f n = -∞" using ‹¦f n¦ = ∞› by (metis ereal_infinity_cases range_eqI) 
    hence "a = -∞" using mem_sums_Minfty False sums_unique2 assms(2) by blast 
    thus ?thesis using mem_sums_Pinfty[of "λn. - f n"] assms
      by (metis MInfty_eq_minfinity ‹f n = - ∞› ereal_uminus_uminus uminus_ereal.simps(3))
  qed
qed

end