OAI/Probability/IsingPerceptron/NoiseTreeKeep.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Noise Tree Keep.

  1. def OAI.IsingPerceptron.noiseTreeKeep line 15
  2. lemma OAI.IsingPerceptron.measurable_noiseTreeKeep line 25
  3. lemma OAI.IsingPerceptron.noiseTreeKeep_forget line 44
  4. lemma OAI.IsingPerceptron.map_powerIntensity_keep_subtree line 69
  5. theorem OAI.IsingPerceptron.noiseTreeKeep_law_succ line 114
  6. lemma OAI.IsingPerceptron.measurable_measure_ae line 158
  7. lemma OAI.IsingPerceptron.normalizeMass_map line 163
  8. lemma OAI.IsingPerceptron.withDensity_map_pullback line 171
  9. def OAI.IsingPerceptron.GoodNoiseTree line 187
  10. lemma OAI.IsingPerceptron.measurableSet_GoodNoiseTree line 193
  11. lemma OAI.IsingPerceptron.noiseCascade_good line 201
  12. def OAI.IsingPerceptron.noiseChildMass line 227
  13. lemma OAI.IsingPerceptron.noiseChildMass_univ line 231
  14. lemma OAI.IsingPerceptron.measurable_noiseChildMass line 237
  15. def OAI.IsingPerceptron.noiseChildKernel line 241
  16. instance OAI.IsingPerceptron.noiseChildKernel_markov line 245
  17. def OAI.IsingPerceptron.NoiseLeaf line 248
  18. instance OAI.IsingPerceptron.noiseLeafMeasurableSpace line 252
  19. instance OAI.IsingPerceptron.noiseLeafNonempty line 257
  20. def OAI.IsingPerceptron.noiseLeafKernelData line 262
  21. def OAI.IsingPerceptron.noiseLeafKernel line 273
  22. instance OAI.IsingPerceptron.noiseLeafKernel_markov line 275
  23. def OAI.IsingPerceptron.noiseLeafForget line 278
  24. lemma OAI.IsingPerceptron.measurable_noiseLeafForget line 283
  25. lemma OAI.IsingPerceptron.noiseChildMass_forget line 295
  26. lemma OAI.IsingPerceptron.noiseChildKernel_forget line 308
  27. lemma OAI.IsingPerceptron.noiseChildKernel_ae line 319
  28. lemma OAI.IsingPerceptron.noiseLeafKernel_succ line 327
  29. lemma OAI.IsingPerceptron.noiseLeafKernel_step line 331
  30. lemma OAI.IsingPerceptron.rawLeafKernel_step line 349
  31. theorem OAI.IsingPerceptron.noiseLeafKernel_forget line 360
  32. def OAI.IsingPerceptron.noiseLeafTerminal line 394
  33. lemma OAI.IsingPerceptron.measurable_noiseLeafTerminal line 401
  34. lemma OAI.IsingPerceptron.noiseChildKernel_lintegral line 410
  35. lemma OAI.IsingPerceptron.noiseLeafKernel_lintegral line 425
  36. lemma OAI.IsingPerceptron.measurable_noiseLeafIntegral line 437
  37. theorem OAI.IsingPerceptron.noiseTreeFactor_leafIntegral line 445
  38. def OAI.IsingPerceptron.noiseLeafProduct line 505
  39. def OAI.IsingPerceptron.noiseLeafKeep line 511
  40. lemma OAI.IsingPerceptron.measurable_noiseLeafProduct line 518
  41. lemma OAI.IsingPerceptron.measurable_noiseLeafKeep line 529
  42. def OAI.IsingPerceptron.noiseWeightedLeafMeasure line 540
  43. lemma OAI.IsingPerceptron.noiseWeightedLeafMeasure_lintegral line 545
  44. lemma OAI.IsingPerceptron.measurable_noiseWeightedLeafMeasure line 563
  45. lemma OAI.IsingPerceptron.measurable_noiseUnnormalizedLeaf line 583