(* Producto_de_sucesiones_convergentes_a_cero.lean
-- Producto de sucesiones convergentes a cero
-- José A. Alonso Jiménez
-- Sevilla, 17 de febrero de 2024
-- ------------------------------------------------------------------ *)

(* ---------------------------------------------------------------------
-- En Isabelle/HOL, una sucesión u₀, u₁, u₂, ... se puede representar
-- mediante una función (u : \<nat> \<rightarrow> \<real>) de forma que u(n) es uₙ.
--
-- Se define que a es el límite de la sucesión u, por
--    definition limite :: "(nat \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool"
--      where "limite u c \<longleftrightarrow> (\<forall>\<epsilon>>0. \<exists>k::nat. \<forall>n\<ge>k. \<bar>u n - c\<bar> < \<epsilon>)"
--
-- Demostrar que si las sucesiones u(n) y v(n) convergen a cero,
-- entonces u(n)\<sqdot>v(n) también converge a cero.
-- ------------------------------------------------------------------ *)

theory Producto_de_sucesiones_convergentes_a_cero
imports Main HOL.Real
begin

definition limite :: "(nat \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool"
  where "limite u c \<longleftrightarrow> (\<forall>\<epsilon>>0. \<exists>k::nat. \<forall>n\<ge>k. \<bar>u n - c\<bar> < \<epsilon>)"

lemma
  assumes "limite u 0"
          "limite v 0"
  shows   "limite (\<lambda> n. u n * v n) 0"
proof (unfold limite_def; intro allI impI)
  fix \<epsilon> :: real
  assume  h\<epsilon> : "0 < \<epsilon>"
  then obtain U where hU : "\<forall>n\<ge>U. \<bar>u n - 0\<bar> < \<epsilon>"
    using assms(1) limite_def
    by auto
  obtain V where hV : "\<forall>n\<ge>V. \<bar>v n - 0\<bar> < 1"
    using h\<epsilon> assms(2) limite_def
    by fastforce
  have "\<forall>n\<ge>max U V. \<bar>u n * v n - 0\<bar> < \<epsilon>"
  proof (intro allI impI)
    fix n
    assume hn : "max U V \<le> n"
    then have "U \<le> n"
      by simp
    then have "\<bar>u n - 0\<bar> < \<epsilon>"
      using hU by blast
    have hnV : "V \<le> n"
      using hn by simp
    then have "\<bar>v n - 0\<bar> < 1"
      using hV by blast
    have "\<bar>u n * v n - 0\<bar> = \<bar>(u n - 0) * (v n - 0)\<bar>"
      by simp
    also have "\<dots> = \<bar>u n - 0\<bar> * \<bar>v n - 0\<bar>"
      by (simp add: abs_mult)
    also have "\<dots> < \<epsilon> * 1"
      using \<open>\<bar>u n - 0\<bar> < \<epsilon>\<close> \<open>\<bar>v n - 0\<bar> < 1\<close>
      by (rule abs_mult_less)
    also have "\<dots> = \<epsilon>"
      by simp
    finally show "\<bar>u n * v n - 0\<bar> < \<epsilon>"
      by this
  qed
  then show "\<exists>k. \<forall>n\<ge>k. \<bar>u n * v n - 0\<bar> < \<epsilon>"
    by (rule exI)
qed

end