English
Independence of functions f and g into arbitrary types is equivalent to the product-form of mixed expectations: for all measurable φ,ψ with appropriate integrability, E[φ(f)·ψ(g)] = E[φ(f)]·E[ψ(g)].
Русский
Независимость функций f и g сводится к тому, что для всех измеримых φ,ψ с подходящей интегрируемостью выполняется E[φ(f)·ψ(g)] = E[φ(f)]·E[ψ(g)].
LaTeX
$$$\text{IndepFun}(f,g,μ) \iff \forall\{φ:β→ℝ\}, \{ψ:β'→ℝ\},\ Measurable(φ) ∧ Measurable(ψ) ∧ Integrable(φ\circ f) μ ∧ Integrable(ψ\circ g) μ \Rightarrow \int μ (φ\circ f) (ψ\circ g) = \int μ (φ\circ f) · \int μ (ψ\circ g)$$$
Lean4
/-- Independence of functions `f` and `g` into arbitrary types is characterized by the relation
`E[(φ ∘ f) * (ψ ∘ g)] = E[φ ∘ f] * E[ψ ∘ g]` for all measurable `φ` and `ψ` with values in `ℝ`
satisfying appropriate integrability conditions. -/
theorem indepFun_iff_integral_comp_mul [IsFiniteMeasure μ] {β β' : Type*} {mβ : MeasurableSpace β}
{mβ' : MeasurableSpace β'} {f : Ω → β} {g : Ω → β'} {hfm : Measurable f} {hgm : Measurable g} :
IndepFun f g μ ↔
∀ {φ : β → ℝ} {ψ : β' → ℝ},
Measurable φ →
Measurable ψ →
Integrable (φ ∘ f) μ →
Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g) :=
by
refine
⟨fun hfg _ _ hφ hψ _ _ =>
hfg.integral_comp_mul_comp hfm.aemeasurable hgm.aemeasurable hφ.aestronglyMeasurable hψ.aestronglyMeasurable, ?_⟩
rw [IndepFun_iff]
rintro h _ _ ⟨A, hA, rfl⟩ ⟨B, hB, rfl⟩
specialize
h (measurable_one.indicator hA) (measurable_one.indicator hB)
((integrable_const 1).indicator (hfm.comp measurable_id hA))
((integrable_const 1).indicator (hgm.comp measurable_id hB))
rwa [← ENNReal.toReal_eq_toReal (measure_ne_top μ _), ENNReal.toReal_mul, ← measureReal_def, ← measureReal_def, ←
measureReal_def, ← integral_indicator_one ((hfm hA).inter (hgm hB)), ← integral_indicator_one (hfm hA), ←
integral_indicator_one (hgm hB), Set.inter_indicator_one]
exact ENNReal.mul_ne_top (measure_ne_top μ _) (measure_ne_top μ _)
