English
The logarithmic derivative of the complex exponential is constant 1: logDeriv(Complex.exp) = 1.
Русский
Логарифмическая производная экспоненты комплексного равна 1.
LaTeX
$$$\logDeriv(\mathrm{Complex}.\exp) = 1$$$
Lean4
/-- Relate the integral `cos x ^ n` over `[0, π/2]` to the integral of `sin x ^ n` over `[0, π]`,
which is studied in `Mathlib/Analysis/Real/Pi/Wallis.lean` and other places. -/
theorem integral_cos_pow_eq (n : ℕ) : (∫ x in (0 : ℝ)..π / 2, cos x ^ n) = 1 / 2 * ∫ x in (0 : ℝ)..π, sin x ^ n :=
by
rw [mul_comm (1 / 2 : ℝ), ← div_eq_iff (one_div_ne_zero (two_ne_zero' ℝ)), ← div_mul, div_one, mul_two]
have L : IntervalIntegrable _ volume 0 (π / 2) := (continuous_sin.pow n).intervalIntegrable _ _
have R : IntervalIntegrable _ volume (π / 2) π := (continuous_sin.pow n).intervalIntegrable _ _
rw [← integral_add_adjacent_intervals L R]
congr 1
· nth_rw 1 [(by ring : 0 = π / 2 - π / 2)]
nth_rw 3 [(by ring : π / 2 = π / 2 - 0)]
rw [← integral_comp_sub_left]
refine integral_congr fun x _ => ?_
rw [cos_pi_div_two_sub]
· nth_rw 3 [(by ring : π = π / 2 + π / 2)]
nth_rw 2 [(by ring : π / 2 = 0 + π / 2)]
rw [← integral_comp_add_right]
refine integral_congr fun x _ => ?_
rw [sin_add_pi_div_two]
