English
If F is dominated and line-differentiable with a bound, then the integral of the line-derivative against a function g is dominated by an integrable bound.
Русский
Если F задано доминированием и имеет линейную производную вдоль направления, то интеграл по линейной производной против g контролируется интегрируемым пределом.
LaTeX
$$$\int F'(x,a) d\mu(a) \le \int bound(a) d\mu(a)$$$
Lean4
theorem integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul (hf : LipschitzWith C f) (hg : Integrable g μ)
(v : E) :
Tendsto (fun (t : ℝ) ↦ ∫ x, (t⁻¹ • (f (x + t • v) - f x)) * g x ∂μ) (𝓝[>] 0)
(𝓝 (∫ x, lineDeriv ℝ f x v * g x ∂μ)) :=
by
apply tendsto_integral_filter_of_dominated_convergence (fun x ↦ (C * ‖v‖) * ‖g x‖)
· filter_upwards with t
apply AEStronglyMeasurable.mul ?_ hg.aestronglyMeasurable
apply aestronglyMeasurable_const.smul
apply AEStronglyMeasurable.sub _ hf.continuous.measurable.aestronglyMeasurable
apply AEMeasurable.aestronglyMeasurable
exact hf.continuous.measurable.comp_aemeasurable' (aemeasurable_id'.add_const _)
· filter_upwards [self_mem_nhdsWithin] with t (ht : 0 < t)
filter_upwards with x
calc
‖t⁻¹ • (f (x + t • v) - f x) * g x‖ = (t⁻¹ * ‖f (x + t • v) - f x‖) * ‖g x‖ := by simp [norm_mul, ht.le]
_ ≤ (t⁻¹ * (C * ‖(x + t • v) - x‖)) * ‖g x‖ := by gcongr; exact LipschitzWith.norm_sub_le hf (x + t • v) x
_ = (C * ‖v‖) * ‖g x‖ := by simp [field, norm_smul, abs_of_nonneg ht.le]
· exact hg.norm.const_mul _
· filter_upwards [hf.ae_lineDifferentiableAt v] with x hx
exact hx.hasLineDerivAt.tendsto_slope_zero_right.mul tendsto_const_nhds
