OAI/Geometry/PolarProducts/TipEstimates.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SymmetricPolar.endpointKernel line 38
  2. lemma OAI.SymmetricPolar.endpointKernel_eq_rpow line 40
  3. lemma OAI.SymmetricPolar.intervalIntegrable_endpointKernel line 45
  4. lemma OAI.SymmetricPolar.beta_three_halves_one_half line 57
  5. lemma OAI.SymmetricPolar.integral_endpointKernel line 72
  6. lemma OAI.SymmetricPolar.endpointKernel_le_one line 96
  7. lemma OAI.SymmetricPolar.intervalIntegrable_dampedEndpointKernel line 101
  8. lemma OAI.SymmetricPolar.integral_dampedEndpointKernel_le line 105
  9. def OAI.SymmetricPolar.movingEndpointIntegral line 163
  10. lemma OAI.SymmetricPolar.movingEndpointIntegral_eq line 167
  11. lemma OAI.SymmetricPolar.movingEndpointIntegral_le line 191
  12. lemma OAI.SymmetricPolar.movingEndpointIntegral_le_linear line 209
  13. def OAI.PlanarLens.tailSlope line 234
  14. theorem OAI.PlanarLens.tailSlope_pos line 236
  15. theorem OAI.PlanarLens.T_rho_ge_abs line 240
  16. theorem OAI.PlanarLens.reciprocal_A_tail line 252
  17. theorem OAI.PlanarLens.integrable_radialError line 279
  18. theorem OAI.PlanarLens.integral_radialLeading line 293
  19. theorem OAI.PlanarLens.outer_integral_bound line 307