Jensen's inequality for the conditional expectation #
theorem
ConvexOn.apply_condexp_le
{α : Type u_1}
{m : MeasurableSpace α}
{mα : MeasurableSpace α}
{ν : MeasureTheory.Measure α}
{f : ℝ → ℝ}
(hm : m ≤ mα)
(hf : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
{g : α → ℝ}
(hg : Measurable g)
(hg_pos : 0 ≤ g)
(h_int1 : MeasureTheory.Integrable g ν)
(h_int2 : MeasureTheory.Integrable (fun (x : α) => f (g x)) ν)
:
(fun (x : α) => f (MeasureTheory.condexp m ν g x)) ≤ᵐ[ν.trim hm] MeasureTheory.condexp m ν fun (x : α) => f (g x)
A specialized version of Jensen's inequality for the conditional expectation.
theorem
ProbabilityTheory.f_condexp_rnDeriv_le
{α : Type u_1}
{m : MeasurableSpace α}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hm : m ≤ mα)
(hf : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
(h_int : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν)
:
(fun (x : α) => f (MeasureTheory.condexp m ν (fun (x : α) => (μ.rnDeriv ν x).toReal) x)) ≤ᵐ[ν.trim hm] MeasureTheory.condexp m ν fun (x : α) => f (μ.rnDeriv ν x).toReal