# Theory CSeries

Up to index of Isabelle/HOL/HOL-Complex

theory CSeries
imports CStar
begin

    (*  Title       : CSeries.thy
        Author      : Jacques D. Fleuriot
        Copyright   : 2002  University of Edinburgh
    *)

    header{*Finite Summation and Infinite Series for Complex Numbers*}

    theory CSeries
    imports CStar
    begin

    consts sumc :: "[nat,nat,(nat=>complex)] => complex"
    primrec
       sumc_0:   "sumc m 0 f = 0"
       sumc_Suc: "sumc m (Suc n) f = (if n < m then 0 else sumc m n f + f(n))"

    (*
    constdefs

       needs convergence of complex sequences

      csums  :: [nat=>complex,complex] => bool     (infixr 80)
       "f sums s  == (%n. sumr 0 n f) ----C> s"

       csummable :: (nat=>complex) => bool
       "csummable f == (EX s. f csums s)"

       csuminf   :: (nat=>complex) => complex
       "csuminf f == (@s. f csums s)"
    *)

    lemma sumc_Suc_zero [simp]: "sumc (Suc n) n f = 0"
    by (induct "n", auto)

    lemma sumc_eq_bounds [simp]: "sumc m m f = 0"
    by (induct "m", auto)

    lemma sumc_Suc_eq [simp]: "sumc m (Suc m) f = f(m)"
    by auto

    lemma sumc_add_lbound_zero [simp]: "sumc (m+k) k f = 0"
    by (induct "k", auto)

    lemma sumc_add: "sumc m n f + sumc m n g = sumc m n (%n. f n + g n)"
    apply (induct "n")
    apply (auto simp add: add_ac)
    done

    lemma sumc_mult: "r * sumc m n f = sumc m n (%n. r * f n)"
    apply (induct "n", auto)
    apply (auto simp add: right_distrib)
    done

    lemma sumc_split_add [rule_format]:
         "n < p --> sumc 0 n f + sumc n p f = sumc 0 p f"
    apply (induct "p")
    apply (auto dest!: leI dest: le_anti_sym)
    done

    lemma sumc_split_add_minus:
         "n < p ==> sumc 0 p f + - sumc 0 n f = sumc n p f"
    apply (drule_tac f1 = f in sumc_split_add [symmetric])
    apply (simp add: add_ac)
    done

    lemma sumc_cmod: "cmod(sumc m n f) ≤ (∑i=m..<n. cmod(f i))"
    apply (induct "n")
    apply (auto intro: complex_mod_triangle_ineq [THEN order_trans])
    done

    lemma sumc_fun_eq [rule_format (no_asm)]:
         "(∀r. m ≤ r & r < n --> f r = g r) --> sumc m n f = sumc m n g"
    by (induct "n", auto)

    lemma sumc_const [simp]: "sumc 0 n (%i. r) = complex_of_real (real n) * r"
    apply (induct "n")
    apply (auto simp add: left_distrib real_of_nat_Suc)
    done

    lemma sumc_add_mult_const:
         "sumc 0 n f + -(complex_of_real(real n) * r) = sumc 0 n (%i. f i + -r)"
    by (simp add: sumc_add [symmetric])

    lemma sumc_diff_mult_const:
         "sumc 0 n f - (complex_of_real(real n)*r) = sumc 0 n (%i. f i - r)"
    by (simp add: diff_minus sumc_add_mult_const)

    lemma sumc_less_bounds_zero [rule_format]: "n < m --> sumc m n f = 0"
    by (induct "n", auto)

    lemma sumc_minus: "sumc m n (%i. - f i) = - sumc m n f"
    by (induct "n", auto)

    lemma sumc_shift_bounds: "sumc (m+k) (n+k) f = sumc m n (%i. f(i + k))"
    by (induct "n", auto)

    lemma sumc_minus_one_complexpow_zero [simp]:
         "sumc 0 (2*n) (%i. (-1) ^ Suc i) = 0"
    by (induct "n", auto)

    lemma sumc_interval_const [rule_format (no_asm)]:
         "(∀n. m ≤ Suc n --> f n = r) & m ≤ na
          --> sumc m na f = (complex_of_real(real (na - m)) * r)"
    apply (induct "na")
    apply (auto simp add: Suc_diff_le real_of_nat_Suc left_distrib)
    done

    lemma sumc_interval_const2 [rule_format (no_asm)]:
         "(∀n. m ≤ n --> f n = r) & m ≤ na
          --> sumc m na f = (complex_of_real(real (na - m)) * r)"
    apply (induct "na")
    apply (auto simp add: left_distrib Suc_diff_le real_of_nat_Suc)
    done

    (***
    Goal "(∀n. m ≤ n --> 0 ≤ cmod(f n)) & m < k --> cmod(sumc 0 m f) ≤ cmod(sumc 0 k f)"
    by (induct_tac "k" 1)
    by (Step_tac 1)
    by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [less_Suc_eq_le])));
    by (ALLGOALS(dres_inst_tac [("x","n")] spec));
    by (Step_tac 1)
    by (dtac le_imp_less_or_eq 1 THEN Step_tac 1)
    by (dtac add_mono 2)
    by (dres_inst_tac [("i","sumr 0 m f")] (order_refl RS add_mono) 1);
    by Auto_tac
    qed_spec_mp "sumc_le";

    Goal "!!f g. (∀r. m ≤ r & r < n --> f r ≤ g r) \
    \                --> sumc m n f ≤ sumc m n g";
    by (induct_tac "n" 1)
    by (auto_tac (claset() addIs [add_mono],
        simpset() addsimps [le_def]));
    qed_spec_mp "sumc_le2";

    Goal "(∀n. 0 ≤ f n) --> 0 ≤ sumc m n f";
    by (induct_tac "n" 1)
    by Auto_tac
    by (dres_inst_tac [("x","n")] spec 1);
    by (arith_tac 1)
    qed_spec_mp "sumc_ge_zero";

    Goal "(∀n. m ≤ n --> 0 ≤ f n) --> 0 ≤ sumc m n f";
    by (induct_tac "n" 1)
    by Auto_tac
    by (dres_inst_tac [("x","n")] spec 1);
    by (arith_tac 1)
    qed_spec_mp "sumc_ge_zero2";
    ***)

    lemma sumr_cmod_ge_zero [iff]: "0 ≤ (∑n=m..<n::nat. cmod (f n))"
    by (induct "n", auto simp add: add_increasing)

    lemma rabs_sumc_cmod_cancel [simp]:
         "abs (∑n=m..<n::nat. cmod (f n)) = (∑n=m..<n. cmod (f n))"
    by (simp add: abs_if linorder_not_less)

    lemma sumc_one_lb_complexpow_zero [simp]: "sumc 1 n (%n. f(n) * 0 ^ n) = 0"
    apply (induct "n")
    apply (case_tac [2] "n", auto)
    done

    lemma sumc_diff: "sumc m n f - sumc m n g = sumc m n (%n. f n - g n)"
    by (simp add: diff_minus sumc_add [symmetric] sumc_minus)

    lemma sumc_subst [rule_format (no_asm)]:
         "(∀p. (m ≤ p & p < m + n --> (f p = g p))) --> sumc m n f = sumc m n g"
    by (induct "n", auto)

    lemma sumc_group [simp]:
         "sumc 0 n (%m. sumc (m * k) (m*k + k) f) = sumc 0 (n * k) f"
    apply (subgoal_tac "k = 0 | 0 < k", auto)
    apply (induct "n")
    apply (auto simp add: sumc_split_add add_commute)
    done

    ML
    {*
    val sumc_Suc_zero = thm "sumc_Suc_zero";
    val sumc_eq_bounds = thm "sumc_eq_bounds";
    val sumc_Suc_eq = thm "sumc_Suc_eq";
    val sumc_add_lbound_zero = thm "sumc_add_lbound_zero";
    val sumc_add = thm "sumc_add";
    val sumc_mult = thm "sumc_mult";
    val sumc_split_add = thm "sumc_split_add";
    val sumc_split_add_minus = thm "sumc_split_add_minus";
    val sumc_cmod = thm "sumc_cmod";
    val sumc_fun_eq = thm "sumc_fun_eq";
    val sumc_const = thm "sumc_const";
    val sumc_add_mult_const = thm "sumc_add_mult_const";
    val sumc_diff_mult_const = thm "sumc_diff_mult_const";
    val sumc_less_bounds_zero = thm "sumc_less_bounds_zero";
    val sumc_minus = thm "sumc_minus";
    val sumc_shift_bounds = thm "sumc_shift_bounds";
    val sumc_minus_one_complexpow_zero = thm "sumc_minus_one_complexpow_zero";
    val sumc_interval_const = thm "sumc_interval_const";
    val sumc_interval_const2 = thm "sumc_interval_const2";
    val sumr_cmod_ge_zero = thm "sumr_cmod_ge_zero";
    val rabs_sumc_cmod_cancel = thm "rabs_sumc_cmod_cancel";
    val sumc_one_lb_complexpow_zero = thm "sumc_one_lb_complexpow_zero";
    val sumc_diff = thm "sumc_diff";
    val sumc_subst = thm "sumc_subst";
    val sumc_group = thm "sumc_group";
    *}

    end

