OAI/NumberTheory/Catalan/Energy/RealSheetIntegral.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.chebyshevT_eval_sheet line 24
  2. theorem OAI.InternalCatalan.chebyshevU_eval_sheet line 38
  3. theorem OAI.InternalCatalan.inv_realCoordinateInv line 65
  4. theorem OAI.InternalCatalan.sqrt_div_realCoordinateInv line 72
  5. theorem OAI.InternalCatalan.rowP_realCoordinateInv line 81
  6. theorem OAI.InternalCatalan.rowD_realCoordinateInv line 93
  7. theorem OAI.InternalCatalan.sheet_natAbs_sum line 117
  8. theorem OAI.InternalCatalan.sheet_natAbs_difference line 131
  9. theorem OAI.InternalCatalan.rowP_realCoordinateInv_signed line 151
  10. theorem OAI.InternalCatalan.rowD_realCoordinateInv_signed line 158
  11. theorem OAI.InternalCatalan.realRowAmplitude_sheet line 171
  12. def OAI.InternalCatalan.realSheetDeterminant line 200
  13. theorem OAI.InternalCatalan.realRowAmplitude_det_eq_sheet line 209
  14. def OAI.InternalCatalan.realFirstSheetMixedMatrix line 246
  15. theorem OAI.InternalCatalan.realFirstSheet_far_monomial line 253
  16. theorem OAI.InternalCatalan.realFirstSheet_near_monomial line 267
  17. theorem OAI.InternalCatalan.realFirstSheet_entry_factor line 282
  18. theorem OAI.InternalCatalan.realSheetDeterminant_firstSheet_factor line 305
  19. theorem OAI.InternalCatalan.realFirstSheet_far_coefficient_abs_le line 329
  20. theorem OAI.InternalCatalan.realFirstSheet_factor_abs_le line 333
  21. theorem OAI.InternalCatalan.realFirstSheet_factor_abs_le_weight line 349
  22. theorem OAI.InternalCatalan.realSheetDeterminant_abs_le_firstSheet_mixed line 355
  23. theorem OAI.InternalCatalan.sqrt_one_add_inv_sq line 372
  24. theorem OAI.InternalCatalan.sheet_far_weight_eq line 379
  25. theorem OAI.InternalCatalan.sheet_near_weight_le line 389
  26. theorem OAI.InternalCatalan.sheet_choice_weight_le line 403
  27. def OAI.InternalCatalan.realSheetCoefficient line 418
  28. def OAI.InternalCatalan.realSheetNode line 421
  29. theorem OAI.InternalCatalan.det_column_sum_bool line 424
  30. theorem OAI.InternalCatalan.realSheetDeterminant_eq_sum line 434
  31. theorem OAI.InternalCatalan.realSheetCoefficient_abs_sum_le line 468
  32. theorem OAI.InternalCatalan.realSheetCoefficient_sum_abs_prod_le line 473
  33. theorem OAI.InternalCatalan.laurent_monomial_det_eq line 490
  34. theorem OAI.InternalCatalan.laurent_monomial_det_abs_le line 504
  35. theorem OAI.InternalCatalan.realSheetDeterminant_abs_le_of_monomial_bound line 520
  36. theorem OAI.InternalCatalan.realSheetDeterminant_abs_le_sqrt line 546
  37. theorem OAI.InternalCatalan.realSheetDeterminant_abs_le line 592
  38. def OAI.InternalCatalan.sheetRealIntegrand line 623
  39. theorem OAI.InternalCatalan.coordinate_productRealIntegrand_eq_sheet line 633
  40. theorem OAI.InternalCatalan.ae_coordinate_productRealIntegrand_eq_sheet line 641
  41. theorem OAI.InternalCatalan.integrable_sheetRealIntegrand line 654
  42. theorem OAI.InternalCatalan.determinant_eq_sheetRealIntegral line 660