OAI/Probability/FreeIsing/Ising/CopySmallLogLoss.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.IsingCopySmallLogLoss.siteVariance line 19
2. def OAI.Problem367.IsingCopySmallLogLoss.logVariance line 23
3. theorem OAI.Problem367.IsingCopySmallLogLoss.siteVariance_nonneg line 28
4. theorem OAI.Problem367.IsingCopySmallLogLoss.logVariance_nonneg line 31
5. theorem OAI.Problem367.IsingCopySmallLogLoss.observable_identDistrib_copies line 34
6. theorem OAI.Problem367.IsingCopySmallLogLoss.logVariance_le_siteVariance line 48
7. theorem OAI.Problem367.IsingCopySmallLogLoss.ae_site_difference_bound line 57
8. theorem OAI.Problem367.IsingCopySmallLogLoss.logVariance_small_time_of_tail line 75