# Theory Hahn_Jordan_Prelims

```theory Hahn_Jordan_Prelims imports
"HOL-Analysis.Analysis"
Extended_Reals_Sums_Compl
begin

section ‹Preliminary results›

lemma diff_union:
shows "A - (⋃ i ≤ n. B i) - B (Suc n) = A - (⋃ i ≤ (Suc n). B i)"
using atMost_Suc by auto

lemma disj_subsets:
assumes "B 0 = A 0"
and "⋀(i::nat). B (Suc i) = A (Suc i) - (⋃ j∈{..i}. A j)"
shows "(⋃i. B i) = (⋃i. A i)"
proof
have "B i ⊆ A i" for i
proof (cases "i = 0")
case True
thus ?thesis using assms by simp
next
case False
hence "∃j. i = Suc j" by (simp add: not0_implies_Suc)
from this obtain j where "i = Suc j" by auto
thus "B i ⊆ A i" using assms by auto
qed
thus "⋃ (range B) ⊆ ⋃ (range A)" by auto
next
have ale: "⋀n. A (Suc n) ⊆ B (Suc n) ∪ (⋃ j∈{0..n}. A j)" using assms by auto
have inc: "⋀n. (⋃ i∈ {0..n}. A i) ⊆ (⋃ i ∈ {0..n}. B i)"
proof -
fix n
show "(⋃ i∈ {0..n}. A i) ⊆ (⋃ i ∈ {0..n}. B i)"
proof (induct n)
case 0
then show ?case using assms by auto
next
case (Suc n)
have "⋃ (A ` {0..Suc n}) = (⋃ (A ` {0.. n})) ∪ A (Suc n)"
by (simp add: Un_commute atLeast0_atMost_Suc)
also have "... ⊆ (⋃ (B ` {0.. n})) ∪ A (Suc n)" using Suc by auto
also have "... ⊆ (⋃ (B ` {0.. n})) ∪ B (Suc n) ∪ (⋃ j∈{0..n}. A j)" using ale by auto
also have "... ⊆ (⋃ (B ` {0.. n})) ∪ B (Suc n) ∪ (⋃ (B ` {0.. n}))" using Suc by auto
also have "... = (⋃ (B ` {0.. n})) ∪ B (Suc n)" by auto
also have "... = (⋃ (B ` {0.. Suc n}))" by (simp add: Un_commute atLeast0_atMost_Suc)
finally show ?case .
qed
qed
have "⋀n. (⋃ i∈ {0..<n}. A i) ⊆ (⋃ i ∈ {0..<n}. B i)"
proof -
fix n
show "(⋃ i∈ {0..<n}. A i) ⊆ (⋃ i ∈ {0..<n}. B i)"
proof (cases "n = 0")
case True
hence "{0..<n} = {}" by simp
thus ?thesis by simp
next
case False
hence "∃m. n = Suc m" by (simp add: not0_implies_Suc)
from this obtain m where "n = Suc m" by auto
hence "{0..<n} = {0..m}" by auto
have "(⋃ i∈ {0..m}. A i) ⊆ (⋃ i ∈ {0..m}. B i)" using inc by simp
thus ?thesis using ‹{0..<n} = {0..m}› by simp
qed
qed
thus "⋃ (range A) ⊆ ⋃ (range B)" using UN_finite2_subset[of A B 0] by simp
qed

lemma disj_Union2:
assumes "⋀i. A i ∈ sets M"
obtains B where "disjoint_family B" and "(⋃(i::nat). B i) = (⋃(i::nat). A i)"
and "⋀i. B i ∈ sets M" and "⋀i. B i ⊆ A i"
proof
define B where "B = (λ(i::nat). A i - (⋃ j∈{..<i}. A j))"
show "⋀i. B i ⊆ A i"
proof -
fix i
show "B i ⊆ A i"
proof (cases "i = 0")
case True
thus ?thesis unfolding B_def by simp
next
case False
hence "∃j. i = Suc j" by (simp add: not0_implies_Suc)
from this obtain j where "i = Suc j" by auto
thus "B i ⊆ A i" unfolding B_def by auto
qed
qed
show "disjoint_family B" unfolding disjoint_family_on_def
proof -
{
fix n m::nat
assume "n <m"
hence "B n ⊆ (⋃ j∈{..<m}. A j)" using ‹⋀i. B i ⊆ A i› by auto
hence "B n ∩ B m = {}" unfolding B_def by auto
}
thus "∀m∈UNIV. ∀n∈UNIV. m ≠ n ⟶ B m ∩ B n = {}" by (metis Int_commute antisym_conv3)
qed
show "(⋃(i::nat). B i) = (⋃(i::nat). A i)"
proof (rule disj_subsets)
show "B 0 = A 0" unfolding B_def by simp
show "⋀i. B (Suc i) = A (Suc i) - ⋃ (A ` {..i})" unfolding B_def by auto
qed
show "⋀i. B i ∈ sets M" unfolding B_def using assms by auto
qed

