OAI/Analysis/FreeEntropy/OrthogonalExpansion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteEntropySeparation.linearExpand line 11
2. theorem OAI.FiniteEntropySeparation.linearExpand_apply line 12
3. theorem OAI.FiniteEntropySeparation.linearExpand_integrable line 15
4. theorem OAI.FiniteEntropySeparation.linearExpand_mul_integrable line 20
5. theorem OAI.FiniteEntropySeparation.linearExpand_integral line 30
6. theorem OAI.FiniteEntropySeparation.linearExpand_inner line 36
7. theorem OAI.FiniteEntropySeparation.linearExpand_orthogonal line 55
8. theorem OAI.FiniteEntropySeparation.integral_center_sq line 77