OAI/Probability/Perceptron/Variational/PiMarkLaw.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.piMarkLaw line 15
  2. lemma OAI.SphericalPerceptronFreeEnergy.fractional_log_moment_sum_pi line 19
  3. theorem OAI.SphericalPerceptronFreeEnergy.finiteCascade_sum_pi line 31
  4. theorem OAI.SphericalPerceptronFreeEnergy.finiteCascade_quadratic_coordinates line 62
  5. def OAI.SphericalPerceptronFreeEnergy.canonicalCoordinateStep line 82
  6. lemma OAI.SphericalPerceptronFreeEnergy.canonicalCoordinateStep_measurable line 86
  7. def OAI.SphericalPerceptronFreeEnergy.canonicalCoordinatePotential line 93
  8. lemma OAI.SphericalPerceptronFreeEnergy.canonicalCoordinatePotential_measurable line 96
  9. lemma OAI.SphericalPerceptronFreeEnergy.canonical_coordinate_spin_log line 99
  10. def OAI.SphericalPerceptronFreeEnergy.canonicalCoordinateLog line 113
  11. lemma OAI.SphericalPerceptronFreeEnergy.canonical_coordinate_recursion line 118
  12. theorem OAI.SphericalPerceptronFreeEnergy.canonical_coordinate_log_mean line 134
  13. lemma OAI.SphericalPerceptronFreeEnergy.canonical_coordinate_log_deviation_le line 147
  14. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_square_memLp_two line 162
  15. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_square_mean line 171
  16. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_square_sum_memLp_two line 176
  17. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_square_sum_mean line 180
  18. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_square_sum_variance line 193
  19. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_square_average_deviation_le line 201
  20. lemma OAI.SphericalPerceptronFreeEnergy.decoratedTerminalTotal_measurable line 219
  21. lemma OAI.SphericalPerceptronFreeEnergy.canonicalCoordinateLog_measurable line 231
  22. lemma OAI.SphericalPerceptronFreeEnergy.product_deviation_le line 238
  23. theorem OAI.SphericalPerceptronFreeEnergy.canonical_coordinate_joint_deviation_le line 263
  24. theorem OAI.SphericalPerceptronFreeEnergy.canonical_coordinate_converges line 309
  25. lemma OAI.SphericalPerceptronFreeEnergy.exponential_ratio_converges line 338
  26. theorem OAI.SphericalPerceptronFreeEnergy.canonical_ratio_converges line 371
  27. lemma OAI.SphericalPerceptronFreeEnergy.canonical_stationary_tail_rates line 389