deriv and integral commute

Stream: new members

[Jack Valmadre]

Hi! I have a function of two variables f x y and I need to use the fact that the integral and derivative wrt different variables commute (by linearity). That is, ∀ x, deriv (fun u => ∫ y, f u y) x = ∫ y, deriv (fun u => f u y) x.

I couldn't find this so I'm trying to write it myself. I thought it might be done using ContinuousLinearMap.flip_apply, and so I tried to first rewrite it using integralCLM. However for the derivative I could only find deriv_clm_apply, which doesn't seem to get me much closer.

I'm a bit stuck, would someone be able to help? Here my attempt below:

import Mathlib.Analysis.Calculus.Deriv.Mul
import Mathlib.Analysis.Calculus.FDeriv.Mul
import Mathlib.MeasureTheory.Integral.Bochner
import Mathlib.MeasureTheory.Measure.Haar.OfBasis

open Real MeasureTheory

variable [NormedAddCommGroup Z] [NormedSpace ℝ Z] [hZ : CompleteSpace Z]

example {f : ℝ → ℝ → Z} (x : ℝ)
    (hf_int : ∀ x, Integrable (f x))
    (hf_deriv : ∀ y, Differentiable ℝ (fun x => f x y))
    (hf_int_deriv : ∀ x, Integrable fun y => deriv (fun u => f u y) x) :
    deriv (fun u => ∫ y, f u y) x = ∫ y, deriv (fun u => f u y) x := by

  have h₁ (x) : ∫ y, f x y = L1.integralCLM ((hf_int x).toL1 _)
  . simp [integral_def, hZ, hf_int x]
    simp [L1.integral_def]
  simp only [h₁]

  rw [deriv_clm_apply]
  rotate_left
  . exact differentiableAt_const _
  . refine Differentiable.differentiableAt ?_
    -- Differentiable ℝ fun u => Integrable.toL1 (f u) _
    sorry

  simp [integral_def, hZ, hf_int_deriv]
  simp [L1.integral_def]
  -- ↑L1.integralCLM (deriv (fun u => Integrable.toL1 (f u) _) x) =
  -- ↑L1.integralCLM (Integrable.toL1 (fun y => deriv (fun u => f u y) x) _)
  sorry

[Jack Valmadre]

Ah, I realised that maybe I need to define derivCLM, which is going to require a topology on the subtype of differentiable functions that I'm considering (in order to use deriv_add)

[Vincent Beffara]

Have you had a look at the results in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Calculus/ParametricIntegral.html ?

[Jack Valmadre]

No, I didn't find this! It looks like it might do what I need. Thanks!!