OAI/Probability/SKValue/GroundState/RotatedCoefficients.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKValueG.gaussian_gibbs_derivative_nonneg line 11
  2. def OAI.SKValueG.rotatedCoefficients line 44
  3. def OAI.SKValueG.rotationVelocity line 47
  4. lemma OAI.SKValueG.hasDerivAt_rotatedProcess line 50
  5. lemma OAI.SKValueG.abs_rotationVelocity_le line 57
  6. lemma OAI.SKValueG.rotation_derivative_bound line 67
  7. lemma OAI.SKValueG.hasDerivAt_expected_rotated_logPartition line 83
  8. lemma OAI.SKValueG.rotation_pair_covariance line 110
  9. lemma OAI.SKValueG.expected_logPartition_le_of_pair_distances line 120
  10. def OAI.SKValueG.finiteMaximum line 149
  11. lemma OAI.SKValueG.le_finiteMaximum line 151
  12. lemma OAI.SKValueG.exists_finiteMaximum line 154
  13. lemma OAI.SKValueG.continuous_finiteMaximum line 157
  14. lemma OAI.SKValueG.abs_finiteMaximum_le line 165
  15. lemma OAI.SKValueG.finiteMaximum_integrable line 171
  16. lemma OAI.SKValueG.scaled_max_le_logPartition line 177
  17. lemma OAI.SKValueG.logPartition_le_scaled_max line 183
  18. lemma OAI.SKValueG.linearProcess_scaled line 187
  19. lemma OAI.SKValueG.expected_max_le_of_pair_distances_orthogonal line 192
  20. lemma OAI.SKValueG.gaussian_integral_reindex line 245
  21. lemma OAI.SKValueG.linearProcess_reindex line 255
  22. lemma OAI.SKValueG.expected_max_reindex line 261
  23. lemma OAI.SKValueG.expected_max_le_of_pair_distances_orthogonal_fintype line 267
  24. def OAI.SKValueG.embedLeft line 284
  25. def OAI.SKValueG.embedRight line 286
  26. lemma OAI.SKValueG.expected_max_embedLeft line 289
  27. lemma OAI.SKValueG.expected_max_embedRight line 304
  28. lemma OAI.SKValueG.expected_max_le_of_pair_distances line 319
  29. def OAI.SKValueG.spin line 332
  30. def OAI.SKValueG.hamiltonian line 333
  31. def OAI.SKValueG.groundStateSequence line 337
  32. def OAI.SKValueG.groundStateValue line 339
  33. def OAI.SKValueG.hamCoeff line 341
  34. def OAI.SKValueG.expectedMaximum line 343
  35. lemma OAI.SKValueG.spin_sq line 346
  36. lemma OAI.SKValueG.abs_spin line 347
  37. lemma OAI.SKValueG.linearProcess_hamCoeff line 349
  38. lemma OAI.SKValueG.groundStateSequence_eq line 359
  39. lemma OAI.SKValueG.twice_upper_sum line 362
  40. lemma OAI.SKValueG.spin_pair_difference line 381