OAI/Analysis/Pureness/Tensor/SpatialCenteredPolynomials.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.spatialCoefficientExpectation_norm_le line 14
2. def OAI.CuntzPureness.centeredGroupPolynomial line 24
3. lemma OAI.CuntzPureness.centeredGroupPolynomial_one line 26
4. lemma OAI.CuntzPureness.spatialGroupPolynomialMap_centered line 30
5. lemma OAI.CuntzPureness.exists_centered_approximation line 46
6. theorem OAI.CuntzPureness.exists_centered_spatial_polynomial line 66