OAI/Probability/FreeIsing/Posterior/FieldMoments.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.gaussianPosteriorField line 15
  2. theorem OAI.Problem367.measurable_gaussianPosteriorField line 21
  3. theorem OAI.Problem367.gaussianPlanted_noise_hasLaw line 27
  4. theorem OAI.Problem367.HasFreeIsingLaw.gaussian_posterior_field_noise_bound line 37
  5. theorem OAI.Problem367.HasFreeIsingLaw.integrable_gaussianPosteriorField_abs_pow line 57
  6. theorem OAI.Problem367.HasFreeIsingLaw.memLp_gaussianPosteriorField_two line 69
  7. theorem OAI.Problem367.HasFreeIsingLaw.gaussianPosteriorField_abs_moment_le line 79
  8. theorem OAI.Problem367.HasFreeIsingLaw.gaussianPosteriorField_second_moment_le line 110
  9. theorem OAI.Problem367.HasFreeIsingLaw.gaussianPosteriorField_second_moment_le_horizon line 126