LeanPool.RlTheoryInLean.MeasureTheory.Function.ConditionalExpectation.Basic

theorem MeasureTheory.ContinuousLinearMap.condExp_comp {Ω : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [NormedAddCommGroup α] [NormedSpace ℝ α] [CompleteSpace α] [BorelSpace α] [NormedAddCommGroup β] [NormedSpace ℝ β] [CompleteSpace β] [MeasurableSpace β] [SecondCountableTopology β] [BorelSpace β] {m m₀ : MeasurableSpace Ω} {μ : Measure Ω} (hm : m ≤ m₀) [SigmaFinite (μ.trim hm)] {f : Ω → α} (hf : Integrable f μ) (L : α →L[ℝ] β) : μ[⇑L ∘ f | m] =ᵐ[μ] ⇑L ∘ μ[f | m]

theorem MeasureTheory.condExp_inner {Ω : Type u_1} {m m₀ : MeasurableSpace Ω} {μ : Measure Ω} {d : ℕ} {f g : Ω → EuclideanSpace ℝ (Fin d)} (hm : m ≤ m₀) [SigmaFinite (μ.trim hm)] (hgInt : Integrable g μ) (hfgInt : ∀ (i : Fin d), Integrable ((fun (ω : Ω) => (f ω).ofLp i) * fun (ω : Ω) => (g ω).ofLp i) μ) (hf : ∀ (i : Fin d), AEStronglyMeasurable (fun (ω : Ω) => (f ω).ofLp i) μ) : μ[fun (ω : Ω) => inner ℝ (f ω) (g ω) | m] =ᵐ[μ] fun (ω : Ω) => inner ℝ (f ω) (μ[g | m] ω)

theorem MeasureTheory.norm_condExp_le_condExp_norm {Ω : Type u_1} {m m₀ : MeasurableSpace Ω} [StandardBorelSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {d : ℕ} {f : Ω → EuclideanSpace ℝ (Fin d)} (hf_i : Integrable f μ) (_hf_m : Measurable f) (_hf_bdd : ∃ (C : ℝ), ∀ (ω : Ω), ‖f ω‖ ≤ C) (hm : m ≤ m₀) : (fun (ω : Ω) => ‖μ[f | m] ω‖) ≤ᵐ[μ] fun (ω : Ω) => μ[fun (ω : Ω) => ‖f ω‖ | m] ω