English
A more elaborate version of isLUB with measurable sets and a.e. equivalences.
Русский
Более подробная версия isLUB с измеримыми множествами и эквивалентностями почти повсеместно.
LaTeX
$$$\forall i,\text{Measurable}(f_i) \Rightarrow \forall s,\ MeasurableSet(s) \Rightarrow (IsLUB\,\dots) \Rightarrow \text{Measurable}(g)$$$
Lean4
theorem isLUB {ι} {μ : Measure δ} [Countable ι] {f : ι → δ → α} {g : δ → α} (hf : ∀ i, AEMeasurable (f i) μ)
(hg : ∀ᵐ b ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)) : AEMeasurable g μ := by
classical
nontriviality α
haveI hα : Nonempty α := inferInstance
rcases isEmpty_or_nonempty ι with hι | hι
· simp only [IsEmpty.exists_iff, setOf_false, isLUB_empty_iff] at hg
exact aemeasurable_const' (hg.mono fun a ha => hg.mono fun b hb => (ha _).antisymm (hb _))
let p : δ → (ι → α) → Prop := fun x f' => IsLUB {a | ∃ i, f' i = a} (g x)
let g_seq := (aeSeqSet hf p).piecewise g fun _ => hα.some
have hg_seq : ∀ b, IsLUB {a | ∃ i, aeSeq hf p i b = a} (g_seq b) :=
by
intro b
simp only [g_seq, aeSeq, Set.piecewise]
split_ifs with h
· have h_set_eq : {a : α | ∃ i : ι, (hf i).mk (f i) b = a} = {a : α | ∃ i : ι, f i b = a} :=
by
ext x
simp_rw [Set.mem_setOf_eq, aeSeq.mk_eq_fun_of_mem_aeSeqSet hf h]
rw [h_set_eq]
exact aeSeq.fun_prop_of_mem_aeSeqSet hf h
· exact IsGreatest.isLUB ⟨(@exists_const (hα.some = hα.some) ι _).2 rfl, fun x ⟨i, hi⟩ => hi.ge⟩
refine ⟨g_seq, Measurable.isLUB (aeSeq.measurable hf p) hg_seq, ?_⟩
exact
(ite_ae_eq_of_measure_compl_zero g (fun _ => hα.some) (aeSeqSet hf p)
(aeSeq.measure_compl_aeSeqSet_eq_zero hf hg)).symm
