Zulip Chat Archive

Stream: new members

Topic: definition of tan

view this post on Zulip Benjamin Davidson (Jul 31 2020 at 17:33):

Hi everyone, I wanted to solicit your advice on some ideas I had regarding improving the definition of the tan function, which can essentially be broken down into 3 parts:
1) Proving ∀ (x:ℝ), cos x = 0 ↔ (∃ (n:ℕ), x = n*π + π/2)
2) Improve the precision of statements that currently use {x // cos x ≠ 0} (i.e. the continuity of tan) so that they instead use {x // ∃ (n:ℕ), x = n*π + π/2}ᶜ
3) Write a proof for the derivative of tan using the lemma described in (1)
What do you think about this? I would appreciate any critiques or suggestions.

view this post on Zulip Kevin Buzzard (Jul 31 2020 at 17:40):

We have cos_eq_zero_iff in analysis.special_functions.trigonometric.

view this post on Zulip Kevin Buzzard (Jul 31 2020 at 17:41):

n needs to be an integer, not a natural. Note that you're not improving the definition of tan, indeed you're not changing the definition of tan at all, you're proving theorems about the definition.

view this post on Zulip Heather Macbeth (Jul 31 2020 at 18:51):

The current lemma for continuity of tan has the statement

lemma continuous_tan : continuous (λ x : {x // cos x  0}, tan x)

and I think Ben is asking, would it be an improvement to change this statement to use {x // ∃ (n:ℕ), x = n*π + π/2}ᶜ instead of {x // cos x ≠ 0} ?

view this post on Zulip Eric Wieser (Aug 02 2020 at 10:41):

Presumably there is already a lemma which can translate one .property into the other?

view this post on Zulip Kevin Buzzard (Aug 02 2020 at 10:41):


Last updated: May 16 2021 at 05:21 UTC