OAI/Probability/SKGap/Localization/TapPotential.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.tapPotential line 14
  2. def OAI.SKGap.weightedTap line 22
  3. lemma OAI.SKGap.singlePotential_hasDerivAt line 25
  4. lemma OAI.SKGap.quadraticForm_derivative_algebra line 34
  5. lemma OAI.SKGap.quadratic_magnetization_hasFDerivAt line 51
  6. lemma OAI.SKGap.squared_magnetization_hasFDerivAt line 83
  7. lemma OAI.SKGap.tapPotential_hasFDerivAt line 98
  8. lemma OAI.SKGap.contDiff_tanh_SK line 137
  9. lemma OAI.SKGap.magnetization_contDiff line 142
  10. lemma OAI.SKGap.spinVariance_contDiff line 146
  11. lemma OAI.SKGap.overlap_contDiff line 150
  12. lemma OAI.SKGap.tapField_contDiff line 154
  13. lemma OAI.SKGap.weightedTap_contDiff line 163
  14. abbrev OAI.SKGap.EField line 169
  15. def OAI.SKGap.tapPotentialE line 171
  16. def OAI.SKGap.weightedTapE line 174
  17. lemma OAI.SKGap.weightedTapE_contDiff line 178
  18. lemma OAI.SKGap.tapPotentialE_hasFDerivAt line 184
  19. def OAI.SKGap.weightedJacobianMap line 200
  20. lemma OAI.SKGap.weightedTap_hasFDerivAt_zero line 206
  21. lemma OAI.SKGap.weightedTapE_fderiv_zero line 219
  22. lemma OAI.SKGap.weighted_jacobian_quadratic_form line 234
  23. lemma OAI.SKGap.weightedTapE_derivative_energy line 252
  24. lemma OAI.SKGap.spinVariance_eq_inv_cosh_sq line 265
  25. lemma OAI.SKGap.spinVariance_bound_on_box line 271
  26. lemma OAI.SKGap.tapField_shift_bound line 280
  27. lemma OAI.SKGap.exists_tapBox_radius line 307
  28. lemma OAI.SKGap.weightedTap_step_box line 316
  29. def OAI.SKGap.fieldBoxE line 339
  30. lemma OAI.SKGap.mem_fieldBoxE line 342
  31. lemma OAI.SKGap.isCompact_fieldBoxE line 355
  32. lemma OAI.SKGap.convex_fieldBoxE line 359
  33. lemma OAI.SKGap.nonempty_fieldBoxE line 363
  34. theorem OAI.SKGap.lyapunov_eventually_hits line 366
  35. theorem OAI.SKGap.lyapunov_fixed_point line 395
  36. def OAI.SKGap.attractionBasin line 405
  37. lemma OAI.SKGap.mem_attractionBasin_iterate_iff line 408
  38. lemma OAI.SKGap.fixed_mem_attractionBasin line 413