English
Under Lipschitz and measurability assumptions, the line-derivative representation is almost everywhere linear with respect to a finite set of directions.
Русский
При липшицевой и измеримости производная по линейному направлению почти везде линейна по конечному числу направлений.
LaTeX
$$$\\text{ae\_lineDeriv\_sum\_eq}$$$
Lean4
theorem integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul' (hf : LipschitzWith C f) (h'f : HasCompactSupport f)
(hg : Continuous 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
let K := cthickening (‖v‖) (tsupport f)
have K_compact : IsCompact K := IsCompact.cthickening h'f
apply tendsto_integral_filter_of_dominated_convergence (K.indicator (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 [Ioc_mem_nhdsGT zero_lt_one] with t ht
have t_pos : 0 < t := ht.1
filter_upwards with x
by_cases hx : x ∈ K
·
calc
‖t⁻¹ • (f (x + t • v) - f x) * g x‖ = (t⁻¹ * ‖f (x + t • v) - f x‖) * ‖g x‖ := by simp [norm_mul, t_pos.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 t_pos.le]
_ = K.indicator (fun x ↦ (C * ‖v‖) * ‖g x‖) x := by rw [indicator_of_mem hx]
· have A : f x = 0 := by
rw [← Function.notMem_support]
contrapose! hx
exact self_subset_cthickening _ (subset_tsupport _ hx)
have B : f (x + t • v) = 0 := by
rw [← Function.notMem_support]
contrapose! hx
apply mem_cthickening_of_dist_le _ _ (‖v‖) (tsupport f) (subset_tsupport _ hx)
simp only [dist_eq_norm, sub_add_cancel_left, norm_neg, norm_smul, Real.norm_eq_abs, abs_of_nonneg t_pos.le]
exact mul_le_of_le_one_left (norm_nonneg v) ht.2
simp only [B, A, _root_.sub_self, smul_eq_mul, mul_zero, zero_mul, norm_zero]
exact indicator_nonneg (fun y _hy ↦ by positivity) _
· rw [integrable_indicator_iff K_compact.measurableSet]
apply ContinuousOn.integrableOn_compact K_compact
exact (Continuous.mul continuous_const hg.norm).continuousOn
· filter_upwards [hf.ae_lineDifferentiableAt v] with x hx
exact hx.hasLineDerivAt.tendsto_slope_zero_right.mul tendsto_const_nhds
