OAI/Probability/FreeIsing/Estimates/CoupledSmallLogLoss.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.cavityLogVarianceCoefficient line 13
  2. def OAI.Problem367.cavityLogTailCoefficient line 16
  3. theorem OAI.Problem367.cavityLogVarianceCoefficient_nonneg line 19
  4. theorem OAI.Problem367.cavityLogTailCoefficient_nonneg line 24
  5. theorem OAI.Problem367.integral_cavity_log_discrepancy_sq_le_of_marginal_tails line 34
  6. theorem OAI.Problem367.integral_cavity_log_discrepancy_small_time line 73
  7. theorem OAI.Problem367.integral_cavity_log_discrepancy_small_time_of_moments line 108
  8. theorem OAI.Problem367.integral_cavity_log_discrepancy_small_time_of_common_law line 144
  9. theorem OAI.Problem367.integral_cavity_log_discrepancy_osgood_of_small_time line 182