Integration by parts

Stream: new members

[Julia Ramos Alves]

Hello to all! I'm working with the following example:

import measure_theory.integral.interval_integral
import data.real.basic
import analysis.special_functions.integrals

example (x : ℝ) (n : ℕ) :
  (2 * ↑real.pi)⁻¹ *
      ∫ (x : ℝ) in
        -real.pi..real.pi,
        ↑x * complex.exp (-complex.I * ↑↑n * ↑x) =
    (-1) ^ n * complex.I / ↑n :=
begin
  sorry,
end

I wanted to be able to apply integration by parts but I have not found such a theorem in the mathlib documentation, can someone help me figure that out?

[Ruben Van de Velde]

docs#interval_integral.integral_mul_deriv_eq_deriv_mul

[Julia Ramos Alves]

I'm still having some trouble in order to set up the necessary conditions to apply integral_mul_deriv_eq_deriv_mul, the current code I have looks like the following:

import analysis.fourier
import measure_theory.integral.interval_integral
import data.real.basic
import analysis.special_functions.integrals

noncomputable
def fourier_coeff (f : ℝ → ℂ) (n : ℤ) : ℂ :=
(2 * real.pi)⁻¹ * ∫ x in -real.pi .. real.pi, (f x) * complex.exp (-complex.I * n * x)

lemma calc_cn (x: ℝ)(f : ℝ → ℂ)(hf: f x = x)(n : ℕ) (g : ℝ → ℂ)
(hg: g x = complex.exp (-(complex.I * ↑n * x))) :
 fourier_coeff f n = (-1)^n * complex.I / n :=
begin
  rw fourier_coeff,
  simp,
  simp_rw ← hg,


  /-rw interval_integral.integral_mul_deriv_eq_deriv_mul,-/
end

I'm trying to set it up in order to avoid the following error:

rewrite tactic failed, did not find instance of the pattern in the target expression
  ∫ (x : ℝ) in ?m_3..?m_4, ?m_1 x * ?m_2 x

But simp_rw fails and I don't really understand why, can someone give me an insight on that?

[Yakov Pechersky]

docs#interval_integral.integral_mul_deriv_eq_deriv_mul doesn't work because that's for real -> real

[Ruben Van de Velde]

Do we not have any more general variants?