lemma conv_0_half:
assumes "f ⇢ (0::real)"
and "⋀n. 0 ≤ f n"
shows "∃N. ∀n ≥ N. f n < 1/2"
proof -
have "∀r>0. ∃no. ∀n≥no. dist (f n) 0 < r" using assms by (simp add: lim_sequentially)
hence "∃no. ∀n≥ no. dist (f n) 0 < 1/2" using half_gt_zero_iff zero_less_one by blast
from this obtain N where "∀n ≥ N. dist (f n) 0 < 1/2" by auto
have "⋀n. dist (f n) 0 = f n" using assms
proof -
fix n
have "dist (f n) 0 = ¦f n¦" by simp
also have "... = f n" using assms by simp
finally show "dist (f n) 0 = f n" .
qed
hence "∀n ≥ N. f n < 1/2" using ‹∀n ≥ N. dist (f n) 0 < 1/2› by simp
thus ?thesis by auto
qed

fixes x::ereal
assumes "0 ≤ x"
and "0 ≤ y"
shows "e2ennreal (x+y) = e2ennreal x + e2ennreal y"
proof (rule ereal_ennreal_cases[of x])
show "x < 0 ⟹ e2ennreal (x + y) = e2ennreal x + e2ennreal y" using assms by simp
show "⋀b. 0 ≤ x ⟹ x = enn2ereal b ⟹ e2ennreal (x + y) = e2ennreal x + e2ennreal y"
proof -
fix b
assume "0 ≤ x" and "x = enn2ereal b"
hence "e2ennreal x= b" by simp
show "e2ennreal (x + y) = e2ennreal x + e2ennreal y"
proof (rule ereal_ennreal_cases[of y])
show "y < 0 ⟹ e2ennreal (x + y) = e2ennreal x + e2ennreal y" using assms by simp
show "⋀b. 0 ≤ y ⟹ y = enn2ereal b ⟹ e2ennreal (x + y) = e2ennreal x + e2ennreal y"
proof -
fix c
assume "0 ≤ y" and "y = enn2ereal c"
hence "e2ennreal y = c" by simp
show "e2ennreal (x + y) = e2ennreal x + e2ennreal y"
proof (rule ereal_ennreal_cases[of "x+y"])
show "x + y < 0 ⟹ e2ennreal (x + y) = e2ennreal x + e2ennreal y" using assms
by (simp add: leD)
show "⋀b. 0 ≤ x + y ⟹ x + y = enn2ereal b ⟹ e2ennreal (x + y) =
e2ennreal x + e2ennreal y"
proof -
fix d
assume "0 ≤ x+y" and "x+y = enn2ereal d"
hence "e2ennreal (x+y) = d" by simp
show "e2ennreal (x + y) = e2ennreal x + e2ennreal y"
using ‹e2ennreal (x+y) = d› ‹e2ennreal x= b› ‹e2ennreal y= c›
by (metis ‹x = enn2ereal b› ‹y = enn2ereal c› e2ennreal_enn2ereal plus_ennreal.rep_eq)
qed
qed
qed
qed
qed
qed

lemma e2ennreal_finite_sum:
shows "finite I ⟹ (⋀i. i∈ I ⟹ 0 ≤ ((A i)::ereal)) ⟹
(∑ i∈ I. e2ennreal (A i)) = e2ennreal (∑i∈ I. A i)"
proof (induct rule: finite_induct)
case empty
then show ?case by (simp add: zero_ennreal.abs_eq)
next
case (insert x F)
hence "(∑ i∈ (insert x F). e2ennreal (A i)) = e2ennreal (A x) + (∑ i∈ F. e2ennreal (A i))"
by simp
also have "... = e2ennreal (A x) + e2ennreal (∑i∈ F. A i)" using insert by simp
also have "... = e2ennreal (A x + (∑i∈ F. A i))"
show "0 ≤ A x" using insert by simp
show "0 ≤ sum A F" using insert by (simp add: sum_nonneg)
qed
also have "... = e2ennreal (∑i∈ insert x F. A i)" using insert by simp
finally show ?case .
qed