lemma sumc_Suc_zero:

      sumc (Suc n) n f = 0

lemma sumc_eq_bounds:

      sumc m m f = 0

lemma sumc_Suc_eq:

      sumc m (Suc m) f = f m

lemma sumc_add_lbound_zero:

      sumc (m + k) k f = 0

lemma sumc_add:

      sumc m n f + sumc m n g = sumc m n (%n. f n + g n)

lemma sumc_mult:

      r * sumc m n f = sumc m n (%n. r * f n)

lemma sumc_split_add:

      n < p ==> sumc 0 n f + sumc n p f = sumc 0 p f

lemma sumc_split_add_minus:

      n < p ==> sumc 0 p f + - sumc 0 n f = sumc n p f

lemma sumc_cmod:

      cmod (sumc m n f) ≤ (∑i = m..<n. cmod (f i))

lemma sumc_fun_eq:

      ∀r. m ≤ r ∧ r < n --> f r = g r ==> sumc m n f = sumc m n g

lemma sumc_const:

      sumc 0 n (%i. r) = complex_of_real (real n) * r

lemma sumc_add_mult_const:

      sumc 0 n f + - (complex_of_real (real n) * r) = sumc 0 n (%i. f i + - r)

lemma sumc_diff_mult_const:

      sumc 0 n f - complex_of_real (real n) * r = sumc 0 n (%i. f i - r)

