OAI/NumberTheory/Catalan/Analysis/RealPairedIntegral.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.realPlaceMeasure line 17
  2. theorem OAI.InternalCatalan.realPlaceWeight_nonneg line 21
  3. theorem OAI.InternalCatalan.measurable_realPlaceDensity line 25
  4. theorem OAI.InternalCatalan.integrable_realPlaceMeasure_iff line 29
  5. theorem OAI.InternalCatalan.integral_realPlaceMeasure line 38
  6. theorem OAI.InternalCatalan.realPlaceMeasure_univ line 46
  7. instance OAI.InternalCatalan.(instance at line 63) line 63
  8. theorem OAI.InternalCatalan.integrable_realPlaceMeasure_prod_iff line 66
  9. theorem OAI.InternalCatalan.integral_realPlaceMeasure_prod line 80
  10. theorem OAI.InternalCatalan.realCoordinateInv_deriv_nonneg line 98
  11. theorem OAI.InternalCatalan.realCoordinate_weighted_comp line 105
  12. theorem OAI.InternalCatalan.integral_realPlaceMeasure_coordinate line 115
  13. theorem OAI.InternalCatalan.integrable_realPlaceMeasure_coordinate_iff line 148
  14. theorem OAI.InternalCatalan.restrict_mixed_rectangle_positive line 193
  15. theorem OAI.InternalCatalan.integrable_positive_zetaPolynomial line 211
  16. theorem OAI.InternalCatalan.integral_positive_zetaPolynomial line 227
  17. theorem OAI.InternalCatalan.integrable_realRowAmplitude line 242
  18. theorem OAI.InternalCatalan.integral_prod_realRowAmplitude line 254
  19. theorem OAI.InternalCatalan.determinantEntry_eq_realRow_integral line 279
  20. theorem OAI.InternalCatalan.integrable_realPlaceRow line 294
  21. theorem OAI.InternalCatalan.determinantEntry_eq_realPlace_product line 301
  22. theorem OAI.InternalCatalan.determinantEntry_eq_realPlace_integral line 310
  23. theorem OAI.InternalCatalan.integrable_pairedDeterminant line 326
  24. theorem OAI.InternalCatalan.determinant_eq_paired_integral line 340
  25. theorem OAI.InternalCatalan.pairedDeterminant_factor line 384
  26. theorem OAI.InternalCatalan.determinant_eq_paired_factored_integral line 402