OAI/Geometry/PolarProducts/RegularizedMaximum.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothPositivePart.primitive line 32
  2. theorem OAI.SmoothPositivePart.hasDerivAt_primitive line 34
  3. theorem OAI.SmoothPositivePart.deriv_primitive line 41
  4. theorem OAI.SmoothPositivePart.primitive_smooth line 44
  5. theorem OAI.SmoothPositivePart.primitive_of_nonpos line 49
  6. theorem OAI.SmoothPositivePart.primitive_one_mem line 58
  7. theorem OAI.SmoothPositivePart.primitive_of_one_le line 72
  8. def OAI.SmoothPositivePart.shift line 87
  9. theorem OAI.SmoothPositivePart.shift_mem line 89
  10. def OAI.SmoothPositivePart.positivePart line 94
  11. theorem OAI.SmoothPositivePart.positivePart_smooth line 96
  12. theorem OAI.SmoothPositivePart.positivePart_zero line 99
  13. theorem OAI.SmoothPositivePart.positivePart_eq_self line 103
  14. theorem OAI.SmoothPositivePart.deriv_positivePart line 108
  15. theorem OAI.SmoothPositivePart.deriv_positivePart_mem line 113
  16. theorem OAI.SmoothPositivePart.second_deriv_positivePart_nonneg line 117
  17. def OAI.SmoothPositivePart.smoothMax line 123
  18. theorem OAI.SmoothPositivePart.smoothMax_left line 125
  19. theorem OAI.SmoothPositivePart.smoothMax_right line 129
  20. theorem OAI.ComplexPotential.IsPSHAt.smoothMax line 149
  21. theorem OAI.ComplexPotential.IsPSHAt.congr line 171
  22. def OAI.ComplexPotential.gluedPotential line 191
  23. theorem OAI.ComplexPotential.gluedPotential_outer line 196
  24. theorem OAI.ComplexPotential.gluedPotential_inner line 202
  25. theorem OAI.ComplexPotential.isPSHAt_gluedPotential line 211