OAI/Analysis/FreeEntropy/CumulantResidual.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteEntropySeparation.FreeSeries.reverseEquiv line 11
2. def OAI.FiniteEntropySeparation.FreeSeries.residual line 17
3. theorem OAI.FiniteEntropySeparation.FreeSeries.residual_heat line 19
4. theorem OAI.FiniteEntropySeparation.FreeSeries.cumulant_residual_identity line 28
5. theorem OAI.FiniteEntropySeparation.series_reverseDerivative_hasSum line 41
6. theorem OAI.FiniteEntropySeparation.inner_selfAdjoint_word line 56
7. theorem OAI.FiniteEntropySeparation.cumulant_residual_hasSum line 62
8. theorem OAI.FiniteEntropySeparation.FreeTensor.heat_cumulant_residual_hasSum line 78