Quelle Limits.thy Sprache: Isabelle

(*  Title:      HOL/Limits.thy
    Author:     Brian Huffman
    Author:     Jacques D. Fleuriot, University of Cambridge
    Author:     Lawrence C Paulson
    Author:     Jeremy Avigad
*)

section \<open>Limits on Real Vector Spaces\<close>

theory Limits
  imports Real_Vector_Spaces
begin

lemma range_mult [simp]:
  fixes a::"real" shows "range ((*) a) = (if a=0 then {0} else UNIV)"
  by (simp add: surj_def) (meson dvdE dvd_field_iff)

subsection \<open>Filter going to infinity norm\<close>

definition at_infinity :: "'a::real_normed_vector filter"
  where "at_infinity = (INF r. principal {x. r \ norm x})"

lemma eventually_at_infinity: "eventually P at_infinity \ (\b. \x. b \ norm x \ P x)"
  unfolding at_infinity_def
  by (subst eventually_INF_base)
     (auto simp: subset_eq eventually_principal intro!: exI[of _ "max a b" for a b])

lemma eventually_at_infinityI:
  fixes P::"'a::real_normed_vector \ bool"
  assumes "\x. c \ norm x \ P x"
  shows "eventually P at_infinity"
unfolding eventually_at_infinity using assms by auto

corollary eventually_at_infinity_pos:
  "eventually p at_infinity \ (\b. 0 < b \ (\x. norm x \ b \ p x))"
  unfolding eventually_at_infinity
  by (meson le_less_trans norm_ge_zero not_le zero_less_one)

lemma at_infinity_eq_at_top_bot: "(at_infinity :: real filter) = sup at_top at_bot"
proof -
  have 1: "\\n\u. A n; \n\v. A n\
       \<Longrightarrow> \<exists>b. \<forall>x. b \<le> \<bar>x\<bar> \<longrightarrow> A x" for A and u v::real
    by (rule_tac x="max (- v) u" in exI) (auto simp: abs_real_def)
  have 2: "\x. u \ \x\ \ A x \ \N. \n\N. A n" for A and u::real
    by (meson abs_less_iff le_cases less_le_not_le)
  have 3: "\x. u \ \x\ \ A x \ \N. \n\N. A n" for A and u::real
    by (metis (full_types) abs_ge_self abs_minus_cancel le_minus_iff order_trans)
  show ?thesis
    by (auto simp: filter_eq_iff eventually_sup eventually_at_infinity
      eventually_at_top_linorder eventually_at_bot_linorder intro: 1 2 3)
qed

lemma at_top_le_at_infinity: "at_top \ (at_infinity :: real filter)"
  unfolding at_infinity_eq_at_top_bot by simp

lemma at_bot_le_at_infinity: "at_bot \ (at_infinity :: real filter)"
  unfolding at_infinity_eq_at_top_bot by simp

lemma filterlim_at_top_imp_at_infinity: "filterlim f at_top F \ filterlim f at_infinity F"
  for f :: "_ \ real"
  by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl])

lemma filterlim_real_at_infinity_sequentially: "filterlim real at_infinity sequentially"
  by (simp add: filterlim_at_top_imp_at_infinity filterlim_real_sequentially)

lemma lim_infinity_imp_sequentially: "(f \ l) at_infinity \ ((\n. f(n)) \ l) sequentially"
  by (simp add: filterlim_at_top_imp_at_infinity filterlim_compose filterlim_real_sequentially)

subsubsection \<open>Boundedness\<close>

definition Bfun :: "('a \ 'b::metric_space) \ 'a filter \ bool"
  where Bfun_metric_def: "Bfun f F = (\y. \K>0. eventually (\x. dist (f x) y \ K) F)"

abbreviation Bseq :: "(nat \ 'a::metric_space) \ bool"
  where "Bseq X \ Bfun X sequentially"

lemma Bseq_conv_Bfun: "Bseq X \ Bfun X sequentially" ..

lemma Bseq_ignore_initial_segment: "Bseq X \ Bseq (\n. X (n + k))"
  unfolding Bfun_metric_def by (subst eventually_sequentially_seg)

lemma Bseq_offset: "Bseq (\n. X (n + k)) \ Bseq X"
  unfolding Bfun_metric_def by (subst (asm) eventually_sequentially_seg)

lemma Bfun_def: "Bfun f F \ (\K>0. eventually (\x. norm (f x) \ K) F)"
  unfolding Bfun_metric_def norm_conv_dist
proof safe
  fix y K
  assume K: "0 < K" and *: "eventually (\x. dist (f x) y \ K) F"
  moreover have "eventually (\x. dist (f x) 0 \ dist (f x) y + dist 0 y) F"
    by (intro always_eventually) (metis dist_commute dist_triangle)
  with * have "eventually (\x. dist (f x) 0 \ K + dist 0 y) F"
    by eventually_elim auto
  with \<open>0 < K\<close> show "\<exists>K>0. eventually (\<lambda>x. dist (f x) 0 \<le> K) F"
    by (intro exI[of _ "K + dist 0 y"] add_pos_nonneg conjI zero_le_dist) auto
qed (force simp del: norm_conv_dist [symmetric])

lemma BfunI:
  assumes K: "eventually (\x. norm (f x) \ K) F"
  shows "Bfun f F"
  unfolding Bfun_def
proof (intro exI conjI allI)
  show "0 < max K 1" by simp
  show "eventually (\x. norm (f x) \ max K 1) F"
    using K by (rule eventually_mono) simp
qed

lemma BfunE:
  assumes "Bfun f F"
  obtains B where "0 < B" and "eventually (\x. norm (f x) \ B) F"
  using assms unfolding Bfun_def by blast

lemma Cauchy_Bseq:
  assumes "Cauchy X" shows "Bseq X"
proof -
  have "\y K. 0 < K \ (\N. \n\N. dist (X n) y \ K)"
    if "\m n. \m \ M; n \ M\ \ dist (X m) (X n) < 1" for M
    by (meson order.order_iff_strict that zero_less_one)
  with assms show ?thesis
    by (force simp: Cauchy_def Bfun_metric_def eventually_sequentially)
qed

subsubsection \<open>Bounded Sequences\<close>

lemma BseqI': "(\n. norm (X n) \ K) \ Bseq X"
  by (intro BfunI) (auto simp: eventually_sequentially)

lemma Bseq_def: "Bseq X \ (\K>0. \n. norm (X n) \ K)"
  unfolding Bfun_def eventually_sequentially
proof safe
  fix N K
  assume "0 < K" "\n\N. norm (X n) \ K"
  then show "\K>0. \n. norm (X n) \ K"
    by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] max.strict_coboundedI2)
       (auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj)
qed auto

lemma BseqE: "Bseq X \ (\K. 0 < K \ \n. norm (X n) \ K \ Q) \ Q"
  unfolding Bseq_def by auto

lemma BseqD: "Bseq X \ \K. 0 < K \ (\n. norm (X n) \ K)"
  by (simp add: Bseq_def)

lemma BseqI: "0 < K \ \n. norm (X n) \ K \ Bseq X"
  by (auto simp: Bseq_def)

lemma Bseq_bdd_above: "Bseq X \ bdd_above (range X)"
  for X :: "nat \ real"
proof (elim BseqE, intro bdd_aboveI2)
  fix K n
  assume "0 < K" "\n. norm (X n) \ K"
  then show "X n \ K"
    by (auto elim!: allE[of _ n])
qed

lemma Bseq_bdd_above': "Bseq X \ bdd_above (range (\n. norm (X n)))"
  for X :: "nat \ 'a :: real_normed_vector"
proof (elim BseqE, intro bdd_aboveI2)
  fix K n
  assume "0 < K" "\n. norm (X n) \ K"
  then show "norm (X n) \ K"
    by (auto elim!: allE[of _ n])
qed

lemma Bseq_bdd_below: "Bseq X \ bdd_below (range X)"
  for X :: "nat \ real"
proof (elim BseqE, intro bdd_belowI2)
  fix K n
  assume "0 < K" "\n. norm (X n) \ K"
  then show "- K \ X n"
    by (auto elim!: allE[of _ n])
qed

lemma Bseq_eventually_mono:
  assumes "eventually (\n. norm (f n) \ norm (g n)) sequentially" "Bseq g"
  shows "Bseq f"
proof -
  from assms(2) obtain K where "0 < K" and "eventually (\n. norm (g n) \ K) sequentially"
    unfolding Bfun_def by fast
  with assms(1) have "eventually (\n. norm (f n) \ K) sequentially"
    by (fast elim: eventually_elim2 order_trans)
  with \<open>0 < K\<close> show "Bseq f"
    unfolding Bfun_def by fast
qed

