Theory Zeta_Library

section ‹Various preliminary material›
theory Zeta_Library
imports
  "HOL-Complex_Analysis.Complex_Analysis"
  "HOL-Real_Asymp.Real_Asymp"
  "Dirichlet_Series.Dirichlet_Series_Analysis"
begin

subsection ‹Facts about limits›

lemma at_within_altdef:
  "at x within A = (INF S{S. open S  x  S}. principal (S  (A - {x})))"
  unfolding at_within_def nhds_def inf_principal [symmetric]
    by (subst INF_inf_distrib [symmetric]) (auto simp: INF_constant)

lemma tendsto_at_left_realI_sequentially:
  fixes f :: "real  'b::first_countable_topology"
  assumes *: "X. filterlim X (at_left c) sequentially  (λn. f (X n))  y"
  shows "(f  y) (at_left c)"
proof -
  obtain A where A: "decseq A" "open (A n)" "y  A n" "nhds y = (INF n. principal (A n))" for n
    by (rule nhds_countable[of y]) (rule that)

  have "m. d<c. x{d<..<c}. f x  A m"
  proof (rule ccontr)
    assume "¬ (m. d<c. x{d<..<c}. f x  A m)"
    then obtain m where **: "d. d < c  x{d<..<c}. f x  A m"
      by auto
    have "X. n. (f (X n)  A m  X n < c)  X (Suc n) > c - max 0 ((c - X n) / 2)"
    proof (intro dependent_nat_choice, goal_cases)
      case 1
      from **[of "c - 1"] show ?case by auto
    next
      case (2 x n)
      with **[of "c - max 0 (c - x) / 2"] show ?case by force
    qed
    then obtain X where X: "n. f (X n)  A m" "n. X n < c" "n. X (Suc n) > c - max 0 ((c - X n) / 2)"
      by auto (metis diff_gt_0_iff_gt half_gt_zero_iff max.absorb3 max.commute)
    have X_ge: "X n  c - (c - X 0) / 2 ^ n" for n
    proof (induction n)
      case (Suc n)
      have "c - (c - X 0) / 2 ^ Suc n = c - (c - (c - (c - X 0) / 2 ^ n)) / 2"
        by simp
      also have "c - (c - (c - (c - X 0) / 2 ^ n)) / 2  c - (c - X n) / 2"
        by (intro diff_left_mono divide_right_mono Suc diff_right_mono) auto
      also have " = c - max 0 ((c - X n) / 2)"
        using X[of n] by (simp add: max_def)
      also have " < X (Suc n)"
        using X[of n] by simp
      finally show ?case by linarith
    qed auto

    have "X  c"
    proof (rule tendsto_sandwich)
      show "eventually (λn. X n  c) sequentially"
        using X by (intro always_eventually) (auto intro!: less_imp_le)
      show "eventually (λn. X n  c - (c - X 0) / 2 ^ n) sequentially"
        using X_ge by (intro always_eventually) auto
    qed real_asymp+
    hence "filterlim X (at_left c) sequentially"
      by (rule tendsto_imp_filterlim_at_left)
         (use X in auto intro!: always_eventually less_imp_le)
    from topological_tendstoD[OF *[OF this] A(2, 3), of m] X(1) show False
      by auto
  qed

  then obtain d where d: "d m < c" "x  {d m<..<c}  f x  A m" for m x
    by metis
  have ***: "at_left c = (INF S{S. open S  c  S}. principal (S  {..<c}))"
    by (simp add: at_within_altdef)
  from d show ?thesis
    unfolding *** A using A(1,2) by (intro filterlim_base[of _ "λm. {d m<..}"]) auto
qed

lemma
  shows at_right_PInf [simp]: "at_right ( :: ereal) = bot"
    and at_left_MInf [simp]: "at_left (- :: ereal) = bot"
proof -
  have "{(::ereal)<..} = {}" "{..<-(::ereal)} = {}"
    by auto
  thus "at_right ( :: ereal) = bot" "at_left (- :: ereal) = bot"
    by (simp_all add: at_within_def)
qed

lemma tendsto_at_left_erealI_sequentially:
  fixes f :: "ereal  'b::first_countable_topology"
  assumes *: "X. filterlim X (at_left c) sequentially  (λn. f (X n))  y"
  shows "(f  y) (at_left c)"
proof (cases c)
  case [simp]: PInf
  have "((λx. f (ereal x))  y) at_top" using assms
    by (intro tendsto_at_topI_sequentially assms)
       (simp_all flip: ereal_tendsto_simps add: o_def filterlim_at)
  thus ?thesis
    by (simp add: at_left_PInf filterlim_filtermap)
next
  case [simp]: MInf
  thus ?thesis by auto
