English
If the mass of {x} under μ.map X is nonzero, then condDistrib Y X μ x s equals (μ.map X {x})^{-1} times μ.map ( (X a, Y a) ) ( {x} × s ).
Русский
Если масса множества {x} под μ.map X ненулевая, то condDistrib Y X μ x s равно (μ.map X {x})^{-1} умноженному на μ.map( (X a, Y a) )( {x} × s ).
LaTeX
$$$$\\text{If } μ.map X {x} \\neq 0, \\quad \\mathrm{condDistrib}(Y,X,μ)(x,s) = (μ.map X{ x})^{-1} \\; μ.map(\\lambda a, (X a, Y a))({x} \\times s).$$$$
Lean4
/-- If the singleton `{x}` has non-zero mass for `μ.map X`, then for all `s : Set Ω`,
`condDistrib Y X μ x s = (μ.map X {x})⁻¹ * μ.map (fun a => (X a, Y a)) ({x} ×ˢ s)` . -/
theorem condDistrib_apply_of_ne_zero [MeasurableSingletonClass β] (hY : Measurable Y) (x : β) (hX : μ.map X { x } ≠ 0)
(s : Set Ω) : condDistrib Y X μ x s = (μ.map X { x })⁻¹ * μ.map (fun a => (X a, Y a)) ({ x } ×ˢ s) :=
by
rw [condDistrib, Measure.condKernel_apply_of_ne_zero _ s]
· rw [Measure.fst_map_prodMk hY]
· rwa [Measure.fst_map_prodMk hY]
