OAI/Probability/IsingPerceptron/NoiseGibbsRegular.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Noise Gibbs Regular.

  1. def OAI.IsingPerceptron.NoiseGibbsRegular line 15
  2. lemma OAI.IsingPerceptron.measurableSet_noiseGibbsRegular line 28
  3. lemma OAI.IsingPerceptron.noiseGibbsRegular_ae line 77
  4. lemma OAI.IsingPerceptron.noiseLeafKernel_unnormalized_lintegral line 121
  5. theorem OAI.IsingPerceptron.noiseWeightedLeafMeasure_eq line 130
  6. lemma OAI.IsingPerceptron.normalizeMass_of_probability line 226
  7. lemma OAI.IsingPerceptron.normalizeMass_smul line 230
  8. lemma OAI.IsingPerceptron.NoiseGibbsRegular.masses line 247
  9. def OAI.IsingPerceptron.noiseTiltedLeafLaw line 257
  10. instance OAI.IsingPerceptron.noiseTiltedLeafLaw_probability line 261
  11. theorem OAI.IsingPerceptron.noiseTiltedLeafLaw_keep line 265
  12. lemma OAI.IsingPerceptron.noiseLeafProduct_telescoping line 308
  13. lemma OAI.IsingPerceptron.normalizeMass_smul_any line 329
  14. def OAI.IsingPerceptron.noiseTerminalGibbsLaw line 350
  15. lemma OAI.IsingPerceptron.noiseTerminalGibbsLaw_eq_tilted line 355
  16. theorem OAI.IsingPerceptron.noiseTerminalGibbsLaw_keep line 376
  17. lemma OAI.IsingPerceptron.infinitePi_prod_join line 394
  18. def OAI.IsingPerceptron.labeledPoissonLaw line 410
  19. instance OAI.IsingPerceptron.labeledPoissonLaw_probability line 414
  20. def OAI.IsingPerceptron.labeledPoissonMeasure line 419
  21. lemma OAI.IsingPerceptron.measurable_labeledPoissonMeasure line 423
  22. lemma OAI.IsingPerceptron.labeledPoissonMeasure_lintegral line 428
  23. lemma OAI.IsingPerceptron.labeledPoissonLaw_push line 433
  24. lemma OAI.IsingPerceptron.finitePoissonProduct_laplace_partial line 446
  25. theorem OAI.IsingPerceptron.finitePoissonProduct_sum_law line 469
  26. theorem OAI.IsingPerceptron.labeledPoissonLaw_law line 493
  27. lemma OAI.IsingPerceptron.finiteCloud_laplace line 499
  28. lemma OAI.IsingPerceptron.finiteCloud_mark_law line 530
  29. lemma OAI.IsingPerceptron.finiteCloud_mark_measure_law line 544
  30. def OAI.IsingPerceptron.labeledMarkedMeasure line 566
  31. lemma OAI.IsingPerceptron.measurable_labeledMarkedMeasure line 570
  32. theorem OAI.IsingPerceptron.labeledMarkedMeasure_law line 578