theorem
MeasurableSpace.comap_prodMk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(X : α → β)
(Y : α → γ)
:
MeasurableSpace.comap (fun (ω : α) => (X ω, Y ω)) inferInstance = MeasurableSpace.comap X mβ ⊔ MeasurableSpace.comap Y mγ
theorem
map_trim_comap
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{f : α → β}
(hf : Measurable f)
:
theorem
ae_map_iff_ae_trim
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{f : α → β}
(hf : Measurable f)
{p : β → Prop}
(hp : MeasurableSet {x : β | p x})
:
theorem
Measurable.coe_nat_enat
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → ℕ}
(hf : Measurable f)
:
Measurable fun (a : α) => ↑(f a)
theorem
Measurable.toNat
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → ℕ∞}
(hf : Measurable f)
:
Measurable fun (a : α) => (f a).toNat
theorem
MeasureTheory.Measure.trim_eq_map
{α : Type u_1}
{m mα : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ mα}
:
theorem
MeasureTheory.Measure.comp_congr
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{μ : Measure α}
{mβ : MeasurableSpace β}
{κ η : ProbabilityTheory.Kernel α β}
(h : ∀ᵐ (a : α) ∂μ, κ a = η a)
:
theorem
MeasureTheory.Measure.copy_comp_map
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{μ : Measure α}
{mβ : MeasurableSpace β}
{X : α → β}
(hX : AEMeasurable X μ)
:
theorem
MeasureTheory.Measure.compProd_deterministic
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{μ : Measure α}
{mβ : MeasurableSpace β}
{X : α → β}
[SFinite μ]
(hX : Measurable X)
:
theorem
MeasureTheory.Measure.trim_comap_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{μ : Measure α}
{mβ : MeasurableSpace β}
{X : α → β}
(hX : Measurable X)
{s : Set β}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.Measure.ext_prod
{α : Type u_7}
{β : Type u_8}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ ν : Measure (α × β)}
[IsFiniteMeasure μ]
[IsFiniteMeasure ν]
(h : ∀ {s : Set α} {t : Set β}, MeasurableSet s → MeasurableSet t → μ (s ×ˢ t) = ν (s ×ˢ t))
:
theorem
MeasureTheory.Measure.ext_prod_iff
{α : Type u_7}
{β : Type u_8}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ ν : Measure (α × β)}
[IsFiniteMeasure μ]
[IsFiniteMeasure ν]
:
theorem
MeasureTheory.Measure.ext_prod₃
{α : Type u_7}
{β : Type u_8}
{γ : Type u_9}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μ ν : Measure (α × β × γ)}
[IsFiniteMeasure μ]
[IsFiniteMeasure ν]
(h :
∀ {s : Set α} {t : Set β} {u : Set γ},
MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u))
:
theorem
MeasureTheory.Measure.ext_prod₃_iff
{α : Type u_7}
{β : Type u_8}
{γ : Type u_9}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μ ν : Measure (α × β × γ)}
[IsFiniteMeasure μ]
[IsFiniteMeasure ν]
:
μ = ν ↔ ∀ {s : Set α} {t : Set β} {u : Set γ},
MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
theorem
MeasureTheory.Measure.ext_prod₃_iff'
{α : Type u_7}
{β : Type u_8}
{γ : Type u_9}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μ ν : Measure ((α × β) × γ)}
[IsFiniteMeasure μ]
[IsFiniteMeasure ν]
:
μ = ν ↔ ∀ {s : Set α} {t : Set β} {u : Set γ},
MeasurableSet s → MeasurableSet t → MeasurableSet u → μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
theorem
MeasureTheory.Measure.ext_prod₃'
{α : Type u_7}
{β : Type u_8}
{γ : Type u_9}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μ ν : Measure ((α × β) × γ)}
[IsFiniteMeasure μ]
[IsFiniteMeasure ν]
:
(∀ {s : Set α} {t : Set β} {u : Set γ},
MeasurableSet s → MeasurableSet t → MeasurableSet u → μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)) →
μ = ν
Alias of the reverse direction of MeasureTheory.Measure.ext_prod₃_iff'.
theorem
ProbabilityTheory.Kernel.prod_apply_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
{η : Kernel α γ}
[IsSFiniteKernel κ]
[IsSFiniteKernel η]
{s : Set β}
{t : Set γ}
{a : α}
:
theorem
ProbabilityTheory.Kernel.compProd_assoc
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{κ : Kernel α β}
{η : Kernel (α × β) γ}
{ξ : Kernel (α × β × γ) δ}
[IsSFiniteKernel κ]
[IsSFiniteKernel η]
[IsSFiniteKernel ξ]
:
(κ.compProd η).compProd ξ = (κ.compProd (η.compProd (ξ.comap ⇑MeasurableEquiv.prodAssoc ⋯))).map ⇑MeasurableEquiv.prodAssoc.symm
theorem
MeasureTheory.Measure.compProd_assoc
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel (α × β) γ}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
:
theorem
MeasureTheory.Measure.compProd_assoc'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel (α × β) γ}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
:
theorem
ProbabilityTheory.CondIndepFun.symm'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[StandardBorelSpace α]
{hm : m ≤ mα}
[MeasureTheory.IsFiniteMeasure μ]
{f : α → β}
{g : α → γ}
(hfg : CondIndepFun m hm f g μ)
:
CondIndepFun m hm g f μ
theorem
ProbabilityTheory.Kernel.indepFun_const_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{κ : Kernel α β}
[IsZeroOrMarkovKernel κ]
(c : δ)
(X : β → γ)
:
IndepFun (fun (x : β) => c) X κ μ
theorem
ProbabilityTheory.Kernel.indepFun_const_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{κ : Kernel α β}
[IsZeroOrMarkovKernel κ]
(X : β → γ)
(c : δ)
:
IndepFun X (fun (x : β) => c) κ μ
theorem
ProbabilityTheory.condIndepFun_const_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[StandardBorelSpace α]
{hm : m ≤ mα}
[MeasureTheory.IsFiniteMeasure μ]
(c : γ)
(X : α → β)
:
CondIndepFun m hm (fun (x : α) => c) X μ
theorem
ProbabilityTheory.condIndepFun_const_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[StandardBorelSpace α]
{hm : m ≤ mα}
[MeasureTheory.IsFiniteMeasure μ]
(X : α → β)
(c : γ)
:
CondIndepFun m hm X (fun (x : α) => c) μ
theorem
ProbabilityTheory.condIndepFun_of_measurable_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[StandardBorelSpace α]
{hm : m ≤ mα}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → γ}
(hX : Measurable X)
(hY : Measurable Y)
:
CondIndepFun m hm X Y μ
theorem
ProbabilityTheory.condIndepFun_of_measurable_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[StandardBorelSpace α]
{hm : m ≤ mα}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → γ}
(hX : Measurable X)
(hY : Measurable Y)
:
CondIndepFun m hm X Y μ
Pretty printer defined by notation3 command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Two functions are conditionally independent if the two measurable space structures they generate
are conditionally independent. For a function f with codomain having measurable space structure
m, the generated measurable space structure is m.comap f.
See ProbabilityTheory.condIndepFun_iff.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ProbabilityTheory.condIndepFun_self_left
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mδ : MeasurableSpace δ}
[StandardBorelSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Z : α → δ}
(hX : Measurable X)
(hZ : Measurable Z)
:
theorem
ProbabilityTheory.condIndepFun_self_right
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mδ : MeasurableSpace δ}
[StandardBorelSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Z : α → δ}
(hX : Measurable X)
(hZ : Measurable Z)
:
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 α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{ε : Type u_7}
{mε : MeasurableSpace ε}
[StandardBorelSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → γ}
{Z : α → δ}
{T : α → ε}
(hZ : Measurable Z)
(h : X ⟂ᵢ[Z, hZ; μ] fun (ω : α) => (Y ω, T ω))
:
theorem
ProbabilityTheory.CondIndepFun.of_prod_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{ε : Type u_7}
{mε : MeasurableSpace ε}
[StandardBorelSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → γ}
{Z : α → δ}
{T : α → ε}
(hZ : Measurable Z)
(h : (fun (ω : α) => (X ω, T ω)) ⟂ᵢ[Z, hZ; μ] Y)
:
theorem
ProbabilityTheory.CondIndepFun.prod_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
[StandardBorelSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → γ}
{Z : α → δ}
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
(h : X ⟂ᵢ[Z, hZ; μ] Y)
:
theorem
ProbabilityTheory.condDistrib_comp_map
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_5}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{X : α → β}
{Y : α → Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
:
theorem
ProbabilityTheory.condDistrib_congr
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_5}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{X : α → β}
{Y : α → Ω}
[MeasureTheory.IsFiniteMeasure μ]
{X' : α → β}
{Y' : α → Ω}
(hY : Y =ᵐ[μ] Y')
(hX : X =ᵐ[μ] X')
:
theorem
ProbabilityTheory.condDistrib_congr_right
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_5}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{X : α → β}
{Y : α → Ω}
[MeasureTheory.IsFiniteMeasure μ]
{X' : α → β}
(hX : X =ᵐ[μ] X')
:
theorem
ProbabilityTheory.condDistrib_congr_left
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_5}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{X : α → β}
{Y : α → Ω}
[MeasureTheory.IsFiniteMeasure μ]
{Y' : α → Ω}
(hY : Y =ᵐ[μ] Y')
:
theorem
ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd₀
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_5}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{X : α → β}
{Y : α → Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
(κ : Kernel β Ω)
[IsFiniteKernel κ]
(hκ : MeasureTheory.Measure.map (fun (x : α) => (X x, Y x)) μ = (MeasureTheory.Measure.map X μ).compProd κ)
:
theorem
ProbabilityTheory.condDistrib_ae_eq_iff_measure_eq_compProd₀
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_5}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{X : α → β}
{Y : α → Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
(κ : Kernel β Ω)
[IsFiniteKernel κ]
:
⇑(condDistrib Y X μ) =ᵐ[MeasureTheory.Measure.map X μ] ⇑κ ↔ MeasureTheory.Measure.map (fun (x : α) => (X x, Y x)) μ = (MeasureTheory.Measure.map X μ).compProd κ
theorem
ProbabilityTheory.condDistrib_comp'
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_5}
{Ω' : Type u_6}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSpace Ω']
[StandardBorelSpace Ω']
[Nonempty Ω']
{X : α → β}
{Y : α → Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
{f : Ω → Ω'}
(hf : Measurable f)
:
theorem
ProbabilityTheory.condDistrib_comp
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_5}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{X : α → β}
[MeasureTheory.IsFiniteMeasure μ]
(hX : AEMeasurable X μ)
{f : β → Ω}
(hf : Measurable f)
:
theorem
ProbabilityTheory.condDistrib_const
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_5}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{X : α → β}
[MeasureTheory.IsFiniteMeasure μ]
(hX : AEMeasurable X μ)
(c : Ω)
:
⇑(condDistrib (fun (x : α) => c) X μ) =ᵐ[MeasureTheory.Measure.map X μ] ⇑(Kernel.deterministic (fun (x : β) => c) ⋯)
theorem
ProbabilityTheory.condDistrib_fst_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{Ω : Type u_5}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{X : α → β}
{Y : α → Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
(ν : MeasureTheory.Measure γ)
[MeasureTheory.IsProbabilityMeasure ν]
:
⇑(condDistrib (fun (ω : α × γ) => Y ω.1) (fun (ω : α × γ) => X ω.1) (μ.prod ν)) =ᵐ[MeasureTheory.Measure.map X μ] ⇑(condDistrib Y X μ)
theorem
ProbabilityTheory.condDistrib_prod_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{Ω : Type u_5}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{X : α → β}
{Y : α → Ω}
{T : α → γ}
[MeasureTheory.IsFiniteMeasure μ]
[StandardBorelSpace β]
[Nonempty β]
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
(hT : AEMeasurable T μ)
:
⇑(condDistrib (fun (ω : α) => (X ω, Y ω)) T μ) =ᵐ[MeasureTheory.Measure.map T μ] ⇑((condDistrib X T μ).compProd (condDistrib Y (fun (ω : α) => (T ω, X ω)) μ))
theorem
ProbabilityTheory.fst_condDistrib_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{Ω : Type u_5}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{X : α → β}
{Y : α → Ω}
{T : α → γ}
[MeasureTheory.IsFiniteMeasure μ]
[StandardBorelSpace β]
[Nonempty β]
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
(hT : AEMeasurable T μ)
:
⇑(condDistrib (fun (ω : α) => (X ω, Y ω)) T μ).fst =ᵐ[MeasureTheory.Measure.map T μ] ⇑(condDistrib X T μ)
theorem
ProbabilityTheory.condDistrib_of_indepFun
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_5}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{X : α → β}
{Y : α → Ω}
[MeasureTheory.IsFiniteMeasure μ]
(h : IndepFun X Y μ)
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
:
⇑(condDistrib Y X μ) =ᵐ[MeasureTheory.Measure.map X μ] ⇑(Kernel.const β (MeasureTheory.Measure.map Y μ))
theorem
ProbabilityTheory.indepFun_iff_condDistrib_eq_const
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_5}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{X : α → β}
{Y : α → Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
:
IndepFun X Y μ ↔ ⇑(condDistrib Y X μ) =ᵐ[MeasureTheory.Measure.map X μ] ⇑(Kernel.const β (MeasureTheory.Measure.map Y μ))
theorem
ProbabilityTheory.Kernel.indepFun_iff_map_prod_eq_prod_map_map
{Ω' : Type u_7}
{α : Type u_8}
{β : Type u_9}
{γ : Type u_10}
{mΩ' : MeasurableSpace Ω'}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{X : α → β}
{T : α → γ}
{μ : MeasureTheory.Measure Ω'}
[MeasureTheory.IsFiniteMeasure μ]
{κ : Kernel Ω' α}
[IsFiniteKernel κ]
[StandardBorelSpace β]
[StandardBorelSpace γ]
(hf : Measurable X)
(hg : Measurable T)
:
theorem
ProbabilityTheory.Kernel.indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map
{Ω' : Type u_7}
{α : Type u_8}
{β : Type u_9}
{γ : Type u_10}
{mΩ' : MeasurableSpace Ω'}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{X : α → β}
{T : α → γ}
{μ : MeasureTheory.Measure Ω'}
[MeasureTheory.IsFiniteMeasure μ]
{κ : Kernel Ω' α}
[IsFiniteKernel κ]
[StandardBorelSpace β]
[StandardBorelSpace γ]
(hf : Measurable X)
(hg : Measurable T)
:
theorem
ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_map_map
{β : Type u_2}
{γ : Type u_3}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{α : Type u_7}
{m mα : MeasurableSpace α}
[StandardBorelSpace α]
{X : α → β}
{T : α → γ}
{hm : m ≤ mα}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[StandardBorelSpace β]
[StandardBorelSpace γ]
(hX : Measurable X)
(hT : Measurable T)
:
CondIndepFun m hm X T μ ↔ ⇑((condExpKernel μ m).map fun (ω : α) => (X ω, T ω)) =ᵐ[μ.trim hm] ⇑(((condExpKernel μ m).map X).prod ((condExpKernel μ m).map T))
theorem
ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_comp_trim
{β : Type u_2}
{γ : Type u_3}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{α : Type u_7}
{m mα : MeasurableSpace α}
[StandardBorelSpace α]
{X : α → β}
{T : α → γ}
{hm : m ≤ mα}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[StandardBorelSpace β]
[StandardBorelSpace γ]
(hX : Measurable X)
(hT : Measurable T)
:
CondIndepFun m hm X T μ ↔ MeasureTheory.Measure.map (fun (ω : α) => (ω, X ω, T ω)) μ = (μ.trim hm).bind ⇑(Kernel.id.prod (((condExpKernel μ m).map X).prod ((condExpKernel μ m).map T)))
theorem
ProbabilityTheory.condDistrib_apply_ae_eq_condExpKernel_map
{β : Type u_2}
{γ : Type u_3}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{α : Type u_7}
{mα : MeasurableSpace α}
[StandardBorelSpace α]
[StandardBorelSpace β]
[Nonempty β]
{X : α → β}
{T : α → γ}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
(hX : Measurable X)
(hT : Measurable T)
{s : Set β}
(hs : MeasurableSet s)
:
(fun (a : α) => ((condDistrib X T μ) (T a)) s) =ᵐ[μ] fun (a : α) =>
(((condExpKernel μ (MeasurableSpace.comap T inferInstance)).map X) a) s
theorem
ProbabilityTheory.condIndepFun_comap_iff_map_prod_eq_prod_condDistrib_prod_condDistrib
{β : Type u_2}
{γ : Type u_3}
{Ω' : Type u_6}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[MeasurableSpace Ω']
[StandardBorelSpace Ω']
{α : Type u_7}
{mα : MeasurableSpace α}
[StandardBorelSpace α]
{X : α → β}
{T : α → γ}
{Z : α → Ω'}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[StandardBorelSpace β]
[StandardBorelSpace γ]
[Nonempty β]
[Nonempty γ]
(hX : Measurable X)
(hT : Measurable T)
(hZ : Measurable Z)
:
(X ⟂ᵢ[Z, hZ; μ] T) ↔ MeasureTheory.Measure.map (fun (ω : α) => (Z ω, X ω, T ω)) μ = (MeasureTheory.Measure.map Z μ).bind ⇑(Kernel.id.prod ((condDistrib X Z μ).prod (condDistrib T Z μ)))
theorem
ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_5}
{Ω' : Type u_6}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSpace Ω']
[StandardBorelSpace Ω']
{X : α → β}
{Y : α → Ω}
{Z : α → Ω'}
[MeasureTheory.IsFiniteMeasure μ]
[StandardBorelSpace α]
[StandardBorelSpace β]
[Nonempty β]
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
:
(Y ⟂ᵢ[Z, hZ; μ] X) ↔ ⇑(condDistrib Y (fun (ω : α) => (X ω, Z ω)) μ) =ᵐ[MeasureTheory.Measure.map (fun (ω : α) => (X ω, Z ω)) μ] ⇑(Kernel.prodMkLeft β (condDistrib Y Z μ))
theorem
ProbabilityTheory.Measure.snd_compProd_prodMkLeft
{α : Type u_7}
{β : Type u_8}
{γ : Type u_9}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μ : MeasureTheory.Measure (α × β)}
[MeasureTheory.SFinite μ]
{κ : Kernel β γ}
[IsSFiniteKernel κ]
:
theorem
ProbabilityTheory.Measure.snd_prodAssoc_compProd_prodMkLeft
{α : Type u_7}
{β : Type u_8}
{γ : Type u_9}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μ : MeasureTheory.Measure (α × β)}
[MeasureTheory.SFinite μ]
{κ : Kernel β γ}
[IsSFiniteKernel κ]
:
(MeasureTheory.Measure.map (⇑MeasurableEquiv.prodAssoc) (μ.compProd (Kernel.prodMkLeft α κ))).snd = μ.snd.compProd κ
theorem
ProbabilityTheory.ProbabilityMeasure.ext_iff_coe
{α : Type u_7}
{mα : MeasurableSpace α}
{μ ν : MeasureTheory.ProbabilityMeasure α}
:
theorem
ProbabilityTheory.FiniteMeasure.ext_iff_coe
{α : Type u_7}
{mα : MeasurableSpace α}
{μ ν : MeasureTheory.FiniteMeasure α}
:
theorem
ProbabilityTheory.FiniteMeasure.le_iff_coe
{α : Type u_1}
{mα : MeasurableSpace α}
{μ ν : MeasureTheory.FiniteMeasure α}
:
noncomputable instance
ProbabilityTheory.instSubFiniteMeasure_leanBandits
{α : Type u_1}
{mα : MeasurableSpace α}
:
Equations
- ProbabilityTheory.instSubFiniteMeasure_leanBandits = { sub := fun (μ ν : MeasureTheory.FiniteMeasure α) => ⟨↑μ - ↑ν, ⋯⟩ }
theorem
ProbabilityTheory.FiniteMeasure.sub_def
{α : Type u_1}
{mα : MeasurableSpace α}
(μ ν : MeasureTheory.FiniteMeasure α)
:
@[simp]
theorem
ProbabilityTheory.FiniteMeasure.toMeasure_sub
{α : Type u_1}
{mα : MeasurableSpace α}
(μ ν : MeasureTheory.FiniteMeasure α)
:
instance
ProbabilityTheory.instCanonicallyOrderedAddFiniteMeasure_leanBandits
{α : Type u_1}
{mα : MeasurableSpace α}
:
instance
ProbabilityTheory.instOrderedSubFiniteMeasure_leanBandits
{α : Type u_1}
{mα : MeasurableSpace α}
:
theorem
ProbabilityTheory.Kernel.prodMkLeft_ae_eq_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
{κ η : Kernel α β}
[IsFiniteKernel κ]
[IsFiniteKernel η]
{μ : MeasureTheory.Measure (γ × α)}
:
theorem
ProbabilityTheory.condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkLeft
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_5}
{Ω' : Type u_6}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSpace Ω']
[StandardBorelSpace Ω']
{X : α → β}
{Y : α → Ω}
{Z : α → Ω'}
[MeasureTheory.IsFiniteMeasure μ]
[StandardBorelSpace α]
[StandardBorelSpace β]
[Nonempty β]
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
{η : Kernel Ω' Ω}
[IsMarkovKernel η]
(h :
⇑(condDistrib Y (fun (ω : α) => (X ω, Z ω)) μ) =ᵐ[MeasureTheory.Measure.map (fun (ω : α) => (X ω, Z ω)) μ] ⇑(Kernel.prodMkLeft β η))
:
theorem
ProbabilityTheory.ae_cond_of_forall_mem
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasurableSet s)
{p : α → Prop}
(h : ∀ x ∈ s, p x)
:
theorem
ProbabilityTheory.condDistrib_ae_eq_cond
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_5}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{X : α → β}
{Y : α → Ω}
[Countable β]
[MeasurableSingletonClass β]
[MeasureTheory.IsFiniteMeasure μ]
(hX : Measurable X)
(hY : Measurable Y)
:
⇑(condDistrib Y X μ) =ᵐ[MeasureTheory.Measure.map X μ] fun (b : β) => MeasureTheory.Measure.map Y μ[|X ⁻¹' {b}]
theorem
ProbabilityTheory.cond_of_indepFun
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{X : α → β}
{T : α → γ}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
(h : IndepFun X T μ)
(hX : Measurable X)
(hT : Measurable T)
{s : Set β}
(hs : MeasurableSet s)
(hμs : μ (X ⁻¹' s) ≠ 0)
:
theorem
ProbabilityTheory.cond_of_condIndepFun
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_5}
{Ω' : Type u_6}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSpace Ω']
[StandardBorelSpace Ω']
{X : α → β}
{Y : α → Ω}
{Z : α → Ω'}
[StandardBorelSpace α]
[StandardBorelSpace β]
[Nonempty β]
[Countable β]
[Countable Ω']
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
(hZ : Measurable Z)
(h : CondIndepFun (MeasurableSpace.comap Z inferInstance) ⋯ Y X μ)
(hX : Measurable X)
(hY : Measurable Y)
{b : β}
{ω : Ω'}
(hμ : μ (X ⁻¹' {b} ∩ Z ⁻¹' {ω}) ≠ 0)
: