OAI/Probability/IsingPerceptron/MomentLogLimit.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Moment Log Limit.

  1. lemma OAI.IsingPerceptron.integrable_pow_of_pos_bounds line 17
  2. lemma OAI.IsingPerceptron.integral_polynomial_of_pos_bounds line 26
  3. lemma OAI.IsingPerceptron.integral_log_polynomial_error line 34
  4. theorem OAI.IsingPerceptron.tendsto_integral_log_of_moments line 56
  5. theorem OAI.IsingPerceptron.exists_positive_factor_of_moments line 110
  6. lemma OAI.IsingPerceptron.factor_log_converges_of_moments line 134
  7. theorem OAI.IsingPerceptron.patternFunctional_factor_law line 161
  8. theorem OAI.IsingPerceptron.freshLog_tendsto_patternFunctional line 189
  9. theorem OAI.IsingPerceptron.uniformPattern_tendsto line 225
  10. lemma OAI.IsingPerceptron.uniformNodal_congr line 255
  11. lemma OAI.IsingPerceptron.uniformNodal_tail_weights line 265
  12. lemma OAI.IsingPerceptron.uniformPattern_tail_comparison line 292
  13. lemma OAI.IsingPerceptron.tail_integral_representative line 314
  14. theorem OAI.IsingPerceptron.patternFunctional_tail_order line 326
  15. lemma OAI.IsingPerceptron.monotone_tail_chord_lower line 354
  16. lemma OAI.IsingPerceptron.monotone_tail_of_cell line 374
  17. lemma OAI.IsingPerceptron.path_tail_interval line 408
  18. lemma OAI.IsingPerceptron.finite_partition_cell line 417
  19. lemma OAI.IsingPerceptron.intervalIntegral_const_of_ae_cell line 440
  20. lemma OAI.IsingPerceptron.monotone_tail_of_ae_cell line 453
  21. lemma OAI.IsingPerceptron.nodal_tails_imply_all_tails line 469
  22. lemma OAI.IsingPerceptron.overlapArrayLaw_gram line 511
  23. theorem OAI.IsingPerceptron.freshPattern_array_limit line 536
  24. lemma OAI.IsingPerceptron.prefix_next_preserving line 591
  25. theorem OAI.IsingPerceptron.integral_next_row_of_prefix line 607