OAI/Analysis/FreeEntropy/WickSeries.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteEntropySeparation.FreeTensor.noiseWickIsometry line 12
2. theorem OAI.FiniteEntropySeparation.FreeTensor.noiseWickIsometry_single line 19
3. theorem OAI.FiniteEntropySeparation.FreeTensor.noiseWickIsometry_norm_sq line 29
4. theorem OAI.FiniteEntropySeparation.FreeTensor.noiseWickIsometry_hasSum line 35
5. theorem OAI.FiniteEntropySeparation.FreeTensor.noiseWickIsometry_inner_hasSum line 43
6. theorem OAI.FiniteEntropySeparation.FreeTensor.wick_series_testing line 52
7. def OAI.FiniteEntropySeparation.FreeTensor.wickCoefficientVector line 69
8. theorem OAI.FiniteEntropySeparation.FreeTensor.fisher_wick_series_bound line 73