src/HOL/Library/Periodic_Fun.thy
author nipkow
Tue, 23 Feb 2016 16:25:08 +0100
changeset 62390 842917225d56
parent 62055 755fda743c49
child 68406 6beb45f6cf67
permissions -rw-r--r--
more canonical names
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62055
755fda743c49 Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents: 62049
diff changeset
     1
(*  Title:    HOL/Library/Periodic_Fun.thy
755fda743c49 Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents: 62049
diff changeset
     2
    Author:   Manuel Eberl, TU M√ľnchen
62049
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
     3
*)
62055
755fda743c49 Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents: 62049
diff changeset
     4
755fda743c49 Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents: 62049
diff changeset
     5
section \<open>Periodic Functions\<close>
755fda743c49 Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents: 62049
diff changeset
     6
62049
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
     7
theory Periodic_Fun
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
     8
imports Complex_Main
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
     9
begin
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    10
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    11
text \<open>
62055
755fda743c49 Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents: 62049
diff changeset
    12
  A locale for periodic functions. The idea is that one proves $f(x + p) = f(x)$
755fda743c49 Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents: 62049
diff changeset
    13
  for some period $p$ and gets derived results like $f(x - p) = f(x)$ and $f(x + 2p) = f(x)$
755fda743c49 Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents: 62049
diff changeset
    14
  for free.
755fda743c49 Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents: 62049
diff changeset
    15
62049
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    16
  @{term g} and @{term gm} are ``plus/minus k periods'' functions. 
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    17
  @{term g1} and @{term gn1} are ``plus/minus one period'' functions.
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    18
  This is useful e.g. if the period is one; the lemmas one gets are then 
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    19
  @{term "f (x + 1) = f x"} instead of @{term "f (x + 1 * 1) = f x"} etc.
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    20
\<close>
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    21
locale periodic_fun = 
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    22
  fixes f :: "('a :: {ring_1}) \<Rightarrow> 'b" and g gm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and g1 gn1 :: "'a \<Rightarrow> 'a"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    23
  assumes plus_1: "f (g1 x) = f x"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    24
  assumes periodic_arg_plus_0: "g x 0 = x"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    25
  assumes periodic_arg_plus_distrib: "g x (of_int (m + n)) = g (g x (of_int n)) (of_int m)"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    26
  assumes plus_1_eq: "g x 1 = g1 x" and minus_1_eq: "g x (-1) = gn1 x" 
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    27
          and minus_eq: "g x (-y) = gm x y"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    28
begin
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    29
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    30
lemma plus_of_nat: "f (g x (of_nat n)) = f x"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    31
  by (induction n) (insert periodic_arg_plus_distrib[of _ 1 "int n" for n], 
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    32
                    simp_all add: plus_1 periodic_arg_plus_0 plus_1_eq)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    33
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    34
lemma minus_of_nat: "f (gm x (of_nat n)) = f x"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    35
proof -
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    36
  have "f (g x (- of_nat n)) = f (g (g x (- of_nat n)) (of_nat n))"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    37
    by (rule plus_of_nat[symmetric])
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    38
  also have "\<dots> = f (g (g x (of_int (- of_nat n))) (of_int (of_nat n)))" by simp
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    39
  also have "\<dots> = f x" 
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    40
    by (subst periodic_arg_plus_distrib [symmetric]) (simp add: periodic_arg_plus_0)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    41
  finally show ?thesis by (simp add: minus_eq)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    42
qed
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    43
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    44
lemma plus_of_int: "f (g x (of_int n)) = f x"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    45
  by (induction n) (simp_all add: plus_of_nat minus_of_nat minus_eq del: of_nat_Suc)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    46
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    47
lemma minus_of_int: "f (gm x (of_int n)) = f x"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    48
  using plus_of_int[of x "of_int (-n)"] by (simp add: minus_eq)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    49
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    50
lemma plus_numeral: "f (g x (numeral n)) = f x"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    51
  by (subst of_nat_numeral[symmetric], subst plus_of_nat) (rule refl)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    52
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    53
lemma minus_numeral: "f (gm x (numeral n)) = f x"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    54
  by (subst of_nat_numeral[symmetric], subst minus_of_nat) (rule refl)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    55
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    56
lemma minus_1: "f (gn1 x) = f x"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    57
  using minus_of_nat[of x 1] by (simp add: minus_1_eq minus_eq[symmetric])
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    58
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    59
lemmas periodic_simps = plus_of_nat minus_of_nat plus_of_int minus_of_int 
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    60
                        plus_numeral minus_numeral plus_1 minus_1
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    61
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    62
end
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    63
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    64
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    65
text \<open>
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    66
  Specialised case of the @{term periodic_fun} locale for periods that are not 1.
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    67
  Gives lemmas @{term "f (x - period) = f x"} etc.
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    68
\<close>
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    69
locale periodic_fun_simple = 
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    70
  fixes f :: "('a :: {ring_1}) \<Rightarrow> 'b" and period :: 'a
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    71
  assumes plus_period: "f (x + period) = f x"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    72
