{"count": 320, "header": "Found 320 declarations mentioning Real.sin.\nOf these, only the first 200 are shown.\n", "heartbeats": 3, "hits": [{"doc": "The real sine function, defined as the real part of the complex sine ", "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.sin", "type": " (x : \u211d) : \u211d"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Complex.ofReal_sin", "type": " (x : \u211d) : \u2191(Real.sin x) = Complex.sin \u2191x"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Complex.sin_ofReal_re", "type": " (x : \u211d) : (Complex.sin \u2191x).re = Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.sin_le_one", "type": " (x : \u211d) : Real.sin x \u2264 1"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.sin_neg", "type": " (x : \u211d) : Real.sin (-x) = -Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.neg_one_le_sin", "type": " (x : \u211d) : -1 \u2264 Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.sin_zero", "type": " : Real.sin 0 = 0"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.abs_sin_le_one", "type": " (x : \u211d) : |Real.sin x| \u2264 1"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Complex.exp_ofReal_mul_I_im", "type": " (x : \u211d) : (Complex.exp (\u2191x * Complex.I)).im = Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.cot_eq_cos_div_sin", "type": " (x : \u211d) : x.cot = Real.cos x / Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.tan_eq_sin_div_cos", "type": " (x : \u211d) : Real.tan x = Real.sin x / Real.cos x"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Complex.exp_im", "type": " (x : \u2102) : (Complex.exp x).im = Real.exp x.re * Real.sin x.im"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.tan_mul_cos", "type": " {x : \u211d} (hx : Real.cos x \u2260 0) : Real.tan x * Real.cos x = Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.sin_sq_le_one", "type": " (x : \u211d) : Real.sin x ^ 2 \u2264 1"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.sin_pos_of_pos_of_le_one", "type": " {x : \u211d} (hx0 : 0 < x) (hx : x \u2264 1) : 0 < Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Complex.exp_ofReal_mul_I", "type": " (x : \u211d) : Complex.exp (\u2191x * Complex.I) = \u2191(Real.cos x) + \u2191(Real.sin x) * Complex.I"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.abs_cos_eq_sqrt_one_sub_sin_sq", "type": " (x : \u211d) : |Real.cos x| = \u221a(1 - Real.sin x ^ 2)"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.abs_sin_eq_sqrt_one_sub_cos_sq", "type": " (x : \u211d) : |Real.sin x| = \u221a(1 - Real.cos x ^ 2)"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.cos_add", "type": " (x y : \u211d) : Real.cos (x + y) = Real.cos x * Real.cos y - Real.sin x * Real.sin y"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.cos_sub", "type": " (x y : \u211d) : Real.cos (x - y) = Real.cos x * Real.cos y + Real.sin x * Real.sin y"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.sin_add", "type": " (x y : \u211d) : Real.sin (x + y) = Real.sin x * Real.cos y + Real.cos x * Real.sin y"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.sin_sub", "type": " (x y : \u211d) : Real.sin (x - y) = Real.sin x * Real.cos y - Real.cos x * Real.sin y"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.sin_pos_of_pos_of_le_two", "type": " {x : \u211d} (hx0 : 0 < x) (hx : x \u2264 2) : 0 < Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.cos_sq'", "type": " (x : \u211d) : Real.cos x ^ 2 = 1 - Real.sin x ^ 2"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.cos_sq_add_sin_sq", "type": " (x : \u211d) : Real.cos x ^ 2 + Real.sin x ^ 2 = 1"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.sin_sq", "type": " (x : \u211d) : Real.sin x ^ 2 = 1 - Real.cos x ^ 2"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.sin_sq_add_cos_sq", "type": " (x : \u211d) : Real.sin x ^ 2 + Real.cos x ^ 2 = 1"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.tan_div_sqrt_one_add_tan_sq", "type": " {x : \u211d} (hx : 0 < Real.cos x) : Real.tan x / \u221a(1 + Real.tan x ^ 2) = Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.sin_two_mul", "type": " (x : \u211d) : Real.sin (2 * x) = 2 * Real.sin x * Real.cos x"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.two_mul_sin_mul_cos", "type": " (x y : \u211d) : 2 * Real.sin x * Real.cos y = Real.sin (x - y) + Real.sin (x + y)"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.two_mul_sin_mul_sin", "type": " (x y : \u211d) : 2 * Real.sin x * Real.sin y = Real.cos (x - y) - Real.cos (x + y)"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.cos_two_mul'", "type": " (x : \u211d) : Real.cos (2 * x) = Real.cos x ^ 2 - Real.sin x ^ 2"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.tan_sq_div_one_add_tan_sq", "type": " {x : \u211d} (hx : Real.cos x \u2260 0) : Real.tan x ^ 2 / (1 + Real.tan x ^ 2) = Real.sin x ^ 2"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.cos_two_mul_eq_one_sub", "type": " (x : \u211d) : Real.cos (2 * x) = 1 - 2 * Real.sin x ^ 2"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Complex.norm_exp_I_mul_ofReal_sub_one", "type": " (x : \u211d) : \u2016Complex.exp (Complex.I * \u2191x) - 1\u2016 = \u20162 * Real.sin (x / 2)\u2016"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.sin_three_mul", "type": " (x : \u211d) : Real.sin (3 * x) = 3 * Real.sin x - 4 * Real.sin x ^ 3"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.sin_sq_eq_half_sub", "type": " (x : \u211d) : Real.sin x ^ 2 = 1 / 2 - Real.cos (2 * x) / 2"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.sin_add_sin", "type": " (x y : \u211d) : Real.sin x + Real.sin y = 2 * Real.sin ((x + y) / 2) * Real.cos ((x - y) / 2)"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.sin_sub_sin", "type": " (x y : \u211d) : Real.sin x - Real.sin y = 2 * Real.sin ((x - y) / 2) * Real.cos ((x + y) / 2)"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.cos_sub_cos", "type": " (x y : \u211d) : Real.cos x - Real.cos y = -2 * Real.sin ((x + y) / 2) * Real.sin ((x - y) / 2)"}, {"doc": null, "module": "Mathlib.Analysis.Complex.Trigonometric", "name": "Real.sin_bound", "type": " {x : \u211d} (hx : |x| \u2264 1) : |Real.sin x - (x - x ^ 3 / 6)| \u2264 |x| ^ 4 * (5 / 96)"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.range_sin_infinite", "type": " : (Set.range Real.sin).Infinite"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_antiperiodic", "type": " : Function.Antiperiodic Real.sin Real.pi"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_pi", "type": " : Real.sin Real.pi = 0"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.continuous_sin", "type": " : Continuous Real.sin"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_pi_sub", "type": " (x : \u211d) : Real.sin (Real.pi - x) = Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.continuousOn_sin", "type": " {s : Set \u211d} : ContinuousOn Real.sin s"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_add_pi", "type": " (x : \u211d) : Real.sin (x + Real.pi) = -Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_sub_pi", "type": " (x : \u211d) : Real.sin (x - Real.pi) = -Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_int_mul_pi", "type": " (n : \u2124) : Real.sin (\u2191n * Real.pi) = 0"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_nat_mul_pi", "type": " (n : \u2115) : Real.sin (\u2191n * Real.pi) = 0"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.abs_sin_eq_sin_abs_of_abs_le_pi", "type": " {x : \u211d} (hx : |x| \u2264 Real.pi) : |Real.sin x| = Real.sin |x|"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.mapsTo_sin", "type": " (s : Set \u211d) : Set.MapsTo Real.sin s (Set.Icc (-1) 1)"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.range_sin", "type": " : Set.range Real.sin = Set.Icc (-1) 1"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_mem_Icc", "type": " (x : \u211d) : Real.sin x \u2208 Set.Icc (-1) 1"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_nonneg_of_nonneg_of_le_pi", "type": " {x : \u211d} (h0x : 0 \u2264 x) (hxp : x \u2264 Real.pi) : 0 \u2264 Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_pos_of_pos_of_lt_pi", "type": " {x : \u211d} (h0x : 0 < x) (hxp : x < Real.pi) : 0 < Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_ne_zero_iff", "type": " {x : \u211d} : Real.sin x \u2260 0 \u2194 \u2200 (n : \u2124), \u2191n * Real.pi \u2260 x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_nonneg_of_mem_Icc", "type": " {x : \u211d} (hx : x \u2208 Set.Icc 0 Real.pi) : 0 \u2264 Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_pos_of_mem_Ioo", "type": " {x : \u211d} (hx : x \u2208 Set.Ioo 0 Real.pi) : 0 < Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_eq_zero_iff", "type": " {x : \u211d} : Real.sin x = 0 \u2194 \u2203 n, \u2191n * Real.pi = x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_neg_of_neg_of_neg_pi_lt", "type": " {x : \u211d} (hx0 : x < 0) (hpx : -Real.pi < x) : Real.sin x < 0"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_nonpos_of_nonpos_of_neg_pi_le", "type": " {x : \u211d} (hx0 : x \u2264 0) (hpx : -Real.pi \u2264 x) : Real.sin x \u2264 0"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_periodic", "type": " : Function.Periodic Real.sin (2 * Real.pi)"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_eq_zero_iff_of_lt_of_lt", "type": " {x : \u211d} (hx\u2081 : -Real.pi < x) (hx\u2082 : x < Real.pi) : Real.sin x = 0 \u2194 x = 0"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.cos_eq_zero_iff_sin_eq", "type": " {x : \u211d} : Real.cos x = 0 \u2194 Real.sin x = 1 \u2228 Real.sin x = -1"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_eq_zero_iff_cos_eq", "type": " {x : \u211d} : Real.sin x = 0 \u2194 Real.cos x = 1 \u2228 Real.cos x = -1"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_two_pi", "type": " : Real.sin (2 * Real.pi) = 0"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_pi_div_two", "type": " : Real.sin (Real.pi / 2) = 1"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_add_two_pi", "type": " (x : \u211d) : Real.sin (x + 2 * Real.pi) = Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_sub_two_pi", "type": " (x : \u211d) : Real.sin (x - 2 * Real.pi) = Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.cos_pi_div_two_sub", "type": " (x : \u211d) : Real.cos (Real.pi / 2 - x) = Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.cos_sub_pi_div_two", "type": " (x : \u211d) : Real.cos (x - Real.pi / 2) = Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_add_pi_div_two", "type": " (x : \u211d) : Real.sin (x + Real.pi / 2) = Real.cos x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_pi_div_two_sub", "type": " (x : \u211d) : Real.sin (Real.pi / 2 - x) = Real.cos x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_two_pi_sub", "type": " (x : \u211d) : Real.sin (2 * Real.pi - x) = -Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.cos_add_pi_div_two", "type": " (x : \u211d) : Real.cos (x + Real.pi / 2) = -Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_sub_pi_div_two", "type": " (x : \u211d) : Real.sin (x - Real.pi / 2) = -Real.cos x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_eq_sqrt_one_sub_cos_sq", "type": " {x : \u211d} (hl : 0 \u2264 x) (hu : x \u2264 Real.pi) : Real.sin x = \u221a(1 - Real.cos x ^ 2)"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_add_int_mul_two_pi", "type": " (x : \u211d) (n : \u2124) : Real.sin (x + \u2191n * (2 * Real.pi)) = Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_add_nat_mul_two_pi", "type": " (x : \u211d) (n : \u2115) : Real.sin (x + \u2191n * (2 * Real.pi)) = Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_sub_int_mul_two_pi", "type": " (x : \u211d) (n : \u2124) : Real.sin (x - \u2191n * (2 * Real.pi)) = Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_sub_nat_mul_two_pi", "type": " (x : \u211d) (n : \u2115) : Real.sin (x - \u2191n * (2 * Real.pi)) = Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_add_int_mul_pi", "type": " (x : \u211d) (n : \u2124) : Real.sin (x + \u2191n * Real.pi) = (-1) ^ n * Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_add_nat_mul_pi", "type": " (x : \u211d) (n : \u2115) : Real.sin (x + \u2191n * Real.pi) = (-1) ^ n * Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_sub_int_mul_pi", "type": " (x : \u211d) (n : \u2124) : Real.sin (x - \u2191n * Real.pi) = (-1) ^ n * Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_sub_nat_mul_pi", "type": " (x : \u211d) (n : \u2115) : Real.sin (x - \u2191n * Real.pi) = (-1) ^ n * Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_int_mul_two_pi_sub", "type": " (x : \u211d) (n : \u2124) : Real.sin (\u2191n * (2 * Real.pi) - x) = -Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_nat_mul_two_pi_sub", "type": " (x : \u211d) (n : \u2115) : Real.sin (\u2191n * (2 * Real.pi) - x) = -Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_int_mul_pi_sub", "type": " (x : \u211d) (n : \u2124) : Real.sin (\u2191n * Real.pi - x) = -((-1) ^ n * Real.sin x)"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_nat_mul_pi_sub", "type": " (x : \u211d) (n : \u2115) : Real.sin (\u2191n * Real.pi - x) = -((-1) ^ n * Real.sin x)"}, {"doc": "The sine of `\u03c0 / 6` is `1 / 2`. ", "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_pi_div_six", "type": " : Real.sin (Real.pi / 6) = 1 / 2"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.injOn_sin", "type": " : Set.InjOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2))"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.monotoneOn_sin", "type": " : MonotoneOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2))"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.strictMonoOn_sin", "type": " : StrictMonoOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2))"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_pi_div_four", "type": " : Real.sin (Real.pi / 4) = \u221a2 / 2"}, {"doc": "The sine of `\u03c0 / 3` is `\u221a3 / 2`. ", "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_pi_div_three", "type": " : Real.sin (Real.pi / 3) = \u221a3 / 2"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.abs_sin_half", "type": " (x : \u211d) : |Real.sin (x / 2)| = \u221a((1 - Real.cos x) / 2)"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_le_sin_of_le_of_le_pi_div_two", "type": " {x y : \u211d} (hx\u2081 : -(Real.pi / 2) \u2264 x) (hy\u2082 : y \u2264 Real.pi / 2) (hxy : x \u2264 y) : Real.sin x \u2264 Real.sin y"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_lt_sin_of_lt_of_le_pi_div_two", "type": " {x y : \u211d} (hx\u2081 : -(Real.pi / 2) \u2264 x) (hy\u2082 : y \u2264 Real.pi / 2) (hxy : x < y) : Real.sin x < Real.sin y"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.tendsto_sin_pi_div_two", "type": " : Filter.Tendsto Real.sin (nhdsWithin (Real.pi / 2) (Set.Iio (Real.pi / 2))) (nhds 1)"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.bijOn_sin", "type": " : Set.BijOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) (Set.Icc (-1) 1)"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.surjOn_sin", "type": " : Set.SurjOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) (Set.Icc (-1) 1)"}, {"doc": "The square of the sine of `\u03c0 / 3` is `3 / 4` (this is sometimes more convenient than the\nresult for cosine itself). ", "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sq_sin_pi_div_three", "type": " : Real.sin (Real.pi / 3) ^ 2 = 3 / 4"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.tendsto_sin_neg_pi_div_two", "type": " : Filter.Tendsto Real.sin (nhdsWithin (-(Real.pi / 2)) (Set.Ioi (-(Real.pi / 2)))) (nhds (-1))"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.cos_eq_sqrt_one_sub_sin_sq", "type": " {x : \u211d} (hl : -(Real.pi / 2) \u2264 x) (hu : x \u2264 Real.pi / 2) : Real.cos x = \u221a(1 - Real.sin x ^ 2)"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_pi_div_eight", "type": " : Real.sin (Real.pi / 8) = \u221a(2 - \u221a2) / 2"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_half_eq_sqrt", "type": " {x : \u211d} (hl : 0 \u2264 x) (hr : x \u2264 2 * Real.pi) : Real.sin (x / 2) = \u221a((1 - Real.cos x) / 2)"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_pi_over_two_pow_succ", "type": " (n : \u2115) : Real.sin (Real.pi / 2 ^ (n + 2)) = \u221a(2 - Real.sqrtTwoAddSeries 0 n) / 2"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_half_eq_neg_sqrt", "type": " {x : \u211d} (hl : -(2 * Real.pi) \u2264 x) (hr : x \u2264 0) : Real.sin (x / 2) = -\u221a((1 - Real.cos x) / 2)"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_pi_div_sixteen", "type": " : Real.sin (Real.pi / 16) = \u221a(2 - \u221a(2 + \u221a2)) / 2"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_sq_pi_over_two_pow", "type": " (n : \u2115) : Real.sin (Real.pi / 2 ^ (n + 1)) ^ 2 = 1 - (Real.sqrtTwoAddSeries 0 n / 2) ^ 2"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_sq_pi_over_two_pow_succ", "type": " (n : \u2115) : Real.sin (Real.pi / 2 ^ (n + 2)) ^ 2 = 1 / 2 - Real.sqrtTwoAddSeries 0 n / 4"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sin_pi_div_thirty_two", "type": " : Real.sin (Real.pi / 32) = \u221a(2 - \u221a(2 + \u221a(2 + \u221a2))) / 2"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.coe_sinOrderIso_apply", "type": " (x : \u2191(Set.Icc (-(Real.pi / 2)) (Real.pi / 2))) : \u2191(Real.sinOrderIso x) = Real.sin \u2191x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", "name": "Real.sinOrderIso_apply", "type": " (x : \u2191(Set.Icc (-(Real.pi / 2)) (Real.pi / 2))) : Real.sinOrderIso x = \u27e8Real.sin \u2191x, \u22ef\u27e9"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle", "name": "Real.Angle.sin_coe", "type": " (x : \u211d) : (\u2191x).sin = Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle", "name": "Real.Angle.sin_toReal", "type": " (\u03b8 : Real.Angle) : Real.sin \u03b8.toReal = \u03b8.sin"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle", "name": "Real.Angle.cos_sin_inj", "type": " {\u03b8 \u03c8 : \u211d} (Hcos : Real.cos \u03b8 = Real.cos \u03c8) (Hsin : Real.sin \u03b8 = Real.sin \u03c8) : \u2191\u03b8 = \u2191\u03c8"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle", "name": "Real.Angle.sin_eq_real_sin_iff_eq_or_add_eq_pi", "type": " {\u03b8 : Real.Angle} {\u03c8 : \u211d} : \u03b8.sin = Real.sin \u03c8 \u2194 \u03b8 = \u2191\u03c8 \u2228 \u03b8 + \u2191\u03c8 = \u2191Real.pi"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle", "name": "Real.Angle.sin_eq_iff_coe_eq_or_add_eq_pi", "type": " {\u03b8 \u03c8 : \u211d} : Real.sin \u03b8 = Real.sin \u03c8 \u2194 \u2191\u03b8 = \u2191\u03c8 \u2228 \u2191\u03b8 + \u2191\u03c8 = \u2191Real.pi"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse", "name": "Real.sin_arcsin", "type": " {x : \u211d} (hx\u2081 : -1 \u2264 x) (hx\u2082 : x \u2264 1) : Real.sin (Real.arcsin x) = x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse", "name": "Real.sin_arcsin'", "type": " {x : \u211d} (hx : x \u2208 Set.Icc (-1) 1) : Real.sin (Real.arcsin x) = x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse", "name": "Real.sin_arccos", "type": " (x : \u211d) : Real.sin (Real.arccos x) = \u221a(1 - x ^ 2)"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse", "name": "Real.arcsin_sin", "type": " {x : \u211d} (hx\u2081 : -(Real.pi / 2) \u2264 x) (hx\u2082 : x \u2264 Real.pi / 2) : Real.arcsin (Real.sin x) = x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse", "name": "Real.arcsin_sin'", "type": " {x : \u211d} (hx : x \u2208 Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) : Real.arcsin (Real.sin x) = x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse", "name": "Real.arcsin_eq_of_sin_eq", "type": " {x y : \u211d} (h\u2081 : Real.sin x = y) (h\u2082 : x \u2208 Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) : Real.arcsin y = x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse", "name": "Real.arcsin_eq_iff_eq_sin", "type": " {x y : \u211d} (hy : y \u2208 Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) : Real.arcsin x = y \u2194 x = Real.sin y"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse", "name": "Real.arcsin_le_iff_le_sin'", "type": " {x y : \u211d} (hy : y \u2208 Set.Ico (-(Real.pi / 2)) (Real.pi / 2)) : Real.arcsin x \u2264 y \u2194 x \u2264 Real.sin y"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse", "name": "Real.arcsin_lt_iff_lt_sin'", "type": " {x y : \u211d} (hy : y \u2208 Set.Ioc (-(Real.pi / 2)) (Real.pi / 2)) : Real.arcsin x < y \u2194 x < Real.sin y"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse", "name": "Real.le_arcsin_iff_sin_le'", "type": " {x y : \u211d} (hx : x \u2208 Set.Ioc (-(Real.pi / 2)) (Real.pi / 2)) : x \u2264 Real.arcsin y \u2194 Real.sin x \u2264 y"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse", "name": "Real.lt_arcsin_iff_sin_lt'", "type": " {x y : \u211d} (hx : x \u2208 Set.Ico (-(Real.pi / 2)) (Real.pi / 2)) : x < Real.arcsin y \u2194 Real.sin x < y"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse", "name": "Real.mapsTo_sin_Ioo", "type": " : Set.MapsTo Real.sin (Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) (Set.Ioo (-1) 1)"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse", "name": "Real.arcsin_le_iff_le_sin", "type": " {x y : \u211d} (hx : x \u2208 Set.Icc (-1) 1) (hy : y \u2208 Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) : Real.arcsin x \u2264 y \u2194 x \u2264 Real.sin y"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse", "name": "Real.arcsin_lt_iff_lt_sin", "type": " {x y : \u211d} (hx : x \u2208 Set.Icc (-1) 1) (hy : y \u2208 Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) : Real.arcsin x < y \u2194 x < Real.sin y"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse", "name": "Real.le_arcsin_iff_sin_le", "type": " {x y : \u211d} (hx : x \u2208 Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) (hy : y \u2208 Set.Icc (-1) 1) : x \u2264 Real.arcsin y \u2194 Real.sin x \u2264 y"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse", "name": "Real.lt_arcsin_iff_sin_lt", "type": " {x y : \u211d} (hx : x \u2208 Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) (hy : y \u2208 Set.Icc (-1) 1) : x < Real.arcsin y \u2194 Real.sin x < y"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Complex.Arg", "name": "Complex.norm_mul_sin_arg", "type": " (x : \u2102) : \u2016x\u2016 * Real.sin x.arg = x.im"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Complex.Arg", "name": "Complex.sin_arg", "type": " (x : \u2102) : Real.sin x.arg = x.im / \u2016x\u2016"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Pow.Real", "name": "Complex.cpow_ofReal_im", "type": " (x : \u2102) (y : \u211d) : (x ^ \u2191y).im = \u2016x\u2016 ^ y * Real.sin (x.arg * y)"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Pow.Real", "name": "Complex.cpow_ofReal", "type": " (x : \u2102) (y : \u211d) : x ^ \u2191y = \u2191(\u2016x\u2016 ^ y) * (\u2191(Real.cos (x.arg * y)) + \u2191(Real.sin (x.arg * y)) * Complex.I)"}, {"doc": null, "module": "Mathlib.MeasureTheory.Function.SpecialFunctions.Basic", "name": "Real.measurable_sin", "type": " : Measurable Real.sin"}, {"doc": null, "module": "Mathlib.MeasureTheory.Function.SpecialFunctions.Basic", "name": "Measurable.sin", "type": " {\u03b1 : Type u_1} {m : MeasurableSpace \u03b1} {f : \u03b1 \u2192 \u211d} (hf : Measurable f) : Measurable fun x => Real.sin (f x)"}, {"doc": null, "module": "Mathlib.MeasureTheory.Function.SpecialFunctions.Basic", "name": "AEMeasurable.sin", "type": " {\u03b1 : Type u_1} {m : MeasurableSpace \u03b1} {\u03bc : MeasureTheory.Measure \u03b1} {f : \u03b1 \u2192 \u211d} (hf : AEMeasurable f \u03bc) : AEMeasurable (fun x => Real.sin (f x)) \u03bc"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Complex.CircleMap", "name": "circleMap_zero_im", "type": " (r \u03b8 : \u211d) : (circleMap 0 r \u03b8).im = r * Real.sin \u03b8"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.logDeriv_sin", "type": " : logDeriv Real.sin = Real.cot"}, {"doc": "The function `Real.sin` is real analytic. ", "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.analyticAt_sin", "type": " {x : \u211d} : AnalyticAt \u211d Real.sin x"}, {"doc": "The function `Real.sin` is real analytic. ", "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.analyticOnNhd_sin", "type": " {s : Set \u211d} : AnalyticOnNhd \u211d Real.sin s"}, {"doc": "The function `Real.sin` is real analytic. ", "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.analyticOn_sin", "type": " {s : Set \u211d} : AnalyticOn \u211d Real.sin s"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.contDiff_sin", "type": " {n : WithTop \u2115\u221e} : ContDiff \u211d n Real.sin"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.isEquivalent_sin", "type": " : Asymptotics.IsEquivalent (nhds 0) Real.sin id"}, {"doc": "The function `Real.sin` is real analytic. ", "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.analyticWithinAt_sin", "type": " {x : \u211d} {s : Set \u211d} : AnalyticWithinAt \u211d Real.sin s x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.abs_iteratedDeriv_sin_le_one", "type": " (n : \u2115) (x : \u211d) : |iteratedDeriv n Real.sin x| \u2264 1"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.deriv_sin", "type": " : deriv Real.sin = Real.cos"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.deriv_cos", "type": " {x : \u211d} : deriv Real.cos x = -Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.deriv_cos'", "type": " : deriv Real.cos = fun x => -Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.iteratedDeriv_add_one_sin", "type": " (n : \u2115) : iteratedDeriv (n + 1) Real.sin = iteratedDeriv n Real.cos"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.differentiable_sin", "type": " : Differentiable \u211d Real.sin"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.differentiableAt_sin", "type": " {x : \u211d} : DifferentiableAt \u211d Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "ContDiff.sin", "type": " {E : Type u_1} [NormedAddCommGroup E] [NormedSpace \u211d E] {f : E \u2192 \u211d} {n : WithTop \u2115\u221e} (h : ContDiff \u211d n f) : ContDiff \u211d n fun x => Real.sin (f x)"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.iteratedDerivWithin_sin_Ioo", "type": " (n : \u2115) {a b x : \u211d} (hx : x \u2208 Set.Ioo a b) : iteratedDerivWithin n Real.sin (Set.Ioo a b) x = iteratedDeriv n Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.iteratedDeriv_add_one_cos", "type": " (n : \u2115) : iteratedDeriv (n + 1) Real.cos = -iteratedDeriv n Real.sin"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "ContDiffAt.sin", "type": " {E : Type u_1} [NormedAddCommGroup E] [NormedSpace \u211d E] {f : E \u2192 \u211d} {x : E} {n : WithTop \u2115\u221e} (hf : ContDiffAt \u211d n f x) : ContDiffAt \u211d n (fun x => Real.sin (f x)) x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "ContDiffOn.sin", "type": " {E : Type u_1} [NormedAddCommGroup E] [NormedSpace \u211d E] {f : E \u2192 \u211d} {s : Set E} {n : WithTop \u2115\u221e} (hf : ContDiffOn \u211d n f s) : ContDiffOn \u211d n (fun x => Real.sin (f x)) s"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "ContDiffWithinAt.sin", "type": " {E : Type u_1} [NormedAddCommGroup E] [NormedSpace \u211d E] {f : E \u2192 \u211d} {x : E} {s : Set E} {n : WithTop \u2115\u221e} (hf : ContDiffWithinAt \u211d n f s x) : ContDiffWithinAt \u211d n (fun x => Real.sin (f x)) s x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.iteratedDerivWithin_sin_Icc", "type": " (n : \u2115) {a b : \u211d} (h : a < b) {x : \u211d} (hx : x \u2208 Set.Icc a b) : iteratedDerivWithin n Real.sin (Set.Icc a b) x = iteratedDeriv n Real.sin x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.differentiable_iteratedDeriv_sin", "type": " (n : \u2115) : Differentiable \u211d (iteratedDeriv n Real.sin)"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.iteratedDeriv_even_sin", "type": " (n : \u2115) : iteratedDeriv (2 * n) Real.sin = (-1) ^ n * Real.sin"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.iteratedDeriv_odd_sin", "type": " (n : \u2115) : iteratedDeriv (2 * n + 1) Real.sin = (-1) ^ n * Real.cos"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.hasDerivAt_sin", "type": " (x : \u211d) : HasDerivAt Real.sin (Real.cos x) x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.hasStrictDerivAt_sin", "type": " (x : \u211d) : HasStrictDerivAt Real.sin (Real.cos x) x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Differentiable.sin", "type": " {E : Type u_1} [NormedAddCommGroup E] [NormedSpace \u211d E] {f : E \u2192 \u211d} (hc : Differentiable \u211d f) : Differentiable \u211d fun x => Real.sin (f x)"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.hasDerivAt_cos", "type": " (x : \u211d) : HasDerivAt Real.cos (-Real.sin x) x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.hasStrictDerivAt_cos", "type": " (x : \u211d) : HasStrictDerivAt Real.cos (-Real.sin x) x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "Real.iteratedDeriv_odd_cos", "type": " (n : \u2115) : iteratedDeriv (2 * n + 1) Real.cos = (-1) ^ (n + 1) * Real.sin"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "DifferentiableAt.sin", "type": " {E : Type u_1} [NormedAddCommGroup E] [NormedSpace \u211d E] {f : E \u2192 \u211d} {x : E} (hc : DifferentiableAt \u211d f x) : DifferentiableAt \u211d (fun x => Real.sin (f x)) x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "DifferentiableOn.sin", "type": " {E : Type u_1} [NormedAddCommGroup E] [NormedSpace \u211d E] {f : E \u2192 \u211d} {s : Set E} (hc : DifferentiableOn \u211d f s) : DifferentiableOn \u211d (fun x => Real.sin (f x)) s"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "DifferentiableWithinAt.sin", "type": " {E : Type u_1} [NormedAddCommGroup E] [NormedSpace \u211d E] {f : E \u2192 \u211d} {x : E} {s : Set E} (hf : DifferentiableWithinAt \u211d f s x) : DifferentiableWithinAt \u211d (fun x => Real.sin (f x)) s x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "deriv_sin", "type": " {f : \u211d \u2192 \u211d} {x : \u211d} (hc : DifferentiableAt \u211d f x) : deriv (fun x => Real.sin (f x)) x = Real.cos (f x) * deriv f x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "deriv_cos", "type": " {f : \u211d \u2192 \u211d} {x : \u211d} (hc : DifferentiableAt \u211d f x) : deriv (fun x => Real.cos (f x)) x = -Real.sin (f x) * deriv f x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "derivWithin_sin", "type": " {f : \u211d \u2192 \u211d} {x : \u211d} {s : Set \u211d} (hf : DifferentiableWithinAt \u211d f s x) (hxs : UniqueDiffWithinAt \u211d s x) : derivWithin (fun x => Real.sin (f x)) s x = Real.cos (f x) * derivWithin f s x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "derivWithin_cos", "type": " {f : \u211d \u2192 \u211d} {x : \u211d} {s : Set \u211d} (hf : DifferentiableWithinAt \u211d f s x) (hxs : UniqueDiffWithinAt \u211d s x) : derivWithin (fun x => Real.cos (f x)) s x = -Real.sin (f x) * derivWithin f s x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "HasDerivAt.sin", "type": " {f : \u211d \u2192 \u211d} {f' x : \u211d} (hf : HasDerivAt f f' x) : HasDerivAt (fun x => Real.sin (f x)) (Real.cos (f x) * f') x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "HasStrictDerivAt.sin", "type": " {f : \u211d \u2192 \u211d} {f' x : \u211d} (hf : HasStrictDerivAt f f' x) : HasStrictDerivAt (fun x => Real.sin (f x)) (Real.cos (f x) * f') x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "HasDerivAt.cos", "type": " {f : \u211d \u2192 \u211d} {f' x : \u211d} (hf : HasDerivAt f f' x) : HasDerivAt (fun x => Real.cos (f x)) (-Real.sin (f x) * f') x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "HasStrictDerivAt.cos", "type": " {f : \u211d \u2192 \u211d} {f' x : \u211d} (hf : HasStrictDerivAt f f' x) : HasStrictDerivAt (fun x => Real.cos (f x)) (-Real.sin (f x) * f') x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "HasDerivWithinAt.sin", "type": " {f : \u211d \u2192 \u211d} {f' x : \u211d} {s : Set \u211d} (hf : HasDerivWithinAt f f' s x) : HasDerivWithinAt (fun x => Real.sin (f x)) (Real.cos (f x) * f') s x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "HasDerivWithinAt.cos", "type": " {f : \u211d \u2192 \u211d} {f' x : \u211d} {s : Set \u211d} (hf : HasDerivWithinAt f f' s x) : HasDerivWithinAt (fun x => Real.cos (f x)) (-Real.sin (f x) * f') s x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "HasFDerivAt.sin", "type": " {E : Type u_1} [NormedAddCommGroup E] [NormedSpace \u211d E] {f : E \u2192 \u211d} {f' : StrongDual \u211d E} {x : E} (hf : HasFDerivAt f f' x) : HasFDerivAt (fun x => Real.sin (f x)) (Real.cos (f x) \u2022 f') x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "HasStrictFDerivAt.sin", "type": " {E : Type u_1} [NormedAddCommGroup E] [NormedSpace \u211d E] {f : E \u2192 \u211d} {f' : StrongDual \u211d E} {x : E} (hf : HasStrictFDerivAt f f' x) : HasStrictFDerivAt (fun x => Real.sin (f x)) (Real.cos (f x) \u2022 f') x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "HasFDerivAt.cos", "type": " {E : Type u_1} [NormedAddCommGroup E] [NormedSpace \u211d E] {f : E \u2192 \u211d} {f' : StrongDual \u211d E} {x : E} (hf : HasFDerivAt f f' x) : HasFDerivAt (fun x => Real.cos (f x)) (-Real.sin (f x) \u2022 f') x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "HasStrictFDerivAt.cos", "type": " {E : Type u_1} [NormedAddCommGroup E] [NormedSpace \u211d E] {f : E \u2192 \u211d} {f' : StrongDual \u211d E} {x : E} (hf : HasStrictFDerivAt f f' x) : HasStrictFDerivAt (fun x => Real.cos (f x)) (-Real.sin (f x) \u2022 f') x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "HasFDerivWithinAt.sin", "type": " {E : Type u_1} [NormedAddCommGroup E] [NormedSpace \u211d E] {f : E \u2192 \u211d} {f' : StrongDual \u211d E} {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) : HasFDerivWithinAt (fun x => Real.sin (f x)) (Real.cos (f x) \u2022 f') s x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "HasFDerivWithinAt.cos", "type": " {E : Type u_1} [NormedAddCommGroup E] [NormedSpace \u211d E] {f : E \u2192 \u211d} {f' : StrongDual \u211d E} {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) : HasFDerivWithinAt (fun x => Real.cos (f x)) (-Real.sin (f x) \u2022 f') s x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "fderiv_sin", "type": " {E : Type u_1} [NormedAddCommGroup E] [NormedSpace \u211d E] {f : E \u2192 \u211d} {x : E} (hc : DifferentiableAt \u211d f x) : fderiv \u211d (fun x => Real.sin (f x)) x = Real.cos (f x) \u2022 fderiv \u211d f x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "fderiv_cos", "type": " {E : Type u_1} [NormedAddCommGroup E] [NormedSpace \u211d E] {f : E \u2192 \u211d} {x : E} (hc : DifferentiableAt \u211d f x) : fderiv \u211d (fun x => Real.cos (f x)) x = -Real.sin (f x) \u2022 fderiv \u211d f x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "fderivWithin_sin", "type": " {E : Type u_1} [NormedAddCommGroup E] [NormedSpace \u211d E] {f : E \u2192 \u211d} {x : E} {s : Set E} (hf : DifferentiableWithinAt \u211d f s x) (hxs : UniqueDiffWithinAt \u211d s x) : fderivWithin \u211d (fun x => Real.sin (f x)) s x = Real.cos (f x) \u2022 fderivWithin \u211d f s x"}, {"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv", "name": "fderivWithin_cos", "type": " {E : Type u_1} [NormedAddCommGroup E] [NormedSpace \u211d E] {f : E \u2192 \u211d} {x : E} {s : Set E} (hf : DifferentiableWithinAt \u211d f s x) (hxs : UniqueDiffWithinAt \u211d s x) : fderivWithin \u211d (fun x => Real.cos (f x)) s x = -Real.sin (f x) \u2022 fderivWithin \u211d f s x"}, {"doc": "This lemma says that `fun x => a ^ x` is strictly differentiable for `a < 0`. Note that these\nvalues of `a` are outside of the \"official\" domain of `a ^ x`, and we may redefine `a ^ x`\nfor negative `a` if some other definition will be more convenient. ", "module": "Mathlib.Analysis.SpecialFunctions.Pow.Deriv", "name": "Real.hasStrictDerivAt_const_rpow_of_neg", "type": " {a x : \u211d} (ha : a < 0) : HasStrictDerivAt (fun x => a ^ x) (a ^ x * Real.log a - Real.exp (Real.log a * x) * Real.sin (x * Real.pi) * Real.pi) x"}, {"doc": "`(x, y) \u21a6 x ^ y` is strictly differentiable at `p : \u211d \u00d7 \u211d` such that `p.fst < 0`. ", "module": "Mathlib.Analysis.SpecialFunctions.Pow.Deriv", "name": "Real.hasStrictFDerivAt_rpow_of_neg", "type": " (p : \u211d \u00d7 \u211d) (hp : p.1 < 0) : HasStrictFDerivAt (fun x => x.1 ^ x.2) ((p.2 * p.1 ^ (p.2 - 1)) \u2022 ContinuousLinearMap.fst \u211d \u211d \u211d + (p.1 ^ p.2 * Real.log p.1 - Real.exp (Real.log p.1 * p.2) * Real.sin (p.2 * Real.pi) * Real.pi) \u2022 ContinuousLinearMap.snd \u211d \u211d \u211d) p"}]}