Fatou Bound for Convex Second Differences

This is the Fatou bound for the distributional second derivatives of a convex function.

Let $E$ be a finite-dimensional real inner-product space with its Borel measurable structure. Let $u:E\to\mathbb R$ be convex, let $\iota$ be a finite type, let $v_i\in E$ and $c_i\geq0$ for $i\in\iota$. Let $\chi:E\to\mathbb R$ be nonnegative, $C^2$, and compactly supported. Let $g:E\to\mathbb R$ be almost everywhere strongly measurable. Assume that, almost everywhere in $x$, for every $\varepsilon>0$ there is $\delta>0$ such that for $0<t<\delta$,

Then

This is an auxiliary distributional inequality used to integrate lower bounds for second differences against nonnegative test functions.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem integral_mul_le_integral_mul_sum_iteratedFDeriv [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {u : E → ℝ} (hconv : ConvexOn ℝ univ u) {ι : Type*} [Fintype ι] (v : ι → E) {c : ι → ℝ}
    (hc : ∀ i, 0 ≤ c i) {χ : E → ℝ} (hχ : ContDiff ℝ 2 χ) (hχc : HasCompactSupport χ)
    (hχ0 : ∀ x, 0 ≤ χ x) {g : E → ℝ} (hgm : AEStronglyMeasurable g (volume : Measure E))
    (hg : ∀ᵐ x ∂(volume : Measure E), ∀ ε > 0, ∃ δ > 0, ∀ t : ℝ, 0 < t → t < δ →
      g x - ε ≤ ∑ i, c i * ((u (x + t • v i) + u (x - t • v i) - 2 * u x) / t ^ 2)) :
    ∫ x, g x * χ x ≤ ∫ x, u x * ∑ i, c i * iteratedFDeriv ℝ 2 χ x (fun _ => v i)

Module navigation

Module: Analysis/Convex/SecondOrder.

Supporting theorems: tendsto_integral_secondDifference_mul.

Previous: tendsto_integral_secondDifference_mul · Next: ae_exists_secondOrder_expansion.

Source excerpt, lines 462–468 · Frozen source 408915f.