OAI/Analysis/FreeEntropy/OptionSeries.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteEntropySeparation.FreeSeries.ignoreLetter line 10
2. theorem OAI.FiniteEntropySeparation.FreeSeries.deriv_ignore_none line 13
3. theorem OAI.FiniteEntropySeparation.FreeSeries.deriv_ignore_some line 16
4. theorem OAI.FiniteEntropySeparation.FreeSeries.ignoreLetter_norm_sq line 18
5. theorem OAI.FiniteEntropySeparation.FreeSeries.ignoreLetter_norm_le line 29
6. def OAI.FiniteEntropySeparation.FreeSeries.vectorMap line 47
7. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_equiv line 54
8. def OAI.FiniteEntropySeparation.FreeSeries.optionFin line 60
9. theorem OAI.FiniteEntropySeparation.FreeSeries.optionFin_none line 65
10. theorem OAI.FiniteEntropySeparation.FreeSeries.optionFin_some line 66