OAI/Probability/FreeIsing/Conditioning/FiniteFieldEntropyExpectation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.FinitePosterior.integral_fieldEntropyGradient_mul_noise line 13
  2. theorem OAI.Problem367.FinitePosterior.integrable_bounded_entropy_test line 43
  3. theorem OAI.Problem367.FinitePosterior.integrable_finiteStandardEntropyGradient line 53
  4. theorem OAI.Problem367.FinitePosterior.integrable_finiteStandardEntropyHessian line 67
  5. theorem OAI.Problem367.FinitePosterior.integrable_finiteStandardEntropyGradient_mul_noise line 81
  6. theorem OAI.Problem367.FinitePosterior.integral_finiteStandardEntropyGradient_mul_noise line 98
  7. theorem OAI.Problem367.FinitePosterior.integral_finiteStandardEntropyVelocity line 118
  8. theorem OAI.Problem367.FinitePosterior.integrable_finiteStandardSignal line 218
  9. theorem OAI.Problem367.FinitePosterior.integrable_finiteStandardObservation line 231
  10. theorem OAI.Problem367.FinitePosterior.integrable_finiteStandardEntropy line 242
  11. theorem OAI.Problem367.FinitePosterior.continuous_normalizedRowEnergy line 256
  12. theorem OAI.Problem367.FinitePosterior.abs_normalizedRowEnergy_le_card line 266