English
A variant formulation expressing monotonicity of the integral under measure-dominance assumptions.
Русский
Вариант формулировки монотонности интеграла при доминировании меры.
LaTeX
$$$$ \\text{(variant of monotonicity under measure domination)} $$$$
Lean4
theorem integral_mono_measure {ν} {f : α →ₛ F} (hf : 0 ≤ᵐ[ν] f) (hμν : μ ≤ ν) (hfν : Integrable f ν) :
f.integral μ ≤ f.integral ν := by
simp only [integral_eq]
apply Finset.sum_le_sum
simp only [forall_mem_range]
intro x
by_cases hx : 0 ≤ f x
· obtain (hx | hx) := hx.eq_or_lt
· simp [← hx]
simp only [measureReal_def]
gcongr
· exact integrable_iff.mp hfν (f x) hx.ne' |>.ne
· exact hμν _
· suffices ν (f ⁻¹' {f x}) = 0
by
have A : μ (f ⁻¹' {f x}) = 0 := by simpa using (hμν _ |>.trans_eq this)
simp [measureReal_def, A, this]
rw [← nonpos_iff_eq_zero, ← ae_iff.mp hf]
refine measure_mono fun y hy ↦ ?_
simp_all
