OAI/Probability/SKGap/Localization/CurieWeiss.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGapCutoff.curieWeiss line 52
  2. lemma OAI.SKGapCutoff.curieWeiss_symm line 55
  3. lemma OAI.SKGapCutoff.curieWeiss_diag line 60
  4. lemma OAI.SKGapCutoff.curieWeiss_energy line 64
  5. def OAI.SKGapCutoff.majority line 82
  6. lemma OAI.SKGapCutoff.magnetization_invert line 85
  7. lemma OAI.SKGapCutoff.majority_invert line 89
  8. lemma OAI.SKGapCutoff.majority_abs_le_one line 93
  9. lemma OAI.SKGapCutoff.majority_centered line 97
  10. lemma OAI.SKGapCutoff.majority_sq line 103
  11. lemma OAI.SKGapCutoff.magnetization_replace line 110
  12. lemma OAI.SKGapCutoff.halfDiff_majority_zero line 125
  13. lemma OAI.SKGapCutoff.halfDiff_majority_abs_le_one line 148
  14. def OAI.SKGapCutoff.centralMass line 155
  15. lemma OAI.SKGapCutoff.majority_variance_lower line 158
  16. lemma OAI.SKGapCutoff.majority_dirichlet_upper line 170
  17. lemma OAI.SKGapCutoff.gibbs_le_exp_energy_diff line 190
  18. lemma OAI.SKGapCutoff.curieWeiss_central_point_bound line 196
  19. lemma OAI.SKGapCutoff.curieWeiss_central_bound line 212
  20. theorem OAI.SKGapCutoff.curieWeiss_gap_bottleneck line 225
  21. lemma OAI.SKGapCutoff.curieWeiss_entry_bound line 238
  22. lemma OAI.SKGapCutoff.curieWeiss_norm_bound line 246
  23. lemma OAI.SKGapCutoff.curieWeiss_bound_exp line 258
  24. lemma OAI.SKGapCutoff.curieWeiss_bound_tendsto_zero line 267
  25. lemma OAI.SKGapCutoff.curieWeiss_n_bound_tendsto_zero line 279
  26. theorem OAI.SKGapCutoff.curieWeiss_no_uniform_gap line 293
  27. lemma OAI.SKGapCutoff.curieWeiss_entries_vanish line 309