Scalar bounds for the Gaussian Carleman estimate

These inequalities combine eq:carleman-I of the Escauriaza–Seregin–Šverák manuscript with the integrated gradient identity and the cross term in eq:carleman-E of the Escauriaza–Seregin–Šverák manuscript.

theorem CKN.gaussCarleman_coefficient_le {q t : ℝ} (hq : 0 ≤ q) (ht : 0 < t) : -t + q * t ^ 2 * (1 / t - 1 / 3) ≤ q * t

The coefficient left after adding the gradient and phase-gradient terms.

theorem CKN.gaussCarleman_absorb {E I P C : ℝ} (hI : 0 ≤ I) (hIP : I ≤ P) (hE : E ≤ 3 * I + |C|) (hC : C ^ 2 ≤ 6 * I * P) : E ≤ (3 + √6) * P

Cauchy–Schwarz and I ≤ P absorb the cross term with the constant √6.

theorem CKN.gaussCarleman_final_absorb {q J E I P : ℝ} (hJ : q * J = 3 * I) (hIP : I ≤ P) (hE : E ≤ (3 + √6) * P) : q * J + 2 * E ≤ (9 + 2 * √6) * P

The scalar estimate with the final unweighted coefficient.

theorem CKN.gaussCarleman_cross_pointwise {q t v L : ℝ} (hq : 1 ≤ q) (ht0 : 0 < t) (ht2 : t < 2) : |t ^ 2 * v * L| ≤ √6 / 2 * (q / 3 * t * v ^ 2 + t ^ 2 * L ^ 2)

A pointwise Young bound for the Gaussian cross term, with the same constant as the Cauchy–Schwarz estimate in eq:carleman-E (ESS).

theorem CKN.gaussCarleman_absorb_young {E I P C : ℝ} (hIP : I ≤ P) (hE : E ≤ 3 * I + |C|) (hC : |C| ≤ √6 / 2 * (I + P)) : E ≤ (3 + √6) * P

The integral Young bound and I ≤ P give the Gaussian energy constant.