SSL Multiseries_Expansion.thy Interaktion und
PortierbarkeitIsabelle

(*
  File:    Multiseries_Expansion.thy
  Author:  Manuel Eberl, TU München

  Asymptotic bases and Multiseries expansions of real-valued functions.
  Contains automation to prove limits and asymptotic relationships between such functions.
*)
section \<open>Multiseries expansions\<close>
theory Multiseries_Expansion
imports
  "HOL-Library.BNF_Corec"
  "HOL-Library.Landau_Symbols"
  Lazy_Eval
  Inst_Existentials
  Eventuallize
begin

(* TODO Move *)
lemma real_powr_at_top:
  assumes "(p::real) > 0"
  shows   "filterlim (\x. x powr p) at_top at_top"
proof (subst filterlim_cong[OF refl refl])
  show "LIM x at_top. exp (p * ln x) :> at_top"
    by (rule filterlim_compose[OF exp_at_top filterlim_tendsto_pos_mult_at_top[OF tendsto_const]])
       (simp_all add: ln_at_top assms)
  show "eventually (\x. x powr p = exp (p * ln x)) at_top"
    using eventually_gt_at_top[of 0] by eventually_elim (simp add: powr_def)
qed

subsection \<open>Streams and lazy lists\<close>

codatatype 'a msstream = MSSCons 'a "'a msstream"

primrec mssnth :: "'a msstream \ nat \ 'a" where
  "mssnth xs 0 = (case xs of MSSCons x xs \ x)"
| "mssnth xs (Suc n) = (case xs of MSSCons x xs \ mssnth xs n)"

codatatype 'a msllist = MSLNil | MSLCons 'a "'a msllist"
  for map: mslmap

fun lcoeff where
  "lcoeff MSLNil n = 0"
| "lcoeff (MSLCons x xs) 0 = x"
| "lcoeff (MSLCons x xs) (Suc n) = lcoeff xs n"

primcorec msllist_of_msstream :: "'a msstream \ 'a msllist" where
  "msllist_of_msstream xs = (case xs of MSSCons x xs \ MSLCons x (msllist_of_msstream xs))"

lemma msllist_of_msstream_MSSCons [simp]:
  "msllist_of_msstream (MSSCons x xs) = MSLCons x (msllist_of_msstream xs)"
  by (subst msllist_of_msstream.code) simp

lemma lcoeff_llist_of_stream [simp]: "lcoeff (msllist_of_msstream xs) n = mssnth xs n"
  by (induction "msllist_of_msstream xs" n arbitrary: xs rule: lcoeff.induct;
      subst msllist_of_msstream.code) (auto split: msstream.splits)

subsection \<open>Convergent power series\<close>

subsubsection \<open>Definition\<close>

definition convergent_powser :: "real msllist \ bool" where
  "convergent_powser cs \ (\R>0. \x. abs x < R \ summable (\n. lcoeff cs n * x ^ n))"

lemma convergent_powser_stl:
  assumes "convergent_powser (MSLCons c cs)"
  shows   "convergent_powser cs"
proof -
  from assms obtain R where "R > 0" "\x. abs x < R \ summable (\n. lcoeff (MSLCons c cs) n * x ^ n)"
    unfolding convergent_powser_def by blast
  hence "summable (\n. lcoeff cs n * x ^ n)" if "abs x < R" for x
    using that by (subst (asm) summable_powser_split_head [symmetric]) simp
  thus ?thesis using \<open>R > 0\<close> by (auto simp: convergent_powser_def)
qed


definition powser :: "real msllist \ real \ real" where
  "powser cs x = suminf (\n. lcoeff cs n * x ^ n)"

lemma isCont_powser:
  assumes "convergent_powser cs"
  shows   "isCont (powser cs) 0"
proof -
  from assms obtain R where R: "R > 0" "\x. abs x < R \ summable (\n. lcoeff cs n * x ^ n)"
    unfolding convergent_powser_def by blast
  hence *: "summable (\n. lcoeff cs n * (R/2) ^ n)" by (intro R) simp_all
  from \<open>R > 0\<close> show ?thesis unfolding powser_def
    by (intro isCont_powser[OF *]) simp_all
qed

lemma powser_MSLNil [simp]: "powser MSLNil = (\_. 0)"
  by (simp add: fun_eq_iff powser_def)

lemma powser_MSLCons:
  assumes "convergent_powser (MSLCons c cs)"
  shows   "eventually (\x. powser (MSLCons c cs) x = x * powser cs x + c) (nhds 0)"
proof -
  from assms obtain R where R: "R > 0" "\x. abs x < R \ summable (\n. lcoeff (MSLCons c cs) n * x ^ n)"
    unfolding convergent_powser_def by blast
  from R have "powser (MSLCons c cs) x = x * powser cs x + c" if "abs x < R" for x
    using that unfolding powser_def by (subst powser_split_head) simp_all
  moreover have "eventually (\x. abs x < R) (nhds 0)"
    using \<open>R > 0\<close> filterlim_ident[of "nhds (0::real)"]
    by (subst (asm) tendsto_iff) (simp add: dist_real_def)
  ultimately show ?thesis by (auto elim: eventually_mono)
qed

definition convergent_powser' :: "real msllist \ (real \ real) \ bool" where
  "convergent_powser' cs f \ (\R>0. \x. abs x < R \ (\n. lcoeff cs n * x ^ n) sums f x)"

lemma convergent_powser'_imp_convergent_powser:
  "convergent_powser' cs f \ convergent_powser cs"
  unfolding convergent_powser_def convergent_powser'_def by (auto simp: sums_iff)

lemma convergent_powser'_eventually:
  assumes "convergent_powser' cs f"
  shows   "eventually (\x. powser cs x = f x) (nhds 0)"
proof -
  from assms obtain R where "R > 0" "\x. abs x < R \ (\n. lcoeff cs n * x ^ n) sums f x"
    unfolding convergent_powser'_def by blast
  hence "powser cs x = f x" if "abs x < R" for x
    using that by (simp add: powser_def sums_iff)
  moreover have "eventually (\x. abs x < R) (nhds 0)"
    using \<open>R > 0\<close> filterlim_ident[of "nhds (0::real)"]
    by (subst (asm) tendsto_iff) (simp add: dist_real_def)
  ultimately show ?thesis by (auto elim: eventually_mono)
qed

subsubsection \<open>Geometric series\<close>

primcorec mssalternate :: "'a \ 'a \ 'a msstream" where
  "mssalternate a b = MSSCons a (mssalternate b a)"

lemma case_mssalternate [simp]:
  "(case mssalternate a b of MSSCons c d \ f c d) = f a (mssalternate b a)"
  by (subst mssalternate.code) simp

lemma mssnth_mssalternate: "mssnth (mssalternate a b) n = (if even n then a else b)"
  by (induction n arbitrary: a b; subst mssalternate.code) simp_all

lemma convergent_powser'_geometric:
  "convergent_powser' (msllist_of_msstream (mssalternate 1 (-1))) (\x. inverse (1 + x))"
proof -
  have "(\n. lcoeff (msllist_of_msstream (mssalternate 1 (-1))) n * x ^ n) sums (inverse (1 + x))"
    if "abs x < 1" for x :: real
  proof -
    have "(\n. (-1) ^ n * x ^ n) sums (inverse (1 + x))"
      using that geometric_sums[of "-x"] by (simp add: field_simps power_mult_distrib [symmetric])
    also have "(\n. (-1) ^ n * x ^ n) =
                 (\<lambda>n. lcoeff (msllist_of_msstream (mssalternate 1 (-1))) n * x ^ n)"
      by (auto simp add: mssnth_mssalternate fun_eq_iff)
    finally show ?thesis .
  qed
  thus ?thesis unfolding convergent_powser'_def by (force intro!: exI[of _ 1])
qed

subsubsection \<open>Exponential series\<close>

primcorec exp_series_stream_aux :: "real \ real \ real msstream" where
  "exp_series_stream_aux acc n = MSSCons acc (exp_series_stream_aux (acc / n) (n + 1))"

lemma mssnth_exp_series_stream_aux:
  "mssnth (exp_series_stream_aux (1 / fact n) (n + 1)) m = 1 / fact (n + m)"
proof (induction m arbitrary: n)
  case (0 n)
  thus ?case by (subst exp_series_stream_aux.code) simp
next
  case (Suc m n)
  from Suc.IH[of "n + 1"] show ?case
    by (subst exp_series_stream_aux.code) (simp add: algebra_simps)
qed

definition exp_series_stream :: "real msstream" where
  "exp_series_stream = exp_series_stream_aux 1 1"

lemma mssnth_exp_series_stream:
  "mssnth exp_series_stream n = 1 / fact n"
  unfolding exp_series_stream_def using mssnth_exp_series_stream_aux[of 0 n] by simp

lemma convergent_powser'_exp:
  "convergent_powser' (msllist_of_msstream exp_series_stream) exp"
