Documentation

LeanPool.Burkholder.Majorants.MajorantPL2

Burkholder majorant for 1 < p < 2 #

Constructs and verifies the Burkholder majorant in the regime 1 < 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 vLeTwo, 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 #

  1. Majorant existence statement

Polynomial growth of the candidate and its first partials #

Continuity of the glued candidate and its first partials #

source
theorem Majorants.exists_majorant_leTwo (p : ℝ) (hp : 1 < p ∧ p < 2) :
∃ (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 1 < p < 2.

This theorem takes the low-exponent candidate and proves it satisfies the same full checklist as in the other regimes: continuity, quantitative growth bounds for u and its first derivatives, the tangent-step inequality, domination of v, and negativity on the opposite-sign region (with strict axis negativity away from the origin).