map_restrict_ae_le_map_indicator_ae

English

For measurable s, the pushforward of ae under the restricted measure is dominated by the pushforward under the indicator map.

Русский

При измеримости s суженная мера Ae под ней подавляется по отношению к Ae под индикаторной картой.

LaTeX

$$$ \\operatorname{map} f (ae(\\mu|_s)) \\le\\; \\operatorname{map}(s.indicator f) (ae\\mu) $$$

Lean4

theorem map_restrict_ae_le_map_indicator_ae [Zero β] (hs : MeasurableSet s) :
    Filter.map f (ae <| μ.restrict s) ≤ Filter.map (s.indicator f) (ae μ) :=
  by
  intro t
  by_cases ht : (0 : β) ∈ t
  · rw [mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem ht hs]
    exact id
  rw [mem_map_indicator_ae_iff_of_zero_notMem ht, mem_map_restrict_ae_iff hs]
  exact fun h => measure_mono_null (Set.inter_subset_left.trans Set.subset_union_left) h

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