OAI/NumberTheory/Catalan/Energy/RealSheetIntegralBound.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.pair_product_eq_zero_of_not_injective line 12
  2. theorem OAI.InternalCatalan.sheetRealIntegrand_eq_zero_of_not_injective_x line 20
  3. theorem OAI.InternalCatalan.sheetRealIntegrand_eq_zero_of_not_injective_s line 32
  4. theorem OAI.InternalCatalan.ae_realCoordinate_pair_domain line 39
  5. theorem OAI.InternalCatalan.realCoordinateListPairMeasure_univ line 63
  6. theorem OAI.InternalCatalan.realCoordinateListPairMeasure_real_univ line 69
  7. theorem OAI.InternalCatalan.ae_abs_sheetRealIntegrand_le_of_regular_bound line 74
  8. theorem OAI.InternalCatalan.determinant_eq_sheetRealPairIntegral line 90
  9. theorem OAI.InternalCatalan.abs_determinant_le_of_sheetRealIntegrand_bound line 97
  10. theorem OAI.InternalCatalan.abs_determinant_le_of_majorantOne_bound line 123