integral is continuously differentiable

Stream: Is there code for X?

[Floris van Doorn]

I am struggling to prove that integrals are continuously differentiable w.r.t. a parameter (see below).
I'm trying to prove this from docs#has_fderiv_at_integral_of_dominated_loc_of_lip, but it still seems very painful. Am I missing something, or will it indeed be quite some work?
(a very WIP attempt is in https://github.com/leanprover-community/sphere-eversion/blob/fpvandoorn/WIP/src/to_mathlib/convolution.lean )
Note: I don't think I can use @Patrick Massot's results on differentiation of integrals, because I cannot assume that my function is differentiable w.r.t. the integration variable.

import analysis.calculus.parametric_integral

open measure_theory topological_space

variables {α : Type*} [measurable_space α] {μ : measure α} {𝕜 : Type*} [is_R_or_C 𝕜]
          {E : Type*} [normed_group E] [normed_space ℝ E]
          [complete_space E] [second_countable_topology E]
          [measurable_space E] [borel_space E]
          {H : Type*} [normed_group H] [normed_space ℝ H] [second_countable_topology $ H →L[ℝ] E]

lemma times_cont_diff_one_integral {F : H → α → E}
  (hF_int : ∀ x, integrable (F x) μ)
  (hF'_int : ∀ x, integrable (λ a, fderiv ℝ (λ x, F x a) x) μ)
  (h_diff : ∀ a, times_cont_diff ℝ 1 (λ x, F x a)) : -- can probably weakened to ∀ x, ∀ᵐ a ∂μ, ...
  times_cont_diff ℝ 1 (λ x, ∫ a, F x a ∂μ) :=
sorry

[Patrick Massot]

What do you call my "results on differentiation of integrals"? I would certainly call docs#has_fderiv_at_integral_of_dominated_loc_of_lip by that name

[Chris Birkbeck]

I had some similar pains when doing the modular forms stuff. I used docs#has_deriv_at_integral_of_dominated_loc_of_deriv_le to prove that you can differentiate integrals of continuous functions. But this is probably more restrictive than what you need. You can look at my ugly way here https://github.com/leanprover-community/mathlib/blob/d66bd49720b317e269b9a1411bbb3b47681f52e9/src/measure_theory/integral/unform_limits_of_holomorphic.lean

I'd be interested to hear if such things are already somewhere, since I'm pretty sure I've done this the long-way-round.

[Chris Birkbeck]

The relevant lemma is cauchy_disk_form_differentiable_on

[Floris van Doorn]

Patrick Massot said:

What do you call my "results on differentiation of integrals"? I would certainly call docs#has_fderiv_at_integral_of_dominated_loc_of_lip by that name

You're right, I wrote it wrong. I meant the results about differentiability w.r.t. the bound and a parameter simultaneously.

[Patrick Massot]

I cannot claim I know how to prove such things without pain. All I know is either next to docs#has_fderiv_at_integral_of_dominated_loc_of_lip in mathlib or in https://github.com/leanprover-community/sphere-eversion/blob/master/src/to_mathlib/measure_theory/parametric_interval_integral.lean

[Patrick Massot]

I hoped I had proved enough, but maybe there are other cases needed.

[Floris van Doorn]

Ok, I'll struggle through it.

I think you've proved the most general versions. There is still some pain in getting more specific versions (with simpler but more restrictive conditions) from the general versions.

[Patrick Massot]

Thanks for your efforts!

[Floris van Doorn]

I think that one of my difficulties is that my proposed lemma is wrong: it needs a bound independent of x that is integrable.

[Patrick Massot]

Floris van Doorn said:

I think that one of my difficulties is that my proposed lemma is wrong

I see. This detail is known to cause issues sometimes.