next
  case [simp]: (real c')
  have "((λx. f (ereal x))  y) (at_left c')"
  proof (intro tendsto_at_left_realI_sequentially assms)
    fix X assume *: "filterlim X (at_left c') sequentially"
    show "filterlim (λn. ereal (X n)) (at_left c) sequentially"
      by (rule filterlim_compose[OF _ *])
         (simp add: sequentially_imp_eventually_within tendsto_imp_filterlim_at_left)
  qed
  thus ?thesis
    by (simp add: at_left_ereal filterlim_filtermap)
qed

lemma tendsto_at_right_realI_sequentially:
  fixes f :: "real  'b::first_countable_topology"
  assumes *: "X. filterlim X (at_right c) sequentially  (λn. f (X n))  y"
  shows "(f  y) (at_right c)"
proof -
  obtain A where A: "decseq A" "open (A n)" "y  A n" "nhds y = (INF n. principal (A n))" for n
    by (rule nhds_countable[of y]) (rule that)

  have "m. d>c. x{c<..<d}. f x  A m"
  proof (rule ccontr)
    assume "¬ (m. d>c. x{c<..<d}. f x  A m)"
    then obtain m where **: "d. d > c  x{c<..<d}. f x  A m"
      by auto
    have "X. n. (f (X n)  A m  X n > c)  X (Suc n) < c + max 0 ((X n - c) / 2)"
    proof (intro dependent_nat_choice, goal_cases)
      case 1
      from **[of "c + 1"] show ?case by auto
    next
      case (2 x n)
      with **[of "c + max 0 (x - c) / 2"] show ?case by force
    qed
    then obtain X where X: "n. f (X n)  A m" "n. X n > c" "n. X (Suc n) < c + max 0 ((X n - c) / 2)"
      by auto (metis add.left_neutral half_gt_zero_iff less_diff_eq max.absorb4) 
    have X_le: "X n  c + (X 0 - c) / 2 ^ n" for n
    proof (induction n)
      case (Suc n)
      have "X (Suc n) < c + max 0 ((X n - c) / 2)"
        by (intro X) 
      also have " = c + (X n - c) / 2"
        using X[of n] by (simp add: field_simps max_def)
      also have "  c + (c + (X 0 - c) / 2 ^ n - c) / 2"
        by (intro add_left_mono divide_right_mono Suc diff_right_mono) auto
      also have " = c + (X 0 - c) / 2 ^ Suc n"
        by simp
      finally show ?case by linarith
    qed auto

    have "X  c"
    proof (rule tendsto_sandwich)
      show "eventually (λn. X n  c) sequentially"
        using X by (intro always_eventually) (auto intro!: less_imp_le)
      show "eventually (λn. X n  c + (X 0 - c) / 2 ^ n) sequentially"
        using X_le by (intro always_eventually) auto
    qed real_asymp+
    hence "filterlim X (at_right c) sequentially"
      by (rule tendsto_imp_filterlim_at_right)
         (use X in auto intro!: always_eventually less_imp_le)
    from topological_tendstoD[OF *[OF this] A(2, 3), of m] X(1) show False
      by auto
  qed

  then obtain d where d: "d m > c" "x  {c<..<d m}  f x  A m" for m x
    by metis
  have ***: "at_right c = (INF S{S. open S  c  S}. principal (S  {c<..}))"
    by (simp add: at_within_altdef)
  from d show ?thesis
    unfolding *** A using A(1,2) by (intro filterlim_base[of _ "λm. {..<d m}"]) auto
qed

lemma tendsto_at_right_erealI_sequentially:
  fixes f :: "ereal  'b::first_countable_topology"
  assumes *: "X. filterlim X (at_right c) sequentially  (λn. f (X n))  y"
  shows "(f  y) (at_right c)"
proof (cases c)
  case [simp]: MInf
  have "((λx. f (-ereal x))  y) at_top" using assms
   by (intro tendsto_at_topI_sequentially assms)
      (simp_all flip: uminus_ereal.simps ereal_tendsto_simps add: o_def filterlim_at)
  thus ?thesis
    by (simp add: at_right_MInf filterlim_filtermap at_top_mirror)
next
  case [simp]: PInf
  thus ?thesis by auto
next
  case [simp]: (real c')
  have "((λx. f (ereal x))  y) (at_right c')"
  proof (intro tendsto_at_right_realI_sequentially assms)
    fix X assume *: "filterlim X (at_right c') sequentially"
    show "filterlim (λn. ereal (X n)) (at_right c) sequentially"
      by (rule filterlim_compose[OF _ *])
         (simp add: sequentially_imp_eventually_within tendsto_imp_filterlim_at_right)
  qed
  thus ?thesis
    by (simp add: at_right_ereal filterlim_filtermap)
qed

proposition analytic_continuation':
  assumes hol: "f holomorphic_on S" "g holomorphic_on S"
      and "open S" and "connected S"
      and "U  S" and "ξ  S"
      and "ξ islimpt U"
      and fU0 [simp]: "z. z  U  f z = g z"
      and "w  S"
    shows "f w = g w"
  using analytic_continuation[OF holomorphic_on_diff[OF hol] assms(3-7) _ assms(9)] assms(8)
  by simp


subsection ‹Various facts about integrals›

lemma continuous_on_imp_set_integrable_cbox:
  fixes h :: "'a :: euclidean_space  'b :: euclidean_space"
  assumes "continuous_on (cbox a b) h"
  shows   "set_integrable lborel (cbox a b) h"
  by (simp add: assms borel_integrable_compact set_integrable_def)


subsection ‹Uniform convergence of integrals›

lemma has_absolute_integral_change_of_variables_1':
  fixes f :: "real  real" and g :: "real  real"
  assumes S: "S  sets lebesgue"
    and der_g: "x. x  S  (g has_field_derivative g' x) (at x within S)"
    and inj: "inj_on g S"
  shows "(λx. ¦g' x¦ *R f(g x)) absolutely_integrable_on S 
           integral S (λx. ¦g' x¦ *R f(g x)) = b
      f absolutely_integrable_on (g ` S)  integral (g ` S) f = b"
proof -
  have "(λx. ¦g' x¦ *R vec (f(g x)) :: real ^ 1) absolutely_integrable_on S 
           integral S (λx. ¦g' x¦ *R vec (f(g x))) = (vec b :: real ^ 1)
          (λx. vec (f x) :: real ^ 1) absolutely_integrable_on (g ` S) 
           integral (g ` S) (λx. vec (f x)) = (vec b :: real ^ 1)"
    using assms unfolding has_real_derivative_iff_has_vector_derivative
    by (intro has_absolute_integral_change_of_variables_1 assms) auto
  thus ?thesis
    by (simp add: absolutely_integrable_on_1_iff integral_on_1_eq)
qed

lemma uniform_limit_set_lebesgue_integral:
  fixes f :: "'a  'b :: euclidean_space  'c :: {banach, second_countable_topology}"
  assumes "set_integrable lborel X' g"
  assumes [measurable]: "X'  sets borel"
  assumes [measurable]: "y. y  Y  set_borel_measurable borel X' (f y)"
  assumes "y. y  Y  (AE tX' in lborel. norm (f y t)  g t)"
  assumes "eventually (λx. X x  sets borel  X x  X') F"
  assumes "filterlim (λx. set_lebesgue_integral lborel (X x) g)
             (nhds (set_lebesgue_integral lborel X' g)) F"
  shows "uniform_limit Y
           (λx y. set_lebesgue_integral lborel (X x) (f y))
           (λy. set_lebesgue_integral lborel X' (f y)) F"
proof (rule uniform_limitI, goal_cases)
  case (1 ε)
  have integrable_g: "set_integrable lborel U g"
    if "U  sets borel" "U  X'" for U
    by (rule set_integrable_subset[OF assms(1)]) (use that in auto)
  have "eventually (λx. dist (set_lebesgue_integral lborel (X x) g)
                             (set_lebesgue_integral lborel X' g) < ε) F"
    using ε > 0 assms by (auto simp: tendsto_iff)
  from this show ?case using eventually (λ_. _  _) F
  proof eventually_elim
    case (elim x)
    hence [measurable]:"X x  sets borel" and "X x  X'" by auto
    have integrable: "set_integrable lborel U (f y)"
      if "y  Y" "U  sets borel" "U  X'" for y U
      apply (rule set_integrable_subset)
        apply (rule set_integrable_bound[OF assms(1)])
         apply (use assms(3) that in simp add: set_borel_measurable_def)
      using assms(4)[OF y  Y] apply eventually_elim apply force
      using that apply simp_all
      done
    show ?case
    proof
      fix y assume "y  Y"
      have "dist (set_lebesgue_integral lborel (X x) (f y))
                 (set_lebesgue_integral lborel X' (f y)) =
            norm (set_lebesgue_integral lborel X' (f y) -
                  set_lebesgue_integral lborel (X x) (f y))"
        by (simp add: dist_norm norm_minus_commute)
      also have "set_lebesgue_integral lborel X' (f y) -
                    set_lebesgue_integral lborel (X x) (f y) =
                 set_lebesgue_integral lborel (X' - X x) (f y)"
        unfolding set_lebesgue_integral_def
        apply (subst Bochner_Integration.integral_diff [symmetric])
        unfolding set_integrable_def [symmetric]
          apply (rule integrable; (fact | simp))
         apply (rule integrable; fact)
        apply (intro Bochner_Integration.integral_cong)
         apply (use X x  X' in auto simp: indicator_def)
        done
      also have "norm   (tX'-X x. norm (f y t) lborel)"
        by (intro set_integral_norm_bound integrable) (fact | simp)+
      also have "AE tX' - X x in lborel. norm (f y t)  g t"
        using assms(4)[OF y  Y] by eventually_elim auto
      with y  Y have "(tX'-X x. norm (f y t) lborel)  (tX'-X x. g t lborel)"
        by (intro set_integral_mono_AE set_integrable_norm integrable integrable_g) auto
      also have " = (tX'. g t lborel) - (tX x. g t lborel)"
        unfolding set_lebesgue_integral_def
        apply (subst Bochner_Integration.integral_diff [symmetric])
        unfolding set_integrable_def [symmetric]
          apply (rule integrable_g; (fact | simp))
         apply (rule integrable_g; fact)
        apply (intro Bochner_Integration.integral_cong)
         apply (use X x  X' in auto simp: indicator_def)
        done
      also have "  dist (tX x. g t lborel) (tX'. g t lborel)"
        by (simp add: dist_norm)
      also have " < ε" by fact
      finally show "dist (set_lebesgue_integral lborel (X x) (f y))
                         (set_lebesgue_integral lborel X' (f y)) < ε" .
    qed
  qed
qed

lemma integral_dominated_convergence_at_right:
  fixes s :: "real  'a  'b::{banach, second_countable_topology}" and w :: "'a  real"
    and f :: "'a  'b" and M and c :: real
  assumes "f  borel_measurable M" "t. s t  borel_measurable M" "integrable M w"
  assumes lim: "AE x in M. ((λi. s i x)  f x) (at_right c)"
  assumes bound: "F i in at_right c. AE x in M. norm (s i x)  w x"
  shows "((λt. integralL M (s t))  integralL M f) (at_right c)"
proof (rule tendsto_at_right_realI_sequentially)
  fix X :: "nat  real" assume X: "filterlim X (at_right c) sequentially"
  from filterlim_iff[THEN iffD1, OF this, rule_format, OF bound]
  obtain N where w: "n. N  n  AE x in M. norm (s (X n) x)  w x"
    by (auto simp: eventually_sequentially)

  show "(λn. integralL M (s (X n)))  integralL M f"
  proof (rule LIMSEQ_offset, rule integral_dominated_convergence)
    show "AE x in M. norm (s (X (n + N)) x)  w x" for n
      by (rule w) auto
    show "AE x in M. (λn. s (X (n + N)) x)  f x"
      using lim
    proof eventually_elim
      fix x assume "((λi. s i x)  f x) (at_right c)"
      then show "(λn. s (X (n + N)) x)  f x"
        by (intro LIMSEQ_ignore_initial_segment filterlim_compose[OF _ X])
    qed
  qed fact+
qed

lemma integral_dominated_convergence_at_left:
  fixes s :: "real  'a  'b::{banach, second_countable_topology}" and w :: "'a  real"
    and f :: "'a  'b" and M and c :: real
  assumes "f  borel_measurable M" "t. s t  borel_measurable M" "integrable M w"
  assumes lim: "AE x in M. ((λi. s i x)  f x) (at_left c)"
  assumes bound: "F i in at_left c. AE x in M. norm (s i x)  w x"
  shows "((λt. integralL M (s t))  integralL M f) (at_left c)"
proof (rule tendsto_at_left_realI_sequentially)
  fix X :: "nat  real" assume X: "filterlim X (at_left c) sequentially"
  from filterlim_iff[THEN iffD1, OF this, rule_format, OF bound]
  obtain N where w: "n. N  n  AE x in M. norm (s (X n) x)  w x"
    by (auto simp: eventually_sequentially)

  show "(λn. integralL M (s (X n)))  integralL M f"
  proof (rule LIMSEQ_offset, rule integral_dominated_convergence)
    show "AE x in M. norm (s (X (n + N)) x)  w x" for n
      by (rule w) auto
    show "AE x in M. (λn. s (X (n + N)) x)  f x"
      using lim
    proof eventually_elim
      fix x assume "((λi. s i x)  f x) (at_left c)"
      then show "(λn. s (X (n + N)) x)  f x"
        by (intro LIMSEQ_ignore_initial_segment filterlim_compose[OF _ X])
    qed
  qed fact+
qed

lemma uniform_limit_interval_integral_right:
  fixes f :: "'a  real  'c :: {banach, second_countable_topology}"
  assumes "interval_lebesgue_integrable lborel a b g"
  assumes [measurable]: "y. y  Y  set_borel_measurable borel (einterval a b) (f y)"
  assumes "y. y  Y  (AE teinterval a b in lborel. norm (f y t)  g t)"
  assumes "a < b"
  shows   "uniform_limit Y (λb' y. LBINT t=a..b'. f y t) (λy. LBINT t=a..b. f y t) (at_left b)"
proof (cases "Y = {}")
  case False
  have g_nonneg: "AE teinterval a b in lborel. g t  0"
  proof -
    from Y  {} obtain y where "y  Y" by auto
    from assms(3)[OF this] show ?thesis 
      by eventually_elim (auto elim: order.trans[rotated])
  qed

  have ev: "eventually (λb'. b'  {a<..<b}) (at_left b)"
    using a < b by (intro eventually_at_leftI)
  with a < b have "?thesis  uniform_limit Y (λb' y. teinterval a (min b b'). f y t lborel)
                                  (λy. teinterval a b. f y t lborel) (at_left b)"
    by (intro filterlim_cong arg_cong2[where f = uniformly_on])
       (auto simp: interval_lebesgue_integral_def fun_eq_iff min_def
             intro!: eventually_mono[OF ev])
  also have 
  proof (rule uniform_limit_set_lebesgue_integral[where g = g], goal_cases)
    show "F b' in at_left b. einterval a (min b b')  sets borel 
                              einterval a (min b b')  einterval a b"
      using ev by eventually_elim (auto simp: einterval_def)
  next
    show "((λb'. set_lebesgue_integral lborel (einterval a (min b b')) g) 
            set_lebesgue_integral lborel (einterval a b) g) (at_left b)"
      unfolding set_lebesgue_integral_def
    proof (intro tendsto_at_left_erealI_sequentially integral_dominated_convergence)
      have *: "set_borel_measurable borel (einterval a b) g"
        using assms(1) less_imp_le[OF a < b]
        by (simp add: interval_lebesgue_integrable_def set_integrable_def set_borel_measurable_def)
      show "(λx. indicat_real (einterval a b) x *R g x)  borel_measurable lborel"
        using * by (simp add: set_borel_measurable_def)
      fix X :: "nat  ereal" and n :: nat
      have "set_borel_measurable borel (einterval a (min b (X n))) g"
        by (rule set_borel_measurable_subset[OF *]) (auto simp: einterval_def)
      thus "(λx. indicat_real (einterval a (min b (X n))) x *R g x)  borel_measurable lborel"
        by (simp add: set_borel_measurable_def)
    next
      fix X :: "nat  ereal"
      assume X: "filterlim X (at_left b) sequentially"
      show "AE x in lborel. (λn. indicat_real (einterval a (min b (X n))) x *R g x)
                indicat_real (einterval a b) x *R g x"
      proof (rule AE_I2)
        fix x :: real
        have "(λt. indicator (einterval a (min b (X t))) x :: real) 
                indicator (einterval a b) x"
        proof (cases "x  einterval a b")
          case False
          hence "x  einterval a (min b (X t))"for t by (auto simp: einterval_def)
          with False show ?thesis by (simp add: indicator_def)
        next
          case True
          with a < b have "eventually (λt. t  {max a x<..<b}) (at_left b)"
            by (intro eventually_at_leftI[of "ereal x"]) (auto simp: einterval_def min_def)
          from this and X have "eventually (λt. X t  {max a x<..<b}) sequentially"
            by (rule eventually_compose_filterlim)
          hence "eventually (λt. indicator (einterval a (min b (X t))) x = (1 :: real)) sequentially"
            by eventually_elim (use True in auto simp: indicator_def einterval_def)
          from tendsto_eventually[OF this] and True show ?thesis
            by (simp add: indicator_def)
        qed
        thus "(λn. indicat_real (einterval a (min b (X n))) x *R g x)
                  indicat_real (einterval a b) x *R g x" by (intro tendsto_intros)
      qed
    next
      fix X :: "nat  ereal" and n :: nat
      show "AE x in lborel. norm (indicator (einterval a (min b (X n))) x *R g x) 
              indicator (einterval a b) x *R g x"
        using g_nonneg by eventually_elim (auto simp: indicator_def einterval_def)
    qed (use assms less_imp_le[OF a < b] in 
         auto simp: interval_lebesgue_integrable_def set_integrable_def) 
  qed (use assms in auto simp: interval_lebesgue_integrable_def)
  finally show ?thesis .
qed auto

lemma uniform_limit_interval_integral_left:
  fixes f :: "'a  real  'c :: {banach, second_countable_topology}"
  assumes "interval_lebesgue_integrable lborel a b g"
  assumes [measurable]: "y. y  Y  set_borel_measurable borel (einterval a b) (f y)"
  assumes "y. y  Y  (AE teinterval a b in lborel. norm (f y t)  g t)"
  assumes "a < b"
  shows   "uniform_limit Y (λa' y. LBINT t=a'..b. f y t) (λy. LBINT t=a..b. f y t) (at_right a)"
proof (cases "Y = {}")
  case False
  have g_nonneg: "AE teinterval a b in lborel. g t  0"
  proof -
    from Y  {} obtain y where "y  Y" by auto
    from assms(3)[OF this] show ?thesis 
      by eventually_elim (auto elim: order.trans[rotated])
  qed

  have ev: "eventually (λb'. b'  {a<..<b}) (at_right a)"
    using a < b by (intro eventually_at_rightI)
  with a < b have "?thesis  uniform_limit Y (λa' y. teinterval (max a a') b. f y t lborel)
                                  (λy. teinterval a b. f y t lborel) (at_right a)"
    by (intro filterlim_cong arg_cong2[where f = uniformly_on])
       (auto simp: interval_lebesgue_integral_def fun_eq_iff max_def
             intro!: eventually_mono[OF ev])
  also have 
  proof (rule uniform_limit_set_lebesgue_integral[where g = g], goal_cases)
    show "F a' in at_right a. einterval (max a a') b  sets borel 
                              einterval (max a a') b  einterval a b"
      using ev by eventually_elim (auto simp: einterval_def)
  next
    show "((λa'. set_lebesgue_integral lborel (einterval (max a a') b) g) 
            set_lebesgue_integral lborel (einterval a b) g) (at_right a)"
      unfolding set_lebesgue_integral_def
    proof (intro tendsto_at_right_erealI_sequentially integral_dominated_convergence)
      have *: "set_borel_measurable borel (einterval a b) g"
        using assms(1) less_imp_le[OF a < b]
        by (simp add: interval_lebesgue_integrable_def set_integrable_def set_borel_measurable_def)
      show "(λx. indicat_real (einterval a b) x *R g x)  borel_measurable lborel"
        using * by (simp add: set_borel_measurable_def)
      fix X :: "nat  ereal" and n :: nat
      have "set_borel_measurable borel (einterval (max a (X n)) b) g"
        by (rule set_borel_measurable_subset[OF *]) (auto simp: einterval_def)
      thus "(λx. indicat_real (einterval (max a (X n)) b) x *R g x)  borel_measurable lborel"
        by (simp add: set_borel_measurable_def)
    next
      fix X :: "nat  ereal"
      assume X: "filterlim X (at_right a) sequentially"
      show "AE x in lborel. (λn. indicat_real (einterval (max a (X n)) b) x *R g x)
                indicat_real (einterval a b) x *R g x"
      proof (rule AE_I2)
        fix x :: real
        have "(λt. indicator (einterval (max a (X t)) b) x :: real) 
                indicator (einterval a b) x"
        proof (cases "x  einterval a b")
          case False
          hence "x  einterval (max a (X t)) b"for t by (auto simp: einterval_def)
          with False show ?thesis by (simp add: indicator_def)
        next
          case True
          with a < b have "eventually (λt. t  {a<..<x}) (at_right a)"
            by (intro eventually_at_rightI[of _ "ereal x"]) (auto simp: einterval_def min_def)
          from this and X have "eventually (λt. X t  {a<..<x}) sequentially"
            by (rule eventually_compose_filterlim)
          hence "eventually (λt. indicator (einterval (max a (X t)) b) x = (1 :: real)) sequentially"
            by eventually_elim (use True in auto simp: indicator_def einterval_def)
          from tendsto_eventually[OF this] and True show ?thesis
            by (simp add: indicator_def)
        qed
        thus "(λn. indicat_real (einterval (max a (X n)) b) x *R g x)
                  indicat_real (einterval a b) x *R g x" by (intro tendsto_intros)
      qed
    next
      fix X :: "nat  ereal" and n :: nat
      show "AE x in lborel. norm (indicator (einterval (max a (X n)) b) x *R g x) 
              indicator (einterval a b) x *R g x"
        using g_nonneg by eventually_elim (auto simp: indicator_def einterval_def)
    qed (use assms less_imp_le[OF a < b] in 
         auto simp: interval_lebesgue_integrable_def set_integrable_def) 
  qed (use assms in auto simp: interval_lebesgue_integrable_def)
  finally show ?thesis .
qed auto

lemma uniform_limit_interval_integral_sequentially:
  fixes f :: "'a  real  'c :: {banach, second_countable_topology}"
  assumes "interval_lebesgue_integrable lborel a b g"
  assumes [measurable]: "y. y  Y  set_borel_measurable borel (einterval a b) (f y)"
  assumes "y. y  Y  (AE teinterval a b in lborel. norm (f y t)  g t)"
  assumes a': "filterlim a' (at_right a) sequentially"
  assumes b': "filterlim b' (at_left b) sequentially"
  assumes "a < b"
  shows   "uniform_limit Y (λn y. LBINT t=a' n..b' n. f y t)
             (λy. LBINT t=a..b. f y t) sequentially"
proof (cases "Y = {}")
  case False
  have g_nonneg: "AE teinterval a b in lborel. g t  0"
  proof -
    from Y  {} obtain y where "y  Y" by auto
    from assms(3)[OF this] show ?thesis 
      by eventually_elim (auto elim: order.trans[rotated])
  qed

  have ev: "eventually (λn. a < a' n  a' n < b' n  b' n < b) sequentially"
  proof -
    from ereal_dense2[OF a < b] obtain t where t: "a < ereal t" "ereal t < b" by blast
    from t have "eventually (λn. a' n  {a<..<t}) sequentially"
      by (intro eventually_compose_filterlim[OF _ a'] eventually_at_rightI[of _ "ereal t"])
    moreover from t have "eventually (λn. b' n  {t<..<b}) sequentially"
      by (intro eventually_compose_filterlim[OF _ b'] eventually_at_leftI[of "ereal t"])
    ultimately show "eventually (λn. a < a' n  a' n < b' n  b' n < b) sequentially"
      by eventually_elim auto
  qed

  have "?thesis  uniform_limit Y (λn y. teinterval (max a (a' n)) (min b (b' n)). f y t lborel)
                      (λy. teinterval a b. f y t lborel) sequentially" using a < b
    by (intro filterlim_cong arg_cong2[where f = uniformly_on])
       (auto simp: interval_lebesgue_integral_def fun_eq_iff min_def max_def
             intro!: eventually_mono[OF ev])
  also have 
  proof (rule uniform_limit_set_lebesgue_integral[where g = g], goal_cases)
    show "F n in sequentially. einterval (max a (a' n)) (min b (b' n))  sets borel 
                                einterval (max a (a' n)) (min b (b' n))  einterval a b"
      using ev by eventually_elim (auto simp: einterval_def)
  next
    show "((λn. set_lebesgue_integral lborel (einterval (max a (a' n)) (min b (b' n))) g) 
            set_lebesgue_integral lborel (einterval a b) g) sequentially"
      unfolding set_lebesgue_integral_def
    proof (intro integral_dominated_convergence)
      have *: "set_borel_measurable borel (einterval a b) g"
        using assms(1) less_imp_le[OF a < b]
        by (simp add: interval_lebesgue_integrable_def set_integrable_def set_borel_measurable_def)
      show "(λx. indicat_real (einterval a b) x *R g x)  borel_measurable lborel"
        using * by (simp add: set_borel_measurable_def)
      fix n :: nat
      have "set_borel_measurable borel (einterval (max a (a' n)) (min b (b' n))) g"
        by (rule set_borel_measurable_subset[OF *]) (auto simp: einterval_def)
      thus "(λx. indicat_real (einterval (max a (a' n)) (min b (b' n))) x *R g x)  borel_measurable lborel"
        by (simp add: set_borel_measurable_def)
    next
      show "AE x in lborel. (λn. indicat_real (einterval (max a (a' n)) (min b (b' n))) x *R g x)
                indicat_real (einterval a b) x *R g x"
      proof (rule AE_I2)
        fix x :: real
        have "(λt. indicator (einterval (max a (a' t)) (min b (b' t))) x :: real) 
                indicator (einterval a b) x"
        proof (cases "x  einterval a b")
          case False
          hence "x  einterval (max a (a' t)) (min b (b' t))"for t
            by (auto simp: einterval_def)
          with False show ?thesis by (simp add: indicator_def)
        next
          case True
          with a < b have "eventually (λt. t  {a<..<x}) (at_right a)"
            by (intro eventually_at_rightI[of _ "ereal x"]) (auto simp: einterval_def min_def)

          have "eventually (λn. x  {a' n<..<b' n}) sequentially"
          proof -
            have "eventually (λn. a' n  {a<..<x}) sequentially" using True
              by (intro eventually_compose_filterlim[OF _ a'] eventually_at_rightI[of _ "ereal x"])
                 (auto simp: einterval_def)
            moreover have "eventually (λn. b' n  {x<..<b}) sequentially" using True
              by (intro eventually_compose_filterlim[OF _ b'] eventually_at_leftI[of "ereal x"])
                 (auto simp: einterval_def)
            ultimately show "eventually (λn. x  {a' n<..<b' n}) sequentially"
              by eventually_elim auto
          qed
          hence "eventually (λt. indicator (einterval (max a (a' t)) (min b (b' t))) x = (1 :: real)) sequentially"
            by eventually_elim (use True in auto simp: indicator_def einterval_def)
          from tendsto_eventually[OF this] and True show ?thesis
            by (simp add: indicator_def)
        qed
        thus "(λn. indicat_real (einterval (max a (a' n)) (min b (b' n))) x *R g x)
                  indicat_real (einterval a b) x *R g x" by (intro tendsto_intros)
      qed
    next
      fix X :: "nat  ereal" and n :: nat
      show "AE x in lborel. norm (indicator (einterval (max a (a' n)) (min b (b' n))) x *R g x) 
              indicator (einterval a b) x *R g x"
        using g_nonneg by eventually_elim (auto simp: indicator_def einterval_def)
    qed (use assms less_imp_le[OF a < b] in 
         auto simp: interval_lebesgue_integrable_def set_integrable_def) 
  qed (use assms in auto simp: interval_lebesgue_integrable_def)
  finally show ?thesis .
qed auto

lemma interval_lebesgue_integrable_combine:
  assumes "interval_lebesgue_integrable lborel A B f"
  assumes "interval_lebesgue_integrable lborel B C f"
  assumes "set_borel_measurable borel (einterval A C) f"
  assumes "A  B" "B  C"
  shows   "interval_lebesgue_integrable lborel A C f"
proof -
  have meas: "set_borel_measurable borel (einterval A B  einterval B C) f"
    by (rule set_borel_measurable_subset[OF assms(3)]) (use assms in auto simp: einterval_def)
  have "set_integrable lborel (einterval A B  einterval B C) f"
    using assms by (intro set_integrable_Un) (auto simp: interval_lebesgue_integrable_def)
  also have "?this  set_integrable lborel (einterval A C) f"
  proof (cases "B  {, -}")
    case True
    with assms have "einterval A B  einterval B C = einterval A C"
      by (auto simp: einterval_def)
    thus ?thesis by simp
  next
    case False
    then obtain B' where [simp]: "B = ereal B'"
      by (cases B) auto
    have "indicator (einterval A C) x = (indicator (einterval A B  einterval B C) x :: real)"
      if "x  B'" for x using assms(4,5) that
      by (cases A; cases C) (auto simp: einterval_def indicator_def)
    hence "{x  space lborel. indicat_real (einterval A B  einterval B C) x *R f x 
              indicat_real (einterval A C) x *R f x}  {B'}" by force
    thus ?thesis unfolding set_integrable_def using meas assms
      by (intro integrable_cong_AE AE_I[of _ _ "{B'}"])
         (simp_all add: set_borel_measurable_def)
  qed
  also have "  ?thesis"
    using order.trans[OF assms(4,5)] by (simp add: interval_lebesgue_integrable_def)
  finally show ?thesis .
qed

lemma interval_lebesgue_integrable_bigo_right:
  fixes A B :: real
  fixes f :: "real  real"
  assumes "f  O[at_left B](g)"
  assumes cont: "continuous_on {A..<B} f"
  assumes meas: "set_borel_measurable borel {A<..<B} f"
  assumes "interval_lebesgue_integrable lborel A B g"
  assumes "A < B"
  shows   "interval_lebesgue_integrable lborel A B f"
proof -
  from assms(1) obtain c where c: "c > 0" "eventually (λx. norm (f x)  c * norm (g x)) (at_left B)"
    by (elim landau_o.bigE)
  then obtain B' where B': "B' < B" "x. x  {B'<..<B}  norm (f x)  c * norm (g x)"
    using A < B by (auto simp: Topological_Spaces.eventually_at_left[of A])

  show ?thesis
  proof (rule interval_lebesgue_integrable_combine)
    show "interval_lebesgue_integrable lborel A (max A B') f"
      using B' assms
      by (intro interval_integrable_continuous_on continuous_on_subset[OF cont]) auto
    show "set_borel_measurable borel (einterval (ereal A) (ereal B)) f"
      using assms by simp
    have meas': "set_borel_measurable borel {max A B'<..<B} f"
      by (rule set_borel_measurable_subset[OF meas]) auto
    have "set_integrable lborel {max A B'<..<B} f"
    proof (rule set_integrable_bound[OF _ _ AE_I2[OF impI]])
      have "set_integrable lborel {A<..<B} (λx. c * g x)"
        using assms by (simp add: interval_lebesgue_integrable_def)
      thus "set_integrable lborel {max A B'<..<B} (λx. c * g x)"
        by (rule set_integrable_subset) auto
    next
      fix x assume "x  {max A B'<..<B}"
      hence "norm (f x)  c * norm (g x)"
        by (intro B') auto
      also have "  norm (c * g x)"
        unfolding norm_mult by (intro mult_right_mono) auto
      finally show  "norm (f x)  norm (c * g x)" .
    qed (use meas' in simp_all add: set_borel_measurable_def)
    thus "interval_lebesgue_integrable lborel (ereal (max A B')) (ereal B) f"
      unfolding interval_lebesgue_integrable_def einterval_eq_Icc using B' < B assms by simp
  qed (use B' assms in auto)
qed

lemma interval_lebesgue_integrable_bigo_left:
  fixes A B :: real
  fixes f :: "real  real"
  assumes "f  O[at_right A](g)"
  assumes cont: "continuous_on {A<..B} f"
  assumes meas: "set_borel_measurable borel {A<..<B} f"
  assumes "interval_lebesgue_integrable lborel A B g"
  assumes "A < B"
  shows   "interval_lebesgue_integrable lborel A B f"
proof -
  from assms(1) obtain c where c: "c > 0" "eventually (λx. norm (f x)  c * norm (g x)) (at_right A)"
    by (elim landau_o.bigE)
  then obtain A' where A': "A' > A" "x. x  {A<..<A'}  norm (f x)  c * norm (g x)"
    using A < B by (auto simp: Topological_Spaces.eventually_at_right[of A])

  show ?thesis
  proof (rule interval_lebesgue_integrable_combine)
    show "interval_lebesgue_integrable lborel (min B A') B f"
      using A' assms
      by (intro interval_integrable_continuous_on continuous_on_subset[OF cont]) auto
    show "set_borel_measurable borel (einterval (ereal A) (ereal B)) f"
      using assms by simp
    have meas': "set_borel_measurable borel {A<..<min B A'} f"
      by (rule set_borel_measurable_subset[OF meas]) auto
    have "set_integrable lborel {A<..<min B A'} f"
    proof (rule set_integrable_bound[OF _ _ AE_I2[OF impI]])
      have "set_integrable lborel {A<..<B} (λx. c * g x)"
        using assms by (simp add: interval_lebesgue_integrable_def)
      thus "set_integrable lborel {A<..<min B A'} (λx. c * g x)"
        by (rule set_integrable_subset) auto
    next
      fix x assume "x  {A<..<min B A'}"
      hence "norm (f x)  c * norm (g x)"
        by (intro A') auto
      also have "  norm (c * g x)"
        unfolding norm_mult by (intro mult_right_mono) auto
      finally show  "norm (f x)  norm (c * g x)" .
    qed (use meas' in simp_all add: set_borel_measurable_def)
    thus "interval_lebesgue_integrable lborel (ereal A) (ereal (min B A')) f"
      unfolding interval_lebesgue_integrable_def einterval_eq_Icc using A' > A assms by simp
  qed (use A' assms in auto)
qed


subsection ‹Other material›

(* TODO: Library *)
lemma summable_comparison_test_bigo:
  fixes f :: "nat  real"
  assumes "summable (λn. norm (g n))" "f  O(g)"
  shows   "summable f"
proof -
  from f  O(g) obtain C where C: "eventually (λx. norm (f x)  C * norm (g x)) at_top"
    by (auto elim: landau_o.bigE)
  thus ?thesis
    by (rule summable_comparison_test_ev) (insert assms, auto intro: summable_mult)
qed

lemma fps_expansion_cong:
  assumes "eventually (λx. g x = h x) (nhds x)"
  shows   "fps_expansion g x = fps_expansion h x"
proof -
  have "(deriv ^^ n) g x = (deriv ^^ n) h x" for n
    by (intro higher_deriv_cong_ev assms refl)
  thus ?thesis by (simp add: fps_expansion_def)
qed

lemma fps_expansion_eq_zero_iff:
  assumes "g holomorphic_on ball z r" "r > 0"
  shows   "fps_expansion g z = 0  (zball z r. g z = 0)"
proof
  assume *: "zball z r. g z = 0"
  have "eventually (λw. w  ball z r) (nhds z)"
    using assms by (intro eventually_nhds_in_open) auto
  hence "eventually (λz. g z = 0) (nhds z)"
    by eventually_elim (use * in auto)
  hence "fps_expansion g z = fps_expansion (λ_. 0) z"
    by (intro fps_expansion_cong)
  thus "fps_expansion g z = 0"
    by (simp add: fps_expansion_def fps_zero_def)
next
  assume *: "fps_expansion g z = 0"
  have "g w = 0" if "w  ball z r" for w
    by (rule holomorphic_fun_eq_0_on_ball[OF assms(1) that])
       (use * in auto simp: fps_expansion_def fps_eq_iff)
  thus "wball z r. g w = 0" by blast
qed

lemma fds_nth_higher_deriv:
  "fds_nth ((fds_deriv ^^ k) F) = (λn. (-1) ^ k * of_real (ln n) ^ k * fds_nth F n)"
  by (induction k) (auto simp: fds_nth_deriv fun_eq_iff simp flip: scaleR_conv_of_real)

lemma binomial_n_n_minus_one [simp]: "n > 0  n choose (n - Suc 0) = n"
  by (cases n) auto

lemma has_field_derivative_complex_powr_right:
  "w  0  ((λz. w powr z) has_field_derivative Ln w * w powr z) (at z within A)"
  by (rule DERIV_subset, rule has_field_derivative_powr_right) auto

lemmas has_field_derivative_complex_powr_right' =
  has_field_derivative_complex_powr_right[THEN DERIV_chain2]

end