Burkholder majorant for p > 2

Constructs and verifies the Burkholder majorant in the regime p > 2, including the explicit derivatives, concavity, and tangent estimates.

Burkholder majorant candidate

This file builds and studies the piecewise candidate uCandidate.

The proof architecture is organized as follows.

1. Definitions. We define the Burkholder parameters, the two local formulas uA1 and vGeTwo, their first partial derivatives, the first quadrant auxiliary function auxFunction1, and finally the four-quadrant function uCandidate.
2. Continuity and boundary compatibility. We prove that the local formulas, their first partials, and the glued functions agree continuously across the sector boundaries.
3. Differentiability and local concavity. Inside each smooth sector we identify first derivatives and prove the relevant second derivatives are non-positive.
4. Tangent inequalities. Local concavity gives tangent inequalities on single sectors. The remaining work is geometric: split horizontal/vertical segments at sector boundaries and glue the local tangent estimates while comparing derivatives at the break points.

Most of the long private lemmas near the end are not new analytic facts; they are bookkeeping private lemmas that move a segment through the sector decomposition of uCandidate.

1. Basic parameters and local formulas

2. Continuity of the local first partials

3. Quadrants and the global candidate

4. Boundary compatibility and continuity of the glued functions

5. Abstract tangent and gluing private lemmas

6. Coordinate-axis tangent inequality under concavity hypotheses

7. Local differentiability and concavity inside smooth sectors

8. First-quadrant geometry and auxFunction1 tangent estimates

9. Boundary-to-boundary tangent estimates for uCandidate

Swap symmetry for the vertical axis case

Polynomial growth of the candidate

Polynomial growth of the first partials

10. Other quadrant wrappers and pointwise differentiability

11. Pointwise majorization

12. uCandidate(p,x,y) <0 If xy=0 e (x,y) ≠ (0,0)

13. Majorant existence statement

theorem Majorants.exists_majorant_geTwo (p : ℝ) (hp : 2 < p) : ∃ (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 : ℝ), x * y = 0 ∧ (x, y) ≠ (0, 0) → u x y < 0

Existence of a Burkholder majorant in the regime p > 2.

Informally, this theorem says the candidate built in this file really has all the properties we need: continuity, derivative growth bounds, the tangent-step inequality for mixed-sign increments, domination of v, and strict negativity on the nontrivial axis points.

So this is the "package everything together" result for the high-exponent case.