OAI/Analysis/FourierExtension/GraphBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Convex graph and affine Fourier bounds.

  1. abbrev OAI.DiagonalExtension.ConvexRadial.GraphSpace line 29
  2. def OAI.DiagonalExtension.ConvexRadial.graphEmbedding line 31
  3. lemma OAI.DiagonalExtension.ConvexRadial.graphEmbedding_continuous line 34
  4. lemma OAI.DiagonalExtension.ConvexRadial.graphEmbedding_pairMap line 38
  5. lemma OAI.DiagonalExtension.ConvexRadial.graphEmbedding_pairMap_le line 43
  6. theorem OAI.DiagonalExtension.ConvexRadial.convex_graph_L4 line 56
  7. def OAI.DiagonalExtension.AffineGraph.haarFactor line 74
  8. lemma OAI.DiagonalExtension.AffineGraph.map_affine line 77
  9. lemma OAI.DiagonalExtension.AffineGraph.pairMap_le line 90
  10. theorem OAI.DiagonalExtension.AffineGraph.L4 line 108