Laws of stepsUntil and rewardByCount #
theorem
ProbabilityTheory.Kernel.IndepFun.of_prod_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{ε : Type u_7}
{Ω : Type u_8}
{mΩ : MeasurableSpace Ω}
{mε : MeasurableSpace ε}
{μ : MeasureTheory.Measure Ω}
{κ : Kernel Ω α}
{X : α → β}
{Y : α → γ}
{T : α → ε}
(h : IndepFun X (fun (ω : α) => (Y ω, T ω)) κ μ)
:
IndepFun X Y κ μ
theorem
ProbabilityTheory.Kernel.IndepFun.of_prod_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{ε : Type u_7}
{Ω : Type u_8}
{mΩ : MeasurableSpace Ω}
{mε : MeasurableSpace ε}
{μ : MeasureTheory.Measure Ω}
{κ : Kernel Ω α}
{X : α → β}
{Y : α → γ}
{T : α → ε}
(h : IndepFun (fun (ω : α) => (X ω, T ω)) Y κ μ)
:
IndepFun X Y κ μ
theorem
ProbabilityTheory.CondIndepFun.of_prod_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{μ : MeasureTheory.Measure α}
{ε : Type u_7}
{mε : MeasurableSpace ε}
[StandardBorelSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → γ}
{Z : α → δ}
{T : α → ε}
(hZ : Measurable Z)
(h : CondIndepFun (MeasurableSpace.comap Z inferInstance) ⋯ X (fun (ω : α) => (Y ω, T ω)) μ)
:
CondIndepFun (MeasurableSpace.comap Z inferInstance) ⋯ X Y μ
theorem
ProbabilityTheory.CondIndepFun.of_prod_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{μ : MeasureTheory.Measure α}
{ε : Type u_7}
{mε : MeasurableSpace ε}
[StandardBorelSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → γ}
{Z : α → δ}
{T : α → ε}
(hZ : Measurable Z)
(h : CondIndepFun (MeasurableSpace.comap Z inferInstance) ⋯ (fun (ω : α) => (X ω, T ω)) Y μ)
:
CondIndepFun (MeasurableSpace.comap Z inferInstance) ⋯ X Y μ
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' μ