Burkholder majorant for p = 2

Constructs the Burkholder majorant in the special case p = 2.

theorem Majorants.exists_majorant_p_eq_2 (p : ℝ) (hp : 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 ↔ u x y = 0

Explicit majorant package in the special case p = 2.

At this exponent the construction becomes very concrete: we can take u(x,y) = x*y, with derivatives du_dx = y and du_dy = x. This theorem checks, one by one, that this choice satisfies the full list of majorant requirements (growth, tangency, domination of v, and sign behavior).