English
Lebesgue differentiation for averages: for locally integrable f, almost every x the averages of f over shrinking balls converge to f(x).
Русский
Лебегова дифференциация по средним: для локально интегрируемой f средние значения по сжимающимся шарам сходятся к f(x) почти в каждой точке.
LaTeX
$$$\forall f, hf, \forall K>1,\ almostEvery x,\ Tendsto (j\mapsto \frac{1}{μ(B(w_j, δ_j))} ∫_{B(w_j, δ_j)} f(y) dμ(y)) (l) (𝓝 f(x)).$$$
Lean4
/-- Given two thresholds `p < q`, the sets `{x | v.limRatio ρ x < p}`
and `{x | q < v.limRatio ρ x}` are obviously disjoint. The key to proving that `v.limRatio ρ` is
almost everywhere measurable is to show that these sets have measurable supersets which are also
disjoint, up to zero measure. This is the content of this lemma. -/
theorem exists_measurable_supersets_limRatio {p q : ℝ≥0} (hpq : p < q) :
∃ a b,
MeasurableSet a ∧
MeasurableSet b ∧ {x | v.limRatio ρ x < p} ⊆ a ∧ {x | (q : ℝ≥0∞) < v.limRatio ρ x} ⊆ b ∧ μ (a ∩ b) = 0 :=
by
/- Here is a rough sketch, assuming that the measure is finite and the limit is well defined
everywhere. Let `u := {x | v.limRatio ρ x < p}` and `w := {x | q < v.limRatio ρ x}`. They
have measurable supersets `u'` and `w'` of the same measure. We will show that these satisfy
the conclusion of the theorem, i.e., `μ (u' ∩ w') = 0`. For this, note that
`ρ (u' ∩ w') = ρ (u ∩ w')` (as `w'` is measurable, see `measure_toMeasurable_add_inter_left`).
The latter set is included in the set where the limit of the ratios is `< p`, and therefore
its measure is `≤ p * μ (u ∩ w')`. Using the same trick in the other direction gives that this
is `p * μ (u' ∩ w')`. We have shown that `ρ (u' ∩ w') ≤ p * μ (u' ∩ w')`. Arguing in the same
way but using the `w` part gives `q * μ (u' ∩ w') ≤ ρ (u' ∩ w')`. If `μ (u' ∩ w')` were nonzero,
this would be a contradiction as `p < q`.
For the rigorous proof, we need to work on a part of the space where the measure is finite
(provided by `spanningSets (ρ + μ)`) and to restrict to the set where the limit is well defined
(called `s` below, of full measure). Otherwise, the argument goes through.
-/
let s := {x | ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)}
let o : ℕ → Set α := spanningSets (ρ + μ)
let u n := s ∩ {x | v.limRatio ρ x < p} ∩ o n
let w n := s ∩ {x | (q : ℝ≥0∞) < v.limRatio ρ x} ∩ o n
refine
⟨toMeasurable μ sᶜ ∪ ⋃ n, toMeasurable (ρ + μ) (u n), toMeasurable μ sᶜ ∪ ⋃ n, toMeasurable (ρ + μ) (w n), ?_, ?_,
?_, ?_, ?_⟩
-- check that these sets are measurable supersets as required
· exact (measurableSet_toMeasurable _ _).union (MeasurableSet.iUnion fun n => measurableSet_toMeasurable _ _)
· exact (measurableSet_toMeasurable _ _).union (MeasurableSet.iUnion fun n => measurableSet_toMeasurable _ _)
· intro x hx
by_cases h : x ∈ s
· refine Or.inr (mem_iUnion.2 ⟨spanningSetsIndex (ρ + μ) x, ?_⟩)
exact subset_toMeasurable _ _ ⟨⟨h, hx⟩, mem_spanningSetsIndex _ _⟩
· exact Or.inl (subset_toMeasurable μ sᶜ h)
· intro x hx
by_cases h : x ∈ s
· refine Or.inr (mem_iUnion.2 ⟨spanningSetsIndex (ρ + μ) x, ?_⟩)
exact subset_toMeasurable _ _ ⟨⟨h, hx⟩, mem_spanningSetsIndex _ _⟩
·
exact
Or.inl
(subset_toMeasurable μ sᶜ h)
-- it remains to check the nontrivial part that these sets have zero measure intersection.
-- it suffices to do it for fixed `m` and `n`, as one is taking countable unions.
suffices H : ∀ m n : ℕ, μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
by
have A :
(toMeasurable μ sᶜ ∪ ⋃ n, toMeasurable (ρ + μ) (u n)) ∩ (toMeasurable μ sᶜ ∪ ⋃ n, toMeasurable (ρ + μ) (w n)) ⊆
toMeasurable μ sᶜ ∪ ⋃ (m) (n), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n) :=
by
simp only [inter_union_distrib_left, union_inter_distrib_right, true_and, subset_union_left, union_subset_iff,
inter_self]
refine ⟨?_, ?_, ?_⟩
· exact inter_subset_right.trans subset_union_left
· exact inter_subset_left.trans subset_union_left
· simp_rw [iUnion_inter, inter_iUnion]; exact subset_union_right
refine le_antisymm ((measure_mono A).trans ?_) bot_le
calc
μ (toMeasurable μ sᶜ ∪ ⋃ (m) (n), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
μ (toMeasurable μ sᶜ) + μ (⋃ (m) (n), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) :=
measure_union_le _ _
_ = μ (⋃ (m) (n), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) := by
have : μ sᶜ = 0 := v.ae_tendsto_div hρ; rw [measure_toMeasurable, this, zero_add]
_ ≤ ∑' (m) (n), μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) :=
((measure_iUnion_le _).trans (ENNReal.tsum_le_tsum fun m => measure_iUnion_le _))
_ = 0 := by
simp only [H, tsum_zero]
-- now starts the nontrivial part of the argument. We fix `m` and `n`, and show that the
-- measurable supersets of `u m` and `w n` have zero measure intersection by using the lemmas
-- `measure_toMeasurable_add_inter_left` (to reduce to `u m` or `w n` instead of the measurable
-- superset) and `measure_le_of_frequently_le` to compare their measures for `ρ` and `μ`.
intro m n
have I : (ρ + μ) (u m) ≠ ∞ :=
by
apply (lt_of_le_of_lt (measure_mono _) (measure_spanningSets_lt_top (ρ + μ) m)).ne
exact inter_subset_right
have J : (ρ + μ) (w n) ≠ ∞ :=
by
apply (lt_of_le_of_lt (measure_mono _) (measure_spanningSets_lt_top (ρ + μ) n)).ne
exact inter_subset_right
have A :
ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
p * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) :=
calc
ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = ρ (u m ∩ toMeasurable (ρ + μ) (w n)) :=
measure_toMeasurable_add_inter_left (measurableSet_toMeasurable _ _) I
_ ≤ (p • μ) (u m ∩ toMeasurable (ρ + μ) (w n)) :=
by
refine v.measure_le_of_frequently_le (p • μ) hρ _ fun x hx => ?_
have L : Tendsto (fun a : Set α => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x)) :=
tendsto_nhds_limUnder hx.1.1.1
have I : ∀ᶠ b : Set α in v.filterAt x, ρ b / μ b < p := (tendsto_order.1 L).2 _ hx.1.1.2
apply I.frequently.mono fun a ha => ?_
rw [coe_nnreal_smul_apply]
refine (ENNReal.div_le_iff_le_mul ?_ (Or.inr (bot_le.trans_lt ha).ne')).1 ha.le
simp only [ENNReal.coe_ne_top, Ne, or_true, not_false_iff]
_ = p * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) := by
simp only [coe_nnreal_smul_apply, measure_toMeasurable_add_inter_right (measurableSet_toMeasurable _ _) I]
have B :
(q : ℝ≥0∞) * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) :=
calc
(q : ℝ≥0∞) * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) =
(q : ℝ≥0∞) * μ (toMeasurable (ρ + μ) (u m) ∩ w n) :=
by
conv_rhs => rw [inter_comm]
rw [inter_comm, measure_toMeasurable_add_inter_right (measurableSet_toMeasurable _ _) J]
_ ≤ ρ (toMeasurable (ρ + μ) (u m) ∩ w n) :=
by
rw [← coe_nnreal_smul_apply]
refine v.measure_le_of_frequently_le _ (.smul_left .rfl _) _ ?_
intro x hx
have L : Tendsto (fun a : Set α => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x)) :=
tendsto_nhds_limUnder hx.2.1.1
have I : ∀ᶠ b : Set α in v.filterAt x, (q : ℝ≥0∞) < ρ b / μ b := (tendsto_order.1 L).1 _ hx.2.1.2
apply I.frequently.mono fun a ha => ?_
rw [coe_nnreal_smul_apply]
exact ENNReal.mul_le_of_le_div ha.le
_ = ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) :=
by
conv_rhs => rw [inter_comm]
rw [inter_comm]
exact (measure_toMeasurable_add_inter_left (measurableSet_toMeasurable _ _) J).symm
by_contra h
apply lt_irrefl (ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)))
calc
ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
p * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) :=
A
_ < q * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) :=
by
gcongr
suffices H : (ρ + μ) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≠ ∞
by
simp only [not_or, ENNReal.add_eq_top, Pi.add_apply, Ne, coe_add] at H
exact H.2
apply (lt_of_le_of_lt (measure_mono inter_subset_left) _).ne
rw [measure_toMeasurable]
apply lt_of_le_of_lt (measure_mono _) (measure_spanningSets_lt_top (ρ + μ) m)
exact inter_subset_right
_ ≤ ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) := B
