OAI/NumberTheory/Catalan/Energy/BarrierPowerLogFormula.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InternalCatalan.barrierFiniteCoeff_S_hasSum line 13
2. theorem OAI.InternalCatalan.barrierTailRow_S_hasSum line 30
3. theorem OAI.InternalCatalan.barrierTail_S_hasSum line 50
4. theorem OAI.InternalCatalan.barrierTrialS_eq_finite_log line 69
5. theorem OAI.InternalCatalan.barrierV2_S_eq_finite_log line 86