OAI/Analysis/FreeEntropy/RealTail.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.FiniteEntropySeparation.integrableOn_Ioi_translateline 8 - theorem
OAI.FiniteEntropySeparation.integral_Ioi_translateline 14 - theorem
OAI.FiniteEntropySeparation.inverseFourth_integrableline 19 - theorem
OAI.FiniteEntropySeparation.inverseFourth_integralline 24