Independent sets in real-valued form

The product rule of independent sets for real-valued masses, the form in which confirmation and relevance measures compute. [UPSTREAM] candidates for Mathlib/Probability/Independence/Basic.lean.

theorem ProbabilityTheory.IndepSet.measureReal_inter_eq_mul {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {s t : Set Ω} (h : IndepSet s t μ) : μ.real (s ∩ t) = μ.real s * μ.real t

theorem ProbabilityTheory.indepSet_iff_measureReal_inter_eq_mul {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {s t : Set Ω} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hs : MeasurableSet s) (ht : MeasurableSet t) : IndepSet s t μ ↔ μ.real (s ∩ t) = μ.real s * μ.real t