chore(analysis/special_functions/trigonometric): review continuity of…

… `tan` (#5429)

* prove that `tan` is discontinuous at `x` whenever `cos x = 0`;
* turn `continuous_at_tan` and `differentiable_at_tan` into `iff` lemmas;
* reformulate various lemmas in terms of `cos x = 0` instead of `∃ k, x = ...`;



Co-authored-by: Patrick Massot <patrickmassot@free.fr>

src/analysis/complex/basic.lean

@@ -120,6 +120,8 @@ calc 1 = ∥continuous_linear_map.im I∥ : by simp
 /-- Continuous linear map version of the canonical embedding of `ℝ` in `ℂ`. -/
 def continuous_linear_map.of_real : ℝ →L[ℝ] ℂ := linear_map.of_real.to_continuous_linear_map
 
+lemma continuous_of_real : continuous (coe : ℝ → ℂ) := continuous_linear_map.of_real.continuous
+
 @[simp] lemma continuous_linear_map.of_real_coe :
   (coe (continuous_linear_map.of_real) : ℝ →ₗ[ℝ] ℂ) = linear_map.of_real := rfl
 

src/analysis/special_functions/trigonometric.lean

@@ -34,7 +34,7 @@ log, sin, cos, tan, arcsin, arccos, arctan, angle, argument
 -/
 
 noncomputable theory
-open_locale classical topological_space
+open_locale classical topological_space filter
 open set filter
 
 namespace complex
@@ -1622,6 +1622,8 @@ begin
   exact div_self (ne_of_gt h),
 end
 
+@[simp] lemma tan_pi_div_two : tan (π / 2) = 0 := by simp [tan_eq_sin_div_cos]
+
 lemma tan_pos_of_pos_of_lt_pi_div_two {x : ℝ} (h0x : 0 < x) (hxp : x < π / 2) : 0 < tan x :=
 by rw tan_eq_sin_div_cos; exact div_pos (sin_pos_of_pos_of_lt_pi h0x (by linarith))
   (cos_pos_of_mem_Ioo ⟨by linarith, hxp⟩)
@@ -2169,19 +2171,46 @@ begin
   refine exists_congr (λ k, or_congr _ _); refine eq.congr rfl _; field_simp; ring
 end
 
-lemma has_deriv_at_tan {x : ℂ} (h : ∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) :
+lemma has_deriv_at_tan {x : ℂ} (h : cos x ≠ 0) :
   has_deriv_at tan (1 / (cos x)^2) x :=
 begin
-  convert has_deriv_at.div (has_deriv_at_sin x) (has_deriv_at_cos x) (cos_ne_zero_iff.mpr h),
+  convert has_deriv_at.div (has_deriv_at_sin x) (has_deriv_at_cos x) h,
   rw ← sin_sq_add_cos_sq x,
   ring,
 end
 
-lemma differentiable_at_tan {x : ℂ} (h : ∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) : differentiable_at ℂ tan x :=
-(has_deriv_at_tan h).differentiable_at
+lemma tendsto_abs_tan_of_cos_eq_zero {x : ℂ} (hx : cos x = 0) :
+  tendsto (λ x, abs (tan x)) (𝓝[{x}ᶜ] x) at_top :=
+begin
+  simp only [tan_eq_sin_div_cos, ← norm_eq_abs, normed_field.norm_div],
+  have A : sin x ≠ 0 := λ h, by simpa [*, pow_two] using sin_sq_add_cos_sq x,
+  have B : tendsto cos (𝓝[{x}ᶜ] (x)) (𝓝[{0}ᶜ] 0),
+  { refine tendsto_inf.2 ⟨tendsto.mono_left _ inf_le_left, tendsto_principal.2 _⟩,
+    exacts [continuous_cos.tendsto' x 0 hx,
+      hx ▸ (has_deriv_at_cos _).eventually_ne (neg_ne_zero.2 A)] },
+  exact tendsto.mul_at_top (norm_pos_iff.2 A) continuous_sin.continuous_within_at.norm
+    (tendsto.inv_tendsto_zero $ tendsto_norm_nhds_within_zero.comp B),
+end
+
+lemma tendsto_abs_tan_at_top (k : ℤ) :
+  tendsto (λ x, abs (tan x)) (𝓝[{(2 * k + 1) * π / 2}ᶜ] ((2 * k + 1) * π / 2)) at_top :=
+tendsto_abs_tan_of_cos_eq_zero $ cos_eq_zero_iff.2 ⟨k, rfl⟩
+
+@[simp] lemma continuous_at_tan {x : ℂ} : continuous_at tan x ↔ cos x ≠ 0 :=
+begin
+  refine ⟨λ hc h₀, _, λ h, (has_deriv_at_tan h).continuous_at⟩,
+  exact not_tendsto_nhds_of_tendsto_at_top (tendsto_abs_tan_of_cos_eq_zero h₀) _
+    (hc.norm.tendsto.mono_left inf_le_left)
+end
+
+@[simp] lemma differentiable_at_tan {x : ℂ} : differentiable_at ℂ tan x ↔ cos x ≠ 0:=
+⟨λ h, continuous_at_tan.1 h.continuous_at, λ h, (has_deriv_at_tan h).differentiable_at⟩
 
-@[simp] lemma deriv_tan {x : ℂ} (h : ∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) : deriv tan x = 1 / (cos x)^2 :=
-(has_deriv_at_tan h).deriv
+@[simp] lemma deriv_tan (x : ℂ) : deriv tan x = 1 / (cos x)^2 :=
+if h : cos x = 0 then
+  have ¬differentiable_at ℂ tan x := mt differentiable_at_tan.1 (not_not.2 h),
+  by simp [deriv_zero_of_not_differentiable_at this, h, pow_two]
+else (has_deriv_at_tan h).deriv
 
 lemma continuous_on_tan : continuous_on tan {x | cos x ≠ 0} :=
 continuous_on_sin.div continuous_on_cos $ λ x, id
@@ -2270,47 +2299,53 @@ lemma sin_eq_sin_iff {x y : ℝ} :
   sin x = sin y ↔ ∃ k : ℤ, y = 2 * k * π + x ∨ y = (2 * k + 1) * π - x :=
 by exact_mod_cast @complex.sin_eq_sin_iff x y
 
-lemma has_deriv_at_tan {x : ℝ} (h : ∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) :
+lemma has_deriv_at_tan {x : ℝ} (h : cos x ≠ 0) :
   has_deriv_at tan (1 / (cos x)^2) x :=
+by exact_mod_cast (complex.has_deriv_at_tan (by exact_mod_cast h)).real_of_complex
+
+lemma tendsto_abs_tan_of_cos_eq_zero {x : ℝ} (hx : cos x = 0) :
+  tendsto (λ x, abs (tan x)) (𝓝[{x}ᶜ] x) at_top :=
 begin
-  convert (complex.has_deriv_at_tan (by { convert h, norm_cast } )).real_of_complex,
-  rw ← complex.of_real_re (1/((cos x)^2)),
-  simp,
+  have hx : complex.cos x = 0, by exact_mod_cast hx,
+  simp only [← complex.abs_of_real, complex.of_real_tan],
+  refine (complex.tendsto_abs_tan_of_cos_eq_zero hx).comp _,
+  refine tendsto.inf complex.continuous_of_real.continuous_at _,
+  exact tendsto_principal_principal.2 (λ y, mt complex.of_real_inj.1)
 end
 
-lemma differentiable_at_tan {x : ℝ} (h : ∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) : differentiable_at ℝ tan x :=
-(has_deriv_at_tan h).differentiable_at
+lemma tendsto_abs_tan_at_top (k : ℤ) :
+  tendsto (λ x, abs (tan x)) (𝓝[{(2 * k + 1) * π / 2}ᶜ] ((2 * k + 1) * π / 2)) at_top :=
+tendsto_abs_tan_of_cos_eq_zero $ cos_eq_zero_iff.2 ⟨k, rfl⟩
 
-@[simp] lemma deriv_tan {x : ℝ} (h : ∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) : deriv tan x = 1 / (cos x)^2 :=
-(has_deriv_at_tan h).deriv
+lemma continuous_at_tan {x : ℝ} : continuous_at tan x ↔ cos x ≠ 0 :=
+begin
+  refine ⟨λ hc h₀, _, λ h, (has_deriv_at_tan h).continuous_at⟩,
+  exact not_tendsto_nhds_of_tendsto_at_top (tendsto_abs_tan_of_cos_eq_zero h₀) _
+    (hc.norm.tendsto.mono_left inf_le_left)
+end
 
-lemma continuous_tan : continuous (λ x : {x | cos x ≠ 0}, tan x) :=
-by simp only [tan_eq_sin_div_cos]; exact
-  (continuous_sin.comp continuous_subtype_val).mul
-  (continuous.inv subtype.property
-    (continuous_cos.comp continuous_subtype_val))
+lemma differentiable_at_tan {x : ℝ} : differentiable_at ℝ tan x ↔ cos x ≠ 0 :=
+⟨λ h, continuous_at_tan.1 h.continuous_at, λ h, (has_deriv_at_tan h).differentiable_at⟩
+
+@[simp] lemma deriv_tan (x : ℝ) : deriv tan x = 1 / (cos x)^2 :=
+if h : cos x = 0 then
+  have ¬differentiable_at ℝ tan x := mt differentiable_at_tan.1 (not_not.2 h),
+  by simp [deriv_zero_of_not_differentiable_at this, h, pow_two]
+else (has_deriv_at_tan h).deriv
 
 lemma continuous_on_tan : continuous_on tan {x | cos x ≠ 0} :=
-by { rw continuous_on_iff_continuous_restrict, convert continuous_tan }
+λ x hx, (continuous_at_tan.2 hx).continuous_within_at
 
 lemma has_deriv_at_tan_of_mem_Ioo {x : ℝ} (h : x ∈ Ioo (-(π/2):ℝ) (π/2)) :
   has_deriv_at tan (1 / (cos x)^2) x :=
-has_deriv_at_tan (cos_ne_zero_iff.mp (ne_of_gt (cos_pos_of_mem_Ioo h)))
+has_deriv_at_tan (cos_pos_of_mem_Ioo h).ne'
 
 lemma differentiable_at_tan_of_mem_Ioo {x : ℝ} (h : x ∈ Ioo (-(π/2):ℝ) (π/2)) :
   differentiable_at ℝ tan x :=
 (has_deriv_at_tan_of_mem_Ioo h).differentiable_at
 
-lemma deriv_tan_of_mem_Ioo {x : ℝ} (h : x ∈ Ioo (-(π/2):ℝ) (π/2)) : deriv tan x = 1 / (cos x)^2 :=
-(has_deriv_at_tan_of_mem_Ioo h).deriv
-
 lemma continuous_on_tan_Ioo : continuous_on tan (Ioo (-(π/2)) (π/2)) :=
-begin
-  refine continuous_on_tan.mono _,
-  intros x hx,
-  simp only [mem_set_of_eq],
-  exact ne_of_gt (cos_pos_of_mem_Ioo hx),
-end
+λ x hx, (differentiable_at_tan_of_mem_Ioo hx).continuous_at.continuous_within_at
 
 open filter
 open_locale topological_space
@@ -2379,7 +2414,7 @@ begin
   have h1 : 0 < 1 + x^2 := by nlinarith,
   have h2 : cos (arctan x) ≠ 0 := by { rw cos_arctan, exact ne_of_gt (one_div_pos.mpr (sqrt_pos.mpr h1)) },
   simpa [(cos_arctan x), sqr_sqrt (le_of_lt h1)] using has_deriv_at.of_local_left_inverse
-    continuous_arctan.continuous_at (has_deriv_at_tan (cos_ne_zero_iff.mp h2))
+    continuous_arctan.continuous_at (has_deriv_at_tan h2)
       (one_div_ne_zero (pow_ne_zero 2 h2)) (by {apply eventually_of_forall, exact tan_arctan} ),
 end