author | wenzelm |
Thu, 01 Sep 2016 16:05:22 +0200 | |
changeset 63750 | 9c8a366778e1 |
parent 62390 | 842917225d56 |
child 68406 | 6beb45f6cf67 |
permissions | -rw-r--r-- |
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 | 132 |
end |