English
For ENNReal-valued f that is locally integrable, a.e. x yields Tendsto of the normalized Lintegral to 0 when measuring the norm distance to f(x).
Русский
Для f: α→E, локально интегрируемой, почти всюду x выполняется Tendsto нормализованного линегрального деления к 0 в пределе к x.
LaTeX
$$$\forall^{\mu}\ x,\ Tendsto(\lambda a.\dfrac{\int_{y∈a} ||f(y)-f(x)|| \;dμ}{μ(a)}) (v.filterAt x) (𝓝 0).$$$
Lean4
theorem ae_tendsto_lintegral_enorm_sub_div'_of_integrable {f : α → E} (hf : Integrable f μ)
(h'f : StronglyMeasurable f) :
∀ᵐ x ∂μ, Tendsto (fun a => (∫⁻ y in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0) := by
/- For every `c`, then `(∫⁻ y in a, ‖f y - c‖ₑ ∂μ) / μ a` tends almost everywhere to `‖f x - c‖`.
We apply this to a countable set of `c` which is dense in the range of `f`, to deduce the
desired convergence.
A minor technical inconvenience is that constants are not integrable, so to apply previous
lemmas we need to replace `c` with the restriction of `c` to a finite measure set `A n` in the
above sketch. -/
let A := MeasureTheory.Measure.finiteSpanningSetsInOpen' μ
rcases h'f.isSeparable_range with ⟨t, t_count, ht⟩
have main :
∀ᵐ x ∂μ,
∀ᵉ (n : ℕ) (c ∈ t),
Tendsto (fun a => (∫⁻ y in a, ‖f y - (A.set n).indicator (fun _ => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
(𝓝 ‖f x - (A.set n).indicator (fun _ => c) x‖ₑ) :=
by
#adaptation_note /-- 2024-04-23
The next two lines were previously just `simp_rw [ae_all_iff, ae_ball_iff t_count]`. -/
simp_rw [ae_all_iff]
intro x; rw [ae_ball_iff t_count]; revert x
intro n c _
apply ae_tendsto_lintegral_div'
· refine (h'f.sub ?_).enorm
exact stronglyMeasurable_const.indicator (IsOpen.measurableSet (A.set_mem n))
· apply ne_of_lt
calc
∫⁻ y, ‖f y - (A.set n).indicator (fun _ : α => c) y‖ₑ ∂μ ≤
∫⁻ y, ‖f y‖ₑ + ‖(A.set n).indicator (fun _ : α => c) y‖ₑ ∂μ :=
lintegral_mono fun x ↦ enorm_sub_le
_ = ∫⁻ y, ‖f y‖ₑ ∂μ + ∫⁻ y, ‖(A.set n).indicator (fun _ : α => c) y‖ₑ ∂μ := (lintegral_add_left h'f.enorm _)
_ < ∞ + ∞ :=
haveI I : Integrable ((A.set n).indicator fun _ : α => c) μ := by
simp only [integrable_indicator_iff (IsOpen.measurableSet (A.set_mem n)), integrableOn_const_iff (C := c),
A.finite n, or_true]
ENNReal.add_lt_add hf.2 I.2
filter_upwards [main, v.ae_eventually_measure_pos] with x hx h'x
have M c (hc : c ∈ t) : Tendsto (fun a => (∫⁻ y in a, ‖f y - c‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 ‖f x - c‖ₑ) :=
by
obtain ⟨n, xn⟩ : ∃ n, x ∈ A.set n := by simpa [← A.spanning] using mem_univ x
specialize hx n c hc
simp only [xn, indicator_of_mem] at hx
apply hx.congr' _
filter_upwards [v.eventually_filterAt_subset_of_nhds (IsOpen.mem_nhds (A.set_mem n) xn),
v.eventually_filterAt_measurableSet x] with a ha h'a
congr 1
apply setLIntegral_congr_fun h'a (fun y hy ↦ ?_)
simp only [ha hy, indicator_of_mem]
apply ENNReal.tendsto_nhds_zero.2 fun ε εpos => ?_
obtain ⟨c, ct, xc⟩ : ∃ c ∈ t, ‖f x - c‖ₑ < ε / 2 :=
by
simp_rw [← edist_eq_enorm_sub]
have : f x ∈ closure t := ht (mem_range_self _)
exact EMetric.mem_closure_iff.1 this (ε / 2) (ENNReal.half_pos (ne_of_gt εpos))
filter_upwards [(tendsto_order.1 (M c ct)).2 (ε / 2) xc, h'x, v.eventually_measure_lt_top x] with a ha h'a h''a
apply ENNReal.div_le_of_le_mul
calc
(∫⁻ y in a, ‖f y - f x‖ₑ ∂μ) ≤ ∫⁻ y in a, ‖f y - c‖ₑ + ‖f x - c‖ₑ ∂μ :=
by
apply lintegral_mono fun x => ?_
simpa only [← edist_eq_enorm_sub] using edist_triangle_right _ _ _
_ = (∫⁻ y in a, ‖f y - c‖ₑ ∂μ) + ∫⁻ _ in a, ‖f x - c‖ₑ ∂μ := (lintegral_add_right _ measurable_const)
_ ≤ ε / 2 * μ a + ε / 2 * μ a := by
gcongr
· rw [ENNReal.div_lt_iff (Or.inl h'a.ne') (Or.inl h''a.ne)] at ha
exact ha.le
· simp only [lintegral_const, Measure.restrict_apply, MeasurableSet.univ, univ_inter]
gcongr
_ = ε * μ a := by rw [← add_mul, ENNReal.add_halves]
