OAI/Probability/IsingPerceptron/ConvexFluctuation.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Convex Fluctuation.

  1. lemma OAI.IsingPerceptron.Main.convex_derivative_deviation line 14
  2. lemma OAI.IsingPerceptron.Main.integrated_derivative_shift_le line 45
  3. lemma OAI.IsingPerceptron.Main.integral_abs_centered_le_sqrt_variance line 71
  4. lemma OAI.IsingPerceptron.Main.expected_convex_derivative_deviation line 81
  5. theorem OAI.IsingPerceptron.Main.integrated_convex_derivative_deviation line 116
  6. lemma OAI.IsingPerceptron.Main.gaussian_logPartition_convex line 140
  7. lemma OAI.IsingPerceptron.Main.mean_gaussian_logPartition_convex line 151
  8. lemma OAI.IsingPerceptron.Main.gaussian_perturbation_mean_cost line 169
  9. lemma OAI.IsingPerceptron.Main.random_linearLogPartition_memLp line 201
  10. theorem OAI.IsingPerceptron.Main.random_gaussian_perturbation_mean_cost line 218
  11. theorem OAI.IsingPerceptron.Main.actual_perturbation_mean_cost line 232
  12. def OAI.IsingPerceptron.Main.fullPerturbedPressure line 246
  13. lemma OAI.IsingPerceptron.Main.perturbationScale_sq_div line 250
  14. theorem OAI.IsingPerceptron.Main.fullPerturbedPressure_mean_cost line 259
  15. abbrev OAI.IsingPerceptron.Main.affineDisorderLaw line 288
  16. def OAI.IsingPerceptron.Main.affineHamiltonian line 291
  17. def OAI.IsingPerceptron.Main.affineLogPartition line 295
  18. def OAI.IsingPerceptron.Main.affineEnergy line 298
  19. def OAI.IsingPerceptron.Main.affineThermal line 302
  20. lemma OAI.IsingPerceptron.Main.affineHamiltonian_eq line 308
  21. lemma OAI.IsingPerceptron.Main.affineLogPartition_derivative line 320
  22. lemma OAI.IsingPerceptron.Main.affineEnergy_derivative line 326
  23. lemma OAI.IsingPerceptron.Main.affineEnergy_bound line 332
  24. lemma OAI.IsingPerceptron.Main.affineThermal_bound line 337
  25. lemma OAI.IsingPerceptron.Main.affineEnergy_measurable line 342
  26. lemma OAI.IsingPerceptron.Main.affineThermal_measurable line 349
  27. lemma OAI.IsingPerceptron.Main.affineEnergy_integrable line 355
  28. lemma OAI.IsingPerceptron.Main.affineThermal_integrable line 363
  29. lemma OAI.IsingPerceptron.Main.affineLogPartition_memLp line 370
  30. lemma OAI.IsingPerceptron.Main.mean_affineLogPartition_derivative line 384
  31. lemma OAI.IsingPerceptron.Main.mean_affineEnergy_derivative line 399
  32. lemma OAI.IsingPerceptron.Main.gaussian_orthogonal_mean_energy_bound line 414
  33. theorem OAI.IsingPerceptron.Main.affine_mean_energy_bound line 441
  34. lemma OAI.IsingPerceptron.Main.affineLogPartition_convex line 458
  35. lemma OAI.IsingPerceptron.Main.mean_affineLogPartition_convex line 462
  36. lemma OAI.IsingPerceptron.Main.affine_centeredEnergy_intervalIntegrable line 476
  37. theorem OAI.IsingPerceptron.Main.orthogonal_block_quenched_integral line 506