proof -
  have "(\n. lcoeff (msllist_of_msstream exp_series_stream) n * x ^ n) sums exp x" for x :: real
    using exp_converges[of x] by (simp add: mssnth_exp_series_stream field_split_simps)
  thus ?thesis by (auto intro: exI[of _ "1::real"] simp: convergent_powser'_def)
qed


subsubsection \<open>Logarithm series\<close>

primcorec ln_series_stream_aux :: "bool \ real \ real msstream" where
  "ln_series_stream_aux b n =
     MSSCons (if b then -inverse n else inverse n) (ln_series_stream_aux (\<not>b) (n+1))"

lemma mssnth_ln_series_stream_aux:
  "mssnth (ln_series_stream_aux b x) n =
     (if b then - ((-1)^n) * inverse (x + real n) else ((-1)^n) * inverse (x + real n))"
  by (induction n arbitrary: b x; subst ln_series_stream_aux.code) simp_all

definition ln_series_stream :: "real msstream" where
  "ln_series_stream = MSSCons 0 (ln_series_stream_aux False 1)"

lemma mssnth_ln_series_stream:
  "mssnth ln_series_stream n = (-1) ^ Suc n / real n"
  unfolding ln_series_stream_def
  by (cases n) (simp_all add: mssnth_ln_series_stream_aux field_simps)

lemma ln_series':
  assumes "abs (x::real) < 1"
  shows   "(\n. - ((-x)^n) / of_nat n) sums ln (1 + x)"
proof -
  have "\n\1. norm (-((-x)^n)) / of_nat n \ norm x ^ n / 1"
    by (intro exI[of _ "1::nat"] allI impI frac_le) (simp_all add: power_abs)
  hence "\N. \n\N. norm (-((-x)^n) / of_nat n) \ norm x ^ n"
    by (intro exI[of _ 1]) simp_all
  moreover from assms have "summable (\n. norm x ^ n)"
    by (intro summable_geometric) simp_all
  ultimately have *: "summable (\n. - ((-x)^n) / of_nat n)"
    by (rule summable_comparison_test)
  moreover from assms have "0 < 1 + x" "1 + x < 2" by simp_all
  from ln_series[OF this]
    have "ln (1 + x) = (\n. - ((-x) ^ Suc n) / real (Suc n))"
    by (simp_all add: power_minus' mult_ac)
  hence "ln (1 + x) = (\n. - ((-x) ^ n / real n))"
    by (subst (asm) suminf_split_head[OF *]) simp_all
  ultimately show ?thesis by (simp add: sums_iff)
qed

lemma convergent_powser'_ln:
  "convergent_powser' (msllist_of_msstream ln_series_stream) (\x. ln (1 + x))"
proof -
  have "(\n. lcoeff (msllist_of_msstream ln_series_stream)n * x ^ n) sums ln (1 + x)"
    if "abs x < 1" for x
  proof -
    from that have "(\n. - ((- x) ^ n) / real n) sums ln (1 + x)" by (rule ln_series')
    also have "(\n. - ((- x) ^ n) / real n) =
                 (\<lambda>n. lcoeff (msllist_of_msstream ln_series_stream) n * x ^ n)"
      by (auto simp: fun_eq_iff mssnth_ln_series_stream power_mult_distrib [symmetric])
    finally show ?thesis .
  qed
  thus ?thesis unfolding convergent_powser'_def by (force intro!: exI[of _ 1])
qed

subsubsection \<open>Generalized binomial series\<close>

primcorec gbinomial_series_aux :: "bool \ real \ real \ real \ real msllist" where
  "gbinomial_series_aux abort x n acc =
     (if abort \<and> acc = 0 then MSLNil else
        MSLCons acc (gbinomial_series_aux abort x (n + 1) ((x - n) / (n + 1) * acc)))"

lemma gbinomial_series_abort [simp]: "gbinomial_series_aux True x n 0 = MSLNil"
  by (subst gbinomial_series_aux.code) simp

definition gbinomial_series :: "bool \ real \ real msllist" where
  "gbinomial_series abort x = gbinomial_series_aux abort x 0 1"

(* TODO Move *)
lemma gbinomial_Suc_rec:
  "(x gchoose (Suc k)) = (x gchoose k) * ((x - of_nat k) / (of_nat k + 1))"
proof -
  have "((x - 1) + 1) gchoose (Suc k) = x * (x - 1 gchoose k) / (1 + of_nat k)"
    by (subst gbinomial_factors) simp
  also have "x * (x - 1 gchoose k) = (x - of_nat k) * (x gchoose k)"
    by (rule gbinomial_absorb_comp [symmetric])
  finally show ?thesis by (simp add: algebra_simps)
qed

lemma lcoeff_gbinomial_series_aux:
  "lcoeff (gbinomial_series_aux abort x m (x gchoose m)) n = (x gchoose (n + m))"
proof (induction n arbitrary: m)
  case 0
  show ?case by (subst gbinomial_series_aux.code) simp
next
  case (Suc n m)
  show ?case
  proof (cases "abort \ (x gchoose m) = 0")
    case True
    with gbinomial_mult_fact[of m x] obtain k where "x = real k" "k < m"
      by auto
    hence "(x gchoose Suc (n + m)) = 0"
      using gbinomial_mult_fact[of "Suc (n + m)" x]
      by (simp add: gbinomial_altdef_of_nat)
    with True show ?thesis by (subst gbinomial_series_aux.code) simp
  next
    case False
    hence "lcoeff (gbinomial_series_aux abort x m (x gchoose m)) (Suc n) =
             lcoeff (gbinomial_series_aux abort x (Suc m) ((x gchoose m) *
             ((x - real m) / (real m + 1)))) n"
      by (subst gbinomial_series_aux.code) (auto simp: algebra_simps)
    also have "((x gchoose m) * ((x - real m) / (real m + 1))) = x gchoose (Suc m)"
      by (rule gbinomial_Suc_rec [symmetric])
    also have "lcoeff (gbinomial_series_aux abort x (Suc m) \) n = x gchoose (n + Suc m)"
      by (rule Suc.IH)
    finally show ?thesis by simp
  qed
qed

lemma lcoeff_gbinomial_series [simp]:
  "lcoeff (gbinomial_series abort x) n = (x gchoose n)"
  using lcoeff_gbinomial_series_aux[of abort x 0 n] by (simp add: gbinomial_series_def)

lemma gbinomial_ratio_limit:
  fixes a :: "'a :: real_normed_field"
  assumes "a \ \"
  shows "(\n. (a gchoose n) / (a gchoose Suc n)) \ -1"
proof (rule Lim_transform_eventually)
  let ?f = "\n. inverse (a / of_nat (Suc n) - of_nat n / of_nat (Suc n))"
  from eventually_gt_at_top[of "0::nat"]
    show "eventually (\n. ?f n = (a gchoose n) /(a gchoose Suc n)) sequentially"
  proof eventually_elim
    fix n :: nat assume n: "n > 0"
    then obtain q where q: "n = Suc q" by (cases n) blast
    let ?P = "\i=0..
    from n have "(a gchoose n) / (a gchoose Suc n) = (of_nat (Suc n) :: 'a) *
                   (?P / (\<Prod>i=0..n. a - of_nat i))"
      by (simp add: gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)
    also from q have "(\i=0..n. a - of_nat i) = ?P * (a - of_nat n)"
      by (simp add: prod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
    also have "?P / \ = (?P / ?P) / (a - of_nat n)" by (rule divide_divide_eq_left[symmetric])
    also from assms have "?P / ?P = 1" by auto
    also have "of_nat (Suc n) * (1 / (a - of_nat n)) =
                   inverse (inverse (of_nat (Suc n)) * (a - of_nat n))" by (simp add: field_simps)
    also have "inverse (of_nat (Suc n)) * (a - of_nat n) =
                 a / of_nat (Suc n) - of_nat n / of_nat (Suc n)"
      by (simp add: field_simps del: of_nat_Suc)
    finally show "?f n = (a gchoose n) / (a gchoose Suc n)" by simp
  qed

  have "(\n. norm a / (of_nat (Suc n))) \ 0"
    unfolding divide_inverse
    by (intro tendsto_mult_right_zero LIMSEQ_inverse_real_of_nat)
  hence "(\n. a / of_nat (Suc n)) \ 0"
    by (subst tendsto_norm_zero_iff[symmetric]) (simp add: norm_divide del: of_nat_Suc)
  hence "?f \ inverse (0 - 1)"
    by (intro tendsto_inverse tendsto_diff LIMSEQ_n_over_Suc_n) simp_all
  thus "?f \ -1" by simp
qed

lemma summable_gbinomial:
  fixes a z :: real
  assumes "norm z < 1"
  shows   "summable (\n. (a gchoose n) * z ^ n)"
proof (cases "z = 0 \ a \ \")
  case False
  define r where "r = (norm z + 1) / 2"
  from assms have r: "r > norm z" "r < 1" by (simp_all add: r_def field_simps)
  from False have "abs z > 0" by auto
  from False have "a \ \" by (auto elim!: Nats_cases)
  hence *: "(\n. norm (z / ((a gchoose n) / (a gchoose (Suc n))))) \ norm (z / (-1))"
    by (intro tendsto_norm tendsto_divide tendsto_const gbinomial_ratio_limit) simp_all
  hence "\\<^sub>F x in at_top. norm (z / ((a gchoose x) / (a gchoose Suc x))) > 0"
    using assms False by (intro order_tendstoD) auto
  hence nz: "\\<^sub>F x in at_top. (a gchoose x) \ 0" by eventually_elim auto

  have "\\<^sub>F x in at_top. norm (z / ((a gchoose x) / (a gchoose Suc x))) < r"
    using assms r by (intro order_tendstoD(2)[OF *]) simp_all
  with nz have "\\<^sub>F n in at_top. norm ((a gchoose (Suc n)) * z) \ r * norm (a gchoose n)"
    by eventually_elim (simp add: field_simps abs_mult split: if_splits)
  hence "\\<^sub>F n in at_top. norm (z ^ n) * norm ((a gchoose (Suc n)) * z) \
                           norm (z ^ n) * (r * norm (a gchoose n))"
    by eventually_elim (insert False, intro mult_left_mono, auto)
  hence "\\<^sub>F n in at_top. norm ((a gchoose (Suc n)) * z ^ (Suc n)) \
                           r * norm ((a gchoose n) * z ^ n)"
    by (simp add: abs_mult mult_ac)
  then obtain N where N: "\n. n \ N \ norm ((a gchoose (Suc n)) * z ^ (Suc n)) \
                                          r * norm ((a gchoose n) * z ^ n)"
    unfolding eventually_at_top_linorder by blast
  show "summable (\n. (a gchoose n) * z ^ n)"
    by (intro summable_ratio_test[OF r(2), of N] N)
next
  case True
  thus ?thesis
  proof
    assume "a \ \"
    then obtain n where [simp]: "a = of_nat n" by (auto elim: Nats_cases)
    from eventually_gt_at_top[of n]
      have "eventually (\n. (a gchoose n) * z ^ n = 0) at_top"
      by eventually_elim (simp add: binomial_gbinomial [symmetric])
    from summable_cong[OF this] show ?thesis by simp
  qed auto
qed

lemma gen_binomial_real:
  fixes z :: real
  assumes "norm z < 1"
  shows   "(\n. (a gchoose n) * z^n) sums (1 + z) powr a"
proof -
  define K where "K = 1 - (1 - norm z) / 2"
  from assms have K: "K > 0" "K < 1" "norm z < K"
     unfolding K_def by (auto simp: field_simps intro!: add_pos_nonneg)
  let ?f = "\n. a gchoose n" and ?f' = "diffs (\n. a gchoose n)"
  have summable_strong: "summable (\n. ?f n * z ^ n)" if "norm z < 1" for z using that
    by (intro summable_gbinomial)
  with K have summable: "summable (\n. ?f n * z ^ n)" if "norm z < K" for z using that by auto
  hence summable': "summable (\n. ?f' n * z ^ n)" if "norm z < K" for z using that
    by (intro termdiff_converges[of _ K]) simp_all

  define f f' where [abs_def]: "f z = (\n. ?f n * z ^ n)" "f' z = (\n. ?f' n * z ^ n)" for z
  {
    fix z :: real assume z: "norm z < K"
    from summable_mult2[OF summable'[OF z], of z]
      have summable1: "summable (\n. ?f' n * z ^ Suc n)" by (simp add: mult_ac)
    hence summable2: "summable (\n. of_nat n * ?f n * z^n)"
      unfolding diffs_def by (subst (asm) summable_Suc_iff)

    have "(1 + z) * f' z = (\n. ?f' n * z^n) + (\n. ?f' n * z^Suc n)"
      unfolding f_f'_def using summable' z by (simp add: algebra_simps suminf_mult)
    also have "(\n. ?f' n * z^n) = (\n. of_nat (Suc n) * ?f (Suc n) * z^n)"
      by (intro suminf_cong) (simp add: diffs_def)
    also have "(\n. ?f' n * z^Suc n) = (\n. of_nat n * ?f n * z ^ n)"
      using summable1 suminf_split_initial_segment[OF summable1] unfolding diffs_def
      by (subst suminf_split_head, subst (asm) summable_Suc_iff) simp_all
    also have "(\n. of_nat (Suc n) * ?f (Suc n) * z^n) + (\n. of_nat n * ?f n * z^n) =
                 (\<Sum>n. a * ?f n * z^n)"
      by (subst gbinomial_mult_1, subst suminf_add)
         (insert summable'[OF z] summable2,
          simp_all add: summable_powser_split_head algebra_simps diffs_def)
    also have "\ = a * f z" unfolding f_f'_def
      by (subst suminf_mult[symmetric]) (simp_all add: summable[OF z] mult_ac)
    finally have "a * f z = (1 + z) * f' z" by simp
  } note deriv = this

  have [derivative_intros]: "(f has_field_derivative f' z) (at z)" if "norm z < of_real K" for z
    unfolding f_f'_def using K that
    by (intro termdiffs_strong[of "?f" K z] summable_strong) simp_all
  have "f 0 = (\n. if n = 0 then 1 else 0)" unfolding f_f'_def by (intro suminf_cong) simp
  also have "\ = 1" using sums_single[of 0 "\_. 1::real"] unfolding sums_iff by simp
  finally have [simp]: "f 0 = 1" .

  have "f z * (1 + z) powr (-a) = f 0 * (1 + 0) powr (-a)"
  proof (rule DERIV_isconst3[where ?f = "\x. f x * (1 + x) powr (-a)"])
    fix z :: real assume z': "z \ {-K<..
    hence z: "norm z < K" using K by auto
    with K have nz: "1 + z \ 0" by (auto dest!: minus_unique)
    from z K have "norm z < 1" by simp
    hence "((\z. f z * (1 + z) powr (-a)) has_field_derivative
              f' z * (1 + z) powr (-a) - a * f z * (1 + z) powr (-a-1)) (at z)" using z
      by (auto intro!: derivative_eq_intros)
    also from z have "a * f z = (1 + z) * f' z" by (rule deriv)
    also have "f' z * (1 + z) powr - a - (1 + z) * f' z * (1 + z) powr (- a - 1) = 0"
      using \<open>norm z < 1\<close> by (auto simp add: field_simps powr_diff)
    finally show "((\z. f z * (1 + z) powr (-a)) has_field_derivative 0) (at z)" .
  qed (insert K, auto)
  also have "f 0 * (1 + 0) powr -a = 1" by simp
  finally have "f z = (1 + z) powr a" using K
    by (simp add: field_simps dist_real_def powr_minus)
  with summable K show ?thesis unfolding f_f'_def by (simp add: sums_iff)
qed

lemma convergent_powser'_gbinomial:
  "convergent_powser' (gbinomial_series abort p) (\x. (1 + x) powr p)"
proof -
  have "(\n. lcoeff (gbinomial_series abort p) n * x ^ n) sums (1 + x) powr p" if "abs x < 1" for x
    using that gen_binomial_real[of x p] by simp
  thus ?thesis unfolding convergent_powser'_def by (force intro!: exI[of _ 1])
qed

lemma convergent_powser'_gbinomial':
  "convergent_powser' (gbinomial_series abort (real n)) (\x. (1 + x) ^ n)"
proof -
  {
    fix x :: real
    have "(\k. if k \ {0..n} then real (n choose k) * x ^ k else 0) sums (x + 1) ^ n"
      using sums_If_finite_set[of "{..n}" "\k. real (n choose k) * x ^ k"]
      by (subst binomial_ring) simp
    also have "(\k. if k \ {0..n} then real (n choose k) * x ^ k else 0) =
                 (\<lambda>k. lcoeff (gbinomial_series abort (real n)) k * x ^ k)"
      by (simp add: fun_eq_iff binomial_gbinomial [symmetric])
    finally have "\ sums (1 + x) ^ n" by (simp add: add_ac)
  }
  thus ?thesis unfolding convergent_powser'_def
    by (auto intro!: exI[of _ 1])
qed

subsubsection \<open>Sine and cosine\<close>

primcorec sin_series_stream_aux :: "bool \ real \ real \ real msstream" where
  "sin_series_stream_aux b acc m =
    MSSCons (if b then -inverse acc else inverse acc)
          (sin_series_stream_aux (\<not>b) (acc * (m + 1) * (m + 2)) (m + 2))"

lemma mssnth_sin_series_stream_aux:
  "mssnth (sin_series_stream_aux b (fact m) m) n =
     (if b then -1 else 1) * (-1) ^ n / (fact (2 * n + m))"
proof (induction n arbitrary: b m)
  case (0 b m)
  thus ?case by (subst sin_series_stream_aux.code) (simp add: field_simps)
next
  case (Suc n b m)
  show ?case using Suc.IH[of "\b" "m + 2"]
    by (subst sin_series_stream_aux.code) (auto simp: field_simps)
qed

definition sin_series_stream where
  "sin_series_stream = sin_series_stream_aux False 1 1"

lemma mssnth_sin_series_stream:
  "mssnth sin_series_stream n = (-1) ^ n / fact (2 * n + 1)"
  using mssnth_sin_series_stream_aux[of False 1 n] unfolding sin_series_stream_def by simp

definition cos_series_stream where
  "cos_series_stream = sin_series_stream_aux False 1 0"

lemma mssnth_cos_series_stream:
  "mssnth cos_series_stream n = (-1) ^ n / fact (2 * n)"
  using mssnth_sin_series_stream_aux[of False 0 n] unfolding cos_series_stream_def by simp

lemma summable_pre_sin: "summable (\n. mssnth sin_series_stream n * (x::real) ^ n)"
proof -
  have *: "summable (\n. 1 / fact n * abs x ^ n)"
    using exp_converges[of "abs x"] by (simp add: sums_iff field_simps)
  {
    fix n :: nat
    have "\x\ ^ n / fact (2 * n + 1) \ \x\ ^ n / fact n"
      by (intro divide_left_mono fact_mono) auto
    hence "norm (mssnth sin_series_stream n * x ^ n) \ 1 / fact n * abs x ^ n"
      by (simp add: mssnth_sin_series_stream abs_mult power_abs field_simps)
  }
  thus ?thesis
    by (intro summable_comparison_test[OF _ *]) (auto intro!: exI[of _ 0])
qed

lemma summable_pre_cos: "summable (\n. mssnth cos_series_stream n * (x::real) ^ n)"
proof -
  have *: "summable (\n. 1 / fact n * abs x ^ n)"
    using exp_converges[of "abs x"] by (simp add: sums_iff field_simps)
  {
    fix n :: nat
    have "\x\ ^ n / fact (2 * n) \ \x\ ^ n / fact n"
      by (intro divide_left_mono fact_mono) auto
    hence "norm (mssnth cos_series_stream n * x ^ n) \ 1 / fact n * abs x ^ n"
      by (simp add: mssnth_cos_series_stream abs_mult power_abs field_simps)
  }
  thus ?thesis
    by (intro summable_comparison_test[OF _ *]) (auto intro!: exI[of _ 0])
qed

lemma cos_conv_pre_cos:
  "cos x = powser (msllist_of_msstream cos_series_stream) (x ^ 2)"
proof -
  have "(\n. cos_coeff (2 * n) * x ^ (2 * n)) sums cos x"
    using cos_converges[of x]
    by (subst sums_mono_reindex[of "\n. 2 * n"])
       (auto simp: strict_mono_def cos_coeff_def elim!: evenE)
  also have "(\n. cos_coeff (2 * n) * x ^ (2 * n)) =
               (\<lambda>n. mssnth cos_series_stream n * (x ^ 2) ^ n)"
    by (simp add: fun_eq_iff mssnth_cos_series_stream cos_coeff_def power_mult)
  finally have sums: "(\n. mssnth cos_series_stream n * x\<^sup>2 ^ n) sums cos x" .
  thus ?thesis by (simp add: powser_def sums_iff)
qed

lemma sin_conv_pre_sin:
  "sin x = x * powser (msllist_of_msstream sin_series_stream) (x ^ 2)"
proof -
  have "(\n. sin_coeff (2 * n + 1) * x ^ (2 * n + 1)) sums sin x"
    using sin_converges[of x]
    by (subst sums_mono_reindex[of "\n. 2 * n + 1"])
       (auto simp: strict_mono_def sin_coeff_def elim!: oddE)
  also have "(\n. sin_coeff (2 * n + 1) * x ^ (2 * n + 1)) =
               (\<lambda>n. x * mssnth sin_series_stream n * (x ^ 2) ^ n)"
    by (simp add: fun_eq_iff mssnth_sin_series_stream sin_coeff_def power_mult [symmetric] algebra_simps)
  finally have sums: "(\n. x * mssnth sin_series_stream n * x\<^sup>2 ^ n) sums sin x" .
  thus ?thesis using summable_pre_sin[of "x^2"]
    by (simp add: powser_def sums_iff suminf_mult [symmetric] mult.assoc)
qed

lemma convergent_powser_sin_series_stream:
  "convergent_powser (msllist_of_msstream sin_series_stream)"
  (is "convergent_powser ?cs")
proof -
  show ?thesis using summable_pre_sin unfolding convergent_powser_def
    by (intro exI[of _ 1]) auto
qed

lemma convergent_powser_cos_series_stream:
  "convergent_powser (msllist_of_msstream cos_series_stream)"
  (is "convergent_powser ?cs")
proof -
  show ?thesis using summable_pre_cos unfolding convergent_powser_def
    by (intro exI[of _ 1]) auto
qed


subsubsection \<open>Arc tangent\<close>

definition arctan_coeffs :: "nat \ 'a :: {real_normed_div_algebra, banach}" where
  "arctan_coeffs n = (if odd n then (-1) ^ (n div 2) / of_nat n else 0)"

lemma arctan_converges:
  assumes "norm x < 1"
  shows   "(\n. arctan_coeffs n * x ^ n) sums arctan x"
proof -
  have A: "(\n. diffs arctan_coeffs n * x ^ n) sums (1 / (1 + x^2))" if "norm x < 1" for x :: real
  proof -
    let ?f = "\n. (if odd n then 0 else (-1) ^ (n div 2)) * x ^ n"
    from that have "norm x ^ 2 < 1 ^ 2" by (intro power_strict_mono) simp_all
    hence "(\n. (-(x^2))^n) sums (1 / (1 - (-(x^2))))" by (intro geometric_sums) simp_all
    also have "1 - (-(x^2)) = 1 + x^2" by simp
    also have "(\n. (-(x^2))^n) = (\n. ?f (2*n))" by (auto simp: fun_eq_iff power_minus' power_mult)
    also have "range ((*) (2::nat)) = {n. even n}"
      by (auto elim!: evenE)
    hence "(\n. ?f (2*n)) sums (1 / (1 + x^2)) \ ?f sums (1 / (1 + x^2))"
      by (intro sums_mono_reindex) (simp_all add: strict_mono_Suc_iff)
    also have "?f = (\n. diffs arctan_coeffs n * x ^ n)"
      by (simp add: fun_eq_iff arctan_coeffs_def diffs_def)
    finally show "(\n. diffs arctan_coeffs n * x ^ n) sums (1 / (1 + x^2))" .
  qed

  have B: "summable (\n. arctan_coeffs n * x ^ n)" if "norm x < 1" for x :: real
  proof (rule summable_comparison_test)
    show "\N. \n\N. norm (arctan_coeffs n * x ^ n) \ 1 * norm x ^ n"
      unfolding norm_mult norm_power
      by (intro exI[of _ "0::nat"] allI impI mult_right_mono)
         (simp_all add: arctan_coeffs_def field_split_simps)
    from that show "summable (\n. 1 * norm x ^ n)"
      by (intro summable_mult summable_geometric) simp_all
  qed

  define F :: "real \ real" where "F = (\x. \n. arctan_coeffs n * x ^ n)"
  have [derivative_intros]:
    "(F has_field_derivative (1 / (1 + x^2))) (at x)" if "norm x < 1" for x :: real
  proof -
    define K :: real where "K = (1 + norm x) / 2"
    from that have K: "norm x < K" "K < 1" by (simp_all add: K_def field_simps)
    have "(F has_field_derivative (\n. diffs arctan_coeffs n * x ^ n)) (at x)"
      unfolding F_def using K by (intro termdiffs_strong[where K = K] B) simp_all
    also from A[OF that] have "(\n. diffs arctan_coeffs n * x ^ n) = 1 / (1 + x^2)"
      by (simp add: sums_iff)
    finally show ?thesis .
  qed
  from assms have "arctan x - F x = arctan 0 - F 0"
    by (intro DERIV_isconst3[of "-1" 1 _ _ "\x. arctan x - F x"])
       (auto intro!: derivative_eq_intros simp: field_simps)
  hence "F x = arctan x" by (simp add: F_def arctan_coeffs_def)
  with B[OF assms] show ?thesis by (simp add: sums_iff F_def)
qed

primcorec arctan_series_stream_aux :: "bool \ real \ real msstream" where
  "arctan_series_stream_aux b n =
     MSSCons (if b then -inverse n else inverse n) (arctan_series_stream_aux (\<not>b) (n + 2))"

lemma mssnth_arctan_series_stream_aux:
  "mssnth (arctan_series_stream_aux b n) m = (-1) ^ (if b then Suc m else m) / (2*m + n)"
  by (induction m arbitrary: b n; subst arctan_series_stream_aux.code)
     (auto simp: field_simps split: if_splits)

definition arctan_series_stream where
  "arctan_series_stream = arctan_series_stream_aux False 1"

lemma mssnth_arctan_series_stream:
  "mssnth arctan_series_stream n = (-1) ^ n / (2 * n + 1)"
  by (simp add: arctan_series_stream_def mssnth_arctan_series_stream_aux)

lemma summable_pre_arctan:
  assumes "norm x < 1"
  shows   "summable (\n. mssnth arctan_series_stream n * x ^ n)" (is "summable ?f")
proof (rule summable_comparison_test)
  show "summable (\n. abs x ^ n)" using assms by (intro summable_geometric) auto
  show "\N. \n\N. norm (?f n) \ abs x ^ n"
  proof (intro exI[of _ 0] allI impI)
    fix n :: nat
    have "norm (?f n) = \x\ ^ n / (2 * real n + 1)"
      by (simp add: mssnth_arctan_series_stream abs_mult power_abs)
    also have "\ \ \x\ ^ n / 1" by (intro divide_left_mono) auto
    finally show "norm (?f n) \ abs x ^ n" by simp
  qed
qed

lemma arctan_conv_pre_arctan:
  assumes "norm x < 1"
  shows   "arctan x = x * powser (msllist_of_msstream arctan_series_stream) (x ^ 2)"
proof -
  from assms have "norm x * norm x < 1 * 1" by (intro mult_strict_mono) auto
  hence norm_less: "norm (x ^ 2) < 1" by (simp add: power2_eq_square)
  have "(\n. arctan_coeffs n * x ^ n) sums arctan x"
    by (intro arctan_converges assms)
  also have "?this \ (\n. arctan_coeffs (2 * n + 1) * x ^ (2 * n + 1)) sums arctan x"
    by (intro sums_mono_reindex [symmetric])
       (auto simp: arctan_coeffs_def strict_mono_def elim!: oddE)
  also have "(\n. arctan_coeffs (2 * n + 1) * x ^ (2 * n + 1)) =
               (\<lambda>n. x * mssnth arctan_series_stream n * (x ^ 2) ^ n)"
    by (simp add: fun_eq_iff mssnth_arctan_series_stream
                  power_mult [symmetric] arctan_coeffs_def mult_ac)
  finally have "(\n. x * mssnth arctan_series_stream n * x\<^sup>2 ^ n) sums arctan x" .
  thus ?thesis using summable_pre_arctan[OF norm_less] assms
    by (simp add: powser_def sums_iff suminf_mult [symmetric] mult.assoc)
qed

lemma convergent_powser_arctan:
  "convergent_powser (msllist_of_msstream arctan_series_stream)"
  unfolding convergent_powser_def
  using summable_pre_arctan by (intro exI[of _ 1]) auto

lemma arctan_inverse_pos: "x > 0 \ arctan x = pi / 2 - arctan (inverse x)"
  using arctan_inverse[of x] by (simp add: field_simps)

lemma arctan_inverse_neg: "x < 0 \ arctan x = -pi / 2 - arctan (inverse x)"
  using arctan_inverse[of x] by (simp add: field_simps)

subsection \<open>Multiseries\<close>

subsubsection \<open>Asymptotic bases\<close>

type_synonym basis = "(real \ real) list"

lemma transp_ln_smallo_ln: "transp (\f g. (\x::real. ln (g x)) \ o(\x. ln (f x)))"
  by (rule transpI, erule landau_o.small.trans)

definition basis_wf :: "basis \ bool" where
  "basis_wf basis \ (\f\set basis. filterlim f at_top at_top) \
                      sorted_wrt (\<lambda>f g. (\<lambda>x. ln (g x)) \<in> o(\<lambda>x. ln (f x))) basis"

lemma basis_wf_Nil [simp]: "basis_wf []"
  by (simp add: basis_wf_def)

lemma basis_wf_Cons:
  "basis_wf (f # basis) \
     filterlim f at_top at_top \<and> (\<forall>g\<in>set basis. (\<lambda>x. ln (g x)) \<in> o(\<lambda>x. ln (f x))) \<and> basis_wf basis"
  unfolding basis_wf_def by auto

(* TODO: Move *)
lemma sorted_wrt_snoc:
  assumes trans: "transp P" and "sorted_wrt P xs" "P (last xs) y"
  shows   "sorted_wrt P (xs @ [y])"
proof (subst sorted_wrt_append, intro conjI ballI)
  fix x y' assume x: "x \ set xs" and y': "y' \ set [y]"
  from y' have [simp]: "y' = y" by simp
  show "P x y'"
  proof (cases "x = last xs")
    case False
    from x have eq: "xs = butlast xs @ [last xs]"
      by (subst append_butlast_last_id) auto
    from x and False have x': "x \ set (butlast xs)" by (subst (asm) eq) auto
    have "sorted_wrt P xs" by fact
    also note eq
    finally have "P x (last xs)" using x'
      by (subst (asm) sorted_wrt_append) auto
    with \<open>P (last xs) y\<close> have "P x y" using transpD[OF trans] by blast
    thus ?thesis by simp
  qed (insert assms, auto)
qed (insert assms, auto)

lemma basis_wf_snoc:
  assumes "bs \ []"
  assumes "basis_wf bs" "filterlim b at_top at_top"
  assumes "(\x. ln (b x)) \ o(\x. ln (last bs x))"
  shows   "basis_wf (bs @ [b])"
proof -
  have "transp (\f g. (\x. ln (g x)) \ o(\x. ln (f x)))"
    by (auto simp: transp_def intro: landau_o.small.trans)
  thus ?thesis using assms
    by (auto simp add: basis_wf_def sorted_wrt_snoc[OF transp_ln_smallo_ln])
qed

lemma basis_wf_singleton: "basis_wf [b] \ filterlim b at_top at_top"
  by (simp add: basis_wf_Cons)

lemma basis_wf_many: "basis_wf (b # b' # bs) \
  filterlim b at_top at_top \<and> (\<lambda>x. ln (b' x)) \<in> o(\<lambda>x. ln (b x)) \<and> basis_wf (b' # bs)"
  unfolding basis_wf_def by (subst sorted_wrt2[OF transp_ln_smallo_ln]) auto

subsubsection \<open>Monomials\<close>

type_synonym monom = "real \ real list"

definition eval_monom :: "monom \ basis \ real \ real" where
  "eval_monom = (\(c,es) basis x. c * prod_list (map (\(b,e). b x powr e) (zip basis es)))"

lemma eval_monom_Nil1 [simp]: "eval_monom (c, []) basis = (\_. c)"
  by (simp add: eval_monom_def split: prod.split)

lemma eval_monom_Nil2 [simp]: "eval_monom monom [] = (\_. fst monom)"
  by (simp add: eval_monom_def split: prod.split)

lemma eval_monom_Cons:
  "eval_monom (c, e # es) (b # basis) = (\x. eval_monom (c, es) basis x * b x powr e)"
  by (simp add: eval_monom_def fun_eq_iff split: prod.split)

definition inverse_monom :: "monom \ monom" where
  "inverse_monom monom = (case monom of (c, es) \ (inverse c, map uminus es))"

lemma length_snd_inverse_monom [simp]:
  "length (snd (inverse_monom monom)) = length (snd monom)"
  by (simp add: inverse_monom_def split: prod.split)

lemma eval_monom_pos:
  assumes "basis_wf basis" "fst monom > 0"
  shows   "eventually (\x. eval_monom monom basis x > 0) at_top"
proof (cases monom)
  case (Pair c es)
  with assms have "c > 0" by simp
  with assms(1) show ?thesis unfolding Pair
  proof (induction es arbitrary: basis)
    case (Cons e es)
    note A = this
    thus ?case
    proof (cases basis)
      case (Cons b basis')
      with A(1)[of basis'] A(2,3)
        have A: "\\<^sub>F x in at_top. eval_monom (c, es) basis' x > 0"
         and B: "eventually (\x. b x > 0) at_top"
        by (simp_all add: basis_wf_Cons filterlim_at_top_dense)
      thus ?thesis by eventually_elim (simp add: Cons eval_monom_Cons)
    qed simp
  qed simp
qed

lemma eval_monom_uminus: "eval_monom (-c, es) basis x = -eval_monom (c, es) basis x"
  by (simp add: eval_monom_def)

lemma eval_monom_neg:
  assumes "basis_wf basis" "fst monom < 0"
  shows   "eventually (\x. eval_monom monom basis x < 0) at_top"
proof -
  from assms have "eventually (\x. eval_monom (-fst monom, snd monom) basis x > 0) at_top"
    by (intro eval_monom_pos) simp_all
  thus ?thesis by (simp add: eval_monom_uminus)
qed

lemma eval_monom_nonzero:
  assumes "basis_wf basis" "fst monom \ 0"
  shows   "eventually (\x. eval_monom monom basis x \ 0) at_top"
proof (cases "fst monom" "0 :: real" rule: linorder_cases)
  case greater
  with assms have "eventually (\x. eval_monom monom basis x > 0) at_top"
    by (simp add: eval_monom_pos)
  thus ?thesis by eventually_elim simp
next
  case less
  with assms have "eventually (\x. eval_monom (-fst monom, snd monom) basis x > 0) at_top"
    by (simp add: eval_monom_pos)
  thus ?thesis by eventually_elim (simp add: eval_monom_uminus)
qed (insert assms, simp_all)

subsubsection \<open>Typeclass for multiseries\<close>

class multiseries = plus + minus + times + uminus + inverse +
  fixes is_expansion :: "'a \ basis \ bool"
    and expansion_level :: "'a itself \ nat"
    and eval :: "'a \ real \ real"
    and zero_expansion :: 'a
    and const_expansion :: "real \ 'a"
    and powr_expansion :: "bool \ 'a \ real \ 'a"
    and power_expansion :: "bool \ 'a \ nat \ 'a"
    and trimmed :: "'a \ bool"
    and dominant_term :: "'a \ monom"

  assumes is_expansion_length:
    "is_expansion F basis \ length basis = expansion_level (TYPE('a))"
  assumes is_expansion_zero:
    "basis_wf basis \ length basis = expansion_level (TYPE('a)) \
       is_expansion zero_expansion basis"
  assumes is_expansion_const:
    "basis_wf basis \ length basis = expansion_level (TYPE('a)) \
       is_expansion (const_expansion c) basis"
  assumes is_expansion_uminus:
    "basis_wf basis \ is_expansion F basis \ is_expansion (-F) basis"
  assumes is_expansion_add:
    "basis_wf basis \ is_expansion F basis \ is_expansion G basis \
       is_expansion (F + G) basis"
  assumes is_expansion_minus:
    "basis_wf basis \ is_expansion F basis \ is_expansion G basis \
       is_expansion (F - G) basis"
  assumes is_expansion_mult:
    "basis_wf basis \ is_expansion F basis \ is_expansion G basis \
       is_expansion (F * G) basis"
  assumes is_expansion_inverse:
    "basis_wf basis \ trimmed F \ is_expansion F basis \
       is_expansion (inverse F) basis"
  assumes is_expansion_divide:
    "basis_wf basis \ trimmed G \ is_expansion F basis \ is_expansion G basis \
       is_expansion (F / G) basis"
  assumes is_expansion_powr:
    "basis_wf basis \ trimmed F \ fst (dominant_term F) > 0 \ is_expansion F basis \
       is_expansion (powr_expansion abort F p) basis"
  assumes is_expansion_power:
    "basis_wf basis \ trimmed F \ is_expansion F basis \
       is_expansion (power_expansion abort F n) basis"

  assumes is_expansion_imp_smallo:
    "basis_wf basis \ is_expansion F basis \ filterlim b at_top at_top \
       (\<forall>g\<in>set basis. (\<lambda>x. ln (g x)) \<in> o(\<lambda>x. ln (b x))) \<Longrightarrow> e > 0 \<Longrightarrow> eval F \<in> o(\<lambda>x. b x powr e)"
  assumes is_expansion_imp_smallomega:
    "basis_wf basis \ is_expansion F basis \ filterlim b at_top at_top \ trimmed F \
       (\<forall>g\<in>set basis. (\<lambda>x. ln (g x)) \<in> o(\<lambda>x. ln (b x))) \<Longrightarrow> e < 0 \<Longrightarrow> eval F \<in> \<omega>(\<lambda>x. b x powr e)"
  assumes trimmed_imp_eventually_sgn:
    "basis_wf basis \ is_expansion F basis \ trimmed F \
       eventually (\<lambda>x. sgn (eval F x) = sgn (fst (dominant_term F))) at_top"
  assumes trimmed_imp_eventually_nz:
    "basis_wf basis \ is_expansion F basis \ trimmed F \
       eventually (\<lambda>x. eval F x \<noteq> 0) at_top"
  assumes trimmed_imp_dominant_term_nz: "trimmed F \ fst (dominant_term F) \ 0"

  assumes dominant_term:
    "basis_wf basis \ is_expansion F basis \ trimmed F \
       eval F \<sim>[at_top] eval_monom (dominant_term F) basis"
  assumes dominant_term_bigo:
    "basis_wf basis \ is_expansion F basis \
       eval F \<in> O(eval_monom (1, snd (dominant_term F)) basis)"
  assumes length_dominant_term:
    "length (snd (dominant_term F)) = expansion_level TYPE('a)"
  assumes fst_dominant_term_uminus [simp]: "fst (dominant_term (- F)) = -fst (dominant_term F)"
  assumes trimmed_uminus_iff [simp]: "trimmed (-F) \ trimmed F"

  assumes add_zero_expansion_left [simp]: "zero_expansion + F = F"
  assumes add_zero_expansion_right [simp]: "F + zero_expansion = F"

  assumes eval_zero [simp]: "eval zero_expansion x = 0"
  assumes eval_const [simp]: "eval (const_expansion c) x = c"
  assumes eval_uminus [simp]: "eval (-F) = (\x. -eval F x)"
  assumes eval_plus [simp]: "eval (F + G) = (\x. eval F x + eval G x)"
  assumes eval_minus [simp]: "eval (F - G) = (\x. eval F x - eval G x)"
  assumes eval_times [simp]: "eval (F * G) = (\x. eval F x * eval G x)"
  assumes eval_inverse [simp]: "eval (inverse F) = (\x. inverse (eval F x))"
  assumes eval_divide [simp]: "eval (F / G) = (\x. eval F x / eval G x)"
  assumes eval_powr [simp]: "eval (powr_expansion abort F p) = (\x. eval F x powr p)"
  assumes eval_power [simp]: "eval (power_expansion abort F n) = (\x. eval F x ^ n)"
  assumes minus_eq_plus_uminus: "F - G = F + (-G)"
  assumes times_const_expansion_1: "const_expansion 1 * F = F"
  assumes trimmed_const_expansion: "trimmed (const_expansion c) \ c \ 0"
begin

definition trimmed_pos where
  "trimmed_pos F \ trimmed F \ fst (dominant_term F) > 0"

definition trimmed_neg where
  "trimmed_neg F \ trimmed F \ fst (dominant_term F) < 0"

lemma trimmed_pos_uminus: "trimmed_neg F \ trimmed_pos (-F)"
  by (simp add: trimmed_neg_def trimmed_pos_def)

lemma trimmed_pos_imp_trimmed: "trimmed_pos x \ trimmed x"
  by (simp add: trimmed_pos_def)

lemma trimmed_neg_imp_trimmed: "trimmed_neg x \ trimmed x"
  by (simp add: trimmed_neg_def)

end

subsubsection \<open>Zero-rank expansions\<close>

instantiation real :: multiseries
begin

inductive is_expansion_real :: "real \ basis \ bool" where
  "is_expansion_real c []"

definition expansion_level_real :: "real itself \ nat" where
  expansion_level_real_def [simp]: "expansion_level_real _ = 0"

definition eval_real :: "real \ real \ real" where
  eval_real_def [simp]: "eval_real c = (\_. c)"

definition zero_expansion_real :: "real" where
  zero_expansion_real_def [simp]: "zero_expansion_real = 0"

definition const_expansion_real :: "real \ real" where
  const_expansion_real_def [simp]: "const_expansion_real x = x"

definition powr_expansion_real :: "bool \ real \ real \ real" where
  powr_expansion_real_def [simp]: "powr_expansion_real _ x p = x powr p"

definition power_expansion_real :: "bool \ real \ nat \ real" where
  power_expansion_real_def [simp]: "power_expansion_real _ x n = x ^ n"

definition trimmed_real :: "real \ bool" where
  trimmed_real_def [simp]: "trimmed_real x \ x \ 0"

definition dominant_term_real :: "real \ monom" where
  dominant_term_real_def [simp]: "dominant_term_real c = (c, [])"

instance proof
  fix basis :: basis and b :: "real \ real" and e F :: real
  assume *: "basis_wf basis" "filterlim b at_top at_top" "is_expansion F basis" "0 < e"
  have "(\x. b x powr e) \ \(\_. 1)"
    by (intro smallomegaI_filterlim_at_infinity filterlim_at_top_imp_at_infinity)
       (auto intro!: filterlim_compose[OF real_powr_at_top] * )
  with * show "eval F \ o(\x. b x powr e)"
    by (cases "F = 0") (auto elim!: is_expansion_real.cases simp: smallomega_iff_smallo)
next
  fix basis :: basis and b :: "real \ real" and e F :: real
  assume *: "basis_wf basis" "filterlim b at_top at_top" "is_expansion F basis"
            "e < 0" "trimmed F"
  from * have pos: "eventually (\x. b x > 0) at_top" by (simp add: filterlim_at_top_dense)
  have "(\x. b x powr -e) \ \(\_. 1)"
    by (intro smallomegaI_filterlim_at_infinity filterlim_at_top_imp_at_infinity)
       (auto intro!: filterlim_compose[OF real_powr_at_top] * )
  with pos have "(\x. b x powr e) \ o(\_. 1)" unfolding powr_minus
    by (subst (asm) landau_omega.small.inverse_eq2)
       (auto elim: eventually_mono simp: smallomega_iff_smallo)
  with * show "eval F \ \(\x. b x powr e)"
    by (auto elim!: is_expansion_real.cases simp: smallomega_iff_smallo)
qed (auto intro!: is_expansion_real.intros elim!: is_expansion_real.cases)

end

lemma eval_real: "eval (c :: real) x = c" by simp

subsubsection \<open>Operations on multiseries\<close>

lemma ms_aux_cases [case_names MSLNil MSLCons]:
  fixes xs :: "('a \ real) msllist"
  obtains "xs = MSLNil" | c e xs' where "xs = MSLCons (c, e) xs'"
proof (cases xs)
  case (MSLCons x xs')
  with that(2)[of "fst x" "snd x" xs'] show ?thesis by auto
qed auto

definition ms_aux_hd_exp :: "('a \ real) msllist \ real option" where
  "ms_aux_hd_exp xs = (case xs of MSLNil \ None | MSLCons (_, e) _ \ Some e)"

primrec ms_exp_gt :: "real \ real option \ bool" where
  "ms_exp_gt x None = True"
| "ms_exp_gt x (Some y) \ x > y"

lemma ms_aux_hd_exp_MSLNil [simp]: "ms_aux_hd_exp MSLNil = None"
  by (simp add: ms_aux_hd_exp_def split: prod.split)

lemma ms_aux_hd_exp_MSLCons [simp]: "ms_aux_hd_exp (MSLCons x xs) = Some (snd x)"
  by (simp add: ms_aux_hd_exp_def split: prod.split)

coinductive is_expansion_aux ::
    "('a :: multiseries \ real) msllist \ (real \ real) \ basis \ bool" where
  is_expansion_MSLNil:
    "eventually (\x. f x = 0) at_top \ length basis = Suc (expansion_level TYPE('a)) \
       is_expansion_aux MSLNil f basis"
| is_expansion_MSLCons:
    "is_expansion_aux xs (\x. f x - eval C x * b x powr e) (b # basis) \
       is_expansion C basis \<Longrightarrow>
       (\<And>e'. e' > e \<Longrightarrow> f \<in> o(\<lambda>x. b x powr e')) \<Longrightarrow> ms_exp_gt e (ms_aux_hd_exp xs) \<Longrightarrow>
       is_expansion_aux (MSLCons (C, e) xs) f (b # basis)"

inductive_cases is_expansion_aux_MSLCons: "is_expansion_aux (MSLCons (c, e) xs) f basis"

lemma is_expansion_aux_basis_nonempty: "is_expansion_aux F f basis \ basis \ []"
  by (erule is_expansion_aux.cases) auto

lemma is_expansion_aux_expansion_level:
  assumes "is_expansion_aux (G :: ('a::multiseries \ real) msllist) g basis"
  shows   "length basis = Suc (expansion_level TYPE('a))"
  using assms by (cases rule: is_expansion_aux.cases) (auto dest: is_expansion_length)

lemma is_expansion_aux_imp_smallo:
  assumes "is_expansion_aux xs f basis" "ms_exp_gt p (ms_aux_hd_exp xs)"
  shows   "f \ o(\x. hd basis x powr p)"
  using assms
proof (cases rule: is_expansion_aux.cases)
  case is_expansion_MSLNil
  show ?thesis by (simp add: landau_o.small.in_cong[OF is_expansion_MSLNil(2)])
next
  case (is_expansion_MSLCons xs C b e basis)
  with assms have "f \ o(\x. b x powr p)"
    by (intro is_expansion_MSLCons) (simp_all add: ms_aux_hd_exp_def)
  thus ?thesis by (simp add: is_expansion_MSLCons)
qed

lemma is_expansion_aux_imp_smallo':
  assumes "is_expansion_aux xs f basis"
  obtains e where "f \ o(\x. hd basis x powr e)"
proof -
  define e where "e = (case ms_aux_hd_exp xs of None \ 0 | Some e \ e + 1)"
  have "ms_exp_gt e (ms_aux_hd_exp xs)"
    by (auto simp add: e_def ms_aux_hd_exp_def split: msllist.splits)
  from assms this have "f \ o(\x. hd basis x powr e)" by (rule is_expansion_aux_imp_smallo)
  from that[OF this] show ?thesis .
qed

lemma is_expansion_aux_imp_smallo'':
  assumes "is_expansion_aux xs f basis" "ms_exp_gt e' (ms_aux_hd_exp xs)"
  obtains e where "e < e'" "f \ o(\x. hd basis x powr e)"
proof -
  define e where "e = (case ms_aux_hd_exp xs of None \ e' - 1 | Some e \ (e' + e) / 2)"
  from assms have "ms_exp_gt e (ms_aux_hd_exp xs)" "e < e'"
    by (cases xs; simp add: e_def field_simps)+
  from assms(1) this(1) have "f \ o(\x. hd basis x powr e)" by (rule is_expansion_aux_imp_smallo)
  from that[OF \<open>e < e'\<close> this] show ?thesis .
qed

definition trimmed_ms_aux :: "('a :: multiseries \ real) msllist \ bool" where
  "trimmed_ms_aux xs = (case xs of MSLNil \ False | MSLCons (C, _) _ \ trimmed C)"

lemma not_trimmed_ms_aux_MSLNil [simp]: "\trimmed_ms_aux MSLNil"
  by (simp add: trimmed_ms_aux_def)

lemma trimmed_ms_aux_MSLCons: "trimmed_ms_aux (MSLCons x xs) = trimmed (fst x)"
  by (simp add: trimmed_ms_aux_def split: prod.split)

lemma trimmed_ms_aux_imp_nz:
  assumes "basis_wf basis" "is_expansion_aux xs f basis" "trimmed_ms_aux xs"
  shows   "eventually (\x. f x \ 0) at_top"
proof (cases xs rule: ms_aux_cases)
  case (MSLCons C e xs')
  from assms this obtain b basis' where *: "basis = b # basis'"
    "is_expansion_aux xs' (\x. f x - eval C x * b x powr e) (b # basis')"
    "ms_exp_gt e (ms_aux_hd_exp xs')" "is_expansion C basis'" "\e'. e' > e \ f \ o(\x. b x powr e')"
    by (auto elim!: is_expansion_aux_MSLCons)
  from assms(1,3) * have nz: "eventually (\x. eval C x \ 0) at_top"
    by (auto simp: trimmed_ms_aux_def MSLCons basis_wf_Cons
             intro: trimmed_imp_eventually_nz[of basis'])
  from assms(1) * have b_limit: "filterlim b at_top at_top" by (simp add: basis_wf_Cons)
  hence b_nz: "eventually (\x. b x > 0) at_top" by (simp add: filterlim_at_top_dense)

  from is_expansion_aux_imp_smallo''[OF *(2,3)]
  obtain e' where e': "e' < e" "(\x. f x - eval C x * b x powr e) \ o(\x. b x powr e')"
    unfolding list.sel by blast
  note this(2)
  also have "\ = o(\x. b x powr (e' - e) * b x powr e)" by (simp add: powr_add [symmetric])
  also from assms * e' have "eval C \ \(\x. b x powr (e' - e))"
    by (intro is_expansion_imp_smallomega[OF _ *(4)])
       (simp_all add: MSLCons basis_wf_Cons trimmed_ms_aux_def)
  hence "(\x. b x powr (e' - e) * b x powr e) \ o(\x. eval C x * b x powr e)"
    by (intro landau_o.small_big_mult is_expansion_imp_smallomega)
       (simp_all add: smallomega_iff_smallo)
  finally have "(\x. f x - eval C x * b x powr e + eval C x * b x powr e) \
                  \<Theta>(\<lambda>x. eval C x * b x powr e)"
    by (subst bigtheta_sym, subst landau_theta.plus_absorb1) simp_all
  hence theta: "f \ \(\x. eval C x * b x powr e)" by simp
  have "eventually (\x. eval C x * b x powr e \ 0) at_top"
    using b_nz nz by eventually_elim simp
  thus ?thesis by (subst eventually_nonzero_bigtheta [OF theta])
qed (insert assms, simp_all add: trimmed_ms_aux_def)

lemma is_expansion_aux_imp_smallomega:
  assumes "basis_wf basis" "is_expansion_aux xs f basis" "filterlim b' at_top at_top"
          "trimmed_ms_aux xs" "\g\set basis. (\x. ln (g x)) \ o(\x. ln (b' x))" "r < 0"
  shows   "f \ \(\x. b' x powr r)"
proof (cases xs rule: ms_aux_cases)
  case (MSLCons C e xs')
  from assms this obtain b basis' where *: "basis = b # basis'" "trimmed C"
    "is_expansion_aux xs' (\x. f x - eval C x * b x powr e) (b # basis')"
    "ms_exp_gt e (ms_aux_hd_exp xs')"
    "is_expansion C basis'" "\e'. e' > e \ f \ o(\x. b x powr e')"
    by (auto elim!: is_expansion_aux_MSLCons simp: trimmed_ms_aux_def)
  from assms * have nz: "eventually (\x. eval C x \ 0) at_top"
    by (intro trimmed_imp_eventually_nz[of basis']) (simp_all add: basis_wf_Cons)
  from assms(1) * have b_limit: "filterlim b at_top at_top" by (simp add: basis_wf_Cons)
  hence b_nz: "eventually (\x. b x > 0) at_top" by (simp add: filterlim_at_top_dense)

  from is_expansion_aux_imp_smallo''[OF *(3,4)]
  obtain e' where e': "e' < e" "(\x. f x - eval C x * b x powr e) \ o(\x. b x powr e')"
    unfolding list.sel by blast
  note this(2)
  also have "\ = o(\x. b x powr (e' - e) * b x powr e)" by (simp add: powr_add [symmetric])
  also from assms * e' have "eval C \ \(\x. b x powr (e' - e))"
    by (intro is_expansion_imp_smallomega[OF _ *(5)])
       (simp_all add: MSLCons basis_wf_Cons trimmed_ms_aux_def)
  hence "(\x. b x powr (e' - e) * b x powr e) \ o(\x. eval C x * b x powr e)"
    by (intro landau_o.small_big_mult is_expansion_imp_smallomega)
       (simp_all add: smallomega_iff_smallo)
  finally have "(\x. f x - eval C x * b x powr e + eval C x * b x powr e) \
                  \<Theta>(\<lambda>x. eval C x * b x powr e)"
    by (subst bigtheta_sym, subst landau_theta.plus_absorb1) simp_all
  hence theta: "f \ \(\x. eval C x * b x powr e)" by simp
  also from * assms e' have "(\x. eval C x * b x powr e) \ \(\x. b x powr (e' - e) * b x powr e)"
    by (intro landau_omega.small_big_mult is_expansion_imp_smallomega[of basis'])
       (simp_all add: basis_wf_Cons)
  also have "\ = \(\x. b x powr e')" by (simp add: powr_add [symmetric])
  also from *(1) assms have "(\x. b x powr e') \ \(\x. b' x powr r)"
    unfolding smallomega_iff_smallo by (intro ln_smallo_imp_flat') (simp_all add: basis_wf_Cons)
  finally show ?thesis .
qed (insert assms, simp_all add: trimmed_ms_aux_def)

definition dominant_term_ms_aux :: "('a :: multiseries \ real) msllist \ monom" where
  "dominant_term_ms_aux xs =
     (case xs of MSLNil \<Rightarrow> (0, replicate (Suc (expansion_level TYPE('a))) 0)
               | MSLCons (C, e) _ \<Rightarrow> case dominant_term C of (c, es) \<Rightarrow> (c, e # es))"

lemma dominant_term_ms_aux_MSLCons:
  "dominant_term_ms_aux (MSLCons (C, e) xs) = map_prod id (\es. e # es) (dominant_term C)"
  by (simp add: dominant_term_ms_aux_def case_prod_unfold map_prod_def)

lemma length_dominant_term_ms_aux [simp]:
  "length (snd (dominant_term_ms_aux (xs :: ('a :: multiseries \ real) msllist))) =
     Suc (expansion_level TYPE('a))"
proof (cases xs rule: ms_aux_cases)
  case (MSLCons C e xs')
  hence "length (snd (dominant_term_ms_aux xs)) = Suc (length (snd (dominant_term C)))"
    by (simp add: dominant_term_ms_aux_def split: prod.splits)
  also note length_dominant_term
  finally show ?thesis .
qed (simp_all add: dominant_term_ms_aux_def split: msllist.splits prod.splits)

definition const_ms_aux :: "real \ ('a :: multiseries \ real) msllist" where
  "const_ms_aux c = MSLCons (const_expansion c, 0) MSLNil"

definition uminus_ms_aux :: "('a :: uminus \ real) msllist \ ('a \ real) msllist" where
  "uminus_ms_aux xs = mslmap (map_prod uminus id) xs"

corec (friend) plus_ms_aux :: "('a :: plus \ real) msllist \ ('a \ real) msllist \ ('a \ real) msllist" where
  "plus_ms_aux xs ys =
     (case (xs, ys) of
        (MSLNil, MSLNil) \<Rightarrow> MSLNil
      | (MSLNil, MSLCons y ys) \<Rightarrow> MSLCons y ys
      | (MSLCons x xs, MSLNil) \<Rightarrow> MSLCons x xs
      | (MSLCons x xs, MSLCons y ys) \<Rightarrow>
          if snd x > snd y then MSLCons x (plus_ms_aux xs (MSLCons y ys))
          else if snd x < snd y then MSLCons y (plus_ms_aux (MSLCons x xs) ys)
          else MSLCons (fst x + fst y, snd x) (plus_ms_aux xs ys))"

context
begin

friend_of_corec mslmap where
  "mslmap (f :: 'a \ 'a) xs =
     (case xs of MSLNil \<Rightarrow> MSLNil | MSLCons x xs \<Rightarrow> MSLCons (f x) (mslmap f xs))"
   by (simp split: msllist.splits, transfer_prover)

corec (friend) times_ms_aux
     :: "('a :: {plus,times} \ real) msllist \ ('a \ real) msllist \ ('a \ real) msllist" where
  "times_ms_aux xs ys =
     (case (xs, ys) of
        (MSLNil, ys) \<Rightarrow> MSLNil
      | (xs, MSLNil) \<Rightarrow> MSLNil
      | (MSLCons x xs, MSLCons y ys) \<Rightarrow>
           MSLCons (fst x * fst y, snd x + snd y)
             (plus_ms_aux (mslmap (map_prod ((*) (fst x)) ((+) (snd x))) ys)
               (times_ms_aux xs (MSLCons y ys))))"

definition scale_shift_ms_aux :: "('a :: times \ real) \ ('a \ real) msllist \ ('a \ real) msllist" where
  "scale_shift_ms_aux = (\(a,b) xs. mslmap (map_prod ((*) a) ((+) b)) xs)"

lemma times_ms_aux_altdef:
  "times_ms_aux xs ys =
     (case (xs, ys) of
        (MSLNil, ys) \<Rightarrow> MSLNil
      | (xs, MSLNil) \<Rightarrow> MSLNil
      | (MSLCons x xs, MSLCons y ys) \<Rightarrow>
          MSLCons (fst x * fst y, snd x + snd y)
            (plus_ms_aux (scale_shift_ms_aux x ys) (times_ms_aux xs (MSLCons y ys))))"
  by (subst times_ms_aux.code) (simp_all add: scale_shift_ms_aux_def split: msllist.splits)
end

corec powser_ms_aux :: "real msllist \ ('a :: multiseries \ real) msllist \ ('a \ real) msllist" where
  "powser_ms_aux cs xs = (case cs of MSLNil \ MSLNil | MSLCons c cs \
     MSLCons (const_expansion c, 0) (times_ms_aux xs (powser_ms_aux cs xs)))"

definition minus_ms_aux :: "('a :: multiseries \ real) msllist \ _" where
  "minus_ms_aux xs ys = plus_ms_aux xs (uminus_ms_aux ys)"

lemma is_expansion_aux_coinduct [consumes 1, case_names is_expansion_aux]:
  fixes xs :: "('a :: multiseries \ real) msllist"
  assumes "X xs f basis" "(\xs f basis. X xs f basis \
     (xs = MSLNil \<and> (\<forall>\<^sub>F x in at_top. f x = 0) \<and> length basis = Suc (expansion_level TYPE('a))) \<or>
     (\<exists>xs' b e basis' C. xs = MSLCons (C, e) xs' \<and> basis = b # basis' \<and>
        (X xs' (\x. f x - eval C x * b x powr e) (b # basis')) \ is_expansion C basis' \
        (\<forall>x>e. f \<in> o(\<lambda>xa. b xa powr x)) \<and> ms_exp_gt e (ms_aux_hd_exp xs')))"
  shows "is_expansion_aux xs f basis"
using assms(1)
proof (coinduction arbitrary: xs f)
  case (is_expansion_aux xs f)
  from assms(2)[OF is_expansion_aux] show ?case by blast
qed

lemma is_expansion_aux_cong:
  assumes "is_expansion_aux F f basis"
  assumes "eventually (\x. f x = g x) at_top"
  shows   "is_expansion_aux F g basis"
  using assms
proof (coinduction arbitrary: F f g rule: is_expansion_aux_coinduct)
  case (is_expansion_aux F f g)
  from this have ev: "eventually (\x. g x = f x) at_top" by (simp add: eq_commute)
  from ev have [simp]: "eventually (\x. g x = 0) at_top \ eventually (\x. f x = 0) at_top"
    by (rule eventually_subst')
  from ev have [simp]: "(\\<^sub>F x in at_top. h x = g x - h' x) \
                          (\<forall>\<^sub>F x in at_top. h x = f x - h' x)" for h h'
      by (rule eventually_subst')
  note [simp] = landau_o.small.in_cong[OF ev]
  from is_expansion_aux(1) show ?case
    by (cases rule: is_expansion_aux.cases) force+
qed

lemma scale_shift_ms_aux_conv_mslmap:
  "scale_shift_ms_aux x = mslmap (map_prod ((*) (fst x)) ((+) (snd x)))"
  by (rule ext) (simp add: scale_shift_ms_aux_def map_prod_def case_prod_unfold)

fun inverse_ms_aux :: "('a :: multiseries \ real) msllist \ ('a \ real) msllist" where
  "inverse_ms_aux (MSLCons x xs) =
     (let c' = inverse (fst x)
      in  scale_shift_ms_aux (c', -snd x)
            (powser_ms_aux (msllist_of_msstream (mssalternate 1 (-1)))
              (scale_shift_ms_aux (c', -snd x) xs)))"

(* TODO: Move? *)
lemma inverse_prod_list: "inverse (prod_list xs :: 'a :: field) = prod_list (map inverse xs)"
  by (induction xs) simp_all

lemma eval_inverse_monom:
  "eval_monom (inverse_monom monom) basis = (\x. inverse (eval_monom monom basis x))"
  by (rule ext) (simp add: eval_monom_def inverse_monom_def zip_map2 o_def case_prod_unfold
                   inverse_prod_list powr_minus)

fun powr_ms_aux :: "bool \ ('a :: multiseries \ real) msllist \ real \ ('a \ real) msllist" where
  "powr_ms_aux abort (MSLCons x xs) p =
      scale_shift_ms_aux (powr_expansion abort (fst x) p, snd x * p)
        (powser_ms_aux (gbinomial_series abort p)
          (scale_shift_ms_aux (inverse (fst x), -snd x) xs))"

fun power_ms_aux :: "bool \ ('a :: multiseries \ real) msllist \ nat \ ('a \ real) msllist" where
  "power_ms_aux abort (MSLCons x xs) n =
      scale_shift_ms_aux (power_expansion abort (fst x) n, snd x * real n)
        (powser_ms_aux (gbinomial_series abort (real n))
          (scale_shift_ms_aux (inverse (fst x), -snd x) xs))"

definition sin_ms_aux' :: "('a :: multiseries \<times> real) msllist \<Rightarrow> ('a \<times> real) msllist" where
  "sin_ms_aux' xs = times_ms_aux xs (powser_ms_aux (msllist_of_msstream sin_series_stream)
                      (times_ms_aux xs xs))"

definition cos_ms_aux' :: "('a :: multiseries \<times> real) msllist \<Rightarrow> ('a \<times> real) msllist" where
  "cos_ms_aux' xs = powser_ms_aux (msllist_of_msstream cos_series_stream) (times_ms_aux xs xs)"

subsubsection \<open>Basic properties of multiseries operations\<close>

lemma uminus_ms_aux_MSLNil [simp]: "uminus_ms_aux MSLNil = MSLNil"
  by (simp add: uminus_ms_aux_def)

lemma uminus_ms_aux_MSLCons: "uminus_ms_aux (MSLCons x xs) = MSLCons (-fst x, snd x) (uminus_ms_aux xs)"
  by (simp add: uminus_ms_aux_def map_prod_def split: prod.splits)

lemma uminus_ms_aux_MSLNil_iff [simp]: "uminus_ms_aux xs = MSLNil \ xs = MSLNil"
  by (simp add: uminus_ms_aux_def)

lemma hd_exp_uminus [simp]: "ms_aux_hd_exp (uminus_ms_aux xs) = ms_aux_hd_exp xs"
  by (simp add: uminus_ms_aux_def ms_aux_hd_exp_def split: msllist.splits prod.split)

lemma scale_shift_ms_aux_MSLNil_iff [simp]: "scale_shift_ms_aux x F = MSLNil \ F = MSLNil"
  by (auto simp: scale_shift_ms_aux_def split: prod.split)

lemma scale_shift_ms_aux_MSLNil [simp]: "scale_shift_ms_aux x MSLNil = MSLNil"
  by (simp add: scale_shift_ms_aux_def split: prod.split)

lemma scale_shift_ms_aux_1 [simp]:
  "scale_shift_ms_aux (1 :: real, 0) xs = xs"
  by (simp add: scale_shift_ms_aux_def map_prod_def msllist.map_id)

lemma scale_shift_ms_aux_MSLCons:
  "scale_shift_ms_aux x (MSLCons y F) = MSLCons (fst x * fst y, snd x + snd y) (scale_shift_ms_aux x F)"
  by (auto simp: scale_shift_ms_aux_def map_prod_def split: prod.split)

lemma hd_exp_basis:
  "ms_aux_hd_exp (scale_shift_ms_aux x xs) = map_option ((+) (snd x)) (ms_aux_hd_exp xs)"
--> --------------------

--> maximum size reached

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

quality99%

¤ Dauer der Verarbeitung: 0.52 Sekunden (vorverarbeitet) ¤

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.

SSL Multiseries_Expansion.thy Interaktion und PortierbarkeitIsabelle

¤ Dauer der Verarbeitung: 0.52 Sekunden (vorverarbeitet) ¤

Haftungshinweis

Bemerkung:

SSL Multiseries_Expansion.thy Interaktion und
PortierbarkeitIsabelle