Burkholder majorants: existence of the special function

Assembles the regime-by-regime constructions into the existence of a Burkholder majorant for every exponent p > 1.

theorem Majorants.exists_majorant_p_g_1 (p : ℝ) (hp : p > 1) : ∃ (u : ℝ → ℝ → ℝ) (du_dx : ℝ → ℝ → ℝ) (du_dy : ℝ → ℝ → ℝ) (C : ℝ), 0 ≤ C ∧ ContinuousOn (fun (z : ℝ × ℝ) => u z.1 z.2) Set.univ ∧ ContinuousOn (fun (z : ℝ × ℝ) => du_dx z.1 z.2) Set.univ ∧ ContinuousOn (fun (z : ℝ × ℝ) => du_dy z.1 z.2) Set.univ ∧ (∀ (x y : ℝ), |u x y| ≤ C * (|x|.rpow p + |y|.rpow p)) ∧ (∀ (x y : ℝ), |du_dx x y| ≤ C * (|x|.rpow (p - 1) + |y|.rpow (p - 1))) ∧ (∀ (x y : ℝ), |du_dy x y| ≤ C * (|x|.rpow (p - 1) + |y|.rpow (p - 1))) ∧ (∀ (x y h k : ℝ), h * k ≤ 0 → u (x + h) (y + k) ≤ u x y + du_dx x y * h + du_dy x y * k) ∧ (∀ (x y : ℝ), v p x y ≤ u x y) ∧ (∀ (x y : ℝ), x * y ≤ 0 → u x y ≤ 0) ∧ ∀ (x y : ℝ), p ≠ 2 ∧ x * y = 0 ∧ (x, y) ≠ (0, 0) → u x y < 0

Main existence theorem for the Burkholder majorant when p > 1.

In plain terms: this says we can build a function u (with first derivatives) that has controlled growth, satisfies the tangent-step inequality used in the martingale argument, dominates the base Burkholder function v, and is nonpositive on the opposite-sign region x * y ≤ 0.

The proof dispatches to the specialized constructions in the three regimes p = 2, p > 2, and 1 < p < 2.