Burkholder majorants: basic definitions

Defines the conjugate exponent q, pStar, the Burkholder expression v, and the sector parameters used to build the majorant.

noncomputable def Majorants.q (p : ℝ) : ℝ

The conjugate exponent, with a harmless value at p = 1.

Equations

• Majorants.q p = if p = 1 then 0 else p / (p - 1)

noncomputable def Majorants.pStar (p : ℝ) : ℝ

pStar = max p q; in the main p ≥ 2 regime this is just p.

Equations

• Majorants.pStar p = max p (Majorants.q p)

noncomputable def Majorants.v (p x y : ℝ) : ℝ

The original Burkholder-type expression, written with pStar.

Equations

• Majorants.v p x y = |(x + y) / 2|.rpow p - |Majorants.pStar p - 1|.rpow p * |(x - y) / 2|.rpow p

noncomputable def Majorants.a (p : ℝ) : ℝ

The slope parameter separating the two smooth sectors in the first quadrant.

Equations

• Majorants.a p = 1 - 2 / Majorants.pStar p

noncomputable def Majorants.alpha (p : ℝ) : ℝ

Normalization constant for the affine-in-y sector formula.

Equations

• Majorants.alpha p = p * (Majorants.pStar p / (Majorants.pStar p - 1)).rpow (1 - p)