English
Integration by parts for line derivatives yields equality of two representations of the same line derivative integration against a test function.
Русский
Интеграция по частям для линейных производных дает равенство двух представлений той же линейной производной.
LaTeX
$$$\int f \cdot \text{lineDeriv}(g) = \int g \cdot \text{lineDeriv}(f).$$$
Lean4
/-- Integration by parts formula for the line derivative of Lipschitz functions, assuming one of
them is compactly supported. -/
theorem integral_lineDeriv_mul_eq (hf : LipschitzWith C f) (hg : LipschitzWith D g) (h'g : HasCompactSupport g)
(v : E) : ∫ x, lineDeriv ℝ f x v * g x ∂μ = ∫ x, lineDeriv ℝ g x (-v) * f x ∂μ := by
/- Write down the line derivative as the limit of `(f (x + t v) - f x) / t` and
`(g (x - t v) - g x) / t`, and therefore the integrals as limits of the corresponding integrals
thanks to the dominated convergence theorem. At fixed positive `t`, the integrals coincide
(with the change of variables `y = x + t v`), so the limits also coincide. -/
have A :
Tendsto (fun (t : ℝ) ↦ ∫ x, (t⁻¹ • (f (x + t • v) - f x)) * g x ∂μ) (𝓝[>] 0)
(𝓝 (∫ x, lineDeriv ℝ f x v * g x ∂μ)) :=
integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul hf (hg.continuous.integrable_of_hasCompactSupport h'g) v
have B :
Tendsto (fun (t : ℝ) ↦ ∫ x, (t⁻¹ • (g (x + t • (-v)) - g x)) * f x ∂μ) (𝓝[>] 0)
(𝓝 (∫ x, lineDeriv ℝ g x (-v) * f x ∂μ)) :=
integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul' hg h'g hf.continuous (-v)
suffices S1 : ∀ (t : ℝ), ∫ x, (t⁻¹ • (f (x + t • v) - f x)) * g x ∂μ = ∫ x, (t⁻¹ • (g (x + t • (-v)) - g x)) * f x ∂μ
by simp only [S1] at A; exact tendsto_nhds_unique A B
intro t
suffices S2 : ∫ x, (f (x + t • v) - f x) * g x ∂μ = ∫ x, f x * (g (x + t • (-v)) - g x) ∂μ by
simp only [smul_eq_mul, mul_assoc, integral_const_mul, S2, mul_comm (f _)]
have S3 : ∫ x, f (x + t • v) * g x ∂μ = ∫ x, f x * g (x + t • (-v)) ∂μ := by
rw [← integral_add_right_eq_self _ (t • (-v))]; simp
simp_rw [_root_.sub_mul, _root_.mul_sub]
rw [integral_sub, integral_sub, S3]
· apply Continuous.integrable_of_hasCompactSupport
· exact hf.continuous.mul (hg.continuous.comp (continuous_add_right _))
· exact (h'g.comp_homeomorph (Homeomorph.addRight (t • (-v)))).mul_left
· exact (hf.continuous.mul hg.continuous).integrable_of_hasCompactSupport h'g.mul_left
· apply Continuous.integrable_of_hasCompactSupport
· exact (hf.continuous.comp (continuous_add_right _)).mul hg.continuous
· exact h'g.mul_left
· exact (hf.continuous.mul hg.continuous).integrable_of_hasCompactSupport h'g.mul_left
