English
For a Lipschitz function taking values in a product space, the line derivative along a sum equals the sum of line derivatives along each component.
Русский
Для Lipschitz-функции, принимающей значения в произведении, линейная производная вдоль суммы равна сумме линейных производных по компонентам.
LaTeX
$$$\\text{ae\_lineDeriv\_sum\_eq}$$$
Lean4
/-- The line derivative of a Lipschitz function is almost everywhere linear with respect to fixed
coefficients. -/
theorem ae_lineDeriv_sum_eq (hf : LipschitzWith C f) {ι : Type*} (s : Finset ι) (a : ι → ℝ) (v : ι → E) :
∀ᵐ x ∂μ, lineDeriv ℝ f x (∑ i ∈ s, a i • v i) = ∑ i ∈ s, a i • lineDeriv ℝ f x (v i) := by
/- Clever argument by Morrey: integrate against a smooth compactly supported function `g`, switch
the derivative to `g` by integration by parts, and use the linearity of the derivative of `g` to
conclude that the initial integrals coincide. -/
apply
ae_eq_of_integral_contDiff_smul_eq (hf.locallyIntegrable_lineDeriv _)
(locallyIntegrable_finset_sum _ (fun i hi ↦ (hf.locallyIntegrable_lineDeriv (v i)).smul (a i)))
(fun g g_smooth g_comp ↦ ?_)
simp_rw [Finset.smul_sum]
have A : ∀ i ∈ s, Integrable (fun x ↦ g x • (a i • fun x ↦ lineDeriv ℝ f x (v i)) x) μ := fun i hi ↦
(g_smooth.continuous.integrable_of_hasCompactSupport g_comp).smul_of_top_left
((hf.memLp_lineDeriv (v i)).const_smul (a i))
rw [integral_finset_sum _ A]
suffices S1 : ∫ x, lineDeriv ℝ f x (∑ i ∈ s, a i • v i) * g x ∂μ = ∑ i ∈ s, a i * ∫ x, lineDeriv ℝ f x (v i) * g x ∂μ
by
dsimp only [smul_eq_mul, Pi.smul_apply]
simp_rw [← mul_assoc, mul_comm _ (a _), mul_assoc, integral_const_mul, mul_comm (g _), S1]
suffices S2 : ∫ x, (∑ i ∈ s, a i * fderiv ℝ g x (v i)) * f x ∂μ = ∑ i ∈ s, a i * ∫ x, fderiv ℝ g x (v i) * f x ∂μ
by
obtain ⟨D, g_lip⟩ : ∃ D, LipschitzWith D g :=
ContDiff.lipschitzWith_of_hasCompactSupport g_comp g_smooth (mod_cast le_top)
simp_rw [integral_lineDeriv_mul_eq hf g_lip g_comp]
simp_rw [(g_smooth.differentiable (mod_cast le_top)).differentiableAt.lineDeriv_eq_fderiv]
simp only [map_neg, _root_.map_sum, map_smul, smul_eq_mul, neg_mul]
simp only [integral_neg, mul_neg, Finset.sum_neg_distrib, neg_inj]
exact S2
suffices B : ∀ i ∈ s, Integrable (fun x ↦ a i * (fderiv ℝ g x (v i) * f x)) μ by
simp_rw [Finset.sum_mul, mul_assoc, integral_finset_sum s B, integral_const_mul]
intro i _hi
let L : StrongDual ℝ E → ℝ := fun f ↦ f (v i)
change Integrable (fun x ↦ a i * ((L ∘ (fderiv ℝ g)) x * f x)) μ
refine (Continuous.integrable_of_hasCompactSupport ?_ ?_).const_mul _
· exact ((g_smooth.continuous_fderiv (mod_cast le_top)).clm_apply continuous_const).mul hf.continuous
· exact ((g_comp.fderiv ℝ).comp_left rfl).mul_right
