OAI/Probability/FreeIsing/Ising/CopySmallTime.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.criticalCopyVarianceConstant line 14
2. theorem OAI.Problem367.criticalCopyVarianceConstant_nonneg line 19
3. theorem OAI.Problem367.IsingConditionalCopyBounds.posteriorInformation_critical_upper line 28
4. theorem OAI.Problem367.IsingConditionalCopyBounds.fieldDifference_secondMoment_critical_upper line 41
5. theorem OAI.Problem367.IsingObservationFactor.field_variance_critical_upper line 75
6. theorem OAI.Problem367.IsingObservationFactor.field_variance_critical_tendsto_zero line 86
7. theorem OAI.Problem367.IsingObservationFactor.field_variance_critical_continuousAt_zero line 107
8. theorem OAI.Problem367.IsingObservationFactor.field_variance_critical_real_tendsto_zero line 118