OAI/Probability/IsingPerceptron/PartitionPowLe.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Partition Pow Le.

  1. lemma OAI.IsingPerceptron.partition_pow_le line 15
  2. lemma OAI.IsingPerceptron.exp_integral_le_partition line 25
  3. lemma OAI.IsingPerceptron.partition_inv_pow_le line 34
  4. lemma OAI.IsingPerceptron.gaussian_field_exp_integrable line 54
  5. lemma OAI.IsingPerceptron.abs_le_exp_add_exp_neg line 90
  6. lemma OAI.IsingPerceptron.gaussian_field_integrable line 97
  7. lemma OAI.IsingPerceptron.gaussian_partition_moments line 110
  8. lemma OAI.IsingPerceptron.exp_weighted_abs_fourth_bound line 143
  9. lemma OAI.IsingPerceptron.gaussian_insertion_numerator_fourth line 171
  10. lemma OAI.IsingPerceptron.square_product_le_fourths line 235
  11. theorem OAI.IsingPerceptron.gaussian_gibbs_abs_insertion_second line 240
  12. lemma OAI.IsingPerceptron.log_square_le_partition_moments line 275
  13. lemma OAI.IsingPerceptron.gaussian_log_partition_second line 290
  14. lemma OAI.IsingPerceptron.uniformIntegrable_of_second_moment_bound line 325
  15. lemma OAI.IsingPerceptron.integral_tendsto_of_second_moment_bound line 370
  16. def OAI.IsingPerceptron.normalizedRestriction line 388
  17. lemma OAI.IsingPerceptron.normalizedRestriction_probability line 391
  18. lemma OAI.IsingPerceptron.integral_normalizedRestriction line 399
  19. lemma OAI.IsingPerceptron.integral_restriction_tendsto line 405
  20. lemma OAI.IsingPerceptron.normalized_restriction_integral_tendsto line 417
  21. lemma OAI.IsingPerceptron.normalized_restriction_gibbs_tendsto line 435
  22. theorem OAI.IsingPerceptron.gaussian_log_restriction_expectation_tendsto line 450
  23. lemma OAI.IsingPerceptron.gaussian_bounded_insertion_second line 479
  24. theorem OAI.IsingPerceptron.gaussian_insertion_restriction_expectation_tendsto line 538
  25. lemma OAI.IsingPerceptron.abs_bounded_gibbs_test_le line 573
  26. theorem OAI.IsingPerceptron.gaussian_bounded_restriction_expectation_tendsto line 598