Burkholder majorants: basic definitions

Defines the conjugate exponent q, pStar, the Burkholder expression v, and the sector parameters used to build the majorant, and a shared reflection lemma for extending the candidate and its first partials to the plane.

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)

theorem Majorants.quarterPlaneExtension_reflection (f g : ℝ → ℝ → ℝ) (σ : ℝ → ℝ) (hσ : Function.Involutive σ) (x y : ℝ) (hy : y < 0) : have extension := fun (x y : ℝ) => if 0 ≤ x ∧ y ≤ x ∧ -x ≤ y then f x y else if x ≤ 0 ∧ y ≤ -x ∧ x ≤ y then σ (f (-x) (-y)) else if 0 ≤ y ∧ -y ≤ x ∧ x ≤ y then g y x else if y ≤ 0 ∧ y ≤ x ∧ x ≤ -y then σ (g (-y) (-x)) else 0; extension x y = σ (extension (-x) (-y))

Central reflection of a four-sector extension, with an involution on its values. This treats the candidate and its odd first partials with the same sector argument. The classical branch decisions match the opaque sector predicates used by the candidates.