[Merged by Bors] - feat(analysis/special_functions/trigonometric): Added lemmas for deriv of tan

[benjamindavidson]

I added lemmas for the derivative of the tangent function in both the complex and real namespaces. I also corrected two typos in comment lines.

[jcommelin]

LGTM

[PatrickMassot]

I don't understand at all why you have this assumption of non-vanishing cosine everywhere. Why not

lemma has_deriv_at_tan {x:ℝ} (h : ∀ k : ℤ, x ≠ (2 * k + 1) * pi / 2) : has_deriv_at tan (1 / (cos x)^2) x :=
begin
  rw [← cos_ne_zero_iff, ← complex.of_real_ne_zero, complex.of_real_cos] at h,
  convert has_deriv_at_real_of_complex (complex.has_deriv_at_tan h),
  rw ← complex.of_real_re (1/((cos x)^2)),
  simp,
end

Even better would be to take the time to do cos_ne_zero_iff for complex cosine as well, and have this assumption in the complex version as well. If you really have an assumption about cos(x) then you can still use cos_ne_zero_iff before using it, but I think the lemma about tan should have the natural statement.

[benjamindavidson]

I made the changes that Patrick requested regarding the assumption in my lemmas, both in complex and in real. See the conversation in this Zulip chat.
I added complex.cos_eq_zero_iff and its corollary complex.cos_ne_zero_iff and rewrote real.cos_eq_zero_iff to be derived from the complex version.
Also added exp_pi_mul_I (Euler's identity).

[PatrickMassot]

Could you please make sure all lines are at most 100+epsilon columns long?

[PatrickMassot]

This lemma doesn't need assumption h.

[PatrickMassot]

This lemma doesn't need assumption h (both sides of the equality vanish when x = (2 * k + 1) * π / 2).

[benjamindavidson]

I tried to accomplish this and I managed to do it in part, but I think that there is not yet the infrastructure in mathlib supporting ¬differentiable_at for me to be able to complete the proof.
I think this is substantiated by the fact that the lemma deriv_inv uses the assumption x≠0, presumably for this very reason.

[PatrickMassot]

Ok, I'll fix this later. Thanks for your work on this PR!
bors merge

[bors]

👎 Rejected by label

[robertylewis]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests