condDistrib_congr — Mathlib

English

If Y equals Y' μ-a.e. and X equals X' μ-a.e., then condDistrib Y X μ = condDistrib Y' X' μ.

Русский

Если Y совпадает с Y' почти наверное и X совпадает с X' почти наверное, то condDistrib Y X μ = condDistrib Y' X' μ.

LaTeX

$$$$\\text{If } Y =_{μ}\\, Y' \\text{ and } X =_{μ}\\, X', \\quad \\mathrm{condDistrib}(Y,X,μ) = \\mathrm{condDistrib}(Y',X',μ). $$$$

Lean4

theorem condDistrib_congr {X' : α → β} {Y' : α → Ω} (hY : Y =ᵐ[μ] Y') (hX : X =ᵐ[μ] X') :
    condDistrib Y X μ = condDistrib Y' X' μ :=
  by
  rw [condDistrib, condDistrib]
  congr 1
  rw [Measure.map_congr]
  filter_upwards [hX, hY] with a ha hb using by rw [ha, hb]

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