English
Finite form of Euler’s sine product: sin(π z) equals a ratio involving a finite product, a cosine integral, and a cosine-power integral.
Русский
Конечная форма бесконечного продукта Эйлера для синуса: sin(π z) равняется отношению, включающему конечный продукт, интеграл косинуса и интеграл косинуса в степенях.
LaTeX
$$$\sin(π z) = \frac{π z \prod_{j=0}^{n-1} \left(1 - \frac{z^{2}}{(j+1)^{2}}\right) \int_{0}^{π/2} \cos(2 z x) \cos^{2 n} x \, dx}{\int_{0}^{π/2} \cos^{2n} x \, dx}$$$
Lean4
/-- Inverse of the `sin` function, returns values in the range `-π / 2 ≤ arcsin x ≤ π / 2`.
It defaults to `-π / 2` on `(-∞, -1)` and to `π / 2` to `(1, ∞)`. -/
@[pp_nodot]
noncomputable def arcsin : ℝ → ℝ :=
Subtype.val ∘ IccExtend (neg_le_self zero_le_one) sinOrderIso.symm
