OAI/NumberTheory/Catalan/Analysis/RealFactoredIntegral.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.realListPairMeasure line 13
  2. theorem OAI.InternalCatalan.list_permute_left_preserving line 18
  3. theorem OAI.InternalCatalan.list_permute_right_preserving line 27
  4. theorem OAI.InternalCatalan.integral_list_permute_left line 36
  5. theorem OAI.InternalCatalan.integral_list_permute_right line 42
  6. theorem OAI.InternalCatalan.integrable_list_permute_left line 48
  7. theorem OAI.InternalCatalan.integrable_list_permute_right line 54
  8. theorem OAI.InternalCatalan.integrable_rawRealIntegrand line 60
  9. theorem OAI.InternalCatalan.determinant_eq_rawRealIntegrand line 70
  10. theorem OAI.InternalCatalan.integrable_leftRealIntegrand line 78
  11. theorem OAI.InternalCatalan.integral_leftRealIntegrand line 87
  12. theorem OAI.InternalCatalan.integrable_doubleRealIntegrand line 106
  13. theorem OAI.InternalCatalan.integral_doubleRealIntegrand line 115
  14. theorem OAI.InternalCatalan.determinant_eq_doubleRealIntegral line 135
  15. theorem OAI.InternalCatalan.ae_realPlace_mem line 154
  16. theorem OAI.InternalCatalan.ae_realPlace_list_mem line 160
  17. theorem OAI.InternalCatalan.ae_unit_list_mem line 165
  18. theorem OAI.InternalCatalan.ae_realList_rectangle line 171
  19. def OAI.InternalCatalan.productRealIntegrand line 183
  20. theorem OAI.InternalCatalan.doubleRealIntegrand_ae_eq_products line 190
  21. theorem OAI.InternalCatalan.integrable_productRealIntegrand line 197
  22. theorem OAI.InternalCatalan.determinant_eq_productRealIntegral line 201