feat(Arctan): add more simp lemmas (#27719)

Also add some `positivity` extensions.

Author: yury-harmonic

Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean

@@ -21,26 +21,27 @@ The result of `arctan x + arctan y` is given by `arctan_add`, `arctan_add_eq_add
 
 noncomputable section
 
-namespace Real
-
 open Set Filter
+open scoped Topology
 
-open scoped Topology Real
+namespace Real
 
-theorem tan_add {x y : ℝ}
+variable {x y : ℝ}
+
+theorem tan_add
     (h : ((∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) ∧ ∀ l : ℤ, y ≠ (2 * l + 1) * π / 2) ∨
       (∃ k : ℤ, x = (2 * k + 1) * π / 2) ∧ ∃ l : ℤ, y = (2 * l + 1) * π / 2) :
     tan (x + y) = (tan x + tan y) / (1 - tan x * tan y) := by
   simpa only [← Complex.ofReal_inj, Complex.ofReal_sub, Complex.ofReal_add, Complex.ofReal_div,
     Complex.ofReal_mul, Complex.ofReal_tan] using
     @Complex.tan_add (x : ℂ) (y : ℂ) (by convert h <;> norm_cast)
 
-theorem tan_add' {x y : ℝ}
+theorem tan_add'
     (h : (∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) ∧ ∀ l : ℤ, y ≠ (2 * l + 1) * π / 2) :
     tan (x + y) = (tan x + tan y) / (1 - tan x * tan y) :=
   tan_add (Or.inl h)
 
-theorem tan_two_mul {x : ℝ} : tan (2 * x) = 2 * tan x / (1 - tan x ^ 2) := by
+theorem tan_two_mul : tan (2 * x) = 2 * tan x / (1 - tan x ^ 2) := by
   have := @Complex.tan_two_mul x
   norm_cast at *
 
@@ -110,7 +111,7 @@ theorem arctan_mem_Ioo (x : ℝ) : arctan x ∈ Ioo (-(π / 2)) (π / 2) :=
 theorem range_arctan : range arctan = Ioo (-(π / 2)) (π / 2) :=
   ((EquivLike.surjective _).range_comp _).trans Subtype.range_coe
 
-theorem arctan_tan {x : ℝ} (hx₁ : -(π / 2) < x) (hx₂ : x < π / 2) : arctan (tan x) = x :=
+theorem arctan_tan (hx₁ : -(π / 2) < x) (hx₂ : x < π / 2) : arctan (tan x) = x :=
   Subtype.ext_iff.1 <| tanOrderIso.symm_apply_apply ⟨x, hx₁, hx₂⟩
 
 theorem cos_arctan_pos (x : ℝ) : 0 < cos (arctan x) :=
@@ -134,7 +135,7 @@ theorem neg_pi_div_two_lt_arctan (x : ℝ) : -(π / 2) < arctan x :=
 theorem arctan_eq_arcsin (x : ℝ) : arctan x = arcsin (x / √(1 + x ^ 2)) :=
   Eq.symm <| arcsin_eq_of_sin_eq (sin_arctan x) (mem_Icc_of_Ioo <| arctan_mem_Ioo x)
 
-theorem arcsin_eq_arctan {x : ℝ} (h : x ∈ Ioo (-(1 : ℝ)) 1) :
+theorem arcsin_eq_arctan (h : x ∈ Ioo (-(1 : ℝ)) 1) :
     arcsin x = arctan (x / √(1 - x ^ 2)) := by
   rw_mod_cast [arctan_eq_arcsin, div_pow, sq_sqrt, one_add_div, div_div, ← sqrt_mul,
     mul_div_cancel₀, sub_add_cancel, sqrt_one, div_one] <;> simp at h <;> nlinarith [h.1, h.2]
@@ -145,17 +146,28 @@ theorem arctan_zero : arctan 0 = 0 := by simp [arctan_eq_arcsin]
 @[mono]
 theorem arctan_strictMono : StrictMono arctan := tanOrderIso.symm.strictMono
 
+theorem arctan_mono : Monotone arctan := arctan_strictMono.monotone
+
 @[gcongr]
-lemma arctan_lt_arctan {x y : ℝ} (hxy : x < y) : arctan x < arctan y := arctan_strictMono hxy
+lemma arctan_lt_arctan (hxy : x < y) : arctan x < arctan y := arctan_strictMono hxy
+
+@[simp]
+theorem arctan_lt_arctan_iff : arctan x < arctan y ↔ x < y := arctan_strictMono.lt_iff_lt
 
 @[gcongr]
-lemma arctan_le_arctan {x y : ℝ} (hxy : x ≤ y) : arctan x ≤ arctan y :=
+lemma arctan_le_arctan (hxy : x ≤ y) : arctan x ≤ arctan y :=
   arctan_strictMono.monotone hxy
 
+@[simp]
+theorem arctan_le_arctan_iff : arctan x ≤ arctan y ↔ x ≤ y := arctan_strictMono.le_iff_le
+
 theorem arctan_injective : arctan.Injective := arctan_strictMono.injective
 
 @[simp]
-theorem arctan_eq_zero_iff {x : ℝ} : arctan x = 0 ↔ x = 0 :=
+theorem arctan_inj : arctan x = arctan y ↔ x = y := arctan_injective.eq_iff
+
+@[simp]
+theorem arctan_eq_zero_iff : arctan x = 0 ↔ x = 0 :=
   .trans (by rw [arctan_zero]) arctan_injective.eq_iff
 
 theorem tendsto_arctan_atTop : Tendsto arctan atTop (𝓝[<] (π / 2)) :=
@@ -164,62 +176,85 @@ theorem tendsto_arctan_atTop : Tendsto arctan atTop (𝓝[<] (π / 2)) :=
 theorem tendsto_arctan_atBot : Tendsto arctan atBot (𝓝[>] (-(π / 2))) :=
   tendsto_Ioo_atBot.mp tanOrderIso.symm.tendsto_atBot
 
-theorem arctan_eq_of_tan_eq {x y : ℝ} (h : tan x = y) (hx : x ∈ Ioo (-(π / 2)) (π / 2)) :
+theorem arctan_eq_of_tan_eq (h : tan x = y) (hx : x ∈ Ioo (-(π / 2)) (π / 2)) :
     arctan y = x :=
   injOn_tan (arctan_mem_Ioo _) hx (by rw [tan_arctan, h])
 
 @[simp]
 theorem arctan_one : arctan 1 = π / 4 :=
   arctan_eq_of_tan_eq tan_pi_div_four <| by constructor <;> linarith [pi_pos]
 
+@[simp]
+theorem arctan_eq_pi_div_four : arctan x = π / 4 ↔ x = 1 := arctan_injective.eq_iff' arctan_one
+
 @[simp]
 theorem arctan_neg (x : ℝ) : arctan (-x) = -arctan x := by simp [arctan_eq_arcsin, neg_div]
 
-theorem arctan_eq_arccos {x : ℝ} (h : 0 ≤ x) : arctan x = arccos (√(1 + x ^ 2))⁻¹ := by
+@[simp]
+theorem arctan_eq_neg_pi_div_four : arctan x = -(π / 4) ↔ x = -1 :=
+  arctan_injective.eq_iff' <| by rw [arctan_neg, arctan_one]
+
+@[simp]
+theorem arctan_pos : 0 < arctan x ↔ 0 < x := by
+  simpa only [arctan_zero] using arctan_lt_arctan_iff (x := 0)
+
+@[simp]
+theorem arctan_lt_zero : arctan x < 0 ↔ x < 0 := by
+  simpa only [arctan_zero] using arctan_lt_arctan_iff (y := 0)
+
+@[simp]
+theorem arctan_nonneg : 0 ≤ arctan x ↔ 0 ≤ x := by
+  simpa only [arctan_zero] using arctan_le_arctan_iff (x := 0)
+
+@[simp]
+theorem arctan_le_zero : arctan x ≤ 0 ↔ x ≤ 0 := by
+  simpa only [arctan_zero] using arctan_le_arctan_iff (y := 0)
+
+theorem arctan_eq_arccos (h : 0 ≤ x) : arctan x = arccos (√(1 + x ^ 2))⁻¹ := by
   rw [arctan_eq_arcsin, arccos_eq_arcsin]; swap; · exact inv_nonneg.2 (sqrt_nonneg _)
   congr 1
   rw_mod_cast [← sqrt_inv, sq_sqrt, ← one_div, one_sub_div, add_sub_cancel_left, sqrt_div,
     sqrt_sq h]
   all_goals positivity
 
 -- The junk values for `arccos` and `sqrt` make this true even for `1 < x`.
-theorem arccos_eq_arctan {x : ℝ} (h : 0 < x) : arccos x = arctan (√(1 - x ^ 2) / x) := by
+theorem arccos_eq_arctan (h : 0 < x) : arccos x = arctan (√(1 - x ^ 2) / x) := by
   rw [arccos, eq_comm]
   refine arctan_eq_of_tan_eq ?_ ⟨?_, ?_⟩
   · rw_mod_cast [tan_pi_div_two_sub, tan_arcsin, inv_div]
   · linarith only [arcsin_le_pi_div_two x, pi_pos]
   · linarith only [arcsin_pos.2 h]
 
-theorem arctan_inv_of_pos {x : ℝ} (h : 0 < x) : arctan x⁻¹ = π / 2 - arctan x := by
+theorem arctan_inv_of_pos (h : 0 < x) : arctan x⁻¹ = π / 2 - arctan x := by
   rw [← arctan_tan (x := _ - _), tan_pi_div_two_sub, tan_arctan]
   · norm_num
     exact (arctan_lt_pi_div_two x).trans (half_lt_self_iff.mpr pi_pos)
   · rw [sub_lt_self_iff, ← arctan_zero]
     exact tanOrderIso.symm.strictMono h
 
-theorem arctan_inv_of_neg {x : ℝ} (h : x < 0) : arctan x⁻¹ = -(π / 2) - arctan x := by
+theorem arctan_inv_of_neg (h : x < 0) : arctan x⁻¹ = -(π / 2) - arctan x := by
   have := arctan_inv_of_pos (neg_pos.mpr h)
   rwa [inv_neg, arctan_neg, neg_eq_iff_eq_neg, neg_sub', arctan_neg, neg_neg] at this
 
 section ArctanAdd
 
-lemma arctan_ne_mul_pi_div_two {x : ℝ} : ∀ (k : ℤ), arctan x ≠ (2 * k + 1) * π / 2 := by
+lemma arctan_ne_mul_pi_div_two : ∀ (k : ℤ), arctan x ≠ (2 * k + 1) * π / 2 := by
   by_contra!
   obtain ⟨k, h⟩ := this
   obtain ⟨lb, ub⟩ := arctan_mem_Ioo x
   rw [h, neg_eq_neg_one_mul, mul_div_assoc, mul_lt_mul_right (by positivity)] at lb
   rw [h, ← one_mul (π / 2), mul_div_assoc, mul_lt_mul_right (by positivity)] at ub
   norm_cast at lb ub; change -1 < _ at lb; omega
 
-lemma arctan_add_arctan_lt_pi_div_two {x y : ℝ} (h : x * y < 1) : arctan x + arctan y < π / 2 := by
+lemma arctan_add_arctan_lt_pi_div_two (h : x * y < 1) : arctan x + arctan y < π / 2 := by
   rcases le_or_gt y 0 with hy | hy
   · rw [← add_zero (π / 2), ← arctan_zero]
     exact add_lt_add_of_lt_of_le (arctan_lt_pi_div_two _) (tanOrderIso.symm.monotone hy)
   · rw [← lt_div_iff₀ hy, ← inv_eq_one_div] at h
     replace h : arctan x < arctan y⁻¹ := tanOrderIso.symm.strictMono h
     rwa [arctan_inv_of_pos hy, lt_tsub_iff_right] at h
 
-theorem arctan_add {x y : ℝ} (h : x * y < 1) :
+theorem arctan_add (h : x * y < 1) :
     arctan x + arctan y = arctan ((x + y) / (1 - x * y)) := by
   rw [← arctan_tan (x := _ + _)]
   · congr
@@ -230,7 +265,7 @@ theorem arctan_add {x y : ℝ} (h : x * y < 1) :
     exact arctan_add_arctan_lt_pi_div_two h
   · exact arctan_add_arctan_lt_pi_div_two h
 
-theorem arctan_add_eq_add_pi {x y : ℝ} (h : 1 < x * y) (hx : 0 < x) :
+theorem arctan_add_eq_add_pi (h : 1 < x * y) (hx : 0 < x) :
     arctan x + arctan y = arctan ((x + y) / (1 - x * y)) + π := by
   have hy : 0 < y := by
     have := mul_pos_iff.mp (zero_lt_one.trans h)
@@ -242,23 +277,23 @@ theorem arctan_add_eq_add_pi {x y : ℝ} (h : 1 < x * y) (hx : 0 < x) :
   field_simp
   rw [show -x + -y = -(x + y) by ring, show x * y - 1 = -(1 - x * y) by ring, neg_div_neg_eq]
 
-theorem arctan_add_eq_sub_pi {x y : ℝ} (h : 1 < x * y) (hx : x < 0) :
+theorem arctan_add_eq_sub_pi (h : 1 < x * y) (hx : x < 0) :
     arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π := by
   rw [← neg_mul_neg] at h
   have k := arctan_add_eq_add_pi h (neg_pos.mpr hx)
   rw [show _ / _ = -((x + y) / (1 - x * y)) by ring, ← neg_inj] at k
   simp only [arctan_neg, neg_add, neg_neg, ← sub_eq_add_neg _ π] at k
   exact k
 
-theorem two_mul_arctan {x : ℝ} (h₁ : -1 < x) (h₂ : x < 1) :
+theorem two_mul_arctan (h₁ : -1 < x) (h₂ : x < 1) :
     2 * arctan x = arctan (2 * x / (1 - x ^ 2)) := by
   rw [two_mul, arctan_add (by nlinarith)]; congr 1; ring
 
-theorem two_mul_arctan_add_pi {x : ℝ} (h : 1 < x) :
+theorem two_mul_arctan_add_pi (h : 1 < x) :
     2 * arctan x = arctan (2 * x / (1 - x ^ 2)) + π := by
   rw [two_mul, arctan_add_eq_add_pi (by nlinarith) (by linarith)]; congr 2; ring
 
-theorem two_mul_arctan_sub_pi {x : ℝ} (h : x < -1) :
+theorem two_mul_arctan_sub_pi (h : x < -1) :
     2 * arctan x = arctan (2 * x / (1 - x ^ 2)) - π := by
   rw [two_mul, arctan_add_eq_sub_pi (by nlinarith) (by linarith)]; congr 2; ring
 
@@ -278,11 +313,35 @@ theorem four_mul_arctan_inv_5_sub_arctan_inv_239 : 4 * arctan 5⁻¹ - arctan 23
 
 end ArctanAdd
 
+theorem sin_arctan_strictMono : StrictMono (sin <| arctan ·) := fun x y h ↦
+  strictMonoOn_sin (Ioo_subset_Icc_self <| arctan_mem_Ioo x)
+    (Ioo_subset_Icc_self <| arctan_mem_Ioo y) (arctan_strictMono h)
+
+@[simp]
+theorem sin_arctan_pos : 0 < sin (arctan x) ↔ 0 < x := by
+  simpa using sin_arctan_strictMono.lt_iff_lt (a := 0)
+
+@[simp]
+theorem sin_arctan_lt_zero : sin (arctan x) < 0 ↔ x < 0 := by
+  simpa using sin_arctan_strictMono.lt_iff_lt (b := 0)
+
+@[simp]
+theorem sin_arctan_eq_zero : sin (arctan x) = 0 ↔ x = 0 :=
+  sin_arctan_strictMono.injective.eq_iff' <| by simp
+
+@[simp]
+theorem sin_arctan_nonneg : 0 ≤ sin (arctan x) ↔ 0 ≤ x := by
+  simpa using sin_arctan_strictMono.le_iff_le (a := 0)
+
+@[simp]
+theorem sin_arctan_le_zero : sin (arctan x) ≤ 0 ↔ x ≤ 0 := by
+  simpa using sin_arctan_strictMono.le_iff_le (b := 0)
+
 @[continuity]
 theorem continuous_arctan : Continuous arctan :=
   continuous_subtype_val.comp tanOrderIso.toHomeomorph.continuous_invFun
 
-theorem continuousAt_arctan {x : ℝ} : ContinuousAt arctan x :=
+theorem continuousAt_arctan : ContinuousAt arctan x :=
   continuous_arctan.continuousAt
 
 /-- `Real.tan` as a `PartialHomeomorph` between `(-(π / 2), π / 2)` and the whole line. -/
@@ -309,3 +368,44 @@ theorem coe_tanPartialHomeomorph_symm : ⇑tanPartialHomeomorph.symm = arctan :=
   rfl
 
 end Real
+
+namespace Mathlib.Meta.Positivity
+open Lean Meta Qq
+
+/-- Extension for `Real.arctan`. -/
+@[positivity Real.arctan _]
+def evalRealArctan : PositivityExt where eval {u α} z p e := do
+  match u, α, e with
+  | 0, ~q(ℝ), ~q(Real.arctan $a) =>
+    let ra ← core z p a
+    assumeInstancesCommute
+    match ra with
+    | .positive pa => return .positive q(Real.arctan_pos.mpr $pa)
+    | .nonnegative na => return .nonnegative q(Real.arctan_nonneg.mpr $na)
+    | .nonzero na => return .nonzero q(mt Real.arctan_eq_zero_iff.mp $na)
+    | .none => return .none
+  | _ => throwError "not Real.arctan"
+
+/-- Extension for `Real.cos (Real.arctan _)`. -/
+@[positivity Real.cos (Real.arctan _)]
+def evalRealCosArctan : PositivityExt where eval {u α} _ _ e := do
+  match u, α, e with
+  | 0, ~q(ℝ), ~q(Real.cos (Real.arctan $a)) =>
+    assumeInstancesCommute
+    return .positive q(Real.cos_arctan_pos _)
+  | _ => throwError "not Real.cos (Real.arctan _)"
+
+/-- Extension for `Real.sin (Real.arctan _)`. -/
+@[positivity Real.sin (Real.arctan _)]
+def evalRealSinArctan : PositivityExt where eval {u α} z p e := do
+  match u, α, e with
+  | 0, ~q(ℝ), ~q(Real.sin (Real.arctan $a)) =>
+    assumeInstancesCommute
+    match ← core z p a with
+    | .positive pa => return .positive q(Real.sin_arctan_pos.mpr $pa)
+    | .nonnegative na => return .nonnegative q(Real.sin_arctan_nonneg.mpr $na)
+    | .nonzero na => return .nonzero q(mt Real.sin_arctan_eq_zero.mp $na)
+    | .none => return .none
+  | _ => throwError "not Real.sin (Real.arctan _)"
+
+end Mathlib.Meta.Positivity

MathlibTest/positivity.lean

@@ -5,6 +5,7 @@ import Mathlib.Data.ENNReal.Basic
 import Mathlib.Analysis.Normed.Group.Basic
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
 import Mathlib.Analysis.SpecialFunctions.Log.Basic
+import Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
 import Mathlib.MeasureTheory.Integral.Bochner.Basic
 import Mathlib.Topology.Algebra.InfiniteSum.Order
 
@@ -419,6 +420,14 @@ example : 0 ≤ Real.log 1 := by positivity
 example : 0 ≤ Real.log 0 := by positivity
 example : 0 ≤ Real.log (-1) := by positivity
 
+example : 0 < Real.arctan 1.1 := by positivity
+example {r : ℝ} (hr : 0 ≤ r) : 0 ≤ Real.arctan r := by positivity
+example {r : ℝ} (hr : r ≠ 0) : Real.arctan r ≠ 0 := by positivity
+example (r : ℝ) : 0 < Real.cos (Real.arctan r) := by positivity
+example {r : ℝ} (hr : 0 < r) : 0 < Real.sin (Real.arctan r) := by positivity
+example {r : ℝ} (hr : r ≠ 0) : Real.sin (Real.arctan r) ≠ 0 := by positivity
+example {r : ℝ} (hr : 0 ≤ r) : 0 ≤ Real.sin (Real.arctan r) := by positivity
+
 end SpecialFunctions
 
 /-! ### `sqrt` on `ℝ` and `ℝ≥0` -/