TODO #
Less explicit arguments to cond_eq_zero_of_meas_eq_zero
theorem
ProbabilityTheory.ae_cond_mem
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{s : Set Ω}
(hs : MeasurableSet s)
:
∀ᵐ (x : Ω) ∂ProbabilityTheory.cond μ s, x ∈ s
theorem
ProbabilityTheory.cond_iInter
{ι : Type u_1}
{Ω : Type u_2}
{α : Type u_3}
{β : Type u_4}
{mΩ : MeasurableSpace Ω}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure Ω}
{X : ι → Ω → α}
{Y : ι → Ω → β}
{f : ι → Set Ω}
{t : ι → Set β}
{s : Finset ι}
[Finite ι]
(hY : ∀ (i : ι), Measurable (Y i))
(h_indep : ProbabilityTheory.iIndepFun (fun (x : ι) => mα.prod mβ) (fun (i : ι) (ω : Ω) => (X i ω, Y i ω)) μ)
(hf : ∀ i ∈ s, MeasurableSet (f i))
(hy : ∀ (i : ι), μ (Y i ⁻¹' t i) ≠ 0)
(ht : ∀ (i : ι), MeasurableSet (t i))
:
(ProbabilityTheory.cond μ (⋂ (i : ι), Y i ⁻¹' t i)) (⋂ i ∈ s, f i) = ∏ i ∈ s, (ProbabilityTheory.cond μ (Y i ⁻¹' t i)) (f i)
The probability of an intersection of preimaαes conditioninα on another intersection factors into a product.
theorem
ProbabilityTheory.iIndepFun.cond
{ι : Type u_1}
{Ω : Type u_2}
{α : Type u_3}
{β : Type u_4}
{mΩ : MeasurableSpace Ω}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure Ω}
{X : ι → Ω → α}
{Y : ι → Ω → β}
{t : ι → Set β}
[Finite ι]
(hY : ∀ (i : ι), Measurable (Y i))
(h_indep : ProbabilityTheory.iIndepFun (fun (x : ι) => mα.prod mβ) (fun (i : ι) (ω : Ω) => (X i ω, Y i ω)) μ)
(hy : ∀ (i : ι), μ (Y i ⁻¹' t i) ≠ 0)
(ht : ∀ (i : ι), MeasurableSet (t i))
:
ProbabilityTheory.iIndepFun (fun (x : ι) => mα) X (ProbabilityTheory.cond μ (⋂ (i : ι), Y i ⁻¹' t i))