English
If t is covered by a countable family of finite-measure sets, then for any measurable s, μ(toMeasurable μ t ∩ s) = μ(t ∩ s).
Русский
Если t покрыто счётной семьей множеств конечной меры, то для любого измеримого s выполняется μ(toMeasurable μ t ∩ s) = μ(t ∩ s).
LaTeX
$$$t \subseteq \bigcup_{n} v(n) \Rightarrow μ(toMeasurable μ t \cap s) = μ(t \cap s)$ for measurable s$$
Lean4
/-- If a set `t` is covered by a countable family of finite measure sets, 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_cover {s : Set α} (hs : MeasurableSet s) {t : Set α} {v : ℕ → Set α}
(hv : t ⊆ ⋃ n, v n) (h'v : ∀ n, μ (t ∩ v n) ≠ ∞) : μ (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 on each member of a spanning family using `toMeasurable`
-- (which is well behaved for finite measure sets thanks to `measure_toMeasurable_inter`), and
-- the desired property passes to the union.
have A : ∃ t', t' ⊇ t ∧ MeasurableSet t' ∧ ∀ u, MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u) :=
by
let w n := toMeasurable μ (t ∩ v n)
have hw : ∀ n, μ (w n) < ∞ := by
intro n
simp_rw [w, measure_toMeasurable]
exact (h'v n).lt_top
set t' := ⋃ n, toMeasurable μ (t ∩ disjointed w n) with ht'
have tt' : t ⊆ t' :=
calc
t ⊆ ⋃ n, t ∩ disjointed w n :=
by
rw [← inter_iUnion, iUnion_disjointed, inter_iUnion]
intro x hx
rcases mem_iUnion.1 (hv hx) with ⟨n, hn⟩
refine mem_iUnion.2 ⟨n, ?_⟩
have : x ∈ t ∩ v n := ⟨hx, hn⟩
exact ⟨hx, subset_toMeasurable μ _ this⟩
_ ⊆ ⋃ n, toMeasurable μ (t ∩ disjointed w n) := iUnion_mono fun n => subset_toMeasurable _ _
refine ⟨t', tt', MeasurableSet.iUnion fun n => measurableSet_toMeasurable μ _, fun u hu => ?_⟩
apply le_antisymm _ (by gcongr)
calc
μ (t' ∩ u) ≤ ∑' n, μ (toMeasurable μ (t ∩ disjointed w n) ∩ u) :=
by
rw [ht', iUnion_inter]
exact measure_iUnion_le _
_ = ∑' n, μ (t ∩ disjointed w n ∩ u) := by
congr 1
ext1 n
apply measure_toMeasurable_inter hu
apply ne_of_lt
calc
μ (t ∩ disjointed w n) ≤ μ (t ∩ w n) := by
gcongr
exact disjointed_le w n
_ ≤ μ (w n) := (measure_mono inter_subset_right)
_ < ∞ := hw n
_ = ∑' n, μ.restrict (t ∩ u) (disjointed w n) := by
congr 1
ext1 n
rw [restrict_apply, inter_comm t _, inter_assoc]
refine MeasurableSet.disjointed (fun n => ?_) n
exact measurableSet_toMeasurable _ _
_ = μ.restrict (t ∩ u) (⋃ n, disjointed w n) :=
by
rw [measure_iUnion]
· exact disjoint_disjointed _
· intro i
refine MeasurableSet.disjointed (fun n => ?_) i
exact measurableSet_toMeasurable _ _
_ ≤ μ.restrict (t ∩ u) univ := (measure_mono (subset_univ _))
_ = μ (t ∩ u) := by
rw [restrict_apply MeasurableSet.univ, univ_inter]
-- 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
