OAI/Probability/IsingPerceptron/RetainedDisplacement.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Retained Displacement.

  1. lemma OAI.IsingPerceptron.map_powerIntensity_retained line 17
  2. theorem OAI.IsingPerceptron.noiseTreeKeep_independent_law line 68
  3. lemma OAI.IsingPerceptron.measurable_probability_pi line 115
  4. lemma OAI.IsingPerceptron.measurable_probability_infinitePi line 136
  5. def OAI.IsingPerceptron.probabilityReplicaKernel line 161
  6. instance OAI.IsingPerceptron.probabilityReplicaKernel_markov line 165
  7. def OAI.IsingPerceptron.markedReplicaLaw line 173
  8. instance OAI.IsingPerceptron.markedReplicaLaw_probability line 178
  9. def OAI.IsingPerceptron.noiseLeafMark line 194
  10. lemma OAI.IsingPerceptron.measurable_noiseLeafMark line 198
  11. lemma OAI.IsingPerceptron.noiseLeafMark_keep line 207
  12. lemma OAI.IsingPerceptron.noiseLeafMark_labeled line 216
  13. lemma OAI.IsingPerceptron.edgeAt_eq_iff_prefix line 227
  14. lemma OAI.IsingPerceptron.noiseLeafMark_eq_iff_prefix line 233
  15. lemma OAI.IsingPerceptron.sampling_replica_morphism line 250
  16. theorem OAI.IsingPerceptron.labeled_marked_replica_law line 285
  17. lemma OAI.IsingPerceptron.normalizeMass_exp line 323
  18. lemma OAI.IsingPerceptron.normalizeMass_weight_map line 338
  19. lemma OAI.IsingPerceptron.kernel_comap_comp_measure line 359
  20. lemma OAI.IsingPerceptron.replica_mark_transport line 367
  21. lemma OAI.IsingPerceptron.measurable_noiseTiltedLeafLaw line 390
  22. theorem OAI.IsingPerceptron.noise_mark_replica_transport line 400
  23. lemma OAI.IsingPerceptron.measurable_random_withDensity line 442
  24. lemma OAI.IsingPerceptron.regular_product_mass line 453
  25. def OAI.IsingPerceptron.labeledWeight line 490
  26. def OAI.IsingPerceptron.labeledWeightedMass line 495
  27. def OAI.IsingPerceptron.labeledWeightedLeafLaw line 500
  28. instance OAI.IsingPerceptron.labeledWeightedLeafLaw_probability line 505
  29. lemma OAI.IsingPerceptron.measurable_labeledWeight line 510
  30. lemma OAI.IsingPerceptron.measurable_labeledWeightedMass line 519
  31. lemma OAI.IsingPerceptron.measurable_labeledWeightedLeafLaw line 527
  32. theorem OAI.IsingPerceptron.labeled_weighted_marked_replica_law line 535
  33. lemma OAI.IsingPerceptron.gaussianReal_shift_density line 581
  34. def OAI.IsingPerceptron.retainedGaussianScale line 595
  35. lemma OAI.IsingPerceptron.retainedGaussianScale_density line 597
  36. lemma OAI.IsingPerceptron.retainedGaussianScale_normalized line 606
  37. theorem OAI.IsingPerceptron.noiseTreeKeep_gaussian_law line 613
  38. lemma OAI.IsingPerceptron.independent_atomless_injective line 634
  39. lemma OAI.IsingPerceptron.gaussian_marks_injective line 652