Derivative of an Integral Against a Translated Test

This proves differentiation under the integral sign for translated test functions.

Let $V$ be a finite-dimensional real inner-product space with its Borel measurable structure, let $m$ be a measure on $V$, and let $h:V\to\mathbb R$ be locally integrable with respect to $m$. Let $\phi:V\to\mathbb R$ be smooth and compactly supported. For $v\in V$ and $t\in\mathbb R$, define

$$F(s)=\int h(x)\phi(x-sv)\,dm(x).$$

Then $F$ has derivative at $t$ equal to

$$F'(t)=-\int h(x)D\phi(x-tv)v\,dm(x).$$

Equivalently,

$$\operatorname{HasDerivAt}\!\left(s\mapsto\int h(x)\phi(x-sv)\,dm(x), -\int h(x)D\phi(x-tv)v\,dm(x),t\right).$$

This is a technical differentiation lemma used to convert a weak derivative condition into translation identities.

Formalization Note The declaration does not assume that $m$ is an additive Haar measure.

Original Lean declaration header

Within namespace FunctionalInequalities.Energy.Euclidean. Shown in its original module context. Proof omitted.

theorem hasDerivAt_integral_mul_translate {h : V → ℝ} (hh : LocallyIntegrable h m) {φ : V → ℝ}
    (hφ : ContDiff ℝ ∞ φ) (hφc : HasCompactSupport φ) (v : V) (t : ℝ) :
    HasDerivAt (fun s : ℝ => ∫ x, h x * φ (x - s • v) ∂m)
      (-∫ x, h x * fderiv ℝ φ (x - t • v) v ∂m) t

Module navigation

Module: Energy/Euclidean/ZeroGradient.

Supporting theorems: norm_mul_fderiv_comp_sub_smul_le.

Previous: norm_mul_fderiv_comp_sub_smul_le · Next: integral_mul_sub_translate_eq_zero.

Source excerpt, lines 89–92 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Euclidean_ZeroGradient

open MeasureTheory Filter Topology
open scoped ContDiff
universe u
variable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
variable [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
  (m : MeasureTheory.Measure V) [m.IsAddHaarMeasure]
omit [m.IsAddHaarMeasure]

theorem FunctionalInequalities.Energy.Euclidean.hasDerivAt_integral_mul_translate_readable {h : V → ℝ} (hh : LocallyIntegrable h m) {φ : V → ℝ}
    (hφ : ContDiff ℝ ∞ φ) (hφc : HasCompactSupport φ) (v : V) (t : ℝ) :
    HasDerivAt (fun s : ℝ => ∫ x, h x * φ (x - s • v) ∂m)
      (-∫ x, h x * fderiv ℝ φ (x - t • v) v ∂m) t := by sorry