English
If μ is finite on Ω and f is a filtration satisfying SigmaFiniteFiltration μ f, then for every i, the restricted measure μ.trim (f.le i) is sigma-finite.
Русский
Пусть μ – конечная мера на Ω и f – фильтрация, удовлетворяющая условию симфинасфинитности; тогда для каждого i мера μ, ограниченная σ‑алгеброй f(i), симфинафинна.
LaTeX
$$$[\\text{SigmaFiniteFiltration } μ f] \\Rightarrow \\forall i, \\ SigmaFinite (μ.trim (f.le i)).$$$
Lean4
noncomputable instance instCompleteLattice : CompleteLattice (Filtration ι m)
where
le := (· ≤ ·)
le_refl _ _ := le_rfl
le_trans _ _ _ h_fg h_gh i := (h_fg i).trans (h_gh i)
le_antisymm _ _ h_fg h_gf := Filtration.ext <| funext fun i => (h_fg i).antisymm (h_gf i)
sup := (· ⊔ ·)
le_sup_left _ _ _ := le_sup_left
le_sup_right _ _ _ := le_sup_right
sup_le _ _ _ h_fh h_gh i := sup_le (h_fh i) (h_gh _)
inf := (· ⊓ ·)
inf_le_left _ _ _ := inf_le_left
inf_le_right _ _ _ := inf_le_right
le_inf _ _ _ h_fg h_fh i := le_inf (h_fg i) (h_fh i)
sSup := sSup
le_sSup _ f hf_mem _ := le_sSup ⟨f, hf_mem, rfl⟩
sSup_le s f h_forall
i :=
sSup_le fun m' hm' => by
obtain ⟨g, hg_mem, hfm'⟩ := hm'
rw [← hfm']
exact h_forall g hg_mem i
sInf := sInf
sInf_le s f hf_mem
i := by
have hs : s.Nonempty := ⟨f, hf_mem⟩
simp only [sInf_def, hs, if_true]
exact sInf_le ⟨f, hf_mem, rfl⟩
le_sInf s f h_forall
i := by
by_cases hs : s.Nonempty
swap; · simp only [sInf_def, hs, if_false]; exact f.le i
simp only [sInf_def, hs, if_true, le_sInf_iff, Set.mem_image, forall_exists_index, and_imp,
forall_apply_eq_imp_iff₂]
exact fun g hg_mem => h_forall g hg_mem i
top := ⊤
bot := ⊥
le_top f i := f.le' i
bot_le _ _ := bot_le
