Relation between the integral of a function and derivative

Stream: Is there code for X?

[Max Bobbin]

Hello,

I am trying to show that if

$$M(t) = \int \rho (V,t) dV$$

then it follows that

$$\frac{d(M(t))}{dt} = \int \frac{\rho (V,t)}{dt} dV$$

Here I have a single varaible function equal to the integral of a multivariable function. The multivariable function is integrated over a variable that is independent of M, so I want to show that the same integral relation holds when we take the derivative of their shared variable. I was hoping to get some suggestions in starting this in Lean. I attached the code I had as well. In the code I wrote have rho being a lambda function that holds V constant as it takes the derivative WRT t.

theorem eq_integral_to_deriv_eq_integral_of_deriv
(ρ : ℝ → ℝ³ → ℝ )(M : ℝ → ℝ)(V1 V2: (ℝ³)) (hV : V1 ≤ V2)
:
 ∀ (t:ℝ), M t = ∫ (V : ℝ³) in set.Icc V1 V2,(λ (t : ℝ), ρ t V) t →  deriv M t = ∫ (V : ℝ³) in set.Icc V1 V2,(deriv(λ t, ρ t V) t)
:=
begin
intro t1,
intro h,
rw measure_theory.integral_Icc_eq_integral_Ioc,
rw measure_theory.integral_Icc_eq_integral_Ioc at h,


end

[Eric Wieser]

By naming convention alone, I'd guess this exists as docs#deriv_integral

[Eric Wieser]

Your first goal should be to eliminate M

[Max Bobbin]

I do see docs#interval_integral.integral_deriv_eq_sub but this seems to be for an integral of the derivative where both the integral and derivative are WRT the same variable. I was hoping that I could show that since the derivative holds V constant, then the integral reduces to

$$\frac{d \rho (V,t)} {dt} V$$

[Max Bobbin]

I was trying to go about that, I was having trouble relating M(t) to deriv M t since I can't just plug in M.

[Eric Wieser]

I think you should be able to rw ←funext_iff at h

[Eric Wieser]

Oh actually, this is just false

[Eric Wieser]

You can't say anything about the derivative of M if you only know its value at a given t

[Max Bobbin]

I have it set for all t, but that may not solve it.

[Patrick Massot]

You should have a look at https://leanprover-community.github.io/mathlib_docs/analysis/calculus/parametric_interval_integral.html

[Patrick Massot]

If this is not enough then what you need is probably in the sphere eversion project, in https://github.com/leanprover-community/sphere-eversion/blob/master/src/to_mathlib/measure_theory/parametric_interval_integral.lean

[Eric Wieser]

I have it set for all t, but that may not solve it.

That's not what your statement currently says

[Max Bobbin]

Eric Wieser said:

I have it set for all t, but that may not solve it.

That's not what your statement currently says

Is that not the beginning part of the proof where it says forall t:R, then the rest of the statement?

[Eric Wieser]

That would be (∀ t, p t) →(∀ t, q t), you have (∀ t, (p t → q t))

[Max Bobbin]

Ahh, ok, my apologies, let me fix that

[Max Bobbin]

Patrick Massot said:

You should have a look at https://leanprover-community.github.io/mathlib_docs/analysis/calculus/parametric_interval_integral.html

Thank you I will look at that!

[Max Bobbin]

I did just have an idea, but I know its wrong, but I'm hoping it sparks a correct idea. I was of pulling the derivative out of the statement, but the problem is then I have the derivative of a proposition which doesn't make sense

[Max Bobbin]

Would the parametric integral stuff be related to the Leibniz integral rule?

[Eric Wieser]

Max Bobbin said:

I did just have an idea, but I know its wrong, but I'm hoping it sparks a correct idea. I was of pulling the derivative out of the statement, but the problem is then I have the derivative of a proposition which doesn't make sense

I've no idea what you mean by that. To be clear, when I say "eliminate M" I mean "get the goal in the form ..."

deriv (λ t, ∫ (V : ℝ³) in set.Icc V1 V2, ρ t V) t
  = ∫ (V : ℝ³) in set.Icc V1 V2, deriv (λ t, ρ t V) t

[Max Bobbin]

Yes, I see what you mean. Apologies, that last thought wasn't fully formed and was illogical. I ahve achieved that, I rearranged how I stated my proof statement so that it looks like this

theorem eq_integral_to_deriv_eq_integral_of_deriv
(ρ : ℝ → ℝ³ → ℝ )(M : ℝ → ℝ)(V1 V2: (ℝ³)) (hV : V1 ≤ V2)
:
 (M = λ (t : ℝ),∫ (V : ℝ³) in set.Icc V1 V2,( ρ t V)  )→  (∀ (t:ℝ), deriv M t = ∫ (V : ℝ³) in set.Icc V1 V2,(deriv(λ t, ρ t V) t))
:=
begin
intro h,
rw h,


end

[Max Bobbin]

Now I'm at where you said, now I have something of the form where, on paper, I would use the Leibniz integral rule. I imagine the links sent above may have what I need to solve this