OAI/Probability/IsingPerceptron/ConvexDerivativeFluctuation.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Convex Derivative Fluctuation.

  1. lemma OAI.IsingPerceptron.convex_derivative_fluctuation line 14
  2. lemma OAI.IsingPerceptron.minimizer_quadratic_remainder line 44
  3. lemma OAI.IsingPerceptron.integral_convex_derivative_fluctuation line 51
  4. lemma OAI.IsingPerceptron.localMin_second_derivative_nonneg line 92
  5. lemma OAI.IsingPerceptron.localMin_quadratic_stationary line 103
  6. lemma OAI.IsingPerceptron.localMin_quadratic_curvature line 113
  7. theorem OAI.IsingPerceptron.quadratic_minimizer_conditions line 130
  8. lemma OAI.IsingPerceptron.tendsto_central_second_difference line 138
  9. lemma OAI.IsingPerceptron.integrable_limit_of_integral_bound line 164
  10. lemma OAI.IsingPerceptron.central_second_difference_nonneg line 197
  11. theorem OAI.IsingPerceptron.expected_curvature_at_minimum line 206
  12. lemma OAI.IsingPerceptron.mem_interior_integrableExpSet_of_all line 234
  13. lemma OAI.IsingPerceptron.contDiff_cgf_of_all_exp line 240
  14. lemma OAI.IsingPerceptron.convexOn_cgf_of_all_exp line 246
  15. theorem OAI.IsingPerceptron.expected_tilted_variance_at_minimum line 256
  16. lemma OAI.IsingPerceptron.probability_thermal_young line 267
  17. theorem OAI.IsingPerceptron.expected_curvature_at_minimum_ae line 290
  18. theorem OAI.IsingPerceptron.expected_tilted_variance_at_minimum_ae line 325
  19. theorem OAI.IsingPerceptron.integral_convex_derivative_fluctuation_ae line 342
  20. lemma OAI.IsingPerceptron.integral_tilted_ratio line 387
  21. lemma OAI.IsingPerceptron.measurable_random_tilted_integral line 393
  22. lemma OAI.IsingPerceptron.integrate_thermal_majorant line 404
  23. lemma OAI.IsingPerceptron.measurable_random_thermal line 419
  24. theorem OAI.IsingPerceptron.expected_tilted_thermal_at_minimum line 432
  25. theorem OAI.IsingPerceptron.expected_tilted_mean_at_minimum line 459
  26. lemma OAI.IsingPerceptron.probability_energy_triangle line 500
  27. theorem OAI.IsingPerceptron.expected_tilted_energy_at_minimum line 513
  28. theorem OAI.IsingPerceptron.random_gaussian_energy_at_minimum line 558
  29. lemma OAI.IsingPerceptron.tilted_singleton line 586
  30. lemma OAI.IsingPerceptron.replica_tilted_pi line 591
  31. lemma OAI.IsingPerceptron.referenceReplicaMean_eq_tilted line 610