OAI/Analysis/FourierExtension/LpEstimate.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Diagonal estimates above four and the remaining low-exponent condition.

  1. lemma OAI.DiagonalExtension.memLp_above_four_of_bounded line 29
  2. theorem OAI.DiagonalExtension.IsSurface.diagonal_extension_of_four_le line 52
  3. theorem OAI.DiagonalExtension.mainStatement_iff_low_exponent_memLp line 94