OAI/Probability/SKGap/Localization/ScalarFixedPointJoined.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SKGap.integrable_tanh line 14
  2. theorem OAI.SKGap.integrable_tanh_sq line 18
  3. def OAI.SKGap.oddVariance line 24
  4. lemma OAI.SKGap.abs_oddVariance_le_one line 26
  5. lemma OAI.SKGap.integrable_oddVariance line 33
  6. lemma OAI.SKGap.gaussianPDFReal_diagonal_factor line 38
  7. lemma OAI.SKGap.gaussianPDFReal_diagonal_symmetry line 48
  8. theorem OAI.SKGap.gaussian_nishimori line 56
  9. lemma OAI.SKGap.tanh_nonneg_of_nonneg line 81
  10. lemma OAI.SKGap.tanh_nonpos_of_nonpos line 85
  11. lemma OAI.SKGap.gaussianPDFReal_reflection_le line 89
  12. theorem OAI.SKGap.gaussian_odd_sign line 97
  13. lemma OAI.SKGap.gaussianAverage_hasDerivAt_mean line 133
  14. lemma OAI.SKGap.gaussianAverage_tanh_mean_deriv line 150
  15. lemma OAI.SKGap.gaussianAverage_tanh_diff_deriv line 160
  16. def OAI.SKGap.gaussianF line 189
  17. lemma OAI.SKGap.gaussianF_zero line 191
  18. lemma OAI.SKGap.continuous_gaussianF line 193
  19. lemma OAI.SKGap.gaussianF_eq_square line 197
  20. lemma OAI.SKGap.gaussianF_nonneg line 203
  21. lemma OAI.SKGap.gaussianF_raw_deriv line 207
  22. lemma OAI.SKGap.gaussian_diagonal_stein line 247
  23. lemma OAI.SKGap.gaussianF_deriv line 270
  24. lemma OAI.SKGap.gaussianF_derivative_bounds line 297
  25. lemma OAI.SKGap.gaussianF_lipschitz line 325
  26. lemma OAI.SKGap.gaussianF_le_self line 337
  27. lemma OAI.SKGap.gaussianF_le_one line 343
  28. lemma OAI.SKGap.gaussian_mean_lipschitz line 349
  29. lemma OAI.SKGap.gaussian_mean_zero line 366
  30. lemma OAI.SKGap.gaussian_mean_fixed_nonneg line 375
  31. lemma OAI.SKGap.gaussian_H_derivative_bounds line 386
  32. lemma OAI.SKGap.gaussian_H_lipschitz line 416
  33. lemma OAI.SKGap.gaussian_H_diagonal_zero line 425
  34. lemma OAI.SKGap.consistent_gaussian_diagonal line 433
  35. lemma OAI.SKGap.gaussianF_pos line 458
  36. lemma OAI.SKGap.gaussian_fixed_unique line 472
  37. lemma OAI.SKGap.exists_gaussian_fixed line 483
  38. def OAI.SKGap.scalarFixedPoint line 496
  39. lemma OAI.SKGap.scalarFixedPoint_spec line 499
  40. lemma OAI.SKGap.scalarFixedPoint_bounds line 504
  41. lemma OAI.SKGap.scalarFixedPoint_zero line 512
  42. lemma OAI.SKGap.scalarFixedPoint_lipschitz line 517
  43. lemma OAI.SKGap.consistent_gaussian_unique line 534
  44. def OAI.SKGap.scalarQ line 549
  45. lemma OAI.SKGap.scalarQ_spec line 551
  46. lemma OAI.SKGap.scalar_fixed_pos line 560