lemma lemma_NBseq_def: "(\K > 0. \n. norm (X n) \ K) \ (\N. \n. norm (X n) \ real(Suc N))"
proof safe
  fix K :: real
  from reals_Archimedean2 obtain n :: nat where "K < real n" ..
  then have "K \ real (Suc n)" by auto
  moreover assume "\m. norm (X m) \ K"
  ultimately have "\m. norm (X m) \ real (Suc n)"
    by (blast intro: order_trans)
  then show "\N. \n. norm (X n) \ real (Suc N)" ..
next
  show "\N. \n. norm (X n) \ real (Suc N) \ \K>0. \n. norm (X n) \ K"
    using of_nat_0_less_iff by blast
qed

text \<open>Alternative definition for \<open>Bseq\<close>.\<close>
lemma Bseq_iff: "Bseq X \ (\N. \n. norm (X n) \ real(Suc N))"
  by (simp add: Bseq_def) (simp add: lemma_NBseq_def)

lemma lemma_NBseq_def2: "(\K > 0. \n. norm (X n) \ K) = (\N. \n. norm (X n) < real(Suc N))"
proof -
  have *: "\N. \n. norm (X n) \ 1 + real N \
         \<exists>N. \<forall>n. norm (X n) < 1 + real N"
    by (metis add.commute le_less_trans less_add_one of_nat_Suc)
  then show ?thesis
    unfolding lemma_NBseq_def
    by (metis less_le_not_le not_less_iff_gr_or_eq of_nat_Suc)
qed

text \<open>Yet another definition for Bseq.\<close>
lemma Bseq_iff1a: "Bseq X \ (\N. \n. norm (X n) < real (Suc N))"
  by (simp add: Bseq_def lemma_NBseq_def2)

subsubsection \<open>A Few More Equivalence Theorems for Boundedness\<close>

text \<open>Alternative formulation for boundedness.\<close>
lemma Bseq_iff2: "Bseq X \ (\k > 0. \x. \n. norm (X n + - x) \ k)"
  by (metis BseqE BseqI' add.commute add_cancel_right_left add_uminus_conv_diff norm_add_leD
            norm_minus_cancel norm_minus_commute)

text \<open>Alternative formulation for boundedness.\<close>
lemma Bseq_iff3: "Bseq X \ (\k>0. \N. \n. norm (X n + - X N) \ k)"
  (is "?P \ ?Q")
proof
  assume ?P
  then obtain K where *: "0 < K" and **: "\n. norm (X n) \ K"
    by (auto simp: Bseq_def)
  from * have "0 < K + norm (X 0)" by (rule order_less_le_trans) simp
  from ** have "\n. norm (X n - X 0) \ K + norm (X 0)"
    by (auto intro: order_trans norm_triangle_ineq4)
  then have "\n. norm (X n + - X 0) \ K + norm (X 0)"
    by simp
  with \<open>0 < K + norm (X 0)\<close> show ?Q by blast
next
  assume ?Q
  then show ?P by (auto simp: Bseq_iff2)
qed

subsubsection \<open>Upper Bounds and Lubs of Bounded Sequences\<close>

lemma Bseq_minus_iff: "Bseq (\n. - (X n) :: 'a::real_normed_vector) \ Bseq X"
  by (simp add: Bseq_def)

lemma Bseq_add:
  fixes f :: "nat \ 'a::real_normed_vector"
  assumes "Bseq f"
  shows "Bseq (\x. f x + c)"
