This a summer project as part of the Xena Project's summer project sessions ran in the summer of 2020. That was a lot of summers! I am formalising and placing the generalised trigonometric functions into Lean and proving simple lemmas about them.

Firstly we are focussing on two types of GTFs, (1) the wonky square GTFs, which are heavily reliant on |x|^m + |y|^m = 1 and (2) the p-GTFs which are heavily reliant on an integral definition.

This is a note on my numbering system. I am proving things in the order that I can work out to prove them. This means the numbering is borked, they are numbers as they are proved.

• (limit of sin x / x as x tends to 0)
• Differentiability
• Differentials

• Define general pi
• Get them to work...
• Work out how to use FTC in lean.

• Continuity
• Monotonicity of pi_p

• Waiting for Integrals

• Defined
• Proved the Zero lemmas
• sinm, cosm periodicity of
• Define the double angle formulae
• Prove that tanm x = tan x

• mathlib doesn't have integrals

• Mahdi, Hisham & Elatrash, Mohammed & Elmadhoun, Samar. (2014). On Generalized Trigonometric Functions. Journal of Mathematical Sciences and Applications. 2. 33-38. 10.12691/jmsa-2-3-2.