ae_snd — Mathlib

English

Given hf: AEStronglyMeasurable f μ, the pair f and (hf.mk f) are identDistrib with μ and μ.

Русский

Пусть hf: AEStronglyMeasurable f μ, тогда пара f и (hf.mk f) идентично распределена относительно μ и μ.

LaTeX

$$$hf : AEStronglyMeasurable f μ \Rightarrow IdentDistrib f (hf.mk f) μ μ$$$

Lean4

theorem ae_snd (h : IdentDistrib f g μ ν) {p : γ → Prop} (pmeas : MeasurableSet {x | p x}) (hp : ∀ᵐ x ∂μ, p (f x)) :
    ∀ᵐ x ∂ν, p (g x) := by
  apply (ae_map_iff h.aemeasurable_snd pmeas).1
  rw [← h.map_eq]
  exact (ae_map_iff h.aemeasurable_fst pmeas).2 hp

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