English
Let f,g map from Ω to types β,β' and μ a finite measure. Then f and g are independent with respect to μ if and only if for every pair of measurable φ:β→ℝ and ψ:β'→ℝ, whenever φ∘f and ψ∘g are integrable, we have ∫(φ∘f)(ω) (ψ∘g)(ω) dμ(ω) = ∫(φ∘f) dμ · ∫(ψ∘g) dμ.
Русский
Пусть f:g отображаются из Ω в β, β' и μ — конечно измеримая мера. Тогда f и g независимы относительно μ тогда и только тогда, когда для любой пары измеримых φ:β→ℝ и ψ:β'→ℝ, если φ∘f и ψ∘g интегрируемы, выполняется ∫(φ∘f)(ω) (ψ∘g)(ω) dμ(ω) = ∫(φ∘f) dμ · ∫(ψ∘g) dμ.
LaTeX
$$$\IndepFun\, f\, g\, μ \iff ∀\{φ:β→ℝ\}, \{ψ:β'→ℝ\},\ Measurable(φ) ∧ Measurable(ψ) ∧ Integrable(φ\circ f) μ ∧ Integrable(ψ\circ g) μ \Rightarrow \int μ (φ\circ f) (ψ\circ g) = \int μ (φ\circ f) \cdot \int μ (ψ\circ g)$$$
Lean4
theorem integral_fun_mul_eq_mul_integral (hXY : IndepFun X Y μ) (hX : AEStronglyMeasurable X μ)
(hY : AEStronglyMeasurable Y μ) : ∫ ω, X ω * Y ω ∂μ = μ[X] * μ[Y] :=
hXY.integral_mul_eq_mul_integral hX hY
