condDistrib_comp_self — Mathlib

English

If f is measurable, then condDistrib (f ∘ X) X μ equals the pushforward by Kernel.deterministic f of μ.map X, i.e., condDistrib (f ∘ X) X μ = a.e. Kernel.deterministic f μ.

Русский

Если f измерим, то condDistrib (f ∘ X) X μ совпадает почти наверняка с Kernel.deterministic f.

LaTeX

$$$$ \\mathrm{condDistrib}(f\\circ X, X, μ) =_{a.e.} \\mathrm{deterministic}(f). $$$$

Lean4

theorem condDistrib_comp_self (X : α → β) {f : β → Ω} (hf : Measurable f) :
    condDistrib (f ∘ X) X μ =ᵐ[μ.map X] Kernel.deterministic f hf :=
  by
  by_cases hX : AEMeasurable X μ
  swap; · simp [Measure.map_of_not_aemeasurable hX, Filter.EventuallyEq]
  refine condDistrib_ae_eq_of_measure_eq_compProd X (by fun_prop) ?_
  rw [Measure.compProd_deterministic, AEMeasurable.map_map_of_aemeasurable (by fun_prop) hX]
  rfl

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