Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: port Analysis.SpecialFunctions.Trigonometric.ComplexDeriv (#4753)
- Loading branch information
1 parent
22a865f
commit 02219c1
Showing
2 changed files
with
83 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
82 changes: 82 additions & 0 deletions
82
Mathlib/Analysis/SpecialFunctions/Trigonometric/ComplexDeriv.lean
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,82 @@ | ||
/- | ||
Copyright (c) 2018 Chris Hughes. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin Davidson | ||
! This file was ported from Lean 3 source module analysis.special_functions.trigonometric.complex_deriv | ||
! leanprover-community/mathlib commit 2c1d8ca2812b64f88992a5294ea3dba144755cd1 | ||
! Please do not edit these lines, except to modify the commit id | ||
! if you have ported upstream changes. | ||
-/ | ||
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex | ||
|
||
/-! | ||
# Complex trigonometric functions | ||
Basic facts and derivatives for the complex trigonometric functions. | ||
-/ | ||
|
||
|
||
noncomputable section | ||
|
||
local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue #2220 | ||
|
||
namespace Complex | ||
|
||
open Set Filter | ||
|
||
open scoped Real | ||
|
||
theorem hasStrictDerivAt_tan {x : ℂ} (h : cos x ≠ 0) : HasStrictDerivAt tan (1 / cos x ^ 2) x := by | ||
convert (hasStrictDerivAt_sin x).div (hasStrictDerivAt_cos x) h using 1 | ||
rw_mod_cast [← sin_sq_add_cos_sq x] | ||
ring | ||
#align complex.has_strict_deriv_at_tan Complex.hasStrictDerivAt_tan | ||
|
||
theorem hasDerivAt_tan {x : ℂ} (h : cos x ≠ 0) : HasDerivAt tan (1 / cos x ^ 2) x := | ||
(hasStrictDerivAt_tan h).hasDerivAt | ||
#align complex.has_deriv_at_tan Complex.hasDerivAt_tan | ||
|
||
open scoped Topology | ||
|
||
theorem tendsto_abs_tan_of_cos_eq_zero {x : ℂ} (hx : cos x = 0) : | ||
Tendsto (fun x => abs (tan x)) (𝓝[≠] x) atTop := by | ||
simp only [tan_eq_sin_div_cos, ← norm_eq_abs, norm_div] | ||
have A : sin x ≠ 0 := fun h => by simpa [*, sq] using sin_sq_add_cos_sq x | ||
have B : Tendsto cos (𝓝[≠] x) (𝓝[≠] 0) := | ||
hx ▸ (hasDerivAt_cos x).tendsto_punctured_nhds (neg_ne_zero.2 A) | ||
exact continuous_sin.continuousWithinAt.norm.mul_atTop (norm_pos_iff.2 A) | ||
(tendsto_norm_nhdsWithin_zero.comp B).inv_tendsto_zero | ||
#align complex.tendsto_abs_tan_of_cos_eq_zero Complex.tendsto_abs_tan_of_cos_eq_zero | ||
|
||
theorem tendsto_abs_tan_atTop (k : ℤ) : | ||
Tendsto (fun x => abs (tan x)) (𝓝[≠] ((2 * k + 1) * π / 2 : ℂ)) atTop := | ||
tendsto_abs_tan_of_cos_eq_zero <| cos_eq_zero_iff.2 ⟨k, rfl⟩ | ||
#align complex.tendsto_abs_tan_at_top Complex.tendsto_abs_tan_atTop | ||
|
||
@[simp] | ||
theorem continuousAt_tan {x : ℂ} : ContinuousAt tan x ↔ cos x ≠ 0 := by | ||
refine' ⟨fun hc h₀ => _, fun h => (hasDerivAt_tan h).continuousAt⟩ | ||
exact not_tendsto_nhds_of_tendsto_atTop (tendsto_abs_tan_of_cos_eq_zero h₀) _ | ||
(hc.norm.tendsto.mono_left inf_le_left) | ||
#align complex.continuous_at_tan Complex.continuousAt_tan | ||
|
||
@[simp] | ||
theorem differentiableAt_tan {x : ℂ} : DifferentiableAt ℂ tan x ↔ cos x ≠ 0 := | ||
⟨fun h => continuousAt_tan.1 h.continuousAt, fun h => (hasDerivAt_tan h).differentiableAt⟩ | ||
#align complex.differentiable_at_tan Complex.differentiableAt_tan | ||
|
||
@[simp] | ||
theorem deriv_tan (x : ℂ) : deriv tan x = 1 / cos x ^ 2 := | ||
if h : cos x = 0 then by | ||
have : ¬DifferentiableAt ℂ tan x := mt differentiableAt_tan.1 (Classical.not_not.2 h) | ||
simp [deriv_zero_of_not_differentiableAt this, h, sq] | ||
else (hasDerivAt_tan h).deriv | ||
#align complex.deriv_tan Complex.deriv_tan | ||
|
||
@[simp] | ||
theorem contDiffAt_tan {x : ℂ} {n : ℕ∞} : ContDiffAt ℂ n tan x ↔ cos x ≠ 0 := | ||
⟨fun h => continuousAt_tan.1 h.continuousAt, contDiff_sin.contDiffAt.div contDiff_cos.contDiffAt⟩ | ||
#align complex.cont_diff_at_tan Complex.contDiffAt_tan | ||
|
||
end Complex |