OAI/NumberTheory/Catalan/Energy/BarrierComplexOctantRange.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.barrierComplex_norm_sq line 20
  2. theorem OAI.InternalCatalan.barrierComplex_norm_sq_pos line 25
  3. theorem OAI.InternalCatalan.barrierComplexLog_re line 30
  4. theorem OAI.InternalCatalan.barrierComplexLog_weighted_re line 35
  5. theorem OAI.InternalCatalan.barrierComplexArg_of_re_pos line 40
  6. theorem OAI.InternalCatalan.barrierComplexArg_one_add_I line 46
  7. theorem OAI.InternalCatalan.barrierComplexArg_one_sub_I line 51
  8. theorem OAI.InternalCatalan.barrierComplexLog_conj line 62
  9. theorem OAI.InternalCatalan.barrierComplexLog_conj_weighted_re line 71
  10. theorem OAI.InternalCatalan.barrierComplexLog_conj_pair_re line 76
  11. theorem OAI.InternalCatalan.barrierComplexLog_conj_pair_re_le line 83
  12. theorem OAI.InternalCatalan.barrierComplexLog_linear_conj line 89
  13. theorem OAI.InternalCatalan.barrierComplexLog_quadratic_conj line 93
  14. def OAI.InternalCatalan.barrierOctantMultiplier line 100
  15. def OAI.InternalCatalan.barrierOctantRotate line 104
  16. theorem OAI.InternalCatalan.barrierOctant_clockwise line 107
  17. theorem OAI.InternalCatalan.barrierOctant_counterclockwise line 112
  18. theorem OAI.InternalCatalan.barrierOctantMultiplier_ne_zero line 117
  19. theorem OAI.InternalCatalan.arg_pow_angle_of_arg line 130
  20. theorem OAI.InternalCatalan.barrierOctantMultiplier_arg line 136
  21. theorem OAI.InternalCatalan.barrierComplexArg_octant line 155
  22. theorem OAI.InternalCatalan.barrierComplexArg_octant_of_eq line 186
  23. theorem OAI.InternalCatalan.barrierOctant_principal_range line 197
  24. theorem OAI.InternalCatalan.barrierComplexArg_octant_rational line 231