begin
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    73
sublocale periodic_fun f "\<lambda>z x. z + x * period" "\<lambda>z x. z - x * period" 
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    74
  "\<lambda>z. z + period" "\<lambda>z. z - period"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    75
  by standard (simp_all add: ring_distribs plus_period)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    76
end
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    77
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    78
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    79
text \<open>
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    80
  Specialised case of the @{term periodic_fun} locale for period 1.
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    81
  Gives lemmas @{term "f (x - 1) = f x"} etc.
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    82
\<close>
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    83
locale periodic_fun_simple' = 
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    84
  fixes f :: "('a :: {ring_1}) \<Rightarrow> 'b"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    85
  assumes plus_period: "f (x + 1) = f x"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    86
begin
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    87
sublocale periodic_fun f "\<lambda>z x. z + x" "\<lambda>z x. z - x" "\<lambda>z. z + 1" "\<lambda>z. z - 1"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    88
  by standard (simp_all add: ring_distribs plus_period)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    89
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    90
lemma of_nat: "f (of_nat n) = f 0" using plus_of_nat[of 0 n] by simp
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    91
lemma uminus_of_nat: "f (-of_nat n) = f 0" using minus_of_nat[of 0 n] by simp
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    92
lemma of_int: "f (of_int n) = f 0" using plus_of_int[of 0 n] by simp
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    93
lemma uminus_of_int: "f (-of_int n) = f 0" using minus_of_int[of 0 n] by simp
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    94
lemma of_numeral: "f (numeral n) = f 0" using plus_numeral[of 0 n] by simp
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    95
lemma of_neg_numeral: "f (-numeral n) = f 0" using minus_numeral[of 0 n] by simp
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    96
lemma of_1: "f 1 = f 0" using plus_of_nat[of 0 1] by simp
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    97
lemma of_neg_1: "f (-1) = f 0" using minus_of_nat[of 0 1] by simp
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    98
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    99
lemmas periodic_simps' = 
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   100
  of_nat uminus_of_nat of_int uminus_of_int of_numeral of_neg_numeral of_1 of_neg_1
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   101
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   102
end
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   103
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   104
lemma sin_plus_pi: "sin ((z :: 'a :: {real_normed_field,banach}) + of_real pi) = - sin z"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   105
  by (simp add: sin_add)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   106
  
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   107
lemma cos_plus_pi: "cos ((z :: 'a :: {real_normed_field,banach}) + of_real pi) = - cos z"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   108
  by (simp add: cos_add)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   109
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   110
interpretation sin: periodic_fun_simple sin "2 * of_real pi :: 'a :: {real_normed_field,banach}"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   111
proof
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   112
  fix z :: 'a
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   113
  have "sin (z + 2 * of_real pi) = sin (z + of_real pi + of_real pi)" by (simp add: ac_simps)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   114
  also have "\<dots> = sin z" by (simp only: sin_plus_pi) simp
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   115
  finally show "sin (z + 2 * of_real pi) = sin z" .
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   116
qed
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   117
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   118
interpretation cos: periodic_fun_simple cos "2 * of_real pi :: 'a :: {real_normed_field,banach}"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   119
proof
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   120
  fix z :: 'a
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   121
  have "cos (z + 2 * of_real pi) = cos (z + of_real pi + of_real pi)" by (simp add: ac_simps)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   122
  also have "\<dots> = cos z" by (simp only: cos_plus_pi) simp
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   123
  finally show "cos (z + 2 * of_real pi) = cos z" .
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   124
qed
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   125
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   126
interpretation tan: periodic_fun_simple tan "2 * of_real pi :: 'a :: {real_normed_field,banach}"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   127
  by standard (simp only: tan_def [abs_def] sin.plus_1 cos.plus_1)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   128
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   129
interpretation cot: periodic_fun_simple cot "2 * of_real pi :: 'a :: {real_normed_field,banach}"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   130
  by standard (simp only: cot_def [abs_def] sin.plus_1 cos.plus_1)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   131
  
62390
842917225d56 more canonical names
nipkow
parents: 62055
diff changeset
   132
end