independent iff mul of laws equals laws of intersection

Stream: maths

[Jiayou]

I am a newbie to Lean andI want to formalize a simple probability proposition/definition saying that two random variables X, Y are independent if and only if their laws satisfies

$$P(X^{-1} (B) \land Y^{-1} (C)) = P(X^{-1} (B)) \times P(Y^{-1}(C))$$

The following is my attempt

import Mathlib

open MeasureTheory ProbabilityTheory
open Set
open scoped ENNReal
open MeasurableSpace MeasureTheory.Measure

set_option diagnostics true

variable {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P] {μ: Measure ℝ}

lemma indep_iff_product_measure_mul_equals (X Y : Ω → ℝ) (hX : Measurable X) (hY : Measurable Y) :
  (IndepFun X Y P) ↔ ∀ B C, (P ((preimage X) B)) * (P ((preimage Y) C)) = P (preimage X B ∩ preimage Y C) := sorry

I have the following questions:

• I don't know how to restrict B, C as Borel sets on \real. Seems I need to define a implicit BorelSpace but I want to know how.
• I am wondering if we can rewrite this by product measure to avoid awkward intersection operator.
• Could someone complete the proof?

[Etienne Marion]

The corresponding lemma in Mathlib is ProbabilityTheory.IndepFun_iff. You should look at the code because the sigma-algebras are not explicit in the doc.

[Rémy Degenne]

ProbabilityTheory.indepFun_iff_measure_inter_preimage_eq_mul is a better match.

The MeasurableSpace instance on Real is the Borel sigma-algebra, so to say that B is a Borel set you simply use MeasurableSet B.