proof -
  from assms obtain K where K: "\x. norm (f x) \ K"
    unfolding Bseq_def by blast
  {
    fix x :: nat
    have "norm (f x + c) \ norm (f x) + norm c" by (rule norm_triangle_ineq)
    also have "norm (f x) \ K" by (rule K)
    finally have "norm (f x + c) \ K + norm c" by simp
  }
  then show ?thesis by (rule BseqI')
qed

lemma Bseq_add_iff: "Bseq (\x. f x + c) \ Bseq f"
  for f :: "nat \ 'a::real_normed_vector"
  using Bseq_add[of f c] Bseq_add[of "\x. f x + c" "-c"] by auto

lemma Bseq_mult:
  fixes f g :: "nat \ 'a::real_normed_field"
  assumes "Bseq f" and "Bseq g"
  shows "Bseq (\x. f x * g x)"
proof -
  from assms obtain K1 K2 where K: "norm (f x) \ K1" "K1 > 0" "norm (g x) \ K2" "K2 > 0"
    for x
    unfolding Bseq_def by blast
  then have "norm (f x * g x) \ K1 * K2" for x
    by (auto simp: norm_mult intro!: mult_mono)
  then show ?thesis by (rule BseqI')
qed

lemma Bfun_const [simp]: "Bfun (\_. c) F"
  unfolding Bfun_metric_def by (auto intro!: exI[of _ c] exI[of _ "1::real"])

lemma Bseq_cmult_iff:
  fixes c :: "'a::real_normed_field"
  assumes "c \ 0"
  shows "Bseq (\x. c * f x) \ Bseq f"
proof
  assume "Bseq (\x. c * f x)"
  with Bfun_const have "Bseq (\x. inverse c * (c * f x))"
    by (rule Bseq_mult)
  with \<open>c \<noteq> 0\<close> show "Bseq f"
    by (simp add: field_split_simps)
qed (intro Bseq_mult Bfun_const)

lemma Bseq_subseq: "Bseq f \ Bseq (\x. f (g x))"
  for f :: "nat \ 'a::real_normed_vector"
  unfolding Bseq_def by auto

lemma Bseq_Suc_iff: "Bseq (\n. f (Suc n)) \ Bseq f"
  for f :: "nat \ 'a::real_normed_vector"
  using Bseq_offset[of f 1] by (auto intro: Bseq_subseq)

lemma increasing_Bseq_subseq_iff:
  assumes "\x y. x \ y \ norm (f x :: 'a::real_normed_vector) \ norm (f y)" "strict_mono g"
  shows "Bseq (\x. f (g x)) \ Bseq f"
proof
  assume "Bseq (\x. f (g x))"
  then obtain K where K: "\x. norm (f (g x)) \ K"
    unfolding Bseq_def by auto
  {
    fix x :: nat
    from filterlim_subseq[OF assms(2)] obtain y where "g y \ x"
      by (auto simp: filterlim_at_top eventually_at_top_linorder)
    then have "norm (f x) \ norm (f (g y))"
      using assms(1) by blast
    also have "norm (f (g y)) \ K" by (rule K)
    finally have "norm (f x) \ K" .
  }
  then show "Bseq f" by (rule BseqI')
qed (use Bseq_subseq[of f g] in simp_all)

lemma nonneg_incseq_Bseq_subseq_iff:
  fixes f :: "nat \ real"
    and g :: "nat \ nat"
  assumes "\x. f x \ 0" "incseq f" "strict_mono g"
  shows "Bseq (\x. f (g x)) \ Bseq f"
  using assms by (intro increasing_Bseq_subseq_iff) (auto simp: incseq_def)

lemma Bseq_eq_bounded: "range f \ {a..b} \ Bseq f"
  for a b :: real
proof (rule BseqI'[where K="max (norm a) (norm b)"])
  fix n assume "range f \ {a..b}"
  then have "f n \ {a..b}"
    by blast
  then show "norm (f n) \ max (norm a) (norm b)"
    by auto
qed

lemma incseq_bounded: "incseq X \ \i. X i \ B \ Bseq X"
  for B :: real
  by (intro Bseq_eq_bounded[of X "X 0" B]) (auto simp: incseq_def)

lemma decseq_bounded: "decseq X \ \i. B \ X i \ Bseq X"
  for B :: real
  by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def)

subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Polynomal function extremal theorem, from HOL Light\<close>

lemma polyfun_extremal_lemma:
    fixes c :: "nat \ 'a::real_normed_div_algebra"
  assumes "0 < e"
    shows "\M. \z. M \ norm(z) \ norm (\i\n. c(i) * z^i) \ e * norm(z) ^ (Suc n)"
proof (induct n)
  case 0 with assms
  show ?case
    apply (rule_tac x="norm (c 0) / e" in exI)
    apply (auto simp: field_simps)
    done
next
  case (Suc n)
  obtain M where M: "\z. M \ norm z \ norm (\i\n. c i * z^i) \ e * norm z ^ Suc n"
    using Suc assms by blast
  show ?case
  proof (rule exI [where x= "max M (1 + norm(c(Suc n)) / e)"], clarsimp simp del: power_Suc)
    fix z::'a
    assume z1: "M \ norm z" and "1 + norm (c (Suc n)) / e \ norm z"
    then have z2: "e + norm (c (Suc n)) \ e * norm z"
      using assms by (simp add: field_simps)
    have "norm (\i\n. c i * z^i) \ e * norm z ^ Suc n"
      using M [OF z1] by simp
    then have "norm (\i\n. c i * z^i) + norm (c (Suc n) * z ^ Suc n) \ e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)"
      by simp
    then have "norm ((\i\n. c i * z^i) + c (Suc n) * z ^ Suc n) \ e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)"
      by (blast intro: norm_triangle_le elim: )
    also have "... \ (e + norm (c (Suc n))) * norm z ^ Suc n"
      by (simp add: norm_power norm_mult algebra_simps)
    also have "... \ (e * norm z) * norm z ^ Suc n"
      by (metis z2 mult.commute mult_left_mono norm_ge_zero norm_power)
    finally show "norm ((\i\n. c i * z^i) + c (Suc n) * z ^ Suc n) \ e * norm z ^ Suc (Suc n)"
      by simp
  qed
qed

lemma polyfun_extremal: (*COMPLEX_POLYFUN_EXTREMAL in HOL Light*)
    fixes c :: "nat \ 'a::real_normed_div_algebra"
  assumes k: "c k \ 0" "1\k" and kn: "k\n"
    shows "eventually (\z. norm (\i\n. c(i) * z^i) \ B) at_infinity"
using kn
proof (induction n)
  case 0
  then show ?case
    using k by simp
next
  case (Suc m)
  show ?case
  proof (cases "c (Suc m) = 0")
    case True
    then show ?thesis using Suc k
      by auto (metis antisym_conv less_eq_Suc_le not_le)
  next
    case False
    then obtain M where M:
          "\z. M \ norm z \ norm (\i\m. c i * z^i) \ norm (c (Suc m)) / 2 * norm z ^ Suc m"
      using polyfun_extremal_lemma [of "norm(c (Suc m)) / 2" c m] Suc
      by auto
    have "\b. \z. b \ norm z \ B \ norm (\i\Suc m. c i * z^i)"
    proof (rule exI [where x="max M (max 1 (\B\ / (norm(c (Suc m)) / 2)))"], clarsimp simp del: power_Suc)
      fix z::'a
      assume z1: "M \ norm z" "1 \ norm z"
         and "\B\ * 2 / norm (c (Suc m)) \ norm z"
      then have z2: "\B\ \ norm (c (Suc m)) * norm z / 2"
        using False by (simp add: field_simps)
      have nz: "norm z \ norm z ^ Suc m"
        by (metis \<open>1 \<le> norm z\<close> One_nat_def less_eq_Suc_le power_increasing power_one_right zero_less_Suc)
      have *: "\y x. norm (c (Suc m)) * norm z / 2 \ norm y - norm x \ B \ norm (x + y)"
        by (metis abs_le_iff add.commute norm_diff_ineq order_trans z2)
      have "norm z * norm (c (Suc m)) + 2 * norm (\i\m. c i * z^i)
            \<le> norm (c (Suc m)) * norm z + norm (c (Suc m)) * norm z ^ Suc m"
        using M [of z] Suc z1  by auto
      also have "... \ 2 * (norm (c (Suc m)) * norm z ^ Suc m)"
        using nz by (simp add: mult_mono del: power_Suc)
      finally show "B \ norm ((\i\m. c i * z^i) + c (Suc m) * z ^ Suc m)"
        using Suc.IH
        apply (auto simp: eventually_at_infinity)
        apply (rule *)
        apply (simp add: field_simps norm_mult norm_power)
        done
    qed
    then show ?thesis
      by (simp add: eventually_at_infinity)
  qed
qed

subsection \<open>Convergence to Zero\<close>

definition Zfun :: "('a \ 'b::real_normed_vector) \ 'a filter \ bool"
  where "Zfun f F = (\r>0. eventually (\x. norm (f x) < r) F)"

lemma ZfunI: "(\r. 0 < r \ eventually (\x. norm (f x) < r) F) \ Zfun f F"
  by (simp add: Zfun_def)

lemma ZfunD: "Zfun f F \ 0 < r \ eventually (\x. norm (f x) < r) F"
  by (simp add: Zfun_def)

lemma Zfun_ssubst: "eventually (\x. f x = g x) F \ Zfun g F \ Zfun f F"
  unfolding Zfun_def by (auto elim!: eventually_rev_mp)

lemma Zfun_zero: "Zfun (\x. 0) F"
  unfolding Zfun_def by simp

lemma Zfun_norm_iff: "Zfun (\x. norm (f x)) F = Zfun (\x. f x) F"
  unfolding Zfun_def by simp

lemma Zfun_imp_Zfun:
  assumes f: "Zfun f F"
    and g: "eventually (\x. norm (g x) \ norm (f x) * K) F"
  shows "Zfun (\x. g x) F"
proof (cases "0 < K")
  case K: True
  show ?thesis
  proof (rule ZfunI)
    fix r :: real
    assume "0 < r"
    then have "0 < r / K" using K by simp
    then have "eventually (\x. norm (f x) < r / K) F"
      using ZfunD [OF f] by blast
    with g show "eventually (\x. norm (g x) < r) F"
    proof eventually_elim
      case (elim x)
      then have "norm (f x) * K < r"
        by (simp add: pos_less_divide_eq K)
      then show ?case
        by (simp add: order_le_less_trans [OF elim(1)])
    qed
  qed
next
  case False
  then have K: "K \ 0" by (simp only: not_less)
  show ?thesis
  proof (rule ZfunI)
    fix r :: real
    assume "0 < r"
    from g show "eventually (\x. norm (g x) < r) F"
    proof eventually_elim
      case (elim x)
      also have "norm (f x) * K \ norm (f x) * 0"
        using K norm_ge_zero by (rule mult_left_mono)
      finally show ?case
        using \<open>0 < r\<close> by simp
    qed
  qed
qed

lemma Zfun_le: "Zfun g F \ \x. norm (f x) \ norm (g x) \ Zfun f F"
  by (erule Zfun_imp_Zfun [where K = 1]) simp

lemma Zfun_add:
  assumes f: "Zfun f F"
    and g: "Zfun g F"
  shows "Zfun (\x. f x + g x) F"
proof (rule ZfunI)
  fix r :: real
  assume "0 < r"
  then have r: "0 < r / 2" by simp
  have "eventually (\x. norm (f x) < r/2) F"
    using f r by (rule ZfunD)
  moreover
  have "eventually (\x. norm (g x) < r/2) F"
    using g r by (rule ZfunD)
  ultimately
  show "eventually (\x. norm (f x + g x) < r) F"
  proof eventually_elim
    case (elim x)
    have "norm (f x + g x) \ norm (f x) + norm (g x)"
      by (rule norm_triangle_ineq)
    also have "\ < r/2 + r/2"
      using elim by (rule add_strict_mono)
    finally show ?case
      by simp
  qed
qed

lemma Zfun_minus: "Zfun f F \ Zfun (\x. - f x) F"
  unfolding Zfun_def by simp

lemma Zfun_diff: "Zfun f F \ Zfun g F \ Zfun (\x. f x - g x) F"
  using Zfun_add [of f F "\x. - g x"] by (simp add: Zfun_minus)

lemma (in bounded_linear) Zfun:
  assumes g: "Zfun g F"
  shows "Zfun (\x. f (g x)) F"
proof -
  obtain K where "norm (f x) \ norm x * K" for x
    using bounded by blast
  then have "eventually (\x. norm (f (g x)) \ norm (g x) * K) F"
    by simp
  with g show ?thesis
    by (rule Zfun_imp_Zfun)
qed

lemma (in bounded_bilinear) Zfun:
  assumes f: "Zfun f F"
    and g: "Zfun g F"
  shows "Zfun (\x. f x ** g x) F"
proof (rule ZfunI)
  fix r :: real
  assume r: "0 < r"
  obtain K where K: "0 < K"
    and norm_le: "norm (x ** y) \ norm x * norm y * K" for x y
    using pos_bounded by blast
  from K have K': "0 < inverse K"
    by (rule positive_imp_inverse_positive)
  have "eventually (\x. norm (f x) < r) F"
    using f r by (rule ZfunD)
  moreover
  have "eventually (\x. norm (g x) < inverse K) F"
    using g K' by (rule ZfunD)
  ultimately
  show "eventually (\x. norm (f x ** g x) < r) F"
  proof eventually_elim
    case (elim x)
    have "norm (f x ** g x) \ norm (f x) * norm (g x) * K"
      by (rule norm_le)
    also have "norm (f x) * norm (g x) * K < r * inverse K * K"
      by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero elim K)
    also from K have "r * inverse K * K = r"
      by simp
    finally show ?case .
  qed
qed

lemma (in bounded_bilinear) Zfun_left: "Zfun f F \ Zfun (\x. f x ** a) F"
  by (rule bounded_linear_left [THEN bounded_linear.Zfun])

lemma (in bounded_bilinear) Zfun_right: "Zfun f F \ Zfun (\x. a ** f x) F"
  by (rule bounded_linear_right [THEN bounded_linear.Zfun])

lemmas Zfun_mult = bounded_bilinear.Zfun [OF bounded_bilinear_mult]
lemmas Zfun_mult_right = bounded_bilinear.Zfun_right [OF bounded_bilinear_mult]
lemmas Zfun_mult_left = bounded_bilinear.Zfun_left [OF bounded_bilinear_mult]

lemma tendsto_Zfun_iff: "(f \ a) F = Zfun (\x. f x - a) F"
  by (simp only: tendsto_iff Zfun_def dist_norm)

lemma tendsto_0_le:
  "(f \ 0) F \ eventually (\x. norm (g x) \ norm (f x) * K) F \ (g \ 0) F"
  by (simp add: Zfun_imp_Zfun tendsto_Zfun_iff)

subsubsection \<open>Distance and norms\<close>

lemma tendsto_dist [tendsto_intros]:
  fixes l m :: "'a::metric_space"
  assumes f: "(f \ l) F"
    and g: "(g \ m) F"
  shows "((\x. dist (f x) (g x)) \ dist l m) F"
proof (rule tendstoI)
  fix e :: real
  assume "0 < e"
  then have e2: "0 < e/2" by simp
  from tendstoD [OF f e2] tendstoD [OF g e2]
  show "eventually (\x. dist (dist (f x) (g x)) (dist l m) < e) F"
  proof (eventually_elim)
    case (elim x)
    then show "dist (dist (f x) (g x)) (dist l m) < e"
      unfolding dist_real_def
      using dist_triangle2 [of "f x" "g x" "l"]
        and dist_triangle2 [of "g x" "l" "m"]
        and dist_triangle3 [of "l" "m" "f x"]
        and dist_triangle [of "f x" "m" "g x"]
      by arith
  qed
qed

lemma continuous_dist[continuous_intros]:
  fixes f g :: "_ \ 'a :: metric_space"
  shows "continuous F f \ continuous F g \ continuous F (\x. dist (f x) (g x))"
  unfolding continuous_def by (rule tendsto_dist)

lemma continuous_on_dist[continuous_intros]:
  fixes f g :: "_ \ 'a :: metric_space"
  shows "continuous_on s f \ continuous_on s g \ continuous_on s (\x. dist (f x) (g x))"
  unfolding continuous_on_def by (auto intro: tendsto_dist)

lemma continuous_at_dist: "isCont (dist a) b"
  using continuous_on_dist [OF continuous_on_const continuous_on_id] continuous_on_eq_continuous_within by blast

lemma tendsto_norm [tendsto_intros]: "(f \ a) F \ ((\x. norm (f x)) \ norm a) F"
  unfolding norm_conv_dist by (intro tendsto_intros)

lemma continuous_norm [continuous_intros]: "continuous F f \ continuous F (\x. norm (f x))"
  unfolding continuous_def by (rule tendsto_norm)

lemma continuous_on_norm [continuous_intros]:
  "continuous_on s f \ continuous_on s (\x. norm (f x))"
  unfolding continuous_on_def by (auto intro: tendsto_norm)

lemma continuous_on_norm_id [continuous_intros]: "continuous_on S norm"
  by (intro continuous_on_id continuous_on_norm)

lemma tendsto_norm_zero: "(f \ 0) F \ ((\x. norm (f x)) \ 0) F"
  by (drule tendsto_norm) simp

lemma tendsto_norm_zero_cancel: "((\x. norm (f x)) \ 0) F \ (f \ 0) F"
  unfolding tendsto_iff dist_norm by simp

lemma tendsto_norm_zero_iff: "((\x. norm (f x)) \ 0) F \ (f \ 0) F"
  unfolding tendsto_iff dist_norm by simp

lemma tendsto_rabs [tendsto_intros]: "(f \ l) F \ ((\x. \f x\) \ \l\) F"
  for l :: real
  by (fold real_norm_def) (rule tendsto_norm)

lemma continuous_rabs [continuous_intros]:
  "continuous F f \ continuous F (\x. \f x :: real\)"
  unfolding real_norm_def[symmetric] by (rule continuous_norm)

lemma continuous_on_rabs [continuous_intros]:
  "continuous_on s f \ continuous_on s (\x. \f x :: real\)"
  unfolding real_norm_def[symmetric] by (rule continuous_on_norm)

lemma tendsto_rabs_zero: "(f \ (0::real)) F \ ((\x. \f x\) \ 0) F"
  by (fold real_norm_def) (rule tendsto_norm_zero)

lemma tendsto_rabs_zero_cancel: "((\x. \f x\) \ (0::real)) F \ (f \ 0) F"
  by (fold real_norm_def) (rule tendsto_norm_zero_cancel)

lemma tendsto_rabs_zero_iff: "((\x. \f x\) \ (0::real)) F \ (f \ 0) F"
  by (fold real_norm_def) (rule tendsto_norm_zero_iff)

subsection \<open>Topological Monoid\<close>

class topological_monoid_add = topological_space + monoid_add +
  assumes tendsto_add_Pair: "LIM x (nhds a \\<^sub>F nhds b). fst x + snd x :> nhds (a + b)"

class topological_comm_monoid_add = topological_monoid_add + comm_monoid_add

lemma tendsto_add [tendsto_intros]:
  fixes a b :: "'a::topological_monoid_add"
  shows "(f \ a) F \ (g \ b) F \ ((\x. f x + g x) \ a + b) F"
  using filterlim_compose[OF tendsto_add_Pair, of "\x. (f x, g x)" a b F]
  by (simp add: nhds_prod[symmetric] tendsto_Pair)

lemma continuous_add [continuous_intros]:
  fixes f g :: "_ \ 'b::topological_monoid_add"
  shows "continuous F f \ continuous F g \ continuous F (\x. f x + g x)"
  unfolding continuous_def by (rule tendsto_add)

lemma continuous_on_add [continuous_intros]:
  fixes f g :: "_ \ 'b::topological_monoid_add"
  shows "continuous_on s f \ continuous_on s g \ continuous_on s (\x. f x + g x)"
  unfolding continuous_on_def by (auto intro: tendsto_add)

lemma tendsto_add_zero:
  fixes f g :: "_ \ 'b::topological_monoid_add"
  shows "(f \ 0) F \ (g \ 0) F \ ((\x. f x + g x) \ 0) F"
  by (drule (1) tendsto_add) simp

lemma tendsto_sum [tendsto_intros]:
  fixes f :: "'a \ 'b \ 'c::topological_comm_monoid_add"
  shows "(\i. i \ I \ (f i \ a i) F) \ ((\x. \i\I. f i x) \ (\i\I. a i)) F"
  by (induct I rule: infinite_finite_induct) (simp_all add: tendsto_add)

lemma tendsto_null_sum:
  fixes f :: "'a \ 'b \ 'c::topological_comm_monoid_add"
  assumes "\i. i \ I \ ((\x. f x i) \ 0) F"
  shows "((\i. sum (f i) I) \ 0) F"
  using tendsto_sum [of I "\x y. f y x" "\x. 0"] assms by simp

lemma continuous_sum [continuous_intros]:
  fixes f :: "'a \ 'b::t2_space \ 'c::topological_comm_monoid_add"
  shows "(\i. i \ I \ continuous F (f i)) \ continuous F (\x. \i\I. f i x)"
  unfolding continuous_def by (rule tendsto_sum)

lemma continuous_on_sum [continuous_intros]:
  fixes f :: "'a \ 'b::topological_space \ 'c::topological_comm_monoid_add"
  shows "(\i. i \ I \ continuous_on S (f i)) \ continuous_on S (\x. \i\I. f i x)"
  unfolding continuous_on_def by (auto intro: tendsto_sum)

instance nat :: topological_comm_monoid_add
  by standard
    (simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal)

instance int :: topological_comm_monoid_add
  by standard
    (simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal)

subsubsection \<open>Topological group\<close>

class topological_group_add = topological_monoid_add + group_add +
  assumes tendsto_uminus_nhds: "(uminus \ - a) (nhds a)"
begin

lemma tendsto_minus [tendsto_intros]: "(f \ a) F \ ((\x. - f x) \ - a) F"
  by (rule filterlim_compose[OF tendsto_uminus_nhds])

end

class topological_ab_group_add = topological_group_add + ab_group_add

instance topological_ab_group_add < topological_comm_monoid_add ..

lemma continuous_minus [continuous_intros]: "continuous F f \ continuous F (\x. - f x)"
  for f :: "'a::t2_space \ 'b::topological_group_add"
  unfolding continuous_def by (rule tendsto_minus)

lemma continuous_on_minus [continuous_intros]: "continuous_on s f \ continuous_on s (\x. - f x)"
  for f :: "_ \ 'b::topological_group_add"
  unfolding continuous_on_def by (auto intro: tendsto_minus)

lemma tendsto_minus_cancel: "((\x. - f x) \ - a) F \ (f \ a) F"
  for a :: "'a::topological_group_add"
  by (drule tendsto_minus) simp

lemma tendsto_minus_cancel_left:
  "(f \ - (y::_::topological_group_add)) F \ ((\x. - f x) \ y) F"
  using tendsto_minus_cancel[of f "- y" F]  tendsto_minus[of f "- y" F]
  by auto

lemma tendsto_diff [tendsto_intros]:
  fixes a b :: "'a::topological_group_add"
  shows "(f \ a) F \ (g \ b) F \ ((\x. f x - g x) \ a - b) F"
  using tendsto_add [of f a F "\x. - g x" "- b"] by (simp add: tendsto_minus)

lemma continuous_diff [continuous_intros]:
  fixes f g :: "'a::t2_space \ 'b::topological_group_add"
  shows "continuous F f \ continuous F g \ continuous F (\x. f x - g x)"
  unfolding continuous_def by (rule tendsto_diff)

lemma continuous_on_diff [continuous_intros]:
  fixes f g :: "_ \ 'b::topological_group_add"
  shows "continuous_on s f \ continuous_on s g \ continuous_on s (\x. f x - g x)"
  unfolding continuous_on_def by (auto intro: tendsto_diff)

lemma continuous_on_op_minus: "continuous_on (s::'a::topological_group_add set) ((-) x)"
  by (rule continuous_intros | simp)+

instance real_normed_vector < topological_ab_group_add
proof
  fix a b :: 'a
  show "((\x. fst x + snd x) \ a + b) (nhds a \\<^sub>F nhds b)"
    unfolding tendsto_Zfun_iff add_diff_add
    using tendsto_fst[OF filterlim_ident, of "(a,b)"] tendsto_snd[OF filterlim_ident, of "(a,b)"]
    by (intro Zfun_add)
       (auto simp: tendsto_Zfun_iff[symmetric] nhds_prod[symmetric] intro!: tendsto_fst)
  show "(uminus \ - a) (nhds a)"
    unfolding tendsto_Zfun_iff minus_diff_minus
    using filterlim_ident[of "nhds a"]
    by (intro Zfun_minus) (simp add: tendsto_Zfun_iff)
qed

lemmas real_tendsto_sandwich = tendsto_sandwich[where 'a=real]

subsubsection \<open>Linear operators and multiplication\<close>

lemma linear_times [simp]: "linear (\x. c * x)"
  for c :: "'a::real_algebra"
  by (auto simp: linearI distrib_left)

lemma (in bounded_linear) tendsto: "(g \ a) F \ ((\x. f (g x)) \ f a) F"
  by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)

lemma (in bounded_linear) continuous: "continuous F g \ continuous F (\x. f (g x))"
  using tendsto[of g _ F] by (auto simp: continuous_def)

lemma (in bounded_linear) continuous_on: "continuous_on s g \ continuous_on s (\x. f (g x))"
  using tendsto[of g] by (auto simp: continuous_on_def)

lemma (in bounded_linear) tendsto_zero: "(g \ 0) F \ ((\x. f (g x)) \ 0) F"
  by (drule tendsto) (simp only: zero)

lemma (in bounded_bilinear) tendsto:
  "(f \ a) F \ (g \ b) F \ ((\x. f x ** g x) \ a ** b) F"
  by (simp only: tendsto_Zfun_iff prod_diff_prod Zfun_add Zfun Zfun_left Zfun_right)

lemma (in bounded_bilinear) continuous:
  "continuous F f \ continuous F g \ continuous F (\x. f x ** g x)"
  using tendsto[of f _ F g] by (auto simp: continuous_def)

lemma (in bounded_bilinear) continuous_on:
  "continuous_on s f \ continuous_on s g \ continuous_on s (\x. f x ** g x)"
  using tendsto[of f _ _ g] by (auto simp: continuous_on_def)

lemma (in bounded_bilinear) tendsto_zero:
  assumes f: "(f \ 0) F"
    and g: "(g \ 0) F"
  shows "((\x. f x ** g x) \ 0) F"
  using tendsto [OF f g] by (simp add: zero_left)

lemma (in bounded_bilinear) tendsto_left_zero:
  "(f \ 0) F \ ((\x. f x ** c) \ 0) F"
  by (rule bounded_linear.tendsto_zero [OF bounded_linear_left])

lemma (in bounded_bilinear) tendsto_right_zero:
  "(f \ 0) F \ ((\x. c ** f x) \ 0) F"
  by (rule bounded_linear.tendsto_zero [OF bounded_linear_right])

lemmas tendsto_of_real [tendsto_intros] =
  bounded_linear.tendsto [OF bounded_linear_of_real]

lemmas tendsto_scaleR [tendsto_intros] =
  bounded_bilinear.tendsto [OF bounded_bilinear_scaleR]

text\<open>Analogous type class for multiplication\<close>
class topological_semigroup_mult = topological_space + semigroup_mult +
  assumes tendsto_mult_Pair: "LIM x (nhds a \\<^sub>F nhds b). fst x * snd x :> nhds (a * b)"

instance real_normed_algebra < topological_semigroup_mult
proof
  fix a b :: 'a
  show "((\x. fst x * snd x) \ a * b) (nhds a \\<^sub>F nhds b)"
    unfolding nhds_prod[symmetric]
    using tendsto_fst[OF filterlim_ident, of "(a,b)"] tendsto_snd[OF filterlim_ident, of "(a,b)"]
    by (simp add: bounded_bilinear.tendsto [OF bounded_bilinear_mult])
qed

lemma tendsto_mult [tendsto_intros]:
  fixes a b :: "'a::topological_semigroup_mult"
  shows "(f \ a) F \ (g \ b) F \ ((\x. f x * g x) \ a * b) F"
  using filterlim_compose[OF tendsto_mult_Pair, of "\x. (f x, g x)" a b F]
  by (simp add: nhds_prod[symmetric] tendsto_Pair)

lemma tendsto_mult_left: "(f \ l) F \ ((\x. c * (f x)) \ c * l) F"
  for c :: "'a::topological_semigroup_mult"
  by (rule tendsto_mult [OF tendsto_const])

lemma tendsto_mult_right: "(f \ l) F \ ((\x. (f x) * c) \ l * c) F"
  for c :: "'a::topological_semigroup_mult"
  by (rule tendsto_mult [OF _ tendsto_const])

lemma tendsto_mult_left_iff [simp]:
   "c \ 0 \ tendsto(\x. c * f x) (c * l) F \ tendsto f l F" for c :: "'a::{topological_semigroup_mult,field}"
  by (auto simp: tendsto_mult_left dest: tendsto_mult_left [where c = "1/c"])

lemma tendsto_mult_right_iff [simp]:
   "c \ 0 \ tendsto(\x. f x * c) (l * c) F \ tendsto f l F" for c :: "'a::{topological_semigroup_mult,field}"
  by (auto simp: tendsto_mult_right dest: tendsto_mult_left [where c = "1/c"])

lemma tendsto_zero_mult_left_iff [simp]:
  fixes c::"'a::{topological_semigroup_mult,field}" assumes "c \ 0" shows "(\n. c * a n)\ 0 \ a \ 0"
  using assms tendsto_mult_left tendsto_mult_left_iff by fastforce

lemma tendsto_zero_mult_right_iff [simp]:
  fixes c::"'a::{topological_semigroup_mult,field}" assumes "c \ 0" shows "(\n. a n * c)\ 0 \ a \ 0"
  using assms tendsto_mult_right tendsto_mult_right_iff by fastforce

lemma tendsto_zero_divide_iff [simp]:
  fixes c::"'a::{topological_semigroup_mult,field}" assumes "c \ 0" shows "(\n. a n / c)\ 0 \ a \ 0"
  using tendsto_zero_mult_right_iff [of "1/c" a] assms by (simp add: field_simps)

lemma lim_const_over_n [tendsto_intros]:
  fixes a :: "'a::real_normed_field"
  shows "(\n. a / of_nat n) \ 0"
  using tendsto_mult [OF tendsto_const [of a] lim_1_over_n] by simp

lemmas continuous_of_real [continuous_intros] =
  bounded_linear.continuous [OF bounded_linear_of_real]

lemmas continuous_scaleR [continuous_intros] =
  bounded_bilinear.continuous [OF bounded_bilinear_scaleR]

lemmas continuous_mult [continuous_intros] =
  bounded_bilinear.continuous [OF bounded_bilinear_mult]

lemmas continuous_on_of_real [continuous_intros] =
  bounded_linear.continuous_on [OF bounded_linear_of_real]

lemmas continuous_on_scaleR [continuous_intros] =
  bounded_bilinear.continuous_on [OF bounded_bilinear_scaleR]

lemmas continuous_on_mult [continuous_intros] =
  bounded_bilinear.continuous_on [OF bounded_bilinear_mult]

lemmas tendsto_mult_zero =
  bounded_bilinear.tendsto_zero [OF bounded_bilinear_mult]

lemmas tendsto_mult_left_zero =
  bounded_bilinear.tendsto_left_zero [OF bounded_bilinear_mult]

lemmas tendsto_mult_right_zero =
  bounded_bilinear.tendsto_right_zero [OF bounded_bilinear_mult]

lemma continuous_mult_left:
  fixes c::"'a::real_normed_algebra"
  shows "continuous F f \ continuous F (\x. c * f x)"
by (rule continuous_mult [OF continuous_const])

lemma continuous_mult_right:
  fixes c::"'a::real_normed_algebra"
  shows "continuous F f \ continuous F (\x. f x * c)"
by (rule continuous_mult [OF _ continuous_const])

lemma continuous_on_mult_left:
  fixes c::"'a::real_normed_algebra"
  shows "continuous_on s f \ continuous_on s (\x. c * f x)"
by (rule continuous_on_mult [OF continuous_on_const])

lemma continuous_on_mult_right:
  fixes c::"'a::real_normed_algebra"
  shows "continuous_on s f \ continuous_on s (\x. f x * c)"
by (rule continuous_on_mult [OF _ continuous_on_const])

lemma continuous_on_mult_const [simp]:
  fixes c::"'a::real_normed_algebra"
  shows "continuous_on s ((*) c)"
  by (intro continuous_on_mult_left continuous_on_id)

lemma tendsto_divide_zero:
  fixes c :: "'a::real_normed_field"
  shows "(f \ 0) F \ ((\x. f x / c) \ 0) F"
  by (cases "c=0") (simp_all add: divide_inverse tendsto_mult_left_zero)

lemma tendsto_power [tendsto_intros]: "(f \ a) F \ ((\x. f x ^ n) \ a ^ n) F"
  for f :: "'a \ 'b::{power,real_normed_algebra}"
  by (induct n) (simp_all add: tendsto_mult)

lemma tendsto_null_power: "\(f \ 0) F; 0 < n\ \ ((\x. f x ^ n) \ 0) F"
    for f :: "'a \ 'b::{power,real_normed_algebra_1}"
  using tendsto_power [of f 0 F n] by (simp add: power_0_left)

lemma continuous_power [continuous_intros]: "continuous F f \ continuous F (\x. (f x)^n)"
  for f :: "'a::t2_space \ 'b::{power,real_normed_algebra}"
  unfolding continuous_def by (rule tendsto_power)

lemma continuous_on_power [continuous_intros]:
  fixes f :: "_ \ 'b::{power,real_normed_algebra}"
  shows "continuous_on s f \ continuous_on s (\x. (f x)^n)"
  unfolding continuous_on_def by (auto intro: tendsto_power)

lemma tendsto_prod [tendsto_intros]:
  fixes f :: "'a \ 'b \ 'c::{real_normed_algebra,comm_ring_1}"
  shows "(\i. i \ S \ (f i \ L i) F) \ ((\x. \i\S. f i x) \ (\i\S. L i)) F"
  by (induct S rule: infinite_finite_induct) (simp_all add: tendsto_mult)

lemma continuous_prod [continuous_intros]:
  fixes f :: "'a \ 'b::t2_space \ 'c::{real_normed_algebra,comm_ring_1}"
  shows "(\i. i \ S \ continuous F (f i)) \ continuous F (\x. \i\S. f i x)"
  unfolding continuous_def by (rule tendsto_prod)

lemma continuous_on_prod [continuous_intros]:
  fixes f :: "'a \ _ \ 'c::{real_normed_algebra,comm_ring_1}"
  shows "(\i. i \ S \ continuous_on s (f i)) \ continuous_on s (\x. \i\S. f i x)"
  unfolding continuous_on_def by (auto intro: tendsto_prod)

lemma tendsto_of_real_iff:
  "((\x. of_real (f x) :: 'a::real_normed_div_algebra) \ of_real c) F \ (f \ c) F"
  unfolding tendsto_iff by simp

lemma tendsto_add_const_iff:
  "((\x. c + f x :: 'a::topological_group_add) \ c + d) F \ (f \ d) F"
  using tendsto_add[OF tendsto_const[of c], of f d]
    and tendsto_add[OF tendsto_const[of "-c"], of "\x. c + f x" "c + d"] by auto

class topological_monoid_mult = topological_semigroup_mult + monoid_mult
class topological_comm_monoid_mult = topological_monoid_mult + comm_monoid_mult

lemma tendsto_power_strong [tendsto_intros]:
  fixes f :: "_ \ 'b :: topological_monoid_mult"
  assumes "(f \ a) F" "(g \ b) F"
  shows   "((\x. f x ^ g x) \ a ^ b) F"
proof -
  have "((\x. f x ^ b) \ a ^ b) F"
    by (induction b) (auto intro: tendsto_intros assms)
  also from assms(2) have "eventually (\x. g x = b) F"
    by (simp add: nhds_discrete filterlim_principal)
  hence "eventually (\x. f x ^ b = f x ^ g x) F"
    by eventually_elim simp
  hence "((\x. f x ^ b) \ a ^ b) F \ ((\x. f x ^ g x) \ a ^ b) F"
    by (intro filterlim_cong refl)
  finally show ?thesis .
qed

lemma continuous_mult' [continuous_intros]:
  fixes f g :: "_ \ 'b::topological_semigroup_mult"
  shows "continuous F f \ continuous F g \ continuous F (\x. f x * g x)"
  unfolding continuous_def by (rule tendsto_mult)

lemma continuous_power' [continuous_intros]:
  fixes f :: "_ \ 'b::topological_monoid_mult"
  shows "continuous F f \ continuous F g \ continuous F (\x. f x ^ g x)"
  unfolding continuous_def by (rule tendsto_power_strong) auto

lemma continuous_on_mult' [continuous_intros]:
  fixes f g :: "_ \ 'b::topological_semigroup_mult"
  shows "continuous_on A f \ continuous_on A g \ continuous_on A (\x. f x * g x)"
  unfolding continuous_on_def by (auto intro: tendsto_mult)

lemma continuous_on_power' [continuous_intros]:
  fixes f :: "_ \ 'b::topological_monoid_mult"
  shows "continuous_on A f \ continuous_on A g \ continuous_on A (\x. f x ^ g x)"
  unfolding continuous_on_def by (auto intro: tendsto_power_strong)

lemma tendsto_mult_one:
  fixes f g :: "_ \ 'b::topological_monoid_mult"
  shows "(f \ 1) F \ (g \ 1) F \ ((\x. f x * g x) \ 1) F"
  by (drule (1) tendsto_mult) simp

lemma tendsto_prod' [tendsto_intros]:
  fixes f :: "'a \ 'b \ 'c::topological_comm_monoid_mult"
  shows "(\i. i \ I \ (f i \ a i) F) \ ((\x. \i\I. f i x) \ (\i\I. a i)) F"
  by (induct I rule: infinite_finite_induct) (simp_all add: tendsto_mult)

lemma tendsto_one_prod':
  fixes f :: "'a \ 'b \ 'c::topological_comm_monoid_mult"
  assumes "\i. i \ I \ ((\x. f x i) \ 1) F"
  shows "((\i. prod (f i) I) \ 1) F"
  using tendsto_prod' [of I "\x y. f y x" "\x. 1"] assms by simp

lemma LIMSEQ_prod_0:
  fixes f :: "nat \ 'a::{semidom,topological_space}"
  assumes "f i = 0"
  shows "(\n. prod f {..n}) \ 0"
proof (subst tendsto_cong)
  show "\\<^sub>F n in sequentially. prod f {..n} = 0"
    using assms eventually_at_top_linorder by auto
qed auto

lemma LIMSEQ_prod_nonneg:
  fixes f :: "nat \ 'a::{linordered_semidom,linorder_topology}"
  assumes 0: "\n. 0 \ f n" and a: "(\n. prod f {..n}) \ a"
  shows "a \ 0"
  by (simp add: "0" prod_nonneg LIMSEQ_le_const [OF a])

lemma continuous_prod' [continuous_intros]:
  fixes f :: "'a \ 'b::t2_space \ 'c::topological_comm_monoid_mult"
  shows "(\i. i \ I \ continuous F (f i)) \ continuous F (\x. \i\I. f i x)"
  unfolding continuous_def by (rule tendsto_prod')

lemma continuous_on_prod' [continuous_intros]:
  fixes f :: "'a \ 'b::topological_space \ 'c::topological_comm_monoid_mult"
  shows "(\i. i \ I \ continuous_on S (f i)) \ continuous_on S (\x. \i\I. f i x)"
  unfolding continuous_on_def by (auto intro: tendsto_prod')

instance nat :: topological_comm_monoid_mult
  by standard
    (simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal)

instance int :: topological_comm_monoid_mult
  by standard
    (simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal)

class comm_real_normed_algebra_1 = real_normed_algebra_1 + comm_monoid_mult

context real_normed_field
begin

subclass comm_real_normed_algebra_1
proof
  from norm_mult[of "1 :: 'a" 1] show "norm 1 = 1" by simp
qed (simp_all add: norm_mult)

end

subsubsection \<open>Inverse and division\<close>

lemma (in bounded_bilinear) Zfun_prod_Bfun:
  assumes f: "Zfun f F"
    and g: "Bfun g F"
  shows "Zfun (\x. f x ** g x) F"
proof -
  obtain K where K: "0 \ K"
    and norm_le: "\x y. norm (x ** y) \ norm x * norm y * K"
    using nonneg_bounded by blast
  obtain B where B: "0 < B"
    and norm_g: "eventually (\x. norm (g x) \ B) F"
    using g by (rule BfunE)
  have "eventually (\x. norm (f x ** g x) \ norm (f x) * (B * K)) F"
  using norm_g proof eventually_elim
    case (elim x)
    have "norm (f x ** g x) \ norm (f x) * norm (g x) * K"
      by (rule norm_le)
    also have "\ \ norm (f x) * B * K"
      by (intro mult_mono' order_refl norm_g norm_ge_zero mult_nonneg_nonneg K elim)
    also have "\ = norm (f x) * (B * K)"
      by (rule mult.assoc)
    finally show "norm (f x ** g x) \ norm (f x) * (B * K)" .
  qed
  with f show ?thesis
    by (rule Zfun_imp_Zfun)
qed

lemma (in bounded_bilinear) Bfun_prod_Zfun:
  assumes f: "Bfun f F"
    and g: "Zfun g F"
  shows "Zfun (\x. f x ** g x) F"
  using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun)

lemma Bfun_inverse:
  fixes a :: "'a::real_normed_div_algebra"
  assumes f: "(f \ a) F"
  assumes a: "a \ 0"
  shows "Bfun (\x. inverse (f x)) F"
proof -
  from a have "0 < norm a" by simp
  then have "\r>0. r < norm a" by (rule dense)
  then obtain r where r1: "0 < r" and r2: "r < norm a"
    by blast
  have "eventually (\x. dist (f x) a < r) F"
    using tendstoD [OF f r1] by blast
  then have "eventually (\x. norm (inverse (f x)) \ inverse (norm a - r)) F"
  proof eventually_elim
    case (elim x)
    then have 1: "norm (f x - a) < r"
      by (simp add: dist_norm)
    then have 2: "f x \ 0" using r2 by auto
    then have "norm (inverse (f x)) = inverse (norm (f x))"
      by (rule nonzero_norm_inverse)
    also have "\ \ inverse (norm a - r)"
    proof (rule le_imp_inverse_le)
      show "0 < norm a - r"
        using r2 by simp
      have "norm a - norm (f x) \ norm (a - f x)"
        by (rule norm_triangle_ineq2)
      also have "\ = norm (f x - a)"
        by (rule norm_minus_commute)
      also have "\ < r" using 1 .
      finally show "norm a - r \ norm (f x)"
        by simp
    qed
    finally show "norm (inverse (f x)) \ inverse (norm a - r)" .
  qed
  then show ?thesis by (rule BfunI)
qed

lemma tendsto_inverse [tendsto_intros]:
  fixes a :: "'a::real_normed_div_algebra"
  assumes f: "(f \ a) F"
    and a: "a \ 0"
  shows "((\x. inverse (f x)) \ inverse a) F"
proof -
  from a have "0 < norm a" by simp
  with f have "eventually (\x. dist (f x) a < norm a) F"
    by (rule tendstoD)
  then have "eventually (\x. f x \ 0) F"
    unfolding dist_norm by (auto elim!: eventually_mono)
  with a have "eventually (\x. inverse (f x) - inverse a =
    - (inverse (f x) * (f x - a) * inverse a)) F"
    by (auto elim!: eventually_mono simp: inverse_diff_inverse)
  moreover have "Zfun (\x. - (inverse (f x) * (f x - a) * inverse a)) F"
    by (intro Zfun_minus Zfun_mult_left
      bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult]
      Bfun_inverse [OF f a] f [unfolded tendsto_Zfun_iff])
  ultimately show ?thesis
    unfolding tendsto_Zfun_iff by (rule Zfun_ssubst)
qed

lemma continuous_inverse:
  fixes f :: "'a::t2_space \ 'b::real_normed_div_algebra"
  assumes "continuous F f"
    and "f (Lim F (\x. x)) \ 0"
  shows "continuous F (\x. inverse (f x))"
  using assms unfolding continuous_def by (rule tendsto_inverse)

lemma continuous_at_within_inverse[continuous_intros]:
  fixes f :: "'a::t2_space \ 'b::real_normed_div_algebra"
  assumes "continuous (at a within s) f"
    and "f a \ 0"
  shows "continuous (at a within s) (\x. inverse (f x))"
  using assms unfolding continuous_within by (rule tendsto_inverse)

lemma continuous_on_inverse[continuous_intros]:
  fixes f :: "'a::topological_space \ 'b::real_normed_div_algebra"
  assumes "continuous_on s f"
    and "\x\s. f x \ 0"
  shows "continuous_on s (\x. inverse (f x))"
  using assms unfolding continuous_on_def by (blast intro: tendsto_inverse)

lemma tendsto_divide [tendsto_intros]:
  fixes a b :: "'a::real_normed_field"
  shows "(f \ a) F \ (g \ b) F \ b \ 0 \ ((\x. f x / g x) \ a / b) F"
  by (simp add: tendsto_mult tendsto_inverse divide_inverse)

lemma continuous_divide:
  fixes f g :: "'a::t2_space \ 'b::real_normed_field"
  assumes "continuous F f"
    and "continuous F g"
    and "g (Lim F (\x. x)) \ 0"
  shows "continuous F (\x. (f x) / (g x))"
  using assms unfolding continuous_def by (rule tendsto_divide)

lemma continuous_at_within_divide[continuous_intros]:
  fixes f g :: "'a::t2_space \ 'b::real_normed_field"
  assumes "continuous (at a within s) f" "continuous (at a within s) g"
    and "g a \ 0"
  shows "continuous (at a within s) (\x. (f x) / (g x))"
  using assms unfolding continuous_within by (rule tendsto_divide)

lemma isCont_divide[continuous_intros, simp]:
  fixes f g :: "'a::t2_space \ 'b::real_normed_field"
  assumes "isCont f a" "isCont g a" "g a \ 0"
  shows "isCont (\x. (f x) / g x) a"
  using assms unfolding continuous_at by (rule tendsto_divide)

lemma continuous_on_divide[continuous_intros]:
  fixes f :: "'a::topological_space \ 'b::real_normed_field"
  assumes "continuous_on s f" "continuous_on s g"
    and "\x\s. g x \ 0"
  shows "continuous_on s (\x. (f x) / (g x))"
  using assms unfolding continuous_on_def by (blast intro: tendsto_divide)

lemma continuous_cmult_left_iff:
  fixes c::"'a::real_normed_field"
  assumes "c \ 0"
  shows "continuous F (\x. c * f x) \ continuous F f"
  by (simp add: assms continuous_def)

lemma continuous_cmult_right_iff:
  fixes c::"'a::real_normed_field"
  assumes "c \ 0"
  shows "continuous F (\x. f x * c) \ continuous F f"
  by (simp add: assms continuous_def)

lemma continuous_cdivide_iff:
  fixes c::"'a::real_normed_field"
  assumes "c \ 0"
  shows "continuous F (\x. f x / c) \ continuous F f"
  using assms by (auto simp: continuous_def divide_inverse)

lemma continuous_cong:
  assumes "eventually (\x. f x = g x) F" "f (Lim F (\x. x)) = g (Lim F (\x. x))"
  shows "continuous F f \ continuous F g"
  unfolding continuous_def using assms filterlim_cong by force

lemma continuous_at_within_cong:
  assumes "f x = g x" "eventually (\x. f x = g x) (at x within S)"
  shows "continuous (at x within S) f \ continuous (at x within S) g"
  using assms by (simp add: continuous_within filterlim_cong)

lemma tendsto_power_int [tendsto_intros]:
  fixes a :: "'a::real_normed_div_algebra"
  assumes f: "(f \ a) F"
    and a: "a \ 0"
  shows "((\x. power_int (f x) n) \ power_int a n) F"
  using assms by (cases n rule: int_cases4) (auto intro!: tendsto_intros simp: power_int_minus)

lemma continuous_power_int:
  fixes f :: "'a::t2_space \ 'b::real_normed_div_algebra"
  assumes "continuous F f"
    and "f (Lim F (\x. x)) \ 0"
  shows "continuous F (\x. power_int (f x) n)"
  using assms unfolding continuous_def by (rule tendsto_power_int)

lemma continuous_at_within_power_int[continuous_intros]:
  fixes f :: "'a::t2_space \ 'b::real_normed_div_algebra"
  assumes "continuous (at a within s) f"
    and "f a \ 0"
  shows "continuous (at a within s) (\x. power_int (f x) n)"
  using assms unfolding continuous_within by (rule tendsto_power_int)

lemma continuous_on_power_int [continuous_intros]:
  fixes f :: "'a::topological_space \ 'b::real_normed_div_algebra"
  assumes "continuous_on s f" and "n \ 0 \ (\x\s. f x \ 0)"
  shows "continuous_on s (\x. power_int (f x) n)"
  using assms by (cases "n \ 0") (auto simp: power_int_def intro!: continuous_intros)

lemma tendsto_power_int' [tendsto_intros]:
  fixes a :: "'a::real_normed_div_algebra"
  assumes f: "(f \ a) F"
    and a: "a \ 0 \ n \ 0"
  shows "((\x. power_int (f x) n) \ power_int a n) F"
  using assms by (cases n rule: int_cases4) (auto intro!: tendsto_intros simp: power_int_minus)

lemma tendsto_sgn [tendsto_intros]: "(f \ l) F \ l \ 0 \ ((\x. sgn (f x)) \ sgn l) F"
  for l :: "'a::real_normed_vector"
  unfolding sgn_div_norm by (simp add: tendsto_intros)

lemma continuous_sgn:
  fixes f :: "'a::t2_space \ 'b::real_normed_vector"
  assumes "continuous F f"
    and "f (Lim F (\x. x)) \ 0"
  shows "continuous F (\x. sgn (f x))"
  using assms unfolding continuous_def by (rule tendsto_sgn)

lemma continuous_at_within_sgn[continuous_intros]:
  fixes f :: "'a::t2_space \ 'b::real_normed_vector"
  assumes "continuous (at a within s) f"
    and "f a \ 0"
  shows "continuous (at a within s) (\x. sgn (f x))"
  using assms unfolding continuous_within by (rule tendsto_sgn)

lemma isCont_sgn[continuous_intros]:
  fixes f :: "'a::t2_space \ 'b::real_normed_vector"
  assumes "isCont f a"
    and "f a \ 0"
  shows "isCont (\x. sgn (f x)) a"
  using assms unfolding continuous_at by (rule tendsto_sgn)

lemma continuous_on_sgn[continuous_intros]:
  fixes f :: "'a::topological_space \ 'b::real_normed_vector"
  assumes "continuous_on s f"
    and "\x\s. f x \ 0"
  shows "continuous_on s (\x. sgn (f x))"
  using assms unfolding continuous_on_def by (blast intro: tendsto_sgn)

lemma filterlim_at_infinity:
  fixes f :: "_ \ 'a::real_normed_vector"
  assumes "0 \ c"
  shows "(LIM x F. f x :> at_infinity) \ (\r>c. eventually (\x. r \ norm (f x)) F)"
  unfolding filterlim_iff eventually_at_infinity
proof safe
  fix P :: "'a \ bool"
  fix b
  assume *: "\r>c. eventually (\x. r \ norm (f x)) F"
  assume P: "\x. b \ norm x \ P x"
  have "max b (c + 1) > c" by auto
  with * have "eventually (\x. max b (c + 1) \ norm (f x)) F"
    by auto
  then show "eventually (\x. P (f x)) F"
  proof eventually_elim
    case (elim x)
    with P show "P (f x)" by auto
  qed
qed force

lemma filterlim_at_infinity_imp_norm_at_top:
  fixes F
  assumes "filterlim f at_infinity F"
  shows   "filterlim (\x. norm (f x)) at_top F"
proof -
  {
    fix r :: real
    have "\\<^sub>F x in F. r \ norm (f x)" using filterlim_at_infinity[of 0 f F] assms
      by (cases "r > 0")
         (auto simp: not_less intro: always_eventually order.trans[OF _ norm_ge_zero])
  }
  thus ?thesis by (auto simp: filterlim_at_top)
qed

lemma filterlim_norm_at_top_imp_at_infinity:
  fixes F
  assumes "filterlim (\x. norm (f x)) at_top F"
  shows   "filterlim f at_infinity F"
  using filterlim_at_infinity[of 0 f F] assms by (auto simp: filterlim_at_top)

lemma filterlim_norm_at_top: "filterlim norm at_top at_infinity"
  by (rule filterlim_at_infinity_imp_norm_at_top) (rule filterlim_ident)

lemma filterlim_at_infinity_conv_norm_at_top:
  "filterlim f at_infinity G \ filterlim (\x. norm (f x)) at_top G"
  by (auto simp: filterlim_at_infinity[OF order.refl] filterlim_at_top_gt[of _ _ 0])

lemma eventually_not_equal_at_infinity:
  "eventually (\x. x \ (a :: 'a :: {real_normed_vector})) at_infinity"
proof -
  from filterlim_norm_at_top[where 'a = 'a]
    have "\\<^sub>F x in at_infinity. norm a < norm (x::'a)" by (auto simp: filterlim_at_top_dense)
  thus ?thesis by eventually_elim auto
qed

lemma filterlim_int_of_nat_at_topD:
  fixes F
  assumes "filterlim (\x. f (int x)) F at_top"
  shows   "filterlim f F at_top"
proof -
  have "filterlim (\x. f (int (nat x))) F at_top"
    by (rule filterlim_compose[OF assms filterlim_nat_sequentially])
  also have "?this \ filterlim f F at_top"
    by (intro filterlim_cong refl eventually_mono [OF eventually_ge_at_top[of "0::int"]]) auto
  finally show ?thesis .
qed

lemma filterlim_int_sequentially [tendsto_intros]:
  "filterlim int at_top sequentially"
  unfolding filterlim_at_top
proof
  fix C :: int
  show "eventually (\n. int n \ C) at_top"
    using eventually_ge_at_top[of "nat \C\"] by eventually_elim linarith
qed

lemma filterlim_real_of_int_at_top [tendsto_intros]:
  "filterlim real_of_int at_top at_top"
  unfolding filterlim_at_top
proof
  fix C :: real
  show "eventually (\n. real_of_int n \ C) at_top"
    using eventually_ge_at_top[of "\C\"] by eventually_elim linarith
qed

lemma filterlim_abs_real: "filterlim (abs::real \ real) at_top at_top"
proof (subst filterlim_cong[OF refl refl])
  from eventually_ge_at_top[of "0::real"] show "eventually (\x::real. \x\ = x) at_top"
    by eventually_elim simp
qed (simp_all add: filterlim_ident)

lemma filterlim_of_real_at_infinity [tendsto_intros]:
  "filterlim (of_real :: real \ 'a :: real_normed_algebra_1) at_infinity at_top"
  by (intro filterlim_norm_at_top_imp_at_infinity) (auto simp: filterlim_abs_real)

lemma not_tendsto_and_filterlim_at_infinity:
  fixes c :: "'a::real_normed_vector"
  assumes "F \ bot"
    and "(f \ c) F"
    and "filterlim f at_infinity F"
  shows False
proof -
  from tendstoD[OF assms(2), of "1/2"]
  have "eventually (\x. dist (f x) c < 1/2) F"
    by simp
  moreover
  from filterlim_at_infinity[of "norm c" f F] assms(3)
  have "eventually (\x. norm (f x) \ norm c + 1) F" by simp
  ultimately have "eventually (\x. False) F"
  proof eventually_elim
    fix x
    assume A: "dist (f x) c < 1/2"
    assume "norm (f x) \ norm c + 1"
    also have "norm (f x) = dist (f x) 0" by simp
    also have "\ \ dist (f x) c + dist c 0" by (rule dist_triangle)
    finally show False using A by simp
  qed
  with assms show False by simp
qed

lemma filterlim_at_infinity_imp_not_convergent:
  assumes "filterlim f at_infinity sequentially"
  shows "\ convergent f"
  by (rule notI, rule not_tendsto_and_filterlim_at_infinity[OF _ _ assms])
     (simp_all add: convergent_LIMSEQ_iff)

lemma filterlim_at_infinity_imp_eventually_ne:
  assumes "filterlim f at_infinity F"
  shows "eventually (\z. f z \ c) F"
proof -
  have "norm c + 1 > 0"
    by (intro add_nonneg_pos) simp_all
  with filterlim_at_infinity[OF order.refl, of f F] assms
  have "eventually (\z. norm (f z) \ norm c + 1) F"
    by blast
  then show ?thesis
    by eventually_elim auto
qed

lemma tendsto_of_nat [tendsto_intros]:
  "filterlim (of_nat :: nat \ 'a::real_normed_algebra_1) at_infinity sequentially"
proof (subst filterlim_at_infinity[OF order.refl], intro allI impI)
  fix r :: real
  assume r: "r > 0"
  define n where "n = nat \r\"
  from r have n: "\m\n. of_nat m \ r"
    unfolding n_def by linarith
--> --------------------

--> maximum size reached

--> --------------------

quality90%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.34Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.