OAI/NumberTheory/Catalan/Estimates/RealCoordinateProduct.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.realCoordinateMeasure line 12
  2. theorem OAI.InternalCatalan.realCoordinateWeight_nonneg line 16
  3. theorem OAI.InternalCatalan.measurable_realCoordinateDensity line 20
  4. theorem OAI.InternalCatalan.integrable_realCoordinateMeasure_iff line 24
  5. theorem OAI.InternalCatalan.integral_realCoordinateMeasure line 33
  6. theorem OAI.InternalCatalan.realCoordinateMeasure_univ line 41
  7. instance OAI.InternalCatalan.(instance at line 56) line 56
  8. theorem OAI.InternalCatalan.integral_realPlace_eq_coordinate line 59
  9. theorem OAI.InternalCatalan.integrable_realPlace_eq_coordinate_iff line 64
  10. theorem OAI.InternalCatalan.map_realCoordinateInv line 70
  11. theorem OAI.InternalCatalan.measurePreserving_realCoordinateInv line 87
  12. theorem OAI.InternalCatalan.ae_realPlace_ne_zero line 91
  13. theorem OAI.InternalCatalan.ae_realPlace_list_ne_zero line 98
  14. theorem OAI.InternalCatalan.ae_realPlace_list_mem_ne_zero line 106
  15. theorem OAI.InternalCatalan.ae_realCoordinate_mem line 114
  16. theorem OAI.InternalCatalan.ae_realCoordinate_ne_zero line 121
  17. theorem OAI.InternalCatalan.ae_realCoordinate_list_regular line 128
  18. def OAI.InternalCatalan.realCoordinateListPairMeasure line 138
  19. theorem OAI.InternalCatalan.measurePreserving_realCoordinate_list line 143
  20. theorem OAI.InternalCatalan.measurePreserving_realCoordinate_pair line 149
  21. theorem OAI.InternalCatalan.integrable_coordinate_productRealIntegrand line 156
  22. theorem OAI.InternalCatalan.integral_coordinate_productRealIntegrand line 163
  23. theorem OAI.InternalCatalan.determinant_eq_coordinateProductIntegral line 180