OAI/Analysis/FreeEntropy/GaussianVolume.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteEntropySeparation.measure_pi_mono line 11
2. theorem OAI.FiniteEntropySeparation.gaussianPDF_le_one line 24
3. theorem OAI.FiniteEntropySeparation.gaussianReal_le_volume line 34
4. theorem OAI.FiniteEntropySeparation.productGaussian_le_volume line 41
5. theorem OAI.FiniteEntropySeparation.productGaussian_toLp_le_volume line 44