Theory Euler_MacLaurin.Euler_MacLaurin_Landau

section ‹Connection of Euler--MacLaurin summation to Landau symbols›
theory Euler_MacLaurin_Landau
imports 
  Euler_MacLaurin
  Landau_Symbols.Landau_More
begin

subsection ‹$O$-bound for the remainder term›  

text ‹
  Landau symbols allow us to state the bounds on the remainder terms 
  from the Euler--MacLaurin formula a bit more nicely.
›

lemma
  fixes f :: "real ⇒ 'a :: {real_normed_field, banach}"
    and g g' :: "real ⇒ real"
  assumes fin:     "finite Y"
  assumes cont_f:  "continuous_on {a..} f"
  assumes cont_g:  "continuous_on {a..} g"
  assumes cont_g': "continuous_on {a..} g'"
  assumes limit_g: "(g ⤏ 0) at_top"
  assumes f_bound: "⋀x. x ≥ a ⟹ norm (f x) ≤ g' x"
  assumes deriv:   "⋀x. x ∈ {a..} - Y ⟹ (g has_field_derivative -g' x) (at x)"
  shows   EM_remainder_strong_bigo_int: "(λx::int. norm (EM_remainder n f x)) ∈ O(g)"
    and   EM_remainder_strong_bigo_nat: "(λx::nat. norm (EM_remainder n f x)) ∈ O(g)"
proof -
  from bounded_pbernpoly[of n] obtain D where D: "∀x. ¦pbernpoly n x¦ ≤ D" by auto
  from norm_EM_remainder_le_strong_int'[OF fin D assms(2-)]
    have *: "⋀x. x ≥ a ⟶ norm (EM_remainder n f x) ≤ D / fact n * g x" by auto
  have **: "eventually (λx::int. norm (EM_remainder n f x) ≤ abs (D / fact n) * abs (g x)) at_top"
    using eventually_ge_at_top[of "ceiling a"]
  proof eventually_elim
    case (elim x)
    with *[of x] have "norm (EM_remainder n f x) ≤ D / fact n * g x" by (simp add: ceiling_le_iff)
    also have "… ≤ abs (D / fact n * g x)" by (rule abs_ge_self)
    also have "… = abs (D / fact n) * abs (g x)" by (simp add: abs_mult)
    finally show ?case .
  qed
  thus "(λx::int. norm (EM_remainder n f x)) ∈ O(g)"
    by (intro bigoI[of _ "abs D / fact n"]) (auto elim!: eventually_mono)
  hence "(λx::nat. norm (EM_remainder n f (int x))) ∈ O(λx. g (of_int (int x)))"
    by (rule landau_o.big.compose) (fact filterlim_int_sequentially)
  thus "(λx::nat. norm (EM_remainder n f x)) ∈ O(g)" by simp
qed


subsection ‹Asymptotic expansion of the harmonic numbers›

text ‹
  We can now show the asymptotic expansion
  \[H_n = \ln n + \gamma + \frac{1}{2n} - \sum_{i=1}^m \frac{B_{2i}}{2i} n^{-2i} + O(n^{-2m-2})\]
›

lemma harm_remainder_bigo:
  assumes "N > 0"
  shows   "harm_remainder N ∈ O(λn. 1 / real n ^ (2 * N + 1))"
proof -
  from harm_remainder_bound[OF assms]
  obtain C where "∀n≥1. norm (harm_remainder N n) ≤ C / real n ^ (2 * N + 1)" ..
  thus ?thesis
    by (intro bigoI[of _ C] eventually_mono[OF eventually_ge_at_top[of 1]]) auto
qed

lemma harm_expansion_bigo:
  fixes N :: nat
  defines "T ≡ λn. ln n + euler_mascheroni + 1 / (2*n) -
                     (∑i=1..N. bernoulli (2*i) / ((2*i) * n ^ (2*i)))"
  defines "S ≡ (λn. bernoulli (2*(Suc N)) / ((2*Suc N) * real n ^ (2*Suc N)))"
  shows "(λn. harm n - T n) ∈ O(λn. 1 / real n ^ (2 * N + 2))"
proof -
  have "(λn. harm n - T n) ∈ Θ(λn. -S n - harm_remainder (Suc N) n)"
    by (intro bigthetaI_cong eventually_mono[OF eventually_gt_at_top[of "0::nat"]]) 
       (auto simp: T_def harm_expansion[of _ "Suc N"] S_def)
  also have "(λn. -S n - harm_remainder (Suc N) n) ∈ O(λn. 1 / real n ^ (2 * N + 2))"
  proof (intro sum_in_bigo)
    show "(λx. - S x) ∈ O(λn. 1 / real n ^ (2 * N + 2))" unfolding S_def
      by (rule landau_o.big.compose[OF _ filterlim_real_sequentially]) simp
    have "harm_remainder (Suc N) ∈ O(λn. 1 / real n ^ (2 * Suc N + 1))"
      by (rule harm_remainder_bigo) simp_all
    also have "(λn. 1 / real n ^ (2 * Suc N + 1)) ∈ O(λn. 1 / real n ^ (2 * N + 2))"
      by (rule landau_o.big.compose[OF _ filterlim_real_sequentially]) simp
    finally show "harm_remainder (Suc N) ∈ …" .
  qed
  finally show ?thesis .
qed

lemma harm_expansion_bigo_simple1:
  "(λn. harm n - (ln n + euler_mascheroni + 1 / (2 * n))) ∈ O(λn. 1 / n ^ 2)"
  using harm_expansion_bigo[of 0] by (simp add: power2_eq_square)

