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 "mUNIV. nUNIV. 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. nno. 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 "AB  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