# 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```