Theory Lambert_Series_Library

section ‹Missing Library Material›
theory Lambert_Series_Library
imports 
  "HOL-Complex_Analysis.Complex_Analysis"
  "HOL-Library.Landau_Symbols"
  "HOL-Real_Asymp.Real_Asymp"
begin

subsection ‹Miscellaneous›

lemma power_less_1_iff: "x ≥ 0 ⟹ (x :: real) ^ n < 1 ⟷ x < 1 ∧ n > 0"
  by (metis not_gr_zero not_less_iff_gr_or_eq power_0 real_root_lt_1_iff real_root_pos2)

lemma fls_nth_sum: "fls_nth (∑x∈A. f x) n = (∑x∈A. fls_nth (f x) n)"
  by (induction A rule: infinite_finite_induct) auto

lemma two_times_choose_two: "2 * (n choose 2) = n * (n - 1)"
  unfolding choose_two by (simp add: algebra_simps)

lemma Nats_not_empty [simp]: "ℕ ≠ {}"
  using Nats_1 by blast


subsection ‹Infinite sums›

lemma has_sum_iff: "(f has_sum S) A ⟷ f summable_on A ∧ infsum f A = S"
  using infsumI summable_iff_has_sum_infsum by blast
  
lemma summable_on_reindex_bij_witness:
  assumes "⋀a. a ∈ S ⟹ i (j a) = a"
  assumes "⋀a. a ∈ S ⟹ j a ∈ T"
  assumes "⋀b. b ∈ T ⟹ j (i b) = b"
  assumes "⋀b. b ∈ T ⟹ i b ∈ S"
  assumes "⋀a. a ∈ S ⟹ h (j a) = g a"
  shows   "g summable_on S ⟷ h summable_on T"
  using has_sum_reindex_bij_witness[of S i j T h g, OF assms refl]
  by (simp add: summable_on_def)

lemma has_sum_diff:
  fixes f g :: "'a ⇒ 'b::{topological_ab_group_add}"
  assumes ‹(f has_sum a) A›
  assumes ‹(g has_sum b) A›
  shows ‹((λx. f x - g x) has_sum (a - b)) A›
  using has_sum_add[of f A a "λx. -g x" "-b"] assms by (simp add: has_sum_uminus)

lemma summable_on_diff:
  fixes f g :: "'a ⇒ 'b::{topological_ab_group_add}"
  assumes ‹f summable_on A›
  assumes ‹g summable_on A›
  shows ‹(λx. f x - g x) summable_on A›
  by (metis (full_types) assms summable_on_def has_sum_diff)

lemma infsum_diff:
  fixes f g :: "'a ⇒ 'b::{topological_ab_group_add, t2_space}"
  assumes ‹f summable_on A›
  assumes ‹g summable_on A›
  shows ‹infsum (λx. f x - g x) A = infsum f A - infsum g A›
proof -
  have ‹((λx. f x - g x) has_sum (infsum f A - infsum g A)) A›
    by (simp add: assms has_sum_diff)
  then show ?thesis
    using infsumI by blast
qed

lemma summable_norm_add:
  assumes "summable (λn. norm (f n))" "summable (λn. norm (g n))"
  shows   "summable (λn. norm (f n + g n))"
proof (rule summable_comparison_test)
  show "summable (λn. norm (f n) + norm (g n))"
    by (intro summable_add assms)
  show "∃N. ∀n≥N. norm (norm (f n + g n)) ≤ norm (f n) + norm (g n)"
    by (intro exI[of _ 0] allI impI) (auto simp: norm_triangle_ineq)
qed

lemma summable_norm_diff:
  assumes "summable (λn. norm (f n))" "summable (λn. norm (g n))"
  shows   "summable (λn. norm (f n - g n))"
  using summable_norm_add[of f "λn. -g n"] assms by simp

lemma sums_imp_has_prod_exp:
  fixes f :: "_ ⇒'a::{real_normed_field,banach}"
  assumes "f sums F"
  shows   "(λn. exp (f n)) has_prod exp F"
proof -
  have "(λn. exp (∑i≤n. f i)) ⇢ exp F"
    by (intro tendsto_intros) (use assms in ‹auto simp: sums_def' atLeast0AtMost›)
  also have "(λn. exp (∑i≤n. f i)) = (λn. ∏i≤n. exp (f i))"
    by (simp add: exp_sum)
  finally have "raw_has_prod (λn. exp (f n)) 0 (exp F)"
    unfolding raw_has_prod_def by auto
  thus ?thesis
    unfolding has_prod_def by blast
qed

lemma telescope_summable_iff:
  fixes f :: "nat ⇒ 'a::{real_normed_vector}"
  shows "summable (λn. f (Suc n) - f n) ⟷ convergent f"
proof
  assume "convergent f"
  thus "summable (λn. f (Suc n) - f n)"
    using telescope_summable[of f] by (auto simp: convergent_def)
next
  assume "summable (λn. f (Suc n) - f n)"
  hence "convergent (λn. ∑i<n. f (Suc i) - f i)"
    by (simp add: summable_iff_convergent)
  also have "(λn. ∑i<n. f (Suc i) - f i) = (λn. f n - f 0)"
    by (subst sum_lessThan_telescope) auto
  also have "convergent … ⟷ convergent f"
    by (rule convergent_diff_const_right_iff)
  finally show "convergent f" .
qed

lemma telescope_summable_iff':
  fixes f :: "nat ⇒ 'a::{real_normed_vector}"
  shows "summable (λn. f n - f (Suc n)) ⟷ convergent f"
  using telescope_summable_iff[of "λn. -f n"] by (simp flip: convergent_minus_iff)

lemma norm_summable_mult_bounded:
  assumes "summable (λn. norm (f n))"
  assumes "g ∈ O(λ_. 1)"
  shows   "summable (λn. norm (f n * g n))"
proof -
  from assms(2) obtain C where C: "C > 0" "eventually (λn. norm (g n) ≤ C) at_top"
    by (auto elim!: landau_o.bigE)
  show ?thesis
  proof (rule summable_comparison_test_ev)
    show "summable (λn. norm (f n) * C)"
      by (subst mult.commute) (intro summable_mult assms)
    show "eventually (λn. norm (norm (f n * g n)) ≤ norm (f n) * C) at_top"
      using C(2) by eventually_elim (use C(1) in ‹auto intro!: mult_mono simp: norm_mult›)
  qed
qed

lemma summable_powser_comparison_test_bigo:
  fixes f g :: "nat ⇒ 'a :: {real_normed_field, banach}"
  assumes "summable f" "g ∈ O(λn. f n * c ^ n)" "norm c < 1"
  shows   "summable (λn. norm (g n))"
proof (rule summable_comparison_test_bigo)
  have "summable (λn. norm (f n * c ^ n))"
    by (rule powser_insidea[of _ 1]) (use assms in auto)
  thus "summable (λn. norm (norm (f n * c ^ n)))"
    by simp
  show "(λn. norm (g n)) ∈ O(λn. norm (f n * c ^ n))"
    using assms(2) by simp
qed
  
lemma geometric_sums_gen:
  assumes "norm (x :: 'a :: real_normed_field) < 1"
  shows   "(λn. x ^ (n + k)) sums (x ^ k / (1 - x))"
proof -
  have "(λn. x ^ k * x ^ n) sums (x ^ k * (1 / (1 - x)))"
    by (intro sums_mult geometric_sums assms)
  thus ?thesis
    by (simp add: power_add mult_ac)
qed

lemma has_sum_geometric:
  fixes x :: "'a :: {real_normed_field, banach}"
  assumes "norm x < 1"
  shows   "((λn. x ^ n) has_sum (x ^ m / (1 - x))) {m..}"
proof -
  have "((λn. x ^ n) has_sum (1 / (1 - x))) UNIV"
    using assms
    by (intro norm_summable_imp_has_sum)
       (auto intro: geometric_sums summable_geometric simp: norm_power)
  hence "((λn. x ^ m * x ^ n) has_sum (x ^ m * (1 / (1 - x)))) UNIV"
    by (rule has_sum_cmult_right)
  also have "?this ⟷ ?thesis"
    by (rule has_sum_reindex_bij_witness[of _ "λn. n - m" "λn. n + m"]) (auto simp: power_add)
  finally show ?thesis .
qed

lemma n_powser_sums:
  fixes q :: "'a :: {real_normed_field,banach}"
  assumes q: "norm q < 1"
  shows   "(λn. of_nat n * q ^ n) sums (q / (1 - q) ^ 2)"
proof -
  have "(λn. q * (of_nat (Suc n) * q ^ n)) sums (q * (1 / (1 - q)⇧2))"
    using q by (intro sums_mult geometric_deriv_sums)
  also have "(λn. q * (of_nat (Suc n) * q ^ n)) = (λn. of_nat (Suc n) * q ^ Suc n)"
    by (simp add: algebra_simps)
  finally have "(λn. of_nat n * q ^ n) sums (q * (1 / (1 - q)⇧2) + of_nat 0 * q ^ 0)"
    by (rule sums_Suc)
  thus "(λn. of_nat n * q ^ n) sums (q / (1 - q) ^ 2)"
    by simp
qed


subsection ‹Convergence radius›

lemma tendsto_imp_conv_radius_eq:
  assumes "(λn. ereal (norm (f n) powr (1 / real n))) ⇢ c'" "c = inverse c'"
  shows   "conv_radius f = c"
proof -
  have "(λn. ereal (root n (norm (f n)))) ⇢ c'"
  proof (rule Lim_transform_eventually)
    show "(λn. ereal (norm (f n) powr (1 / real n))) ⇢ c'"
      using assms by simp
    show "∀⇩F x in sequentially. ereal (norm (f x) powr (1 / real x)) = 
                                ereal (root x (norm (f x)))"
      using eventually_gt_at_top[of 0] 
    proof eventually_elim
      case (elim n)
      show ?case using elim
        by (cases "f n = 0") (simp_all add: root_powr_inverse)
    qed
  qed
  thus ?thesis
    unfolding conv_radius_def using assms by (simp add: limsup_root_limit)
qed

lemma conv_radius_powr_real: "conv_radius (λn. real n powr a) = 1"
proof (rule tendsto_imp_conv_radius_eq)
  have "(λn. ereal ((real n powr a) powr (1 / real n))) ⇢ ereal 1"
    by (rule tendsto_ereal) real_asymp
  thus "(λn. ereal (norm (real n powr a) powr (1 / real n))) ⇢ ereal 1"
    by simp
qed (simp_all add: one_ereal_def)

lemma conv_radius_one_over: "conv_radius (λn. 1 / of_nat n :: 'a :: {real_normed_field, banach}) = 1"
proof (rule tendsto_imp_conv_radius_eq)
  have "(λn. ereal ((1 / n) powr (1 / real n))) ⇢ ereal 1"
    by (rule tendsto_ereal) real_asymp
  thus "(λn. ereal (norm (1 / of_nat n :: 'a) powr (1 / real n))) ⇢ ereal 1"
    by (simp add: norm_divide)
qed (simp_all add: one_ereal_def)

lemma conv_radius_mono:
  assumes "eventually (λn. norm (f n) ≥ norm (g n)) sequentially"
  shows   "conv_radius f ≤ conv_radius g"
  unfolding conv_radius_def
proof (rule ereal_inverse_antimono[OF _ Limsup_mono])
  have "limsup (λn. 0) ≤ limsup (λn. ereal (root n (norm (g n))))"
    by (rule Limsup_mono) (auto intro!: eventually_mono[OF eventually_gt_at_top[of 0]])
  thus "limsup (λn. ereal (root n (norm (g n)))) ≥ 0"
    by (simp add: Limsup_const)
next
  show "∀⇩F x in sequentially. ereal (root x (norm (g x))) ≤ ereal (root x (norm (f x)))"
    using assms eventually_gt_at_top[of 0] by eventually_elim auto
qed

lemma conv_radius_const [simp]:
  assumes "c ≠ 0"
  shows   "conv_radius (λ_. c) = 1"
proof (rule tendsto_imp_conv_radius_eq)
  show "(λn. ereal (norm c powr (1 / real n))) ⇢ ereal 1"
    by (rule tendsto_ereal) (use assms in real_asymp)
qed auto

lemma conv_radius_bigo_polynomial:
  assumes "f ∈ O(λn. of_nat n ^ k)"
  shows   "conv_radius f ≥ 1"
proof -
  from assms obtain C where ev: "C > 0" "eventually (λn. norm (f n) ≤ C * real n ^ k) at_top"
    by (elim landau_o.bigE) (auto simp: norm_power)
  have "(λx. (C * real x ^ k) powr (1 / real x)) ⇢ 1"
    using ev(1) by real_asymp
  hence "conv_radius (λn. C * real n ^ k) = inverse (ereal 1)" using ev(1)
    by (intro tendsto_imp_conv_radius_eq[OF _ refl] tendsto_ereal)
       (simp add: norm_mult norm_power abs_mult)
  moreover have "conv_radius (λn. C * real n ^ k) ≤ conv_radius f"
    by (intro conv_radius_mono eventually_mono[OF ev(2)]) auto
  ultimately show ?thesis
    by (simp add: one_ereal_def)
qed


subsection ‹Limits›

lemma oscillation_imp_not_tendsto:
  assumes "eventually (λn. f (g n) ∈ A) sequentially" "filterlim g F sequentially"
  assumes "eventually (λn. f (h n) ∈ B) sequentially" "filterlim h F sequentially"
  assumes "closed A" "closed B" "A ∩ B = {}"
  shows   "¬filterlim f (nhds c) F"
proof
  assume *: "filterlim f (nhds c) F"
  have "filterlim (λn. f (g n)) (nhds c) sequentially"
    using * assms(2) by (rule filterlim_compose)
  with assms(1,5) have "c ∈ A"
    by (metis Lim_in_closed_set sequentially_bot)
  have "filterlim (λn. f (h n)) (nhds c) sequentially"
    using * assms(4) by (rule filterlim_compose)
  with assms(3,6) have "c ∈ B"
    by (metis Lim_in_closed_set sequentially_bot)
  with ‹c ∈ A› and ‹A ∩ B = {}› show False
    by blast
qed

lemma oscillation_imp_not_convergent:
  assumes "frequently (λn. f n ∈ A) sequentially"
  assumes "frequently (λn. f n ∈ B) sequentially"
  assumes "closed A" "closed B" "A ∩ B = {}"
  shows   "¬convergent f"
proof -
  obtain g :: "nat ⇒ nat" where g: "strict_mono g" "⋀n. f (g n) ∈ A"
    using assms(1) infinite_enumerate
    unfolding cofinite_eq_sequentially [symmetric] INFM_iff_infinite
    by blast
  obtain h :: "nat ⇒ nat" where h: "strict_mono h" "⋀n. f (h n) ∈ B"
    using assms(2) infinite_enumerate
    unfolding cofinite_eq_sequentially [symmetric] INFM_iff_infinite
    by blast
  have "¬f ⇢ L" for L
  proof (rule oscillation_imp_not_tendsto)
    show "∀⇩F n in sequentially. f (g n) ∈ A" "∀⇩F n in sequentially. f (h n) ∈ B"
      using g h by auto
  qed (use g h assms in ‹auto intro: filterlim_subseq›)
  thus ?thesis
    unfolding convergent_def by blast
qed

lemma seq_bigo_1_iff:
  "g ∈ O(λ_::nat. 1) ⟷ bounded (range g)"
proof
  assume "g ∈ O(λ_. 1)"
  then obtain C where"eventually (λn. norm (g n) ≤ C) at_top"
    by (elim landau_o.bigE) auto
  then obtain N where N: "⋀n. n ≥ N ⟹ norm (g n) ≤ C" 
    by (auto simp: eventually_at_top_linorder)
  hence "norm (g n) ≤ Max (insert C (norm ` g ` {..<N}))" for n
    by (cases "n < N") (auto simp: Max_ge_iff)
  thus "bounded (range g)"
    by (auto simp: bounded_iff)
next
  assume "bounded (range g)"
  then obtain C where "norm (g n) ≤ C" for n
    by (auto simp: bounded_iff)
  thus "g ∈ O(λ_. 1)"
    by (intro bigoI[where c = C]) auto
qed

lemma incseq_convergent':
  assumes "incseq (g :: nat ⇒ real)" "g ∈ O(λ_. 1)"
  shows   "convergent g"
proof -
  from assms(2) have "bounded (range g)"
    by (simp add: seq_bigo_1_iff)
  then obtain C where C: "¦g n¦ ≤ C" for n
    unfolding bounded_iff by auto
  show ?thesis
  proof (rule incseq_convergent)
    show "incseq g"
      by fact
  next
    have "g i ≤ C" for i :: nat
      using C[of i] by auto
    thus "∀i. g i ≤ C"
      by blast
  qed (auto simp: convergent_def)
qed

lemma decseq_convergent':
  assumes "decseq (g :: nat ⇒ real)" "g ∈ O(λ_. 1)"
  shows   "convergent g"
  using incseq_convergent'[of "λn. -g n "] assms
  by (simp flip: convergent_minus_iff add: decseq_eq_incseq)

lemma filterlim_of_int_iff:
  fixes c :: "'a :: real_normed_algebra_1"
  assumes "F ≠ bot"
  shows "filterlim (λx. of_int (f x)) (nhds c) F ⟷
           (∃c'. c = of_int c' ∧ eventually (λx. f x = c') F)"
proof
  assume "∃c'. c = of_int c' ∧ eventually (λx. f x = c') F"
  then obtain c' where c': "c = of_int c'" "eventually (λx. f x = c') F"
    by blast
  from c'(2) have "eventually (λx. of_int (f x) = c) F"
    by eventually_elim (auto simp: c'(1))
  thus "filterlim (λx. of_int (f x)) (nhds c) F"
    by (rule tendsto_eventually)    
next
  assume *: "filterlim (λx. of_int (f x)) (nhds c) F"
  show "(∃c'. c = of_int c' ∧ eventually (λx. f x = c') F)"
  proof (cases "c ∈ ℤ")
    case False
    hence "setdist {c} ℤ > 0"
      by (subst setdist_gt_0_compact_closed) auto
    with * have "eventually (λx. dist (of_int (f x)) c < setdist {c} ℤ) F"
      unfolding tendsto_iff by blast
    then obtain x where "dist (of_int (f x)) c < setdist {c} ℤ"
      using ‹F ≠ bot› eventually_happens by blast
    moreover have "dist c (of_int (f x)) ≥ setdist {c} ℤ"
      by (rule setdist_le_dist) auto
    ultimately show ?thesis
      by (simp add: dist_commute)
  next
    case True
    then obtain c' where c: "c = of_int c'"
      by (elim Ints_cases)
    have "eventually (λx. dist (of_int (f x)) c < 1) F"
      using * unfolding tendsto_iff by auto
    hence "eventually (λx. f x = c') F"
      by eventually_elim (auto simp: c dist_of_int)
    with c show ?thesis
      by auto
  qed
qed

lemma filterlim_of_nat_iff:
  fixes c :: "'a :: real_normed_algebra_1"
  assumes "F ≠ bot"
  shows "filterlim (λx. of_nat (f x)) (nhds c) F ⟷
           (∃c'. c = of_nat c' ∧ eventually (λx. f x = c') F)"
proof
  assume "∃c'. c = of_nat c' ∧ eventually (λx. f x = c') F"
  then obtain c' where c': "c = of_nat c'" "eventually (λx. f x = c') F"
    by blast
  from c'(2) have "eventually (λx. of_nat (f x) = c) F"
    by eventually_elim (auto simp: c'(1))
  thus "filterlim (λx. of_nat (f x)) (nhds c) F"
    by (rule tendsto_eventually)    
next
  assume *: "filterlim (λx. of_nat (f x)) (nhds c) F"
  show "(∃c'. c = of_nat c' ∧ eventually (λx. f x = c') F)"
  proof (cases "c ∈ ℕ")
    case False
    hence "setdist {c} ℕ > 0"
      by (subst setdist_gt_0_compact_closed) auto
    with * have "eventually (λx. dist (of_nat (f x)) c < setdist {c} ℕ) F"
      unfolding tendsto_iff by blast
    then obtain x where "dist (of_nat (f x)) c < setdist {c} ℕ"
      using ‹F ≠ bot› eventually_happens by blast
    moreover have "dist c (of_nat (f x)) ≥ setdist {c} ℕ"
      by (rule setdist_le_dist) auto
    ultimately show ?thesis
      by (simp add: dist_commute)
  next
    case True
    then obtain c' where c: "c = of_nat c'"
      by (elim Nats_cases)
    have "eventually (λx. dist (of_nat (f x)) c < 1) F"
      using * unfolding tendsto_iff by auto
    hence "eventually (λx. f x = c') F"
      by eventually_elim (auto simp: c dist_of_nat)
    with c show ?thesis
      by auto
  qed
qed

lemma uniform_limit_compose:
  assumes "uniform_limit B (λx y. f x y) (λy. f' y) F" "⋀y. y ∈ A ⟹ g y ∈ B"
  shows   "uniform_limit A (λx y. f x (g y)) (λy. f' (g y)) F"
proof -
  have "uniform_limit (g ` A) (λx y. f x y) (λy. f' y) F"
    using assms(1) by (rule uniform_limit_on_subset) (use assms(2) in blast)
  thus "uniform_limit A (λx y. f x (g y)) (λy. f' (g y)) F"
    unfolding uniform_limit_iff by auto
qed

lemma uniform_limit_const':
  assumes "filterlim f (nhds c) F"
  shows   "uniform_limit A (λx y. f x) (λy. c) F"
proof -
  have "∀⇩F n in F. ∀x∈A. dist (f n) c < ε" if ε: "ε > 0" for ε :: real
  proof -
    from assms and ε have "∀⇩F n in F. dist (f n) c < ε"
      unfolding tendsto_iff by blast
    thus ?thesis
      by eventually_elim auto
  qed
  thus ?thesis
    unfolding uniform_limit_iff by blast
qed

lemma uniform_limit_singleton_iff [simp]:
  "uniform_limit {x} f g F ⟷ filterlim (λy. f y x) (nhds (g x)) F"
  by (simp add: uniform_limit_iff tendsto_iff)

end