differentiation under the integral sign

Stream: Is there code for X?

[Tomas Skrivan]

Is there a theorem stating differentiation under the integral sign?

I have found docs#hasFDerivAt_integral_of_dominated_loc_of_lip but that does not allow for the measure to vary.

Here is the statement I would like to have:

import Mathlib.Analysis.Calculus.FDeriv.Basic
import Mathlib.MeasureTheory.Integral.Bochner

open MeasureTheory

variable
  {X} [NormedAddCommGroup X] [NormedSpace ℝ X]
  {Y} [MeasurableSpace Y]
  {Z} [NormedAddCommGroup Z] [NormedSpace ℝ Z]

theorem deriv_under_integral_sign (μ : X → Measure Y) (f : X → Y → Z) (x dx : X)
    /- some conditions on f and μ   -/ :
    fderiv ℝ (fun x => ∫ y, f x y ∂(μ x)) x dx
    =
    fderiv ℝ (fun x' => ∫ y, f x y ∂(μ x')) x dx
    +
    ∫ y, fderiv ℝ (f · y) x dx ∂(μ x) := sorr

Not entirely sure what the condition on μ should be, on f I'm expecting:

    (bound : Y → ℝ)
    (hf_integ : ∀ x, Integrable (f x) (μ x))
    (hf_diff : ∀ x', ∀ᵐ (y : Y) ∂(μ x'), Differentiable ℝ (f · y))
    (hf_bound : ∀ x', ∀ᵐ y ∂(μ x'), ‖fderiv ℝ (f · y) x‖ ≤ bound y)
    (hbound_integ : ∀ x, Integrable bound (μ x))

[Tomas Skrivan]

(deleted)

[Tomas Skrivan]

Alternatively one could ask under what conditions on μ and f is true that:

   Differentiable ℝ fun (x : X×X) => ∫ y, f x.1 y ∂(μ x.2)

Then the desired result can be obtained using differentiation of uncurried function and docs#hasFDerivAt_integral_of_dominated_loc_of_lip

[Patrick Massot]

I’m pretty sure we don’t have anything about the case where the measure is moving.

[Tomas Skrivan]

Not even a 1D case where you integrate over an interval?

[Patrick Massot]

My source of information may be outdated but there was nothing at all in this direction when I needed it for the sphere eversion project and I definitely didn’t add things about moving measures.

[Yury G. Kudryashov]

In order to get your statement, you want to know that the function fun (a, b) => ∫ y, f a y ∂(μ b) is differentiable as a function of 2 variables.

[Yury G. Kudryashov]

UPD: wrote this before reading the whole message, sorry.

[Yury G. Kudryashov]

@Patrick Massot Do you know the right assumptions?

[Patrick Massot]

No