OAI/Probability/FreeIsing/Posterior/NormalizedPosteriorLimit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.integrable_sq_and_integral_le_of_tendsto_ae line 16
2. theorem OAI.Problem367.posteriorResponse_integrable_sq_of_uniform_bound line 48
3. theorem OAI.Problem367.posteriorResponse_row_energy_of_uniform_bounds line 64
4. def OAI.Problem367.gaussianPosteriorResponse line 96
5. theorem OAI.Problem367.HasFreeIsingLaw.finiteObservation_posteriorResponse line 104
6. theorem OAI.Problem367.HasFreeIsingLaw.gaussian_posteriorResponse_tendsto_ae line 128
7. theorem OAI.Problem367.HasFreeIsingLaw.gaussian_posteriorResponse_integrable_sq line 152
8. theorem OAI.Problem367.HasFreeIsingLaw.gaussian_posteriorResponse_meanSquare line 180