OAI/Probability/IsingPerceptron/ActualQuenched.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Actual Quenched.

  1. def OAI.IsingPerceptron.Main.blockEnergy line 16
  2. theorem OAI.IsingPerceptron.Main.block_quenched_integral line 20
  3. def OAI.IsingPerceptron.Main.selectedParameter line 46
  4. lemma OAI.IsingPerceptron.Main.fullTensorCoefficient_update line 48
  5. lemma OAI.IsingPerceptron.Main.fullTensorCoefficient_disjoint line 59
  6. lemma OAI.IsingPerceptron.Main.selectedTensorBound_squares line 71
  7. lemma OAI.IsingPerceptron.Main.fullTensorCard_pos line 82
  8. def OAI.IsingPerceptron.Main.selectedTensorEnergy line 87
  9. lemma OAI.IsingPerceptron.Main.selectedTensorEnergy_eq_block line 92
  10. theorem OAI.IsingPerceptron.Main.selectedTensor_quenched_integral line 103
  11. lemma OAI.IsingPerceptron.Main.affine_mean_thermal_intervalIntegrable line 153
  12. theorem OAI.IsingPerceptron.Main.affine_mean_thermal_integral line 169
  13. def OAI.IsingPerceptron.Main.blockThermal line 183
  14. theorem OAI.IsingPerceptron.Main.block_thermal_integral line 188
  15. def OAI.IsingPerceptron.Main.selectedTensorThermal line 211
  16. lemma OAI.IsingPerceptron.Main.selectedTensorThermal_eq_block line 216
  17. theorem OAI.IsingPerceptron.Main.selectedTensor_thermal_integral line 229
  18. lemma OAI.IsingPerceptron.Main.finiteGibbs_mono line 242
  19. lemma OAI.IsingPerceptron.Main.finiteGibbs_abs_young line 246
  20. lemma OAI.IsingPerceptron.Main.mean_uniform_intervalIntegrable line 254
  21. def OAI.IsingPerceptron.Main.affineThermalAbs line 270
  22. lemma OAI.IsingPerceptron.Main.affineThermalAbs_measurable line 276
  23. lemma OAI.IsingPerceptron.Main.affineThermalAbs_bound line 283
  24. lemma OAI.IsingPerceptron.Main.affineThermalAbs_integrable line 290
  25. theorem OAI.IsingPerceptron.Main.affine_thermal_abs_integral line 298
  26. def OAI.IsingPerceptron.Main.affineDeviation line 329
  27. lemma OAI.IsingPerceptron.Main.affineDeviation_measurable line 335
  28. lemma OAI.IsingPerceptron.Main.affineDeviation_bound line 348
  29. lemma OAI.IsingPerceptron.Main.affineDeviation_integrable line 364
  30. lemma OAI.IsingPerceptron.Main.affineDeviation_split line 372
  31. theorem OAI.IsingPerceptron.Main.orthogonal_block_deviation_integral line 383
  32. def OAI.IsingPerceptron.Main.blockDeviation line 429
  33. theorem OAI.IsingPerceptron.Main.block_deviation_integral line 435
  34. def OAI.IsingPerceptron.Main.selectedTensorDeviation line 463
  35. lemma OAI.IsingPerceptron.Main.selectedTensorDeviation_eq_block line 469
  36. lemma OAI.IsingPerceptron.Main.selectedTensor_update_bound line 483
  37. theorem OAI.IsingPerceptron.Main.selectedTensor_deviation_integral line 502
  38. def OAI.IsingPerceptron.Main.selectedTensorObservable line 544
  39. lemma OAI.IsingPerceptron.Main.fullTensorEnergy_selected line 548
  40. def OAI.IsingPerceptron.Main.rawTensorMean line 560
  41. def OAI.IsingPerceptron.Main.rawTensorDeviation line 565
  42. lemma OAI.IsingPerceptron.Main.selectedTensorEnergy_scale line 571
  43. lemma OAI.IsingPerceptron.Main.selectedTensorDeviation_scale line 580
  44. theorem OAI.IsingPerceptron.Main.rawTensor_deviation_integral line 587