lemma sumc_less_bounds_zero:

      n < m ==> sumc m n f = 0

lemma sumc_minus:

      sumc m n (%i. - f i) = - sumc m n f

lemma sumc_shift_bounds:

      sumc (m + k) (n + k) f = sumc m n (%i. f (i + k))

lemma sumc_minus_one_complexpow_zero:

      sumc 0 (2 * n) (%i. -1 ^ Suc i) = 0

lemma sumc_interval_const:

      (∀n. m ≤ Suc n --> f n = r) ∧ m ≤ na
      ==> sumc m na f = complex_of_real (real (na - m)) * r

lemma sumc_interval_const2:

      (∀n≥m. f n = r) ∧ m ≤ na ==> sumc m na f = complex_of_real (real (na - m)) * r

lemma sumr_cmod_ge_zero:

      0 ≤ (∑n = m..<n. cmod (f n))

lemma rabs_sumc_cmod_cancel:

      ¦∑n = m..<n. cmod (f n)¦ = (∑n = m..<n. cmod (f n))

lemma sumc_one_lb_complexpow_zero:

      sumc 1 n (%n. f n * 0 ^ n) = 0

lemma sumc_diff:

      sumc m n f - sumc m n g = sumc m n (%n. f n - g n)

lemma sumc_subst:

      ∀p. m ≤ p ∧ p < m + n --> f p = g p ==> sumc m n f = sumc m n g

lemma sumc_group:

      sumc 0 n (%m. sumc (m * k) (m * k + k) f) = sumc 0 (n * k) f