theory FPS_Prodinf
  imports "HOL-Computational_Algebra.Computational_Algebra"
begin

(* This should really go in the library *)
lemma tendsto_fpsI:
  assumes "\<And>m. eventually (\<lambda>x. fps_nth (f x) m = fps_nth g m) F"
  shows   "(f \<longlongrightarrow> g) F"
proof
  fix e :: real assume e: "e > 0"
  define m where "m = nat \<lceil>log 2 e\<rceil>"
  then obtain m where "2 ^ m > inverse e"
    by (metis ceiling_less_cancel ceiling_of_int  le_less
         le_less_trans nat_le_iff of_int_numeral of_int_power of_nat_less_two_power)
  with e have "inverse (2 ^ m) < e" by (simp add: field_simps)

  from assms have "eventually (\<lambda>x. \<forall>m'\<in>{..m}. fps_nth (f x) m' = fps_nth g m') F"
    by (subst eventually_ball_finite_distrib) auto
  thus "eventually (\<lambda>x. dist (f x) g < e) F"
  proof eventually_elim
    case (elim x)
    show ?case
    proof (cases "f x = g")
      case False
      hence "subdegree (f x - g) \<ge> m" using elim
        by (intro subdegree_geI) auto
      hence "dist (f x) g \<le> inverse (2 ^ m)" by (simp add: dist_fps_def)
      also have "\<dots> < e" by fact
      finally show ?thesis .
    qed (insert e, auto)
  qed
qed

lemma myprod: "(\<Prod>k<n. 1 + fps_X ^ (2 ^ k)) = Abs_fps (\<lambda>i. if i < 2 ^ n then 1 else 0)"
  (is "?F n = ?G n")
proof (induction n)
  case (Suc n)
  have "?F (Suc n) = ?F n + fps_X ^ (2 ^ n) * ?F n"
    by (simp add: algebra_simps)
  also have "?F n = ?G n" by (fact Suc.IH)
  also have "?G n + fps_X ^ (2 ^ n) * ?G n = ?G (Suc n)"
    by  (auto simp: fps_X_power_mult_nth fps_eq_iff)
  finally show ?case .
qed (auto simp: fps_eq_iff)


lemma myprod': "(\<lambda>n. \<Prod>k<n. 1 + fps_X ^ (2 ^ k) :: real fps) \<longlonglongrightarrow> Abs_fps (\<lambda>_. 1)"
proof (rule tendsto_fpsI, goal_cases)
  case (1 m)
  have "eventually (\<lambda>n. n \<ge> m) sequentially" by (rule eventually_ge_at_top)
  thus ?case
  proof eventually_elim
    case (elim n)
    note \<open>m \<le> n\<close>
    also have "n < 2 ^ n" by (induction n) auto
    finally have "m < 2 ^ n" .
    thus ?case by (subst myprod) auto
  qed
qed

end