Integration by parts for `fderiv`

Stream: Is there code for X?

[Tomas Skrivan]

I want a generalization of integration by parts docs#MeasureTheory.integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable but for fderiv instead.

Something like this (not sure about the exact assumptions on X):

import Mathlib

open MeasureTheory

variable
  {X E F G : Type*}
  [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [MeasurableSpace X]
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G]
  {μ : Measure X} [μ.IsAddHaarMeasure]
  {L : E →L[ℝ] F →L[ℝ] G} {u : X → E} {v : X → F} {u' : X → X →L[ℝ] E} {v' : X → X →L[ℝ] F}
  {m n : G}

theorem integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable (dx : X)
    (hu : ∀ x, HasFDerivAt u (u' x) x) (hv : ∀ x, HasFDerivAt v (v' x) x)
    (huv' : Integrable (fun x ↦ L (u x) (v' x dx)) μ) (hu'v : Integrable (fun x ↦ L (u' x dx) (v x)) μ)
    (huv : Integrable (fun x ↦ L (u x) (v x)) μ) :
    ∫ (x : X), L (u x) (v' x dx) ∂μ = - ∫ (x : X), L (u' x dx) (v x) ∂μ := sorry

I'm not sure what is the best approach here and I want the result be general enough such that I can have things like X = ℝ × EuclideanSpace (Fin 10) ℝ.

[Tomas Skrivan]

Ohh never mind, there is docs#integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable