OAI/Analysis/FourierExtension/RadialMeasure.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Radial pushforward estimates for convex phases.

  1. abbrev OAI.DiagonalExtension.ConvexRadial.E2 line 25
  2. def OAI.DiagonalExtension.ConvexRadial.symPhase line 27
  3. def OAI.DiagonalExtension.ConvexRadial.symPhaseDeriv line 30
  4. lemma OAI.DiagonalExtension.ConvexRadial.hasDerivAt_line line 33
  5. lemma OAI.DiagonalExtension.ConvexRadial.hasDerivAt_line_sub line 38
  6. lemma OAI.DiagonalExtension.ConvexRadial.hasDerivAt_symPhase line 43
  7. lemma OAI.DiagonalExtension.ConvexRadial.hasDerivAt_directional line 51
  8. lemma OAI.DiagonalExtension.ConvexRadial.radial_deriv_lower line 64
  9. lemma OAI.DiagonalExtension.ConvexRadial.symPhase_continuous line 81
  10. lemma OAI.DiagonalExtension.ConvexRadial.symPhase_strictMonoOn line 85
  11. lemma OAI.DiagonalExtension.ConvexRadial.radial_lintegral_le line 98
  12. def OAI.DiagonalExtension.ConvexRadial.pairEquiv line 133
  13. lemma OAI.DiagonalExtension.ConvexRadial.pairEquiv_measurePreserving line 136
  14. lemma OAI.DiagonalExtension.ConvexRadial.pairEquiv_apply line 140
  15. lemma OAI.DiagonalExtension.ConvexRadial.pairEquiv_continuous line 142
  16. def OAI.DiagonalExtension.ConvexRadial.direction line 146
  17. lemma OAI.DiagonalExtension.ConvexRadial.direction_norm line 148
  18. lemma OAI.DiagonalExtension.ConvexRadial.pairEquiv_polar line 155
  19. lemma OAI.DiagonalExtension.ConvexRadial.polar_lintegral_le line 159
  20. lemma OAI.DiagonalExtension.ConvexRadial.pair_graph_lintegral_le line 204
  21. def OAI.DiagonalExtension.ConvexRadial.pairGraph line 265
  22. lemma OAI.DiagonalExtension.ConvexRadial.pairGraph_continuous line 268
  23. lemma OAI.DiagonalExtension.ConvexRadial.pairGraph_map_le line 272