OAI/Probability/SKRatio/Calculus/SpectralLower.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKRatio.Calculus.transition_balance line 15
  2. def OAI.SKRatio.Calculus.stationaryInner line 26
  3. def OAI.SKRatio.Calculus.stationaryPairingCLM line 29
  4. lemma OAI.SKRatio.Calculus.stationaryPairingCLM_apply line 39
  5. lemma OAI.SKRatio.Calculus.stationaryInner_symm line 42
  6. lemma OAI.SKRatio.Calculus.generator_symmetric line 46
  7. lemma OAI.SKRatio.Calculus.stationaryInner_pow_symm line 72
  8. lemma OAI.SKRatio.Calculus.stationaryInner_exp_symm line 86
  9. lemma OAI.SKRatio.Calculus.semigroup_symmetric line 105
  10. lemma OAI.SKRatio.Calculus.exp_apply_of_eigenvector line 116
  11. def OAI.SKRatio.Calculus.gibbsEuclideanEquiv line 130
  12. lemma OAI.SKRatio.Calculus.gibbsEuclideanEquiv_apply line 143
  13. lemma OAI.SKRatio.Calculus.gibbsEuclideanEquiv_inner line 146
  14. def OAI.SKRatio.Calculus.negativeGeneratorEuclidean line 155
  15. lemma OAI.SKRatio.Calculus.negativeGeneratorEuclidean_lift line 160
  16. lemma OAI.SKRatio.Calculus.negativeGeneratorEuclidean_symmetric line 165
  17. def OAI.SKRatio.Calculus.spinEigenvalues line 176
  18. def OAI.SKRatio.Calculus.spinEigenbasis line 179
  19. def OAI.SKRatio.Calculus.spectralCoefficient line 183
  20. lemma OAI.SKRatio.Calculus.spectral_parseval line 187
  21. lemma OAI.SKRatio.Calculus.spectral_generator_coordinates line 193
  22. def OAI.SKRatio.Calculus.scalarEigenfunction line 201
  23. lemma OAI.SKRatio.Calculus.lift_scalarEigenfunction line 204
  24. lemma OAI.SKRatio.Calculus.generator_scalarEigenfunction line 208
  25. lemma OAI.SKRatio.Calculus.semigroup_scalarEigenfunction line 218
  26. lemma OAI.SKRatio.Calculus.spectral_coordinates_inner line 226
  27. lemma OAI.SKRatio.Calculus.spectral_semigroup_coordinates line 232
  28. lemma OAI.SKRatio.Calculus.stationary_correlation_lower line 242
  29. lemma OAI.SKRatio.Calculus.gibbsMean_siteKernel line 278
  30. lemma OAI.SKRatio.Calculus.gibbsMean_spin_times_mean line 286
  31. lemma OAI.SKRatio.Calculus.stationary_weight_le_one line 300
  32. lemma OAI.SKRatio.Calculus.stationaryEnergy_spin_le_one line 313
  33. lemma OAI.SKRatio.Calculus.spin_correlation_lower line 324
  34. def OAI.SKRatio.Calculus.linearObservable line 333
  35. lemma OAI.SKRatio.Calculus.halfDiff_linearObservable line 335
  36. lemma OAI.SKRatio.Calculus.unweightedGradient_linearObservable line 344
  37. lemma OAI.SKRatio.Calculus.gibbsMean_linearObservable_zero line 348
  38. lemma OAI.SKRatio.Calculus.stationaryEnergy_linearObservable_le line 359
  39. lemma OAI.SKRatio.Calculus.stationary_linearObservable_variance_le line 369
  40. lemma OAI.SKRatio.Calculus.semigroup_linearObservable line 377
  41. lemma OAI.SKRatio.Calculus.exists_distinguishing_linear line 385
  42. lemma OAI.SKRatio.Calculus.continuousDistance_lower_of_linear_variances line 421
  43. lemma OAI.SKRatio.Calculus.exp_quarter_log_div line 465
  44. theorem OAI.SKRatio.Calculus.uniform_strong_lower_of_small_set line 475
  45. theorem OAI.SKRatio.Calculus.uniform_median_lower_of_small_set line 513