OAI/NumberTheory/Catalan/Estimates/RealPermutationAlgebra.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.InternalCatalan.rawRealIntegrandline 12 - def
OAI.InternalCatalan.leftRealIntegrandline 16 - def
OAI.InternalCatalan.doubleRealIntegrandline 21 - theorem
OAI.InternalCatalan.sum_rawRealIntegrand_permute_leftline 26 - theorem
OAI.InternalCatalan.sum_leftRealIntegrand_permute_rightline 47