OAI/Probability/FreeIsing/Energy/NormalizedResponseTime.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem367.NormalizedResponseTime.observedRow_abs_le_one line 14
2. lemma OAI.Problem367.NormalizedResponseTime.infiniteGibbsResponse_eq_gaussianPosteriorResponse line 29
3. theorem OAI.Problem367.NormalizedResponseTime.observedRow_tendsto_ae_gaussian line 40
4. theorem OAI.Problem367.NormalizedResponseTime.observedRow_tendsto_ae_brownian line 54
5. theorem OAI.Problem367.NormalizedResponseTime.observedRow_time_meanSquare_brownian line 83