OAI/Probability/FreeIsing/Conditioning/FiniteEntropySmallTime.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.gaussian_channel_fourth_moment line 17
2. theorem OAI.Problem367.finiteIsingBrownianEntropy_le_information line 79
3. theorem OAI.Problem367.brownianTerminal_information_eq_gaussian line 154
4. theorem OAI.Problem367.HasFreeIsingLaw.finiteIsingBrownian_critical_information_upper line 199
5. def OAI.Problem367.criticalEntropyEnvelope line 221
6. theorem OAI.Problem367.HasFreeIsingLaw.finiteIsingBrownianEntropy_le_criticalEnvelope line 229
7. theorem OAI.Problem367.criticalEntropyEnvelope_zero line 251
8. theorem OAI.Problem367.continuous_criticalEntropyEnvelope line 254