Theory More_Infinite_Products

subsection ‹Additional facts about infinite products›
theory More_Infinite_Products
  imports "HOL-Analysis.Analysis"
begin

(*
  grouping factors into chunks of the same size

  Only one direction; other direction requires "real_normed_field" (see below).
  Not sure if real_normed_field is really necessary, but I don't see how else to do it.
*)
lemma has_prod_group_nonzero: 
  fixes f :: "nat ⇒ 'a :: {semidom, t2_space}"
  assumes "f has_prod P" "k > 0" "P ≠ 0"
  shows   "(λn. (∏i∈{n*k..<n*k+k}. f i)) has_prod P"
proof -
  have "(λn. ∏k<n. f k) ⇢ P"
    using assms(1) by (intro has_prod_imp_tendsto')
  hence "(λn. ∏k<n*k. f k) ⇢ P"
    by (rule filterlim_compose) (use ‹k > 0› in real_asymp)
  also have "(λn. ∏k<n*k. f k) = (λn. ∏m<n. prod f {m*k..<m*k+k})"
    by (subst prod.nat_group [symmetric]) auto
  finally have "(λn. ∏m≤n. prod f {m*k..<m*k+k}) ⇢ P"
    by (subst (asm) LIMSEQ_lessThan_iff_atMost)
  hence "raw_has_prod (λn. prod f {n*k..<n*k+k}) 0 P"
    using ‹P ≠ 0› by (auto simp: raw_has_prod_def)
  thus ?thesis
    by (auto simp: has_prod_def)
qed

lemma has_prod_group:
  fixes f :: "nat ⇒ 'a :: real_normed_field"
  assumes "f has_prod P" "k > 0"
  shows   "(λn. (∏i∈{n*k..<n*k+k}. f i)) has_prod P"
proof (rule convergent_prod_tendsto_imp_has_prod)
  have "(λn. ∏k<n. f k) ⇢ P"
    using assms(1) by (intro has_prod_imp_tendsto')
  hence "(λn. ∏k<n*k. f k) ⇢ P"
    by (rule filterlim_compose) (use ‹k > 0› in real_asymp)
  also have "(λn. ∏k<n*k. f k) = (λn. ∏m<n. prod f {m*k..<m*k+k})"
    by (subst prod.nat_group [symmetric]) auto
  finally show "(λn. ∏m≤n. prod f {m*k..<m*k+k}) ⇢ P"
    by (subst (asm) LIMSEQ_lessThan_iff_atMost)
next
  from assms obtain N P' where prod1: "raw_has_prod f N P'"
    by (auto simp: has_prod_def)
  define N' where "N' = nat ⌈real N / real k⌉"
  have "k * N' ≥ N"
  proof -
    have "(real N / real k * real k) ≤ real (N' * k)"
      unfolding N'_def of_nat_mult by (intro mult_right_mono) (use ‹k > 0› in auto)
    also have "real N / real k * real k = real N"
      using ‹k > 0› by simp
    finally show ?thesis
      by (simp only: mult.commute of_nat_le_iff)
  qed

  obtain P'' where prod2: "raw_has_prod f (k * N') P''"
    using prod1 ‹k * N' ≥ N› by (rule raw_has_prod_ignore_initial_segment)
  hence "P'' ≠ 0"
    by (auto simp: raw_has_prod_def)
  from prod2 have "raw_has_prod (λn. f (n + k * N')) 0 P''"
    by (simp add: raw_has_prod_def)
  hence "(λn. f (n + k * N')) has_prod P''"
    by (auto simp: has_prod_def)
  hence "(λn. ∏i=n*k..<n*k+k. f (i + k * N')) has_prod P''"
    by (rule has_prod_group_nonzero) fact+
  hence "convergent_prod (λn. ∏i=n*k..<n*k+k. f (i + k * N'))"
    using has_prod_iff by blast
  also have "(λn. ∏i=n*k..<n*k+k. f (i + k * N')) = (λn. ∏i=(n+N')*k..<(n+N')*k+k. f i)"
  proof
    fix n :: nat
    show "(∏i=n*k..<n*k+k. f (i + k * N')) = (∏i=(n+N')*k..<(n+N')*k+k. f i)"
      by (rule prod.reindex_bij_witness[of _ "λn. n - k*N'" "λn. n + k*N'"])
         (auto simp: algebra_simps)
  qed
  also have "convergent_prod … ⟷ convergent_prod (λn. (∏i=n*k..<n*k+k. f i))"
    by (rule convergent_prod_iff_shift)
  finally show "convergent_prod (λn. prod f {n * k..<n * k + k})" .
qed

end