OAI/Probability/IsingPerceptron/SamplingIndependent.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

Sampling Independent.

  1. lemma OAI.IsingPerceptron.independent_marks_sampling line 19
  2. abbrev OAI.IsingPerceptron.PrefixPattern line 47
  3. def OAI.IsingPerceptron.labelPrefixPattern line 49
  4. def OAI.IsingPerceptron.markPrefixPattern line 52
  5. lemma OAI.IsingPerceptron.measurable_markPrefixPattern line 55
  6. lemma OAI.IsingPerceptron.markPrefixPattern_labeled line 64
  7. lemma OAI.IsingPerceptron.noiseLeafProduct_exp_marks line 72
  8. lemma OAI.IsingPerceptron.noiseLeafProduct_retained_labeled line 83
  9. lemma OAI.IsingPerceptron.noiseLeafProduct_single_level line 93
  10. lemma OAI.IsingPerceptron.measurable_selected_coordinate line 117
  11. lemma OAI.IsingPerceptron.selected_coordinate_prod_law line 124
  12. lemma OAI.IsingPerceptron.selected_gaussian_score line 145
  13. def OAI.IsingPerceptron.cascadeReplicaLaw line 169
  14. instance OAI.IsingPerceptron.cascadeReplicaLaw_probability line 173
  15. def OAI.IsingPerceptron.replicaMarkPath line 176
  16. lemma OAI.IsingPerceptron.measurable_replicaMarkPath line 179
  17. def OAI.IsingPerceptron.coordinateMarkPath line 185
  18. lemma OAI.IsingPerceptron.measurable_coordinateMarkPath line 188
  19. theorem OAI.IsingPerceptron.marked_path_law line 198
  20. def OAI.IsingPerceptron.retainedLabelLeafLaw line 234
  21. instance OAI.IsingPerceptron.retainedLabelLeafLaw_probability line 239
  22. lemma OAI.IsingPerceptron.measurable_retainedLabelLeafLaw line 243
  23. def OAI.IsingPerceptron.retainedLabelBase line 248
  24. instance OAI.IsingPerceptron.retainedLabelBase_probability line 252
  25. def OAI.IsingPerceptron.retainedLabelJoint line 255
  26. instance OAI.IsingPerceptron.retainedLabelJoint_probability line 260
  27. def OAI.IsingPerceptron.sampledMarkPath line 263
  28. lemma OAI.IsingPerceptron.measurable_sampledMarkPath line 266
  29. theorem OAI.IsingPerceptron.retained_joint_path_law line 270
  30. lemma OAI.IsingPerceptron.tilted_sub_constant line 318
  31. lemma OAI.IsingPerceptron.retainedLabelLeafLaw_single_tilted line 326
  32. def OAI.IsingPerceptron.leafLevelCoefficients line 344
  33. lemma OAI.IsingPerceptron.leafLevelCoefficients_field line 347
  34. lemma OAI.IsingPerceptron.leafLevelCoefficients_bound line 351
  35. lemma OAI.IsingPerceptron.leafLevelCoefficients_diag line 355
  36. lemma OAI.IsingPerceptron.leafLevelCoefficients_cross line 359
  37. def OAI.IsingPerceptron.rawLeafGibbs line 364
  38. instance OAI.IsingPerceptron.rawLeafGibbs_probability line 368
  39. lemma OAI.IsingPerceptron.measurable_rawLeafGibbs line 371
  40. def OAI.IsingPerceptron.rawLabelBase line 380
  41. instance OAI.IsingPerceptron.rawLabelBase_probability line 383
  42. def OAI.IsingPerceptron.rawLabelJoint line 386
  43. instance OAI.IsingPerceptron.rawLabelJoint_probability line 390
  44. lemma OAI.IsingPerceptron.rawLeafGibbs_retained line 393
  45. lemma OAI.IsingPerceptron.rawLeafGibbs_retained_ae line 408
  46. lemma OAI.IsingPerceptron.compProd_base_map line 425
  47. def OAI.IsingPerceptron.rawLabelToRetained line 457
  48. lemma OAI.IsingPerceptron.measurable_rawLabelToRetained line 461
  49. lemma OAI.IsingPerceptron.raw_retained_joint_preserving line 464
  50. lemma OAI.IsingPerceptron.rawJoint_integral_reference line 478
  51. def OAI.IsingPerceptron.pathPrefixPattern line 512
  52. lemma OAI.IsingPerceptron.measurable_pathPrefixPattern line 515
  53. lemma OAI.IsingPerceptron.measurable_labelPrefixPattern line 524
  54. lemma OAI.IsingPerceptron.measurable_infiniteLabelPattern line 527
  55. lemma OAI.IsingPerceptron.pathPrefixPattern_coordinates line 531
  56. def OAI.IsingPerceptron.gaussianMarkedPathLaw line 539
  57. lemma OAI.IsingPerceptron.gaussianMarkedPathLaw_eq line 542
  58. lemma OAI.IsingPerceptron.path_shape_ae_coordinates line 548
  59. theorem OAI.IsingPerceptron.gaussian_marked_shape line 559
  60. theorem OAI.IsingPerceptron.gaussian_marked_shape_score line 579
  61. lemma OAI.IsingPerceptron.selected_gaussian_score_integrable line 614
  62. lemma OAI.IsingPerceptron.gaussian_marked_shape_score_integrable line 632