Laws of stepsUntil and rewardByCount #
theorem
ProbabilityTheory.IndepFun.of_measurable
{α : Type u_1}
{γ : Type u_3}
{δ : Type u_4}
{γ' : Type u_5}
{δ' : Type u_6}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{mγ' : MeasurableSpace γ'}
{mδ' : MeasurableSpace δ'}
[StandardBorelSpace δ']
[Nonempty δ']
[StandardBorelSpace γ']
[Nonempty γ']
{μ : MeasureTheory.Measure α}
{Y : α → γ}
{Z : α → δ}
{Y' : α → γ'}
{Z' : α → δ'}
(h_indep : IndepFun Y Z μ)
(hY_meas : Measurable Y')
(hZ_meas : Measurable Z')
:
IndepFun Y' Z' μ
theorem
ProbabilityTheory.IndepFun.of_measurable_left
{α : Type u_1}
{γ : Type u_3}
{δ : Type u_4}
{γ' : Type u_5}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{mγ' : MeasurableSpace γ'}
[StandardBorelSpace γ']
[Nonempty γ']
{μ : MeasureTheory.Measure α}
{Y : α → γ}
{Z : α → δ}
{Y' : α → γ'}
(h_indep : IndepFun Y Z μ)
(hY_meas : Measurable Y')
:
IndepFun Y' Z μ
theorem
ProbabilityTheory.IndepFun.of_measurable_right
{α : Type u_1}
{γ : Type u_3}
{δ : Type u_4}
{δ' : Type u_6}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{mδ' : MeasurableSpace δ'}
[StandardBorelSpace δ']
[Nonempty δ']
{μ : MeasureTheory.Measure α}
{Y : α → γ}
{Z : α → δ}
{Z' : α → δ'}
(h_indep : IndepFun Y Z μ)
(hZ_meas : Measurable Z')
:
IndepFun Y Z' μ
theorem
ProbabilityTheory.CondIndepFun.of_measurable
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{γ' : Type u_5}
{δ' : Type u_6}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{mγ' : MeasurableSpace γ'}
{mδ' : MeasurableSpace δ'}
[StandardBorelSpace δ']
[Nonempty δ']
[StandardBorelSpace γ']
[Nonempty γ']
{μ : MeasureTheory.Measure α}
{X : α → β}
{hX : Measurable X}
{Y : α → γ}
{Z : α → δ}
{Y' : α → γ'}
{Z' : α → δ'}
[StandardBorelSpace α]
[MeasureTheory.IsFiniteMeasure μ]
(h_indep : CondIndepFun (MeasurableSpace.comap X inferInstance) ⋯ Y Z μ)
(hY_meas : Measurable Y')
(hZ_meas : Measurable Z')
:
CondIndepFun (MeasurableSpace.comap X inferInstance) ⋯ Y' Z' μ
theorem
ProbabilityTheory.CondIndepFun.of_measurable_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{γ' : Type u_5}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{mγ' : MeasurableSpace γ'}
[StandardBorelSpace γ']
[Nonempty γ']
{μ : MeasureTheory.Measure α}
{X : α → β}
{hX : Measurable X}
{Y : α → γ}
{Z : α → δ}
{Y' : α → γ'}
[StandardBorelSpace α]
[MeasureTheory.IsFiniteMeasure μ]
(h_indep : CondIndepFun (MeasurableSpace.comap X inferInstance) ⋯ Y Z μ)
(hY_meas : Measurable Y')
:
CondIndepFun (MeasurableSpace.comap X inferInstance) ⋯ Y' Z μ
theorem
ProbabilityTheory.CondIndepFun.of_measurable_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{δ' : Type u_6}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{mδ' : MeasurableSpace δ'}
[StandardBorelSpace δ']
[Nonempty δ']
{μ : MeasureTheory.Measure α}
{X : α → β}
{hX : Measurable X}
{Y : α → γ}
{Z : α → δ}
{Z' : α → δ'}
[StandardBorelSpace α]
[MeasureTheory.IsFiniteMeasure μ]
(h_indep : CondIndepFun (MeasurableSpace.comap X inferInstance) ⋯ Y Z μ)
(hZ_meas : Measurable Z')
:
CondIndepFun (MeasurableSpace.comap X inferInstance) ⋯ Y Z' μ