OAI/Probability/SKGap/Stability/StableFields.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SKGap.Field line 13
  2. def OAI.SKGap.magnetization line 15
  3. def OAI.SKGap.overlap line 16
  4. def OAI.SKGap.onsager line 17
  5. def OAI.SKGap.spinVariance line 18
  6. def OAI.SKGap.tapField line 20
  7. def OAI.SKGap.hessianCore line 24
  8. def OAI.SKGap.fieldHessian line 29
  9. def OAI.SKGap.vectorSqNorm line 33
  10. def OAI.SKGap.quadraticForm line 35
  11. theorem OAI.SKGap.overlap_nonneg line 38
  12. theorem OAI.SKGap.overlap_lt_one line 41
  13. theorem OAI.SKGap.spinVariance_pos line 53
  14. theorem OAI.SKGap.spinVariance_le_one line 56
  15. theorem OAI.SKGap.fieldHessian_symm line 59
  16. theorem OAI.SKGap.tapField_sub_external line 66
  17. theorem OAI.SKGap.vectorSqNorm_nonneg line 72
  18. theorem OAI.SKGap.vectorSqNorm_eq_zero line 75
  19. theorem OAI.SKGap.hessian_quadratic_formula line 80
  20. theorem OAI.SKGap.hessian_lower_bound line 115
  21. def OAI.SKGap.fieldJacobian line 151
  22. theorem OAI.SKGap.hasDerivAt_tanh line 155
  23. theorem OAI.SKGap.magnetization_hasFDerivAt line 162
  24. def OAI.SKGap.overlapDerivative line 167
  25. theorem OAI.SKGap.overlap_hasFDerivAt line 170
  26. theorem OAI.SKGap.onsager_hasFDerivAt line 187
  27. theorem OAI.SKGap.tapField_hasFDerivAt line 194
  28. theorem OAI.SKGap.fieldHessian_variance_intertwine line 232
  29. theorem OAI.SKGap.fieldHessian_variance_mulVec line 244
  30. theorem OAI.SKGap.quadraticForm_eq_dot_mulVec line 256
  31. theorem OAI.SKGap.jacobian_injective_of_hessian_coercive line 261
  32. def OAI.SKGap.vectorNorm line 292
  33. theorem OAI.SKGap.vectorNorm_nonneg line 295
  34. theorem OAI.SKGap.vectorNorm_sq line 297
  35. theorem OAI.SKGap.vectorNorm_add_le line 300
  36. theorem OAI.SKGap.vectorNorm_sub_le line 304
  37. theorem OAI.SKGap.vectorNorm_smul line 308
  38. theorem OAI.SKGap.vector_dot_abs_le line 312
  39. theorem OAI.SKGap.vectorNorm_diag_le line 318
  40. def OAI.SKGap.sqrtVarianceMul line 332
  41. theorem OAI.SKGap.sqrtVarianceMul_norm_le line 335
  42. theorem OAI.SKGap.sqrtVarianceMul_twice line 344
  43. theorem OAI.SKGap.weighted_inverse_bound line 350
  44. theorem OAI.SKGap.hessianCore_mulVec line 373
  45. theorem OAI.SKGap.hessianCore_norm_le line 396
  46. theorem OAI.SKGap.fieldJacobian_mulVec line 442
  47. theorem OAI.SKGap.fieldJacobian_inverse_bound line 451