Burkholder's function and the scalar Bellman estimates

For a real exponent p, Burkholder's function is Φ_p(x, y) = (x + y) ^ (p - 1) * ((p - 1) * x - y), evaluated at nonnegative arguments. For 2 ≤ p it satisfies the two scalar Bellman estimates behind Burkholder's proof that martingale difference sequences, and in particular the Haar system, are unconditional in Lᵖ:

• a majorization: ((p - 1) ^ (p - 1) / p ^ (p - 2)) * Φ_p(x, y) ≤ (p - 1) ^ p * x ^ p - y ^ p for x, y ≥ 0;
• a zigzag convexity: for real x, y and ε = ±1, the function t ↦ Φ_p(|x + t|, |y + ε t|) is convex, so that Φ_p(|x + a|, |y + ε a|) + Φ_p(|x - a|, |y - ε a|) ≥ 2 Φ_p(|x|, |y|).

Up to the factor -(p - 1) ^ (p - 1) / p ^ (p - 2), Φ_p(|x|, |y|) is the function U of Burkholder for the exponent p ≥ 2, and the two estimates are V ≤ U and the concavity of U along lines of slope ±1, where V(x, y) = |y| ^ p - (p - 1) ^ p |x| ^ p. Integrated over dyadic intervals, the midpoint inequality is the scalar input to the bound p - 1 for Haar sign transforms on Lᵖ([0, 1]).

Main definitions and statements

• TauCeti.burkholderPhi p x y: the function Φ_p(x, y).
• TauCeti.burkholderPhi_mul_mul: positive homogeneity of degree p.
• TauCeti.mul_burkholderPhi_le: the majorization estimate.
• TauCeti.convexOn_burkholderPhi_abs_add: convexity of t ↦ Φ_p(|x + t|, |y + ε t|).
• TauCeti.two_mul_burkholderPhi_abs_le: the midpoint inequality.

References

• D. L. Burkholder, Boundary value problems and sharp inequalities for martingale transforms, Ann. Probab. 12 (1984), 647–702.
• F. Albiac and N. J. Kalton, Topics in Banach Space Theory, 2nd ed., Graduate Texts in Mathematics 233, Springer, 2016, §6.1 (Lemmas 6.1.5 and 6.1.6).

noncomputable def TauCeti.burkholderPhi (p x y : ℝ) : ℝ

Burkholder's function Φ_p(x, y) = (x + y) ^ (p - 1) * ((p - 1) * x - y). It is intended for nonnegative arguments, typically x = |f| and y = |g| for a function f and a transform g of it.

theorem TauCeti.burkholderPhi_def (p x y : ℝ) : burkholderPhi p x y = (x + y) ^ (p - 1) * ((p - 1) * x - y)

The defining formula for Burkholder's function.

@[simp]

theorem TauCeti.burkholderPhi_zero_zero (p : ℝ) : burkholderPhi p 0 0 = 0

Burkholder's function vanishes at the origin, for every exponent p.

theorem TauCeti.burkholderPhi_mul_mul {p : ℝ} (hp : p ≠ 0) {c x y : ℝ} (hc : 0 ≤ c) (hxy : 0 ≤ x + y) : burkholderPhi p (c * x) (c * y) = c ^ p * burkholderPhi p x y

Burkholder's function is positively homogeneous of degree p: Φ_p(c x, c y) = c ^ p Φ_p(x, y) for c ≥ 0 and x + y ≥ 0.

The majorization estimate

theorem TauCeti.mul_burkholderPhi_le {p : ℝ} (hp : 2 ≤ p) {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : (p - 1) ^ (p - 1) / p ^ (p - 2) * burkholderPhi p x y ≤ (p - 1) ^ p * x ^ p - y ^ p

The scalar Bellman majorization estimate. For 2 ≤ p and x, y ≥ 0, ((p - 1) ^ (p - 1) / p ^ (p - 2)) Φ_p(x, y) ≤ (p - 1) ^ p x ^ p - y ^ p.

Convexity along the diagonal

theorem TauCeti.convexOn_burkholderPhi_abs_add {p : ℝ} (hp : 2 ≤ p) (x y : ℝ) {ε : ℝ} (hε : |ε| = 1) : ConvexOn ℝ Set.univ fun (t : ℝ) => burkholderPhi p |x + t| |y + ε * t|

Zigzag convexity of Burkholder's function. For 2 ≤ p, real x, y and ε with |ε| = 1, the function t ↦ Φ_p(|x + t|, |y + ε t|) is convex on ℝ.

theorem TauCeti.two_mul_burkholderPhi_abs_le {p : ℝ} (hp : 2 ≤ p) (x y a : ℝ) {ε : ℝ} (hε : |ε| = 1) : 2 * burkholderPhi p |x| |y| ≤ burkholderPhi p |x + a| |y + ε * a| + burkholderPhi p |x - a| |y - ε * a|

The scalar Bellman midpoint estimate. For 2 ≤ p, real x, y, a and ε with |ε| = 1, 2 Φ_p(|x|, |y|) ≤ Φ_p(|x + a|, |y + ε a|) + Φ_p(|x - a|, |y - ε a|).