OAI/Probability/IsingPerceptron/JointShapes.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Joint Shapes.

  1. lemma OAI.IsingPerceptron.retained_joint_shape_ae line 18
  2. lemma OAI.IsingPerceptron.measurable_sampledLabelPattern line 31
  3. theorem OAI.IsingPerceptron.retained_joint_shape line 36
  4. theorem OAI.IsingPerceptron.retained_joint_shape_score line 53
  5. lemma OAI.IsingPerceptron.prefixPattern_bound line 83
  6. lemma OAI.IsingPerceptron.retained_joint_shape_score_integrable line 89
  7. lemma OAI.IsingPerceptron.raw_joint_shape_score_integrable line 106
  8. lemma OAI.IsingPerceptron.raw_joint_shape line 118
  9. lemma OAI.IsingPerceptron.raw_joint_shape_score line 128
  10. lemma OAI.IsingPerceptron.randomReplicaAverage_shape line 138
  11. lemma OAI.IsingPerceptron.randomReplicaEnergy_shape line 151
  12. def OAI.IsingPerceptron.prefixPatternMean line 171
  13. def OAI.IsingPerceptron.patternReindex line 174
  14. def OAI.IsingPerceptron.boolReal line 177
  15. lemma OAI.IsingPerceptron.patternReindex_label line 179
  16. lemma OAI.IsingPerceptron.leafLevelCoefficients_cross_bool line 182
  17. lemma OAI.IsingPerceptron.prefixPatternMean_const line 189
  18. theorem OAI.IsingPerceptron.cascade_prefix_gg line 193
  19. lemma OAI.IsingPerceptron.prefix_pair_mean line 226
  20. lemma OAI.IsingPerceptron.replica_injective_map_reindex line 242
  21. lemma OAI.IsingPerceptron.replicaLaw_integral_injective_eq line 252
  22. lemma OAI.IsingPerceptron.cascadeReplicaLaw_eq_replicaLaw line 276
  23. lemma OAI.IsingPerceptron.cascade_integral_injective line 281
  24. lemma OAI.IsingPerceptron.prefixPatternMean_injective line 299
  25. lemma OAI.IsingPerceptron.prefixPatternMean_congr line 306
  26. lemma OAI.IsingPerceptron.prefixPatternMean_integrable line 311
  27. lemma OAI.IsingPerceptron.prefixPatternMean_add line 317
  28. lemma OAI.IsingPerceptron.prefixPatternMean_sub line 321
  29. lemma OAI.IsingPerceptron.prefixPatternMean_mul line 325
  30. lemma OAI.IsingPerceptron.prefixPatternMean_sum line 328
  31. def OAI.IsingPerceptron.lastToFront line 332
  32. lemma OAI.IsingPerceptron.lastToFront_injective line 334
  33. lemma OAI.IsingPerceptron.prefix_fresh_reindex line 342
  34. lemma OAI.IsingPerceptron.cascade_prefix_gg_first line 354
  35. lemma OAI.IsingPerceptron.prefixPatternMean_perm line 373
  36. lemma OAI.IsingPerceptron.patternReindex_perm_cancel line 380
  37. lemma OAI.IsingPerceptron.prefix_fresh_permuted line 385
  38. lemma OAI.IsingPerceptron.prefix_old_permuted line 400
  39. lemma OAI.IsingPerceptron.cascade_prefix_gg_all line 413
  40. def OAI.IsingPerceptron.prefixVectorValue line 434
  41. lemma OAI.IsingPerceptron.sum_prefix_telescope line 437
  42. lemma OAI.IsingPerceptron.prefixVectorValue_label line 465
  43. lemma OAI.IsingPerceptron.prefixPatternMean_restrict line 487
  44. def OAI.IsingPerceptron.prefixGGResidual line 490
  45. lemma OAI.IsingPerceptron.prefixGGResidual_const line 504
  46. lemma OAI.IsingPerceptron.prefix_pair_mean_01 line 512
  47. lemma OAI.IsingPerceptron.prefixGGResidual_level line 519
  48. lemma OAI.IsingPerceptron.prefixGGResidual_value line 533
  49. def OAI.IsingPerceptron.cascadeScalarArray line 553
  50. lemma OAI.IsingPerceptron.measurable_cascadeScalarArray line 556
  51. lemma OAI.IsingPerceptron.prefixVectorValue_pattern line 563
  52. lemma OAI.IsingPerceptron.integral_ite_one_eq line 567
  53. lemma OAI.IsingPerceptron.integral_ite_one_mul_eq line 572
  54. theorem OAI.IsingPerceptron.cascade_scalar_gg line 583