src/HOL/Library/Periodic_Fun.thy
changeset 62055 755fda743c49
parent 62049 b0f941e207cf
child 62390 842917225d56
     1.1 --- a/src/HOL/Library/Periodic_Fun.thy	Mon Jan 04 22:13:53 2016 +0100
     1.2 +++ b/src/HOL/Library/Periodic_Fun.thy	Tue Jan 05 13:35:06 2016 +0100
     1.3 @@ -1,16 +1,18 @@
     1.4 -(*
     1.5 -  Title:    HOL/Library/Periodic_Fun.thy
     1.6 -  Author:   Manuel Eberl, TU München
     1.7 -  
     1.8 -  A locale for periodic functions. The idea is that one proves $f(x + p) = f(x)$
     1.9 -  for some period $p$ and gets derived results like $f(x - p) = f(x)$ and $f(x + 2p) = f(x)$
    1.10 -  for free.
    1.11 +(*  Title:    HOL/Library/Periodic_Fun.thy
    1.12 +    Author:   Manuel Eberl, TU München
    1.13  *)
    1.14 +
    1.15 +section \<open>Periodic Functions\<close>
    1.16 +
    1.17  theory Periodic_Fun
    1.18  imports Complex_Main
    1.19  begin
    1.20  
    1.21  text \<open>
    1.22 +  A locale for periodic functions. The idea is that one proves $f(x + p) = f(x)$
    1.23 +  for some period $p$ and gets derived results like $f(x - p) = f(x)$ and $f(x + 2p) = f(x)$
    1.24 +  for free.
    1.25 +
    1.26    @{term g} and @{term gm} are ``plus/minus k periods'' functions. 
    1.27    @{term g1} and @{term gn1} are ``plus/minus one period'' functions.
    1.28    This is useful e.g. if the period is one; the lemmas one gets are then