lemma e2ennreal_less_top:
fixes x::ereal
assumes "x < ∞"
shows "e2ennreal x < ∞"
proof (rule ereal_ennreal_cases[of x])
assume "x < 0"
hence "e2ennreal x = 0" using e2ennreal_neg by simp
thus "e2ennreal x < ∞" by simp
next
fix b
assume "0 ≤  x" and "x = enn2ereal b"
hence "b = e2ennreal x" by simp
have "b < ∞"
proof (rule ccontr)
assume "¬ b < ∞"
hence "b = ∞" by (simp add: less_ennreal.rep_eq)
hence "x = ∞" using enn2ereal_eq_top_iff ‹x = enn2ereal b› by simp
thus False using assms by simp
qed
thus "e2ennreal x < ∞" using ‹b = e2ennreal x› by simp
qed

assumes "measure_space (space M) (sets M) (λx. e2ennreal (m1 x))"
and "∀x∈ sets M. 0 ≤ m1 x"
shows "additive (sets M) m1"
fix A B
assume "A∈ sets M" and "B∈ sets M" and "A∩ B = {}" note abprops = this
define M1 where "M1 = (λx. e2ennreal (m1 x))"
sets.ring_of_sets_axioms assms unfolding measure_space_def M1_def by auto
have "A∪B ∈ sets M" using abprops by simp
hence "m1 (A∪ B) = enn2ereal (M1 (A∪ B))" unfolding M1_def using assms enn2ereal_e2ennreal
abprops by presburger
also have "... = enn2ereal (M1 A + M1 B)" using ‹additive (sets M) M1› abprops
unfolding additive_def by simp
also have "... = enn2ereal (M1 A) + enn2ereal (M1 B)" by (simp add: plus_ennreal.rep_eq)
also have "... = m1 A + m1 B" unfolding M1_def using assms enn2ereal_e2ennreal
abprops by presburger
finally show "m1 (A∪ B) = m1 A + m1 B" .
qed

subsection ‹Some summability properties›

lemma shift_denum:
shows "1/(x i - (1::nat)) ≤ 2/x i"
proof (cases "x i ≤ 1")
case True
hence "x i - 1 = 0" by simp
thus ?thesis by simp
next
case False
hence "2 ≤ x i" by simp
hence "0 < x i * (x i - 1)" by simp
hence "0 ≤ (2 * (x i - 1) - x i)/(x i * (x i - 1))" using ‹2 ≤ x i› by simp
also have "... = (real (2 * (x i - 1)) - real (x i))/(x i * (x i - 1))"
using of_nat_diff by auto
also have "... = (2 * (x i - 1))/(x i * (x i - 1)) - x i/(x i * (x i - 1))"
using diff_divide_distrib[of "2 * (x i - 1)" "x i" "x i * (x i - 1)"] by simp
also have "... = 2/x i - x i/(x i * (x i - 1))"  using ‹2 ≤ x i› by auto
also have "... = 2/x i - 1/(x i - 1)" by simp
finally have "0 ≤ 2/x i - 1/(x i - 1)" .
thus ?thesis by simp
qed

lemma shift_denum':
assumes "⋀i. k ≤ x i ⟹ k +e  ≤ ((x i)::nat)"
and "⋀i. 0 < x i"
and "⋀i. x i < p"
and "0 < e"
shows "∃c. ∀i. 1/(x i - k) ≤ c/(x i)"
proof
have "⋀i. k ≤ x i ⟹ e ≤ x i - k"
proof -
fix i
assume "k ≤ x i"
hence "k + e ≤ x i" using assms by simp
thus "e ≤ x i - k" using assms by simp
qed
have "⋀i. k ≤ x i ⟹ 0 < (x i)*(x i - k)"
proof -
fix i
assume "k ≤ x i"
thus "0 < (x i)*(x i - k)" using assms by force
qed
define cw where "cw = p/e"
have "0 < p" using assms  using neq0_conv by blast
hence "0 < cw" unfolding cw_def by (simp add: assms(4))
show "∀i. 1 / (x i - k) ≤ cw / x i"
proof
fix i
show "1 / (x i - k) ≤ cw / x i"
proof (cases "k ≤ x i")
case True
hence "0 ≤ (p - x i)/((x i) * (x i - k))" using ‹⋀i. k ≤ x i ⟹0 < x i * (x i - k)› assms(3)
divide_nonneg_pos[of "p - x i" "x i * (x i - k)"] by (simp add: less_eq_real_def)
also have "... = (cw * e - x i)/((x i) * (x i - k))" unfolding cw_def using assms True
by (metis divide_less_cancel division_ring_divide_zero eq_divide_imp nat_less_le
of_nat_0_less_iff of_nat_diff times_divide_eq_left)
also have "... ≤ (cw * (x i - k) - x i)/((x i) * (x i - k))"
proof -
have "cw * (x i - k) - x i ≥ cw * e - x i" using ‹k ≤ x i ⟹ e ≤ x i - k› ‹0 < cw› True
by simp
thus ?thesis using ‹k ≤ x i ⟹ 0 < (x i)*(x i - k)›
divide_right_mono[of "cw * e - x i" "cw * (x i - k) - x i" "(x i) * (x i - k)"] by simp
qed
also have "... = (cw * (x i -k))/((x i)*(x i - k)) - x i/((x i) * (x i - k))"
using assms diff_divide_distrib by blast
also have "... = cw / x i - 1/(x i-k)"
proof -
have "1/(x i-k) = x i/((x i) * (x i - k))" using assms(2) less_imp_neq by fastforce
thus ?thesis using ‹⋀i. k ≤ x i ⟹ 0 < x i * (x i - k)› assms(2) zero_less_mult_pos
proof -
have f1: "∀r ra. (1::real) / (ra / r) = r / ra"
by simp
have "real (x i * (x i - k)) ≠ 0"
by (metis True  ‹⋀i. k ≤ x i ⟹ 0 < x i * (x i - k)› neq0_conv of_nat_0 of_nat_le_0_iff)
thus ?thesis using f1 by (metis ‹1 / real (x i - k) = real (x i) / real (x i * (x i - k))›
div_by_1 divide_divide_eq_right nonzero_mult_div_cancel_left)
qed
qed
finally have "0 ≤ cw / x i - 1/(x i-k)" .
thus "1 / (x i - k) ≤ cw / x i" by simp
next
case False
hence "real (x i - k) = 0" by simp
hence "1/ real (x i - k) = 0" by simp
thus "1 / real (x i - k) ≤ cw / real (x i)" by (simp add: cw_def)
qed
qed
qed

