OAI/Probability/IsingPerceptron/CascadeFreshMoments.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Cascade Fresh Moments.

  1. lemma OAI.IsingPerceptron.freshPatternFactor_replica_moment line 16
  2. def OAI.IsingPerceptron.cascadeFreshFactor line 40
  3. lemma OAI.IsingPerceptron.measurable_cascadeFreshFactor line 46
  4. lemma OAI.IsingPerceptron.cascadeFreshFactor_bound line 52
  5. theorem OAI.IsingPerceptron.cascadeFreshFactor_moment line 59
  6. lemma OAI.IsingPerceptron.measurable_scalar_root_factor line 93
  7. lemma OAI.IsingPerceptron.scalarFreshFactor_nodes line 113
  8. lemma OAI.IsingPerceptron.scalarFresh_log_bound line 123
  9. theorem OAI.IsingPerceptron.scalarFresh_log_recursion line 132
  10. theorem OAI.IsingPerceptron.cascadeFresh_log_value line 181
  11. lemma OAI.IsingPerceptron.cell_subset_unit line 209
  12. lemma OAI.IsingPerceptron.uniformCellAverage_eq_cellAverage line 218
  13. lemma OAI.IsingPerceptron.uniformPattern_root_tail line 229
  14. lemma OAI.IsingPerceptron.cascadeFresh_uniformPattern line 252
  15. def OAI.IsingPerceptron.unitClip line 279
  16. lemma OAI.IsingPerceptron.unitClip_mem line 280
  17. lemma OAI.IsingPerceptron.unitClip_eq line 282
  18. lemma OAI.IsingPerceptron.continuous_unitClip line 284
  19. def OAI.IsingPerceptron.scalarJointEntry line 286
  20. lemma OAI.IsingPerceptron.continuous_scalarJointEntry line 288
  21. def OAI.IsingPerceptron.compactScalarArray line 292
  22. lemma OAI.IsingPerceptron.continuous_compactScalarArray line 293
  23. lemma OAI.IsingPerceptron.spinArray_compactScalarArray line 297
  24. def OAI.IsingPerceptron.cascadeCompactLaw line 302
  25. lemma OAI.IsingPerceptron.cascade_patch_mem line 306
  26. lemma OAI.IsingPerceptron.cascadeCompact_spin line 314
  27. lemma OAI.IsingPerceptron.cascade_integral_GG line 332
  28. lemma OAI.IsingPerceptron.cascade_patch_integral_GG line 351
  29. lemma OAI.IsingPerceptron.cascadeCompact_integral line 387
  30. lemma OAI.IsingPerceptron.cascadeCompact_residual line 395
  31. lemma OAI.IsingPerceptron.cascadeCompact_limit_GG line 410
  32. lemma OAI.IsingPerceptron.cascade_patch_gram line 429
  33. lemma OAI.IsingPerceptron.cascade_patch_ultra line 453
  34. lemma OAI.IsingPerceptron.cascadeCompact_geometry line 460
  35. lemma OAI.IsingPerceptron.cascadeCompact_limit_geometry line 477
  36. lemma OAI.IsingPerceptron.cellAverage_integral_tendsto line 499
  37. lemma OAI.IsingPerceptron.cascadeCompact_pair_integral line 513
  38. lemma OAI.IsingPerceptron.cascadeCompact_limit_pairLaw line 533
  39. lemma OAI.IsingPerceptron.gaussianMoment_blockLaw line 556
  40. lemma OAI.IsingPerceptron.gaussianMoment_blockLaw_congr line 569
  41. lemma OAI.IsingPerceptron.cascadeFreshFactor_compact_moment line 580
  42. theorem OAI.IsingPerceptron.cascadeFresh_moments_tendsto line 613