OAI/Probability/IsingPerceptron/FullPerturbation.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Full Perturbation.

  1. abbrev OAI.IsingPerceptron.Main.FullTensorIndex line 14
  2. def OAI.IsingPerceptron.Main.fullTensorEnumeration line 16
  3. def OAI.IsingPerceptron.Main.tensorAmplitude line 19
  4. def OAI.IsingPerceptron.Main.fullTensorCoefficient line 21
  5. def OAI.IsingPerceptron.Main.fullTensorEnergy line 26
  6. lemma OAI.IsingPerceptron.Main.fullTensorEnergy_eq line 30
  7. def OAI.IsingPerceptron.Main.fullTensorBound line 52
  8. lemma OAI.IsingPerceptron.Main.fullTensorCoefficient_abs line 57
  9. lemma OAI.IsingPerceptron.Main.fullTensorBound_squares line 62
  10. theorem OAI.IsingPerceptron.Main.fullTensor_logPartition_variance line 73
  11. lemma OAI.IsingPerceptron.Main.linearLogPartition_bound line 95
  12. theorem OAI.IsingPerceptron.Main.mixed_logPartition_variance line 109
  13. abbrev OAI.IsingPerceptron.Main.PatternRows line 164
  14. def OAI.IsingPerceptron.Main.rowEvaluation line 166
  15. def OAI.IsingPerceptron.Main.patternEnergy line 169
  16. def OAI.IsingPerceptron.Main.perturbationScale line 172
  17. abbrev OAI.IsingPerceptron.Main.PerturbedDisorder line 174
  18. def OAI.IsingPerceptron.Main.perturbedDisorderLaw line 177
  19. def OAI.IsingPerceptron.Main.perturbedLogPartition line 181
  20. def OAI.IsingPerceptron.Main.omittedPressure line 185
  21. lemma OAI.IsingPerceptron.Main.patternEnergy_bound line 189
  22. lemma OAI.IsingPerceptron.Main.patternEnergy_row_difference line 196
  23. lemma OAI.IsingPerceptron.Main.perturbedLogPartition_variance line 207
  24. lemma OAI.IsingPerceptron.Main.quarter_sum_le line 222
  25. lemma OAI.IsingPerceptron.Main.totalTensor_variance_uniform line 232
  26. lemma OAI.IsingPerceptron.Main.perturbationScale_sq_le line 255
  27. theorem OAI.IsingPerceptron.Main.omittedPressure_variance line 262
  28. lemma OAI.IsingPerceptron.Main.finiteLogPartition_derivative line 294
  29. lemma OAI.IsingPerceptron.Main.finiteGibbs_nonneg line 303
  30. lemma OAI.IsingPerceptron.Main.finiteGibbs_centered_square line 307
  31. lemma OAI.IsingPerceptron.Main.gaussian_parameter_derivative line 315
  32. lemma OAI.IsingPerceptron.Main.gaussian_parameter_thermal_derivative line 324
  33. def OAI.IsingPerceptron.Main.gaussianLinearBound line 336
  34. lemma OAI.IsingPerceptron.Main.gaussianLinearBound_memLp line 340
  35. lemma OAI.IsingPerceptron.Main.gaussianLinear_abs_bound line 347
  36. lemma OAI.IsingPerceptron.Main.gaussianLinearBound_nonneg line 356
  37. lemma OAI.IsingPerceptron.Main.gaussian_logPartition_integrable line 360
  38. theorem OAI.IsingPerceptron.Main.mean_gaussian_parameter_derivative line 377
  39. def OAI.IsingPerceptron.Main.gaussianThermalVariance line 398
  40. lemma OAI.IsingPerceptron.Main.gaussianThermalVariance_nonneg line 403
  41. lemma OAI.IsingPerceptron.Main.gaussianThermalVariance_bound line 407
  42. lemma OAI.IsingPerceptron.Main.gaussianThermalVariance_measurable line 421
  43. lemma OAI.IsingPerceptron.Main.gaussian_mean_energy_integrable line 426
  44. theorem OAI.IsingPerceptron.Main.mean_gaussian_thermal_derivative line 435
  45. lemma OAI.IsingPerceptron.Main.coefficient_cov_bound line 452
  46. theorem OAI.IsingPerceptron.Main.gaussian_mean_energy_bound line 460
  47. lemma OAI.IsingPerceptron.Main.meanThermal_measurable line 489
  48. lemma OAI.IsingPerceptron.Main.meanThermal_intervalIntegrable line 494
  49. theorem OAI.IsingPerceptron.Main.gaussian_thermal_integral line 516
  50. theorem OAI.IsingPerceptron.Main.tensor_thermal_integral line 533
  51. lemma OAI.IsingPerceptron.Main.gaussianThermalVariance_scaled line 544
  52. theorem OAI.IsingPerceptron.Main.tensor_scaled_thermal_integral line 567