lemma sum_le:
assumes "⋀i. f i ≤ ((g i) :: real)"
shows "sum f {.. (n::nat)} ≤ sum g {.. n}"
proof (induct n)
case 0
then show ?case using assms by simp
next
case (Suc n)
have "sum f {..Suc n} = sum f {.. n} + f (Suc n)" by simp
also have "... ≤ sum g {.. n} + f (Suc n)" using Suc by simp
also have "... ≤ sum g {.. n} + g (Suc n)" using assms by simp
also have "... = sum g {.. Suc n}" by simp
finally show ?case .
qed

lemma summable_bounded:
assumes "⋀i. 0 ≤ ((f i)::real)"
and "⋀i. f i ≤ g i"
and "summable g"
shows "summable f"
proof (rule bounded_imp_summable, (auto simp add: assms))
fix n
have "⋀i. 0 ≤ g i" using assms dual_order.trans by blast
have "sum f {.. n} ≤ sum g {.. n}" using assms sum_le by simp
also have "... ≤ suminf g" by (rule sum_le_suminf, (auto simp add: assms ‹⋀i. 0 ≤ g i›))
finally show "sum f {.. n} ≤ suminf g" .
qed

lemma sum_shift_denum:
assumes "summable (λi. 1/((f i)::nat))"
shows "summable (λi. 1/(f i - 1))"
proof -
have "∀i. 1/(f i - 1) ≤ 2 / f i" using shift_denum[of f] by auto
have "summable (λi. 2/ f i)" using assms summable_mult[of "λn. 1/ f n"] by simp
thus ?thesis using summable_bounded[of "λi. 1/(f i - 1)" "λi. 2 * 1/f i"]
‹∀i. 1 / real (f i - 1) ≤ 2 / real (f i)› by auto
qed

lemma sum_shift_denum':
assumes "summable (λi. 1/(f i))"
and "0 < e"
and "⋀i. k ≤ f i ⟹ k + e ≤ ((f i)::nat)"
and "⋀i. 0 < f i"
and "⋀i. f i < p"
shows "summable (λi. 1/(f i - k))"
proof -
have "⋀i. 0 ≤ 1/(f i - k)"
proof -
fix i
have "0 ≤ f i - k" using assms by simp
thus "0 ≤ 1/(f i - k)" by simp
qed
have "∃c. ∀i. 1/(f i - k) ≤ c / f i" using shift_denum'[of k f e p] assms by simp
from this obtain c where "∀i. 1/(f i - k) ≤ c / f i" by auto
have "summable (λi. c * 1/ f i)" using assms summable_mult[of "λn. 1/ f n"] by simp
thus ?thesis using summable_bounded[of "λi. 1/(f i - k)" "λi. c * 1/f i"]
‹⋀i. 0 ≤ 1/(f i - k)› by (simp add: ‹∀i. 1 / (f i - k) ≤ c / f i›)
qed

end```