exchange order of differentiation and integration

Stream: new members

[Nicholas Wilson]

How do I (what theorems apply) exchange the order of differentiation in a parametric integral?

import Mathlib.MeasureTheory.Integral.Bochner
import Mathlib.MeasureTheory.Measure.Haar.OfBasis
import Mathlib.Data.Real.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Complex.Exponential
import Mathlib.Analysis.MellinTransform
open Complex
open Real

example (f:ℝ → ℝ ) (a b :ℝ ): deriv (fun w => ∫ (x : ℝ) , f x * (Real.cos (a * x) * Real.sinh (w * x))) b =
    ∫ (x : ℝ), x* f x * (Real.cos (a * x) * Real.cosh (b * x)) := by sorry

[Patrick Massot]

See https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Calculus/ParametricIntegral.html

[Nicholas Wilson]

That is one impenetrable page full of jargon, the more I read the less I comprehend. I'm going to assume that I want derivs and not fderivs.

If I am reading that correctly (which it is entirely possible I am not) the one I want is hasDerivAt_integral_of_dominated_loc_of_deriv_le and
F (x,a) has deriv (w.r.t. a) F'(x,a).
The result of the theorem is that :F' (x,a)is integrable w.r.t a for some x (dependant of the other hypotheses that I need to supply, which I barely understand individually and I have no idea how to construct) , and deriv (fun x ↦ ∫a, F x a) y for some given y is equal to ∫a, F' y a) via the HasDerivAt.

First, is that a correct assessment? How do I use the HasDerivAt result to invert the order of integration and differentiation? h_diff is understand conceptually to be the requirement that F' (x,a) = d/da F(x,a), though I don't quite follow the radius epsilon metric ball definition. I understand hF_int. I don't understand the other requirements.

[Patrick Massot]

Nicholas Wilson said:

That is one impenetrable page full of jargon, the more I read the less I comprehend.

Do you mean it's full of mathematics? Yes, we do that sometimes in Mathlib, sorry. Actually I wrote my message in a hurry without having time to check statements in this file, and I can see I misremembered how much was incorporated from the sphere eversion project into Mathlib. SE has more elementary statements that are consequences of the abstract statements in this file. I'll try to open PRs soon (please ping me if I forget).

[Patrick Massot]

You can take a look at https://github.com/leanprover-community/sphere-eversion/blob/master/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean in the mean time.

[Patrick Massot]

Also note that the example that you wrote at the beginning of this thread has no reason to be true (unless you get lucky and it reduces to 0 = 0 when it doesn't make sense) and this is also an obstacle to answering your question.

[Nicholas Wilson]

Haha, no need to apologise. I don't particularly care for the strict integrability (or differentiability) requirements (I'm an engineer if you can't tell). I'm using lean to prove the bits of theorems I care about as a first pass as a check on my algebra and logic, and to have an (as fleshed out as I can make it) skeleton of the formal proof. So I'm happy to leave them stubbed out by sorry for now.

Yes I had noticed that. I'm using sorry for purely the integral/differentiation oder exchange now and letting simp do the differential calculus for me (I should have done that first really, that's the whole reason for using a proof assistant in the first place!).

I'll circle back to these integrability and differentiability requirements at a later date when I have the rest of the rest of the proof done and hope that the full proof is sufficiently enticing for others to help complete the formalisation, as dealing with these technical minutiae is not particularly exciting and doesn't help me move forward with the proof.

It would be much appreciated to have a set of simplified theorems that an engineer can understand.