OAI/Probability/FreeIsing/Gaussian/FiniteFieldGaussianEnergy.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Problem367.FinitePosterior.covariance_eq_centered_sum_entropy line 14
  2. theorem OAI.Problem367.FinitePosterior.abs_covariance_le_spin_variance_entropy line 23
  3. theorem OAI.Problem367.FinitePosterior.abs_tiltResponse_le_one_entropy line 63
  4. def OAI.Problem367.FinitePosterior.fieldEntropy line 75
  5. def OAI.Problem367.FinitePosterior.fieldEntropyGradient line 79
  6. def OAI.Problem367.FinitePosterior.fieldEntropyHessianDiagonal line 83
  7. lemma OAI.Problem367.FinitePosterior.fieldVariance_pos_entropy line 90
  8. theorem OAI.Problem367.FinitePosterior.abs_normalizedFieldCovariance_le_one_entropy line 98
  9. theorem OAI.Problem367.FinitePosterior.continuous_normalizedFieldCovariance_entropy line 107
  10. theorem OAI.Problem367.FinitePosterior.continuous_fieldEntropy line 116
  11. theorem OAI.Problem367.FinitePosterior.hasFDerivAt_fieldEntropy line 124
  12. theorem OAI.Problem367.FinitePosterior.continuous_fieldEntropyGradient line 146
  13. theorem OAI.Problem367.FinitePosterior.continuous_fieldEntropyHessianDiagonal line 154
  14. theorem OAI.Problem367.FinitePosterior.abs_fieldEntropyGradient_le line 164
  15. theorem OAI.Problem367.FinitePosterior.abs_fieldEntropyHessianDiagonal_le line 181
  16. lemma OAI.Problem367.FinitePosterior.normalizedFieldCovariance_coordinate_tilt_entropy line 215
  17. theorem OAI.Problem367.FinitePosterior.hasDerivAt_fieldEntropyGradient_coordinate line 222
  18. theorem OAI.Problem367.FinitePosterior.hasDerivAt_fieldEntropyGradient_update line 247
  19. theorem OAI.Problem367.FinitePosterior.fieldEntropy_generator_identity line 261
  20. theorem OAI.Problem367.FinitePosterior.fieldEntropy_eq_log_cosh line 274
  21. theorem OAI.Problem367.FinitePosterior.fieldEntropy_nonneg line 287
  22. theorem OAI.Problem367.FinitePosterior.fieldEntropy_le_abs_field line 297
  23. theorem OAI.Problem367.FinitePosterior.norm_fderiv_fieldEntropy_le line 313
  24. theorem OAI.Problem367.FinitePosterior.lipschitzWith_fieldEntropy line 335
  25. theorem OAI.Problem367.FinitePosterior.integrable_fieldEntropy_comp line 348