OAI/Probability/InvariantIsing/Core/LogMeanLoss.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

One Gaussian backward step propagates a terminal loss by expectation under its canonical tilted transition. No lower bound on its positive exponent is required.

  1. lemma OAI.InvariantIsing.integral_le_log_integral_exp line 15
  2. theorem OAI.InvariantIsing.logMean_loss_le_tilted_mean line 24