le_ae_join — Mathlib

English

For a measure m on measures, the a.e.-image (ae m).bind ae is dominated by ae m.join.

Русский

При мере m над множествами мер, образ ae m через связывание ae не превосходит ae m.join.

LaTeX

$$$(ae\\,m).bind\\ ae \\leq ae\\,m.join.$$$

Lean4

theorem le_ae_join (m : Measure (Measure α)) : (ae m).bind ae ≤ ae m.join :=
  by
  intro s hs
  rcases exists_measurable_superset_of_null hs with ⟨t, hst, htm, ht⟩
  rw [join_apply htm, lintegral_eq_zero_iff (measurable_coe htm)] at ht
  rw [mem_bind']
  exact ht.mono fun _ ↦ measure_mono_null hst

Похожие утверждения