Jensen's inequality for integrals

TheoremUpper bound for the integral of the logarithm of a probability density over a set#●ready to prove

Let \(\mu\) be a measure on a measurable space \(X\) and let \(f : X \to \mathbb{R}\) be integrable with respect to \(\mu\), with \(f(x) > 0\) for every \(x \in X\) and \(\int_X f\,d\mu = 1\). Then for every measurable set \(E \subseteq X\) with \(0 < \mu(E) < \infty\) such that \(\log f\) is integrable on \(E\),

\[ \int_E \log f\,d\mu \le \mu(E)\log\frac{1}{\mu(E)}. \]

The integrability of \(\log f\) on \(E\) is assumed so that the statement is real-valued: the positive part of \(\log f\) is integrable on \(E\) (since \((\log f)^{+}\le f\)), so if \(\log f\) is not integrable on \(E\) then \(\int_E(\log f)\,d\mu=-\infty\) and the inequality holds in \(\mathbb{R}\cup\{-\infty\}\).

public theorem_wanted setIntegral_log_le_measure_mul_log_inv_measure (f : X → ℝ)
    (hf_pos : ∀ x, 0 < f x)
    (hf_int : Integrable f μ)
    (hf_one : (∫ x, f x ∂μ) = 1)
    (E : Set X) (hE_meas : MeasurableSet E)
    (hE_pos : 0 < μ E)
    (hE_fin : μ E < ⊤)
    (hf_log_int : IntegrableOn (fun x => Real.log (f x)) E μ) :
    (∫ x in E, Real.log (f x) ∂μ) ≤ (μ E).toReal * Real.log (1 / (μ E).toReal)

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Measure and integration; Classical measure theory), problem ma_proofbench_l1_82.

TheoremTwo-sided bound for the integral of the square root of one plus a square#●ready to prove

Let \(\mu\) be a probability measure on a measurable space \(\Omega\) and let \(h : \Omega \to [0,\infty)\) be a measurable function with \(\int_\Omega h\,d\mu < \infty\). If \(A = \int_\Omega h\,d\mu\), then

\[ \sqrt{1+A^2}\le \int_\Omega \sqrt{1+h^2}\,d\mu \le 1+A. \]

public theorem_wanted sqrt_one_add_sq_integral_le_and_le_one_add
    {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
    (h : Ω → NNReal) (hmeas : Measurable h)
    (hA_finite : (∫⁻ x, h x ∂μ) ≠ ⊤) (A : ℝ) (hA : A = (∫⁻ x, h x ∂μ).toReal) :
    Real.sqrt (1 + A ^ 2) ≤ ∫ x, Real.sqrt (1 + (h x).toReal ^ 2) ∂μ ∧
      (∫ x, Real.sqrt (1 + (h x).toReal ^ 2) ∂μ) ≤ 1 + A

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Measure and integration; Classical measure theory), problem ma_proofbench_l1_66.

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.