OAI/Probability/SKRatio/FiniteChain/EntropicCovariance.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SKRatio.Observation.Prior line 15
  2. instance OAI.SKRatio.Observation.(instance at line 20) line 20
  3. lemma OAI.SKRatio.Observation.Prior.ext line 22
  4. def OAI.SKRatio.Observation.avg line 25
  5. def OAI.SKRatio.Observation.var line 27
  6. def OAI.SKRatio.Observation.ent line 29
  7. lemma OAI.SKRatio.Observation.avg_const line 31
  8. lemma OAI.SKRatio.Observation.avg_nonneg line 34
  9. lemma OAI.SKRatio.Observation.avg_pos line 37
  10. lemma OAI.SKRatio.Observation.avg_mono line 43
  11. lemma OAI.SKRatio.Observation.avg_add line 46
  12. lemma OAI.SKRatio.Observation.avg_sub line 49
  13. lemma OAI.SKRatio.Observation.avg_const_mul line 52
  14. lemma OAI.SKRatio.Observation.avg_mul_const line 55
  15. lemma OAI.SKRatio.Observation.var_eq line 58
  16. def OAI.SKRatio.Observation.tiltZ line 61
  17. lemma OAI.SKRatio.Observation.tiltZ_pos line 63
  18. def OAI.SKRatio.Observation.tilt line 66
  19. lemma OAI.SKRatio.Observation.tilt_apply line 73
  20. lemma OAI.SKRatio.Observation.tiltZ_zero line 76
  21. lemma OAI.SKRatio.Observation.tilt_zero line 79
  22. lemma OAI.SKRatio.Observation.avg_tilt line 83
  23. lemma OAI.SKRatio.Observation.hasDerivAt_tiltZ line 90
  24. lemma OAI.SKRatio.Observation.hasDerivAt_tiltNumerator line 98
  25. lemma OAI.SKRatio.Observation.hasDerivAt_logTiltZ line 108
  26. lemma OAI.SKRatio.Observation.hasDerivAt_tiltedMean line 113
  27. lemma OAI.SKRatio.Observation.quadratic_upper_of_derivatives line 121
  28. theorem OAI.SKRatio.Observation.logTiltZ_le line 164
  29. theorem OAI.SKRatio.Observation.mean_displacement_sq line 173
  30. def OAI.SKRatio.Observation.linear line 193
  31. lemma OAI.SKRatio.Observation.avg_linear line 195
  32. theorem OAI.SKRatio.Observation.vector_mean_displacement_sq line 203
  33. def OAI.SKRatio.Observation.reweight line 228
  34. lemma OAI.SKRatio.Observation.avg_reweight line 233
  35. lemma OAI.SKRatio.Observation.relativeEntropy_reweight line 238
  36. theorem OAI.SKRatio.Observation.covariance_entropy line 256
  37. def OAI.SKRatio.Observation.gibbsPrior line 281
  38. lemma OAI.SKRatio.Observation.weight_field_tilt line 284
  39. lemma OAI.SKRatio.Observation.tilt_gibbs_linear line 292
  40. theorem OAI.SKRatio.Observation.spin_covariance_entropy line 305