English
If f and g are equal almost everywhere and their set integrals agree on all measurable subsets, then f = g almost everywhere.
Русский
Если две функции равны почти всюду и интегралы по всем измеримым подмножествам совпадают, то функции равны почти всюду.
LaTeX
$$$$ f =_{a.e.} g \;\Rightarrow\; \\forall s, \\text{Measurable}(s), \\int_s f = \\int_s g. $$$$
Lean4
/-- Given an integrable function `g`, the conditional expectations of `g` with respect to
a sequence of sub-σ-algebras is uniformly integrable. -/
theorem uniformIntegrable_condExp {ι : Type*} [IsFiniteMeasure μ] {g : α → ℝ} (hint : Integrable g μ)
{ℱ : ι → MeasurableSpace α} (hℱ : ∀ i, ℱ i ≤ m0) : UniformIntegrable (fun i => μ[g|ℱ i]) 1 μ :=
by
let A : MeasurableSpace α := m0
have hmeas : ∀ n, ∀ C, MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} := fun n C =>
measurableSet_le measurable_const (stronglyMeasurable_condExp.mono (hℱ n)).measurable.nnnorm
have hg : MemLp g 1 μ := memLp_one_iff_integrable.2 hint
refine
uniformIntegrable_of le_rfl ENNReal.one_ne_top
(fun n => (stronglyMeasurable_condExp.mono (hℱ n)).aestronglyMeasurable) fun ε hε => ?_
by_cases hne : eLpNorm g 1 μ = 0
· rw [eLpNorm_eq_zero_iff hg.1 one_ne_zero] at hne
refine
⟨0, fun n =>
(le_of_eq <|
(eLpNorm_eq_zero_iff ((stronglyMeasurable_condExp.mono (hℱ n)).aestronglyMeasurable.indicator (hmeas n 0))
one_ne_zero).2
?_).trans
(zero_le _)⟩
filter_upwards [condExp_congr_ae (m := ℱ n) hne] with x hx
simp only [zero_le', Set.setOf_true, Set.indicator_univ, Pi.zero_apply, hx, condExp_zero]
obtain ⟨δ, hδ, h⟩ := hg.eLpNorm_indicator_le le_rfl ENNReal.one_ne_top hε
set C : ℝ≥0 := ⟨δ, hδ.le⟩⁻¹ * (eLpNorm g 1 μ).toNNReal with hC
have hCpos : 0 < C := mul_pos (inv_pos.2 hδ) (ENNReal.toNNReal_pos hne hg.eLpNorm_lt_top.ne)
have : ∀ n, μ {x : α | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ :=
by
intro n
have :
C ^ ENNReal.toReal 1 * μ {x | ENNReal.ofNNReal C ≤ ‖μ[g|ℱ n] x‖₊} ≤ eLpNorm μ[g|ℱ n] 1 μ ^ ENNReal.toReal 1 :=
by
rw [ENNReal.toReal_one, ENNReal.rpow_one]
convert
mul_meas_ge_le_pow_eLpNorm μ one_ne_zero ENNReal.one_ne_top
(stronglyMeasurable_condExp.mono (hℱ n)).aestronglyMeasurable C
· rw [ENNReal.toReal_one, ENNReal.rpow_one, enorm_eq_nnnorm]
rw [ENNReal.toReal_one, ENNReal.rpow_one, mul_comm, ←
ENNReal.le_div_iff_mul_le (Or.inl (ENNReal.coe_ne_zero.2 hCpos.ne')) (Or.inl ENNReal.coe_lt_top.ne)] at this
simp_rw [ENNReal.coe_le_coe] at this
refine this.trans ?_
rw [ENNReal.div_le_iff_le_mul (Or.inl (ENNReal.coe_ne_zero.2 hCpos.ne')) (Or.inl ENNReal.coe_lt_top.ne), hC,
Nonneg.inv_mk, ENNReal.coe_mul, ENNReal.coe_toNNReal hg.eLpNorm_lt_top.ne, ← mul_assoc, ←
ENNReal.ofReal_eq_coe_nnreal, ← ENNReal.ofReal_mul hδ.le, mul_inv_cancel₀ hδ.ne', ENNReal.ofReal_one, one_mul,
ENNReal.rpow_one]
exact eLpNorm_one_condExp_le_eLpNorm _
refine ⟨C, fun n => le_trans ?_ (h {x : α | C ≤ ‖(μ[g|ℱ n]) x‖₊} (hmeas n C) (this n))⟩
have hmeasℱ : MeasurableSet[ℱ n] {x : α | C ≤ ‖(μ[g|ℱ n]) x‖₊} :=
@measurableSet_le _ _ _ _ _ (ℱ n) _ _ _ _ _ measurable_const
(@Measurable.nnnorm _ _ _ _ _ (ℱ n) _ stronglyMeasurable_condExp.measurable)
rw [← eLpNorm_congr_ae (condExp_indicator hint hmeasℱ)]
exact eLpNorm_one_condExp_le_eLpNorm _
