English
If μ is the sum of a countable family of measures m_n and each t has finite μ-measure on intersections with s, then μ(toMeasurable μ t ∩ s) = μ(t ∩ s).
Русский
Если μ распадается на счётное множество мер m_n и каждая пара t ∩ s имеет конечную меру, то μ(toMeasurable μ t ∩ s) = μ(t ∩ s).
LaTeX
$$$μ(\mathrm{toMeasurable}(μ,t) \cap s) = μ(t \cap s)$ under μ = ∑ m_n with finiteness$$
Lean4
/-- If a measure `μ` is the sum of a countable family `mₙ`, and a set `t` has finite measure for
each `mₙ`, then its measurable superset `toMeasurable μ t` (which has the same measure as `t`)
satisfies, for any measurable set `s`, the equality `μ (toMeasurable μ t ∩ s) = μ (t ∩ s)`. -/
theorem measure_toMeasurable_inter_of_sum {s : Set α} (hs : MeasurableSet s) {t : Set α} {m : ℕ → Measure α}
(hv : ∀ n, m n t ≠ ∞) (hμ : μ = sum m) : μ (toMeasurable μ t ∩ s) = μ (t ∩ s) := by
-- we show that there is a measurable superset of `t` satisfying the conclusion for any
-- measurable set `s`. It is built for each measure `mₙ` using `toMeasurable`
-- (which is well behaved for finite measure sets thanks to `measure_toMeasurable_inter`), and
-- then taking the intersection over `n`.
have A : ∃ t', t' ⊇ t ∧ MeasurableSet t' ∧ ∀ u, MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u) :=
by
let w n := toMeasurable (m n) t
have T : t ⊆ ⋂ n, w n := subset_iInter (fun i ↦ subset_toMeasurable (m i) t)
have M : MeasurableSet (⋂ n, w n) := MeasurableSet.iInter (fun i ↦ measurableSet_toMeasurable (m i) t)
refine ⟨⋂ n, w n, T, M, fun u hu ↦ ?_⟩
refine le_antisymm ?_ (by gcongr)
rw [hμ, sum_apply _ (M.inter hu)]
apply le_trans _ (le_sum_apply _ _)
apply ENNReal.tsum_le_tsum (fun i ↦ ?_)
calc
m i ((⋂ n, w n) ∩ u) ≤ m i (w i ∩ u) := by gcongr; apply iInter_subset
_ = m i (t ∩ u) :=
measure_toMeasurable_inter hu
(hv i)
-- thanks to the definition of `toMeasurable`, the previous property will also be shared
-- by `toMeasurable μ t`, which is enough to conclude the proof.
rw [toMeasurable]
split_ifs with ht
· apply measure_congr
exact ae_eq_set_inter ht.choose_spec.2.2 (ae_eq_refl _)
· exact A.choose_spec.2.2 s hs
