OAI/Geometry/PolarProducts/HorizontalIntegrals.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothPaths.integralPath line 44
  2. theorem OAI.SmoothPaths.integralPath_apply line 47
  3. theorem OAI.SmoothPaths.contDiff_integralPath line 50
  4. theorem OAI.SmoothExtension.exists_global_near_closed line 66
  5. def OAI.PlanarLens.density line 93
  6. def OAI.PlanarLens.J line 95
  7. theorem OAI.PlanarLens.density_nonneg line 97
  8. theorem OAI.PlanarLens.contDiffOn_density line 100
  9. theorem OAI.PlanarLens.continuousOn_density line 112
  10. theorem OAI.PlanarLens.integrable_density line 115
  11. theorem OAI.PlanarLens.hasDerivAt_J line 122
  12. theorem OAI.PlanarLens.J_zero line 136
  13. theorem OAI.PlanarLens.J_nonneg line 138
  14. def OAI.PlanarLens.horizontalPath line 142
  15. theorem OAI.PlanarLens.horizontalPath_apply line 160
  16. theorem OAI.PlanarLens.J_affine line 163
  17. theorem OAI.PlanarLens.contDiffOn_J line 171
  18. def OAI.PlanarLens.rho line 218
  19. def OAI.PlanarLens.rhoD line 219
  20. theorem OAI.PlanarLens.rho_pos line 222
  21. theorem OAI.PlanarLens.hasDerivAt_rho line 229
  22. theorem OAI.PlanarLens.rhoD_pos line 241
  23. theorem OAI.PlanarLens.continuousOn_rho line 245
  24. theorem OAI.PlanarLens.density_radial line 251
  25. theorem OAI.PlanarLens.deriv_F_neg line 266
  26. theorem OAI.PlanarLens.deriv_F_conj line 274
  27. theorem OAI.PlanarLens.density_neg_conj line 284
  28. theorem OAI.PlanarLens.J_neg line 292