Derivative of the integral of exp (u + t v)

For continuous functions u and v on a compact space with a finite measure, this file differentiates t ↦ ∫ exp (u + t v) dμ under the integral sign:

d/dt ∫ exp (u + t v) dμ = ∫ v exp (u + t v) dμ.

This is the directional derivative of the exponential integral ∫ e^u dμ at u in the direction v, the derivative of the exponential term in Liouville-type energies such as TauCeti.Manifold.liouvilleEnergy.

Main declarations

• TauCeti.hasDerivAt_integral_exp_add_mul: the derivative of t ↦ ∫ exp (u + t v) dμ.

theorem TauCeti.hasDerivAt_integral_exp_add_mul {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] {u v : X → ℝ} (hu : Continuous u) (hv : Continuous v) (t₀ : ℝ) : HasDerivAt (fun (t : ℝ) => ∫ (x : X), Real.exp (u x + t * v x) ∂μ) (∫ (x : X), v x * Real.exp (u x + t₀ * v x) ∂μ) t₀

Differentiating ∫ exp (u + t v) dμ. For continuous u and v on a compact space with a finite measure, the derivative of t ↦ ∫ exp (u + t v) dμ at t₀ is ∫ v exp (u + t₀ v) dμ.