Documentation

LeanBandits.ForMathlib.IdentDistrib

theorem ProbabilityTheory.IdentDistrib.prod {Ω : Type u_1} {Ω' : Type u_2} { : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'} {X Y : Ω} {Z W : Ω'} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hXZ : IdentDistrib X Z μ ν) (hYW : IdentDistrib Y W μ ν) (hXY : IndepFun X Y μ) (hZW : IndepFun Z W ν) :
IdentDistrib (fun (ω : Ω) => (X ω, Y ω)) (fun (ω' : Ω') => (Z ω', W ω')) μ ν
theorem ProbabilityTheory.IdentDistrib.pi {Ω : Type u_1} {Ω' : Type u_2} {ι : Type u_3} { : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'} [Countable ι] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {X : ιΩ} {Y : ιΩ'} (h : ∀ (i : ι), IdentDistrib (X i) (Y i) μ ν) (hX_ind : iIndepFun X μ) (hY_ind : iIndepFun Y ν) :
IdentDistrib (fun (ω : Ω) (x : ι) => X x ω) (fun (ω : Ω') (x : ι) => Y x ω) μ ν