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.trim_comap_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{μ : Measure α}
{mβ : MeasurableSpace β}
{X : α → β}
(hX : Measurable X)
{s : Set β}
(hs : MeasurableSet s)
:
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.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 : 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 α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{ε : 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.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 : CondIndepFun (MeasurableSpace.comap Z inferInstance) ⋯ X Y μ)
:
CondIndepFun (MeasurableSpace.comap Z inferInstance) ⋯ X (fun (ω : α) => (Y ω, Z ω)) μ
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 μ)
:
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 μ)
:
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 μ)
:
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 μ ↔ ⇑𝓛[Y | X; μ] =ᵐ[MeasureTheory.Measure.map X μ] ⇑(Kernel.const β (MeasureTheory.Measure.map Y μ))
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_compProd_prodMkRight
{α : 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.Measure.todo
{α : Type u_7}
{β : Type u_8}
{γ : Type u_9}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μ : MeasureTheory.Measure (α × β)}
[MeasureTheory.SFinite μ]
{κ : Kernel α γ}
[IsSFiniteKernel κ]
:
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.Kernel.prodMkRight_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_prodMkRight
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_5}
{Ω' : Type u_6}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[mΩ' : MeasurableSpace Ω']
{X : α → β}
{Y : α → Ω}
{Z : α → Ω'}
[MeasureTheory.IsFiniteMeasure μ]
[StandardBorelSpace α]
[StandardBorelSpace β]
[Nonempty β]
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
{η : Kernel Ω' Ω}
[IsMarkovKernel η]
(h :
⇑𝓛[Y | fun (ω : α) => (Z ω, X ω); μ] =ᵐ[MeasureTheory.Measure.map (fun (ω : α) => (Z ω, X ω)) μ] ⇑(Kernel.prodMkRight β η))
:
CondIndepFun (MeasurableSpace.comap Z inferInstance) ⋯ Y X μ
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 Ω]
[mΩ' : MeasurableSpace Ω']
{X : α → β}
{Y : α → Ω}
{Z : α → Ω'}
[MeasureTheory.IsFiniteMeasure μ]
[StandardBorelSpace α]
[StandardBorelSpace β]
[Nonempty β]
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
{η : Kernel Ω' Ω}
[IsMarkovKernel η]
(h :
⇑𝓛[Y | fun (ω : α) => (X ω, Z ω); μ] =ᵐ[MeasureTheory.Measure.map (fun (ω : α) => (X ω, Z ω)) μ] ⇑(Kernel.prodMkLeft β η))
:
CondIndepFun (MeasurableSpace.comap Z inferInstance) ⋯ Y X μ
Law of Y conditioned on X.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ProbabilityTheory.condIndepFun_fst_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{Ω : Type u_5}
{Ω' : Type u_6}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[mΩ' : MeasurableSpace Ω']
{X : α → β}
{Y : α → Ω}
{Z : α → Ω'}
[MeasureTheory.IsFiniteMeasure μ]
[StandardBorelSpace α]
[StandardBorelSpace β]
[Nonempty β]
[StandardBorelSpace γ]
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
(ν : MeasureTheory.Measure γ)
[MeasureTheory.IsProbabilityMeasure ν]
(h_indep : CondIndepFun (MeasurableSpace.comap Z mΩ') ⋯ Y X μ)
:
CondIndepFun (MeasurableSpace.comap (fun (ω : α × γ) => Z ω.1) mΩ') ⋯ (fun (ω : α × γ) => Y ω.1)
(fun (ω : α × γ) => X ω.1) (μ.prod ν)
theorem
ProbabilityTheory.indepFun_fst_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{Ω : Type u_5}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[MeasurableSpace Ω]
{X : α → β}
{Y : α → Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
(h_indep : IndepFun X Y μ)
(ν : MeasureTheory.Measure γ)
[MeasureTheory.IsProbabilityMeasure ν]
:
theorem
ProbabilityTheory.indepFun_snd_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{Ω : Type u_5}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[MeasurableSpace Ω]
{X : α → β}
{Y : α → Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
(h_indep : IndepFun X Y μ)
(ν : MeasureTheory.Measure γ)
[MeasureTheory.IsProbabilityMeasure ν]
:
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)
:
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 Ω]
[mΩ' : 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μ : μ (Z ⁻¹' {ω} ∩ X ⁻¹' {b}) ≠ 0)
: