OAI/Probability/IsingPerceptron/WeightedPartitionNumeratorIncrement.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Weighted Partition Numerator Increment.

  1. theorem OAI.IsingPerceptron.weightedPartitionNumerator_increment line 15
  2. theorem OAI.IsingPerceptron.weightedPartitionNumerator_descendant_congr line 39
  3. def OAI.IsingPerceptron.poissonFiberIntegral line 66
  4. lemma OAI.IsingPerceptron.measurable_poissonFiberIntegral line 71
  5. lemma OAI.IsingPerceptron.poissonLaw_fiber_null line 81
  6. lemma OAI.IsingPerceptron.poissonFiberIntegral_insert line 88
  7. theorem OAI.IsingPerceptron.poissonFiberIntegral_eq_ae line 105
  8. def OAI.IsingPerceptron.noiseTreeSpace line 136
  9. abbrev OAI.IsingPerceptron.NoiseTree line 142
  10. instance OAI.IsingPerceptron.noiseTreeMeasurableSpace line 143
  11. instance OAI.IsingPerceptron.noiseTreeNonempty line 144
  12. def OAI.IsingPerceptron.noiseCascadeLaw line 150
  13. lemma OAI.IsingPerceptron.noiseCascadeLaw_succ line 159
  14. def OAI.IsingPerceptron.noiseTreeForget line 164
  15. lemma OAI.IsingPerceptron.measurable_noiseTreeForget line 169
  16. lemma OAI.IsingPerceptron.noiseCascadeLaw_forget line 175
  17. def OAI.IsingPerceptron.noiseTreeTotal line 200
  18. lemma OAI.IsingPerceptron.measurable_noiseTreeTotal line 203
  19. lemma OAI.IsingPerceptron.noiseTreeTotal_succ line 207
  20. lemma OAI.IsingPerceptron.measurable_map_sigmaPart_param line 221
  21. def OAI.IsingPerceptron.noiseTreeDisplace line 238
  22. lemma OAI.IsingPerceptron.measurable_noiseTreeDisplace line 248
  23. lemma OAI.IsingPerceptron.map_powerIntensity_subtree line 273
  24. theorem OAI.IsingPerceptron.noiseTreeDisplace_law line 316
  25. lemma OAI.IsingPerceptron.integrable_of_square line 364
  26. lemma OAI.IsingPerceptron.integral_difference_same_law line 375
  27. theorem OAI.IsingPerceptron.noiseTreeDisplace_log_ratio line 418
  28. def OAI.IsingPerceptron.noiseTreeFactor line 442
  29. lemma OAI.IsingPerceptron.measurable_noiseTreeFactor line 452
  30. theorem OAI.IsingPerceptron.noiseTreeDisplace_total line 470
  31. lemma OAI.IsingPerceptron.noiseTreeFactor_total_identity line 527
  32. theorem OAI.IsingPerceptron.noiseCascade_log_integral line 538