OAI/Probability/IsingPerceptron/MonomialGgAtMinimum.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Monomial Gg At Minimum.

  1. theorem OAI.IsingPerceptron.monomial_gg_at_minimum line 14
  2. def OAI.IsingPerceptron.logMean line 51
  3. lemma OAI.IsingPerceptron.integral_exp_pos line 54
  4. theorem OAI.IsingPerceptron.logMean_normalized_moment line 61
  5. lemma OAI.IsingPerceptron.logMean_bounds line 80
  6. def OAI.IsingPerceptron.cascadeRecursion line 120
  7. lemma OAI.IsingPerceptron.measurable_cascadeRecursion line 127
  8. lemma OAI.IsingPerceptron.cascadeRecursion_bound line 140
  9. def OAI.IsingPerceptron.stoppedUpdate line 155
  10. lemma OAI.IsingPerceptron.measurable_stoppedUpdate line 158
  11. def OAI.IsingPerceptron.backwardValue line 165
  12. lemma OAI.IsingPerceptron.measurable_backwardValue line 170
  13. lemma OAI.IsingPerceptron.backwardValue_step line 177
  14. lemma OAI.IsingPerceptron.backwardValue_terminal line 186
  15. theorem OAI.IsingPerceptron.backwardValue_multiplier_moment line 191
  16. def OAI.IsingPerceptron.terminalTreeFactor line 224
  17. lemma OAI.IsingPerceptron.noiseTreeFactor_terminal line 234
  18. lemma OAI.IsingPerceptron.terminalTreeFactor_update_congr line 247
  19. lemma OAI.IsingPerceptron.backwardValue_treeFactor line 262
  20. theorem OAI.IsingPerceptron.bounded_noiseCascade_recursion line 272
  21. lemma OAI.IsingPerceptron.backwardValue_multiplier_moment_admissible line 297
  22. theorem OAI.IsingPerceptron.admissible_noiseCascade_recursion line 315
  23. lemma OAI.IsingPerceptron.logMean_mono line 345
  24. lemma OAI.IsingPerceptron.logMean_const_add line 355
  25. def OAI.IsingPerceptron.ExponentialNormMoments line 369
  26. def OAI.IsingPerceptron.HasLinearGrowth line 372
  27. lemma OAI.IsingPerceptron.integrable_exp_of_linearGrowth line 376
  28. lemma OAI.IsingPerceptron.HasLinearGrowth.add_left line 393
  29. lemma OAI.IsingPerceptron.linearGrowth_norm_mul line 403
  30. lemma OAI.IsingPerceptron.logMean_hasLinearGrowth line 407
  31. lemma OAI.IsingPerceptron.cascadeRecursion_linearGrowth line 452
  32. lemma OAI.IsingPerceptron.backwardValue_linearGrowth_moments line 466
  33. lemma OAI.IsingPerceptron.gaussianReal_exponentialNormMoments line 484
  34. theorem OAI.IsingPerceptron.linearGrowth_noiseCascade_recursion line 493
  35. lemma OAI.IsingPerceptron.abs_log_cosh_le line 512
  36. lemma OAI.IsingPerceptron.logCosh_linearGrowth line 524
  37. lemma OAI.IsingPerceptron.measurable_logCosh line 528
  38. theorem OAI.IsingPerceptron.gaussian_logCosh_cascade line 531
  39. lemma OAI.IsingPerceptron.logMean_const_add_integrable line 548
  40. lemma OAI.IsingPerceptron.logMean_abs_sub_le line 554
  41. theorem OAI.IsingPerceptron.cascadeRecursion_lipschitz line 570