OAI/Analysis/FreeEntropy/WickCoefficients.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteEntropySeparation.FreeSeries.vectorReverse line 11
2. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_reverse line 18
3. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_conj line 24
4. def OAI.FiniteEntropySeparation.FreeSeries.wickCoefficients line 28
5. theorem OAI.FiniteEntropySeparation.FreeSeries.wickCoefficients_cancel line 32
6. theorem OAI.FiniteEntropySeparation.FreeSeries.wickCoefficients_degree_sq line 36
7. theorem OAI.FiniteEntropySeparation.FreeSeries.residual_degree line 49
8. theorem OAI.FiniteEntropySeparation.FreeSeries.residual_degree_short line 54
9. theorem OAI.FiniteEntropySeparation.FreeSeries.residual_degree_sum line 60
10. theorem OAI.FiniteEntropySeparation.FreeSeries.wickCoefficients_degree_sum line 70