class ProbabilityTheory.Kernel.IsCondExp {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} (π : Kernel X X) (μ : MeasureTheory.Measure X) : Prop

• condExp_ae_eq_kernel_apply ⦃A : Set X⦄ : MeasurableSet A → μ[A.indicator 1 | 𝓑] =ᵐ[μ] fun (a : X) => ((π a) A).toReal

theorem ProbabilityTheory.Kernel.isCondExp_iff {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} (π : Kernel X X) (μ : MeasureTheory.Measure X) : π.IsCondExp μ ↔ ∀ ⦃A : Set X⦄, MeasurableSet A → μ[A.indicator 1 | 𝓑] =ᵐ[μ] fun (a : X) => ((π a) A).toReal

theorem ProbabilityTheory.Kernel.isCondExp_iff_bind_eq_left {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : Kernel X X} {μ : MeasureTheory.Measure X} (hπ : π.IsProper) (h𝓑𝓧 : 𝓑 ≤ 𝓧) [MeasureTheory.IsFiniteMeasure μ] : π.IsCondExp μ ↔ μ.bind ⇑π = μ

theorem ProbabilityTheory.Kernel.condExp_ae_eq_kernel_apply {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : Kernel X X} {μ : MeasureTheory.Measure X} (h : ∀ (f : X → ℝ), Bornology.IsBounded (Set.range f) → Measurable f → μ[f | 𝓑] =ᵐ[μ] fun (x₀ : X) => ∫ (x : X), f x ∂π x₀) {A : Set X} (A_mble : MeasurableSet A) : μ[A.indicator fun (x : X) => 1 | 𝓑] =ᵐ[μ] fun (x : X) => ((π x) A).toReal

theorem ProbabilityTheory.Kernel.condExp_ae_eq_integral {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : Kernel X X} {μ : MeasureTheory.Measure X} [π.IsCondExp μ] (hπ : π.IsProper) (h𝓑𝓧 : 𝓑 ≤ 𝓧) (f : X → ℝ) [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Integrable f μ) : μ[f | 𝓑] =ᵐ[μ] fun (x₀ : X) => ∫ (x : X), f x ∂π x₀