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

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