lemma harm_expansion_bigo_simple2:
  "(λn. harm n - (ln n + euler_mascheroni)) ∈ O(λn. 1 / n)"
proof -
  have "(λn. harm n - (ln n + euler_mascheroni + 1 / (2 * n)) + 1 / (2 * n)) ∈ O(λn. 1 / n)"
  proof (rule sum_in_bigo)
    have "(λn. harm n - (ln n + euler_mascheroni + 1 / (2 * n))) ∈ O(λn. 1 / real n ^ 2)"
      using harm_expansion_bigo_simple1 by simp
    also have "(λn. 1 / real n ^ 2) ∈ O(λn. 1 / real n)"
      by (rule landau_o.big.compose[OF _ filterlim_real_sequentially]) simp_all
    finally show "(λn. harm n - (ln n + euler_mascheroni + 1 / (2 * n))) ∈ O(λn. 1 / n)" by simp
  qed simp_all
  thus ?thesis by (simp add: algebra_simps)
qed

lemma harm_expansion_bigo_simple':
  "harm =o (λn. ln n + euler_mascheroni + 1 / (2 * n)) +o O(λn. 1 / n ^ 2)"
  using harm_expansion_bigo_simple1
  by (subst set_minus_plus [symmetric]) (simp_all add: fun_diff_def)


subsection ‹Asymptotic expansion of the sum of inverse squares›

text ‹
  Similarly to before, we show
  \[\sum_{i=1}^n \frac{1}{i^2} = \frac{\pi^2}{6} - \frac{1}{n} + \frac{1}{2n^2} - 
     \sum_{i=1}^m B_{2i} n^{-2i-1} + O(n^{-2m-3})\]  
›

context
  fixes R :: "nat ⇒ nat ⇒ real"
  defines "R ≡ (λN n. EM_remainder (2*N+1) (λx. -fact (2*N+2) / x ^ (2*N+3)) (int n))"
begin

lemma sum_inverse_squares_remainder_bigo:
  assumes "N > 0"
  shows   "R N ∈ O(λn. 1 / real n ^ (2 * N + 2))"
proof -
  from sum_inverse_squares_remainder_bound[OF assms]
  obtain C
    where "∀n≥1. norm (EM_remainder (2 * N + 1) (λx. - fact (2 * N + 2) / x ^ (2 * N + 3)) (int n))
      ≤ C / real n ^ (2 * N + 2)" ..
  thus ?thesis
    by (intro bigoI[of _ C] eventually_mono[OF eventually_ge_at_top[of 1]]) (auto simp: R_def)
qed

lemma sum_inverse_squares_expansion_bigo:
  fixes N :: nat
  defines "T ≡ λn. pi ^ 2 / 6 - 1 / n + 1 / (2*n ^ 2) -
                     (∑i=1..N. bernoulli (2*i) / (n ^ (2*i+1)))"
  defines "S ≡ (λn. bernoulli (2*(Suc N)) / (real n ^ (2*N+3)))"
  shows "(λn. (∑i=1..n. 1 / real i ^ 2) - T n) ∈ O(λn. 1 / real n ^ (2 * N + 3))"
proof -
  have 3: "3 = Suc (Suc (Suc 0))" by simp
  have "(λn. (∑i=1..n. 1 / real i ^ 2) - T n) ∈ Θ(λn. -S n - R (Suc N) n)" unfolding R_def
    by (intro bigthetaI_cong eventually_mono[OF eventually_gt_at_top[of "0::nat"]])
       (auto simp: T_def sum_inverse_squares_expansion[of _ "Suc N"] S_def 3
             simp del: One_nat_def)
  also have "(λn. -S n - R (Suc N) n) ∈ O(λn. 1 / real n ^ (2 * N + 3))"
  proof (intro sum_in_bigo)
    show "(λx. - S x) ∈ O(λn. 1 / real n ^ (2 * N + 3))" unfolding S_def
      by (rule landau_o.big.compose[OF _ filterlim_real_sequentially]) simp
    have "R (Suc N) ∈ O(λn. 1 / real n ^ (2 * Suc N + 2))"
      by (rule sum_inverse_squares_remainder_bigo) simp_all
    also have "2 * Suc N + 2 = 2 * N + 4" by simp
    also have "(λn. 1 / real n ^ (2 * N + 4)) ∈ O(λn. 1 / real n ^ (2 * N + 3))"
      by (rule landau_o.big.compose[OF _ filterlim_real_sequentially]) simp
    finally show "R (Suc N) ∈ …" .
  qed
  finally show ?thesis .
qed

lemma sum_inverse_squares_expansion_bigo_simple:
  "(λn. (∑i=1..n. 1 / real i ^ 2) - (pi ^ 2 / 6 - 1 / n + 1 / (2*n^2))) ∈ O(λn. 1 / n ^ 3)"
  using sum_inverse_squares_expansion_bigo[of 0] by (simp add: power2_eq_square)

lemma sum_inverse_squares_expansion_bigo_simple':
  "(λn. (∑i=1..n. 1 / real i ^ 2)) =o (λn. pi ^ 2 / 6 - 1 / n + 1 / (2*n^2)) +o O(λn. 1 / n^3)"
  using sum_inverse_squares_expansion_bigo_simple
  by (subst set_minus_plus [symmetric]) (simp_all add: fun_diff_def)

end

end