English
A set of logical equivalences showing that certain rearrangements of frestrictLe/restrictLe correspondences preserve equalities.
Русский
Логические эквивалентности, показывающие, что перестановки между frestrictLe/restrictLe сохраняют равенства.
LaTeX
$$$\\text{(simplicity lemmas relating frestrictLe, restrictLe, piCongrLeft, etc.)}$$$
Lean4
theorem filtrationOfSet_eq_natural [MulZeroOneClass β] [Nontrivial β] {s : ι → Set Ω}
(hsm : ∀ i, MeasurableSet[m] (s i)) :
filtrationOfSet hsm =
natural (fun i => (s i).indicator (fun _ => 1 : Ω → β)) fun i => stronglyMeasurable_one.indicator (hsm i) :=
by
simp only [filtrationOfSet, natural, measurableSpace_iSup_eq, exists_prop, mk.injEq]
ext1 i
refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_)
· rintro _ ⟨j, hij, rfl⟩
refine measurableSet_generateFrom ⟨j, measurableSet_generateFrom ⟨hij, ?_⟩⟩
rw [comap_eq_generateFrom]
refine measurableSet_generateFrom ⟨{ 1 }, measurableSet_singleton 1, ?_⟩
ext x
simp
· rintro t ⟨n, ht⟩
suffices
MeasurableSpace.generateFrom
{t | n ≤ i ∧ MeasurableSet[MeasurableSpace.comap ((s n).indicator (fun _ => 1 : Ω → β)) mβ] t} ≤
MeasurableSpace.generateFrom {t | ∃ (j : ι), j ≤ i ∧ s j = t}
by exact this _ ht
refine generateFrom_le ?_
rintro t ⟨hn, u, _, hu'⟩
obtain heq | heq | heq | heq := Set.indicator_const_preimage (s n) u (1 : β)
on_goal 4 => rw [Set.mem_singleton_iff] at heq
all_goals rw [heq] at hu'; rw [← hu']
exacts [MeasurableSet.univ, measurableSet_generateFrom ⟨n, hn, rfl⟩,
MeasurableSet.compl (measurableSet_generateFrom ⟨n, hn, rfl⟩), measurableSet_empty _]
