OAI/Probability/SKGap/Localization/Character.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SKGapCutoff.exp_apply_hasSum line 10
  2. theorem OAI.SKGapCutoff.exp_apply_of_apply_eq_zero line 19
  3. theorem OAI.SKGapCutoff.semigroup_const line 34
  4. theorem OAI.SKGapCutoff.exp_smul_identity line 41
  5. theorem OAI.SKGapCutoff.semigroup_uniformization line 47
  6. theorem OAI.SKGapCutoff.semigroup_nonneg line 66
  7. theorem OAI.SKGapCutoff.continuousKernel_nonneg line 88
  8. theorem OAI.SKGapCutoff.continuousKernel_sum line 92
  9. theorem OAI.SKGapCutoff.spin_sq line 101
  10. theorem OAI.SKGapCutoff.spin_mul_self line 105
  11. theorem OAI.SKGapCutoff.field_zero line 108
  12. theorem OAI.SKGapCutoff.mean_zero line 111
  13. theorem OAI.SKGapCutoff.energy_zero line 114
  14. theorem OAI.SKGapCutoff.card_spin line 117
  15. theorem OAI.SKGapCutoff.partition_zero line 120
  16. theorem OAI.SKGapCutoff.gibbs_zero line 123
  17. def OAI.SKGapCutoff.character line 126
  18. theorem OAI.SKGapCutoff.character_empty line 129
  19. theorem OAI.SKGapCutoff.character_sq line 132
  20. lemma OAI.SKGapCutoff.character_erase line 135
  21. lemma OAI.SKGapCutoff.spin_replace_of_ne line 139
  22. lemma OAI.SKGapCutoff.character_replace_of_not_mem line 143
  23. lemma OAI.SKGapCutoff.character_replace_of_mem line 149
  24. lemma OAI.SKGapCutoff.halfDiff_character line 156
  25. lemma OAI.SKGapCutoff.spin_mul_halfDiff_character line 163
  26. lemma OAI.SKGapCutoff.generator_zero_character line 170
  27. theorem OAI.SKGapCutoff.exp_apply_of_eigenvector line 178
  28. lemma OAI.SKGapCutoff.semigroup_zero_character line 192
  29. lemma OAI.SKGapCutoff.attempt_zero_character line 200
  30. lemma OAI.SKGapCutoff.attempt_pow_zero_character line 207
  31. lemma OAI.SKGapCutoff.character_eq_prod_univ line 216
  32. lemma OAI.SKGapCutoff.character_inner line 220
  33. lemma OAI.SKGapCutoff.character_sum line 248
  34. lemma OAI.SKGapCutoff.character_delta_sum line 252
  35. lemma OAI.SKGapCutoff.delta_character_expansion line 274
  36. lemma OAI.SKGapCutoff.character_parseval line 283
  37. def OAI.SKGapCutoff.fourierKernel line 298
  38. lemma OAI.SKGapCutoff.continuousKernel_zero_fourier line 302
  39. lemma OAI.SKGapCutoff.discreteKernel_zero_fourier line 314
  40. def OAI.SKGapCutoff.centeredFourier line 326
  41. lemma OAI.SKGapCutoff.centeredFourier_sum_sq line 329
  42. lemma OAI.SKGapCutoff.centeredFourier_expansion line 337
  43. lemma OAI.SKGapCutoff.fourierKernel_sub_uniform line 343
  44. lemma OAI.SKGapCutoff.fourierKernel_chiSquare line 350
  45. lemma OAI.SKGapCutoff.totalVariation_fourier_sq_le line 360
  46. lemma OAI.SKGapCutoff.sum_pow_card line 372
  47. lemma OAI.SKGapCutoff.exp_card_sq line 378
  48. lemma OAI.SKGapCutoff.continuous_zero_tv_sq_le line 385
  49. lemma OAI.SKGapCutoff.discrete_character_sq_le line 396
  50. lemma OAI.SKGapCutoff.discrete_zero_tv_sq_le line 416