Documentation

LeanBandits.ForMathlib.CondDistrib

theorem ae_map_iff_ae_trim {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} {μ : MeasureTheory.Measure α} { : MeasurableSpace β} {f : αβ} (hf : Measurable f) {p : βProp} (hp : MeasurableSet {x : β | p x}) :
(∀ᵐ (y : β) MeasureTheory.Measure.map f μ, p y) ∀ᵐ (x : α) μ.trim , p (f x)
theorem Measurable.coe_nat_enat {α : Type u_1} { : MeasurableSpace α} {f : α} (hf : Measurable f) :
Measurable fun (a : α) => (f a)
theorem Measurable.toNat {α : Type u_1} { : MeasurableSpace α} {f : αℕ∞} (hf : Measurable f) :
Measurable fun (a : α) => (f a).toNat
theorem MeasureTheory.Measure.trim_eq_map {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {hm : m } :
μ.trim hm = map id μ
theorem MeasureTheory.Measure.trim_comap_apply {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} {μ : Measure α} { : MeasurableSpace β} {X : αβ} (hX : Measurable X) {s : Set β} (hs : MeasurableSet s) :
(μ.trim ) (X ⁻¹' s) = (map X μ) s
theorem ProbabilityTheory.CondIndepFun.symm' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} { : MeasurableSpace β} { : MeasurableSpace γ} [StandardBorelSpace α] {hm : 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} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} {ε : Type u_7} {Ω : Type u_8} { : MeasurableSpace Ω} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} {ε : Type u_7} {Ω : Type u_8} { : MeasurableSpace Ω} { : 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} { : MeasurableSpace α} {μ : MeasureTheory.Measure α} { : MeasurableSpace β} { : MeasurableSpace γ} { : MeasurableSpace δ} {ε : Type u_7} { : MeasurableSpace ε} [StandardBorelSpace α] [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αγ} {Z : αδ} {T : αε} (hZ : Measurable Z) (h : CondIndepFun (MeasurableSpace.comap Z inferInstance) X (fun (ω : α) => (Y ω, T ω)) μ) :
theorem ProbabilityTheory.CondIndepFun.of_prod_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} { : MeasurableSpace α} {μ : MeasureTheory.Measure α} { : MeasurableSpace β} { : MeasurableSpace γ} { : MeasurableSpace δ} {ε : Type u_7} { : MeasurableSpace ε} [StandardBorelSpace α] [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αγ} {Z : αδ} {T : αε} (hZ : Measurable Z) (h : CondIndepFun (MeasurableSpace.comap Z inferInstance) (fun (ω : α) => (X ω, T ω)) Y μ) :
theorem ProbabilityTheory.CondIndepFun.prod_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} { : MeasurableSpace α} {μ : MeasureTheory.Measure α} { : MeasurableSpace β} { : MeasurableSpace γ} { : 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} { : MeasurableSpace α} {μ : MeasureTheory.Measure α} { : MeasurableSpace β} { : MeasurableSpace γ} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {X : αβ} {Y : αΩ} {T : αγ} [MeasureTheory.IsFiniteMeasure μ] [StandardBorelSpace β] [Nonempty β] (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hT : AEMeasurable T μ) :
𝓛[fun (ω : α) => (X ω, Y ω) | T; μ] =ᵐ[MeasureTheory.Measure.map T μ] (𝓛[X | T; μ].compProd 𝓛[Y | fun (ω : α) => (T ω, X ω); μ])
theorem ProbabilityTheory.fst_condDistrib_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Ω : Type u_5} { : MeasurableSpace α} {μ : MeasureTheory.Measure α} { : MeasurableSpace β} { : MeasurableSpace γ} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {X : αβ} {Y : αΩ} {T : αγ} [MeasureTheory.IsFiniteMeasure μ] [StandardBorelSpace β] [Nonempty β] (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hT : AEMeasurable T μ) :
𝓛[fun (ω : α) => (X ω, Y ω) | T; μ].fst =ᵐ[MeasureTheory.Measure.map T μ] 𝓛[X | T; μ]
theorem ProbabilityTheory.condDistrib_of_indepFun {α : Type u_1} {β : Type u_2} {Ω : Type u_5} { : MeasurableSpace α} {μ : MeasureTheory.Measure α} { : 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} { : MeasurableSpace α} {μ : MeasureTheory.Measure α} { : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {X : αβ} {Y : αΩ} [MeasureTheory.IsFiniteMeasure μ] (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) :
theorem ProbabilityTheory.Measure.snd_compProd_prodMkLeft {α : Type u_7} {β : Type u_8} {γ : Type u_9} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} {μ : MeasureTheory.Measure (α × β)} [MeasureTheory.SFinite μ] {κ : Kernel β γ} [IsSFiniteKernel κ] :
(μ.compProd (Kernel.prodMkLeft α κ)).snd = μ.snd.bind κ
theorem ProbabilityTheory.Measure.snd_compProd_prodMkRight {α : Type u_7} {β : Type u_8} {γ : Type u_9} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} {μ : MeasureTheory.Measure (α × β)} [MeasureTheory.SFinite μ] {κ : Kernel α γ} [IsSFiniteKernel κ] :
(μ.compProd (Kernel.prodMkRight β κ)).snd = μ.fst.bind κ
theorem ProbabilityTheory.FiniteMeasure.ext_iff_coe {α : Type u_7} { : MeasurableSpace α} {μ ν : MeasureTheory.FiniteMeasure α} :
μ = ν μ = ν
theorem ProbabilityTheory.FiniteMeasure.sub_def {α : Type u_1} { : MeasurableSpace α} (μ ν : MeasureTheory.FiniteMeasure α) :
μ - ν = μ - ν,
@[simp]
theorem ProbabilityTheory.FiniteMeasure.toMeasure_sub {α : Type u_1} { : MeasurableSpace α} (μ ν : MeasureTheory.FiniteMeasure α) :
↑(μ - ν) = μ - ν
theorem ProbabilityTheory.Kernel.prodMkLeft_ae_eq_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} [MeasurableSpace.CountableOrCountablyGenerated α β] {κ η : Kernel α β} [IsFiniteKernel κ] [IsFiniteKernel η] {μ : MeasureTheory.Measure (γ × α)} :
(prodMkLeft γ κ) =ᵐ[μ] (prodMkLeft γ η) κ =ᵐ[μ.snd] η
theorem ProbabilityTheory.Kernel.prodMkRight_ae_eq_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} [MeasurableSpace.CountableOrCountablyGenerated α β] {κ η : Kernel α β} [IsFiniteKernel κ] [IsFiniteKernel η] {μ : MeasureTheory.Measure (α × γ)} :
(prodMkRight γ κ) =ᵐ[μ] (prodMkRight γ η) κ =ᵐ[μ.fst] η
theorem ProbabilityTheory.condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkRight {α : Type u_1} {β : Type u_2} {Ω : Type u_5} {Ω' : Type u_6} { : MeasurableSpace α} {μ : MeasureTheory.Measure α} { : 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 β η)) :
theorem ProbabilityTheory.condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkLeft {α : Type u_1} {β : Type u_2} {Ω : Type u_5} {Ω' : Type u_6} { : MeasurableSpace α} {μ : MeasureTheory.Measure α} { : 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 β η)) :

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} { : MeasurableSpace α} {μ : MeasureTheory.Measure α} { : MeasurableSpace β} { : 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} { : MeasurableSpace α} {μ : MeasureTheory.Measure α} { : MeasurableSpace β} { : MeasurableSpace γ} [MeasurableSpace Ω] {X : αβ} {Y : αΩ} [MeasureTheory.IsFiniteMeasure μ] (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (h_indep : IndepFun X Y μ) (ν : MeasureTheory.Measure γ) [MeasureTheory.IsProbabilityMeasure ν] :
    IndepFun (fun (ω : α × γ) => X ω.1) (fun (ω : α × γ) => Y ω.1) (μ.prod ν)
    theorem ProbabilityTheory.indepFun_snd_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Ω : Type u_5} { : MeasurableSpace α} {μ : MeasureTheory.Measure α} { : MeasurableSpace β} { : MeasurableSpace γ} [MeasurableSpace Ω] {X : αβ} {Y : αΩ} [MeasureTheory.IsFiniteMeasure μ] (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (h_indep : IndepFun X Y μ) (ν : MeasureTheory.Measure γ) [MeasureTheory.IsProbabilityMeasure ν] :
    IndepFun (fun (ω : γ × α) => X ω.2) (fun (ω : γ × α) => Y ω.2) (ν.prod μ)
    theorem ProbabilityTheory.condDistrib_ae_eq_cond {α : Type u_1} {β : Type u_2} {Ω : Type u_5} { : MeasurableSpace α} {μ : MeasureTheory.Measure α} { : 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} { : MeasurableSpace α} {μ : MeasureTheory.Measure α} { : MeasurableSpace β} { : 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} { : MeasurableSpace α} {μ : MeasureTheory.Measure α} { : 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 : β} {ω : Ω'} ( : μ (Z ⁻¹' {ω} X ⁻¹' {b}) 0) :