English
Let f be convex on [0, ∞) and continuous at 0, and let μ ≪ ν with ν a probability measure. Then f(μ(real universum)) ≤ ∫ f((μ rnDeriv ν)(x)).toReal dν(x).
Русский
Пусть f выпуклая на [0, ∞) и непрерывна в 0, и пусть μ совершенно непрерывна относительно ν, где ν — вероятностная мера. Тогда f(μ(совокупность)) ≤ ∫ f((dμ/dν)(x)) dν(x).
LaTeX
$$$f\left(\mu(\mathrm{univ})\right) \le \int x\, f\left(\frac{d\mu}{d\nu}(x)\right) \, d\nu(x).$$$
Lean4
/-- For a convex continuous function `f` on `[0, ∞)`, if `μ` is absolutely continuous
with respect to a probability measure `ν`, then
`f μ.real univ ≤ ∫ x, f (μ.rnDeriv ν x).toReal ∂ν`. -/
theorem le_integral_rnDeriv_of_ac [IsFiniteMeasure μ] [IsProbabilityMeasure ν] (hf_cvx : ConvexOn ℝ (Ici 0) f)
(hf_cont : ContinuousWithinAt f (Ici 0) 0) (hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν)
(hμν : μ ≪ ν) : f (μ.real univ) ≤ ∫ x, f (μ.rnDeriv ν x).toReal ∂ν :=
by
have hf_cont' : ContinuousOn f (Ici 0) := by
intro x hx
rcases eq_or_lt_of_le (α := ℝ) (hx : 0 ≤ x) with rfl | hx_pos
· exact hf_cont
· have h := hf_cvx.continuousOn_interior x
simp only [nonempty_Iio, interior_Ici', mem_Ioi] at h
rw [continuousWithinAt_iff_continuousAt (Ioi_mem_nhds hx_pos)] at h
exact (h hx_pos).continuousWithinAt
calc
f (μ.real univ) = f (∫ x, (μ.rnDeriv ν x).toReal ∂ν) := by rw [Measure.integral_toReal_rnDeriv hμν]
_ ≤ ∫ x, f (μ.rnDeriv ν x).toReal ∂ν :=
by
rw [← average_eq_integral, ← average_eq_integral]
exact ConvexOn.map_average_le hf_cvx hf_cont' isClosed_Ici (by simp) Measure.integrable_toReal_rnDeriv hf_int
