OAI/Probability/FreeIsing/Posterior/ResponseTruncation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.capped_mul_sq_le line 14
  2. theorem OAI.Problem367.summable_capped_mul_error_sq line 28
  3. theorem OAI.Problem367.integrable_capped_mul_error_row line 37
  4. theorem OAI.Problem367.tendsto_integral_capped_mul_error_row line 63
  5. def OAI.Problem367.cappedGibbsResponse line 99
  6. theorem OAI.Problem367.measurable_cappedGibbsResponse line 104
  7. theorem OAI.Problem367.cappedGibbsResponse_abs_le line 110
  8. theorem OAI.Problem367.isStronglyProgressive_cappedGibbsResponse line 120
  9. theorem OAI.Problem367.cappedGibbsResponse_meanSquare_of_energy line 132
  10. theorem OAI.Problem367.HasFreeIsingLaw.cappedGibbsResponse_meanSquare_time_of_strict line 168