English
Under monotone or surjective assumptions, comap_ofFunction equality holds with the pullback measure.
Русский
При монотонных или сюръективных условиях равенство comap_ofFunction выполняется для меры-обратной композиции.
LaTeX
$$$\\text{comap}_f (\\text{OuterMeasure.ofFunction } m m\\_empty) = \\text{OuterMeasure.ofFunction } (m \\circ f) m\\_empty.$$$
Lean4
theorem comap_ofFunction {β} (f : β → α) (h : Monotone m ∨ Surjective f) :
comap f (OuterMeasure.ofFunction m m_empty) =
OuterMeasure.ofFunction (fun s => m (f '' s)) (by simp; simp [m_empty]) :=
by
refine le_antisymm (le_ofFunction.2 fun s => ?_) fun s => ?_
· rw [comap_apply]
apply ofFunction_le
· rw [comap_apply, ofFunction_apply, ofFunction_apply]
refine iInf_mono' fun t => ⟨fun k => f ⁻¹' t k, ?_⟩
refine iInf_mono' fun ht => ?_
rw [Set.image_subset_iff, preimage_iUnion] at ht
refine ⟨ht, ENNReal.tsum_le_tsum fun n => ?_⟩
rcases h with hl | hr
exacts [hl (image_preimage_subset _ _), (congr_arg m (hr.image_preimage (t n))).le]
