OAI/NumberTheory/Catalan/Energy/RealTwoSheetIntegralBound.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.InternalCatalan.FirstSheetBoundaryL2 line 28
  2. def OAI.InternalCatalan.firstSheetBoundaryToLp line 30
  3. def OAI.InternalCatalan.firstSheetBoundaryVector line 33
  4. theorem OAI.InternalCatalan.firstSheetBoundary_inner line 37
  5. theorem OAI.InternalCatalan.firstSheetBoundary_inner_function line 42
  6. theorem OAI.InternalCatalan.firstSheetBoundary_norm_sq line 51
  7. theorem OAI.InternalCatalan.firstSheetBoundary_norm_sq_function line 61
  8. def OAI.InternalCatalan.firstSheetKernelVector line 68
  9. theorem OAI.InternalCatalan.firstSheetBoundary_inner_kernel line 72
  10. def OAI.InternalCatalan.firstSheetNumerator line 90
  11. def OAI.InternalCatalan.firstSheetDenominator line 93
  12. def OAI.InternalCatalan.firstSheetRational line 96
  13. def OAI.InternalCatalan.firstSheetReverse line 100
  14. def OAI.InternalCatalan.firstSheetBoundaryNormSq line 108
  15. theorem OAI.InternalCatalan.firstSheetReverse_involutive line 112
  16. theorem OAI.InternalCatalan.firstSheetDenominator_ne_zero line 118
  17. theorem OAI.InternalCatalan.firstSheetDenominator_conj line 124
  18. theorem OAI.InternalCatalan.firstSheetDenominator_norm_inv line 128
  19. theorem OAI.InternalCatalan.firstSheetNumerator_reverse line 133
  20. theorem OAI.InternalCatalan.firstSheetNumerator_reverse_norm line 155
  21. theorem OAI.InternalCatalan.firstSheetRational_reverse_norm line 161
  22. theorem OAI.InternalCatalan.firstSheetBoundaryNormSq_reverse line 168
  23. theorem OAI.InternalCatalan.firstSheetNumerator_analyticAt line 182
  24. theorem OAI.InternalCatalan.firstSheetDenominator_analyticAt line 189
  25. theorem OAI.InternalCatalan.firstSheetRational_analyticOnNhd_closedDisk line 196
  26. def OAI.InternalCatalan.firstSheetEvaluation line 213
  27. theorem OAI.InternalCatalan.firstSheetEvaluation_apply line 217
  28. theorem OAI.InternalCatalan.firstSheetEvaluation_det_ne_zero line 222
  29. def OAI.InternalCatalan.firstSheetEvaluationEquiv line 228
  30. theorem OAI.InternalCatalan.firstSheetEvaluationEquiv_apply line 234
  31. theorem OAI.InternalCatalan.firstSheetNumerator_eq_zero_of_eval_zero line 242
  32. theorem OAI.InternalCatalan.firstSheetEvaluation_eq_denominator_mul_value line 249
  33. def OAI.InternalCatalan.firstSheetNodeMultiplier line 258
  34. def OAI.InternalCatalan.firstSheetInterpolatingMultiplier line 264
  35. theorem OAI.InternalCatalan.firstSheetInterpolatingMultiplier_eval line 269
  36. def OAI.InternalCatalan.firstSheetEvaluationOperator line 281
  37. theorem OAI.InternalCatalan.firstSheetEvaluation_cancellation line 285
  38. def OAI.InternalCatalan.firstSheetMixedEvaluationMatrix line 309
  39. theorem OAI.InternalCatalan.firstSheetNumerator_single line 313
  40. theorem OAI.InternalCatalan.firstSheetReverse_single line 318
  41. theorem OAI.InternalCatalan.firstSheetMixedEvaluationMatrix_eq line 333
  42. theorem OAI.InternalCatalan.firstSheetReverse_det_norm line 346
  43. theorem OAI.InternalCatalan.firstSheetEvaluation_det line 359
  44. theorem OAI.InternalCatalan.firstSheetMixedEvaluationMatrix_det line 366
  45. theorem OAI.InternalCatalan.firstSheetMixedEvaluationMatrix_norm_div line 376
  46. def OAI.InternalCatalan.firstSheetKernelNumerator line 396
  47. def OAI.InternalCatalan.firstSheetKernelCoefficients line 399
  48. theorem OAI.InternalCatalan.firstSheetNumerator_coefficients line 402
  49. theorem OAI.InternalCatalan.firstSheetKernelNumerator_natDegree_lt line 418
  50. theorem OAI.InternalCatalan.firstSheetKernelCoefficients_numerator line 433
  51. theorem OAI.InternalCatalan.firstSheetRational_kernelCoefficients line 440
  52. def OAI.InternalCatalan.firstSheetRationalBoundaryMap line 464
  53. def OAI.InternalCatalan.firstSheetRationalEmbedding line 481
  54. theorem OAI.InternalCatalan.firstSheetRationalEmbedding_apply line 485
  55. theorem OAI.InternalCatalan.firstSheetRationalEmbedding_inner_kernel line 491
  56. theorem OAI.InternalCatalan.firstSheetRationalEmbedding_injective line 499
  57. def OAI.InternalCatalan.firstSheetSpace line 512
  58. instance OAI.InternalCatalan.firstSheetSpace_finiteDimensional line 515
  59. theorem OAI.InternalCatalan.firstSheetKernelVector_mem_space line 520
  60. theorem OAI.InternalCatalan.firstSheetRationalEmbedding_norm_sq line 530
  61. theorem OAI.InternalCatalan.firstSheetRationalEmbedding_reverse_norm line 536
  62. def OAI.InternalCatalan.firstSheetProjection line 544
  63. theorem OAI.InternalCatalan.firstSheetProjection_norm_le line 548
  64. theorem OAI.InternalCatalan.firstSheetProjection_inner_kernel line 553
  65. theorem OAI.InternalCatalan.firstSheetBoundary_mul_norm_le line 573
  66. theorem OAI.InternalCatalan.firstSheetProjection_mul_eq line 601
  67. theorem OAI.InternalCatalan.firstSheetInterpolatingMultiplier_norm_le line 634
  68. theorem OAI.InternalCatalan.firstSheetEvaluationOperator_norm_le line 646
  69. def OAI.InternalCatalan.firstSheetSpaceEquiv line 675
  70. theorem OAI.InternalCatalan.firstSheetSpaceEquiv_coe line 680
  71. theorem OAI.InternalCatalan.firstSheetSpace_finrank line 684
  72. def OAI.InternalCatalan.firstSheetSpaceOperator line 689
  73. theorem OAI.InternalCatalan.firstSheetSpaceOperator_norm_le line 695
  74. theorem OAI.InternalCatalan.firstSheetSpaceOperator_det line 709
  75. theorem OAI.InternalCatalan.firstSheetMixedEvaluationMatrix_norm_le line 723
  76. theorem OAI.InternalCatalan.firstSheet_uniform_mixed_determinant_bound line 739
  77. theorem OAI.InternalCatalan.firstSheet_norm_ofReal_det line 770
  78. theorem OAI.InternalCatalan.firstSheet_uniform_real_mixed_determinant_bound line 776
  79. theorem OAI.InternalCatalan.firstSheet_laurent_vandermonde_weight line 799
  80. theorem OAI.InternalCatalan.realSheetDeterminant_first_sheet_bound line 823
  81. theorem OAI.InternalCatalan.abs_sheetRealIntegrand_le_majorantTwo line 874
  82. theorem OAI.InternalCatalan.abs_determinant_le_of_two_majorant_bounds line 903