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 lemma e2ennreal_add: 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))" proof (rule e2ennreal_add[symmetric]) 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 lemma pos_e2ennreal_additive: assumes "measure_space (space M) (sets M) (λx. e2ennreal (m1 x))" and "∀x∈ sets M. 0 ≤ m1 x" shows "additive (sets M) m1" proof (auto simp add: additive_def) 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))" have "additive (sets M) M1" using ring_of_sets.countably_additive_additive 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