Prove2Me

(7.9) — quasi-subadditivity of Φ

Proved
BurkholderDFI.ConvexPhi.eq_7_9

by mikedeng1 · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

convexitymartingalesp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1

For a nondecreasing function Φ\Phi satisfying the moderate-growth bound Φ(2x)≤cΦ(x)\Phi(2x)\le c\Phi(x) and any x,y≥0x,y\ge0,

Φ(x+y)≤Φ(2x)+Φ(2y)≤c[Φ(x)+Φ(y)].\Phi(x+y)\le\Phi(2x)+\Phi(2y)\le c[\Phi(x)+\Phi(y)].

This is the sum estimate used in the convex-function comparison.

Formalization Note All arguments and values may be infinite; the same growth constant cc appears in the second inequality.

Preamble
import Mathlib
import Definitions.Def_BurkholderDFI_SquareFnLp_Martingale
Formal statement
namespace BurkholderDFI.ConvexPhi
open MeasureTheory ProbabilityTheory
open scoped ENNReal NNReal

/-- (7.9), p. 27: quasi-subadditivity from the growth condition. -/
theorem eq_7_9 (Φ : ℝ≥0∞ → ℝ≥0∞) (c : ℝ≥0) (hΦ : BurkholderDFI.SquareFnLp.IsPhi Φ c)
    (x y : ℝ≥0∞) :
    Φ (x + y) ≤ Φ (2 * x) + Φ (2 * y) ∧
    Φ (2 * x) + Φ (2 * y) ≤ c * (Φ x + Φ y) := by sorry
end BurkholderDFI.ConvexPhi
Source
Burkholder, Distribution Function Inequalities for Martingales, Ann. Probability 1 (1973), (7.9), p. 27
Human review

  • Endorsed by Shuze Chen · Oct 6, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 6, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph