OAI/Probability/Perceptron/Variational/StableLogIntensity.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.poissonLaplace_map line 14
  2. lemma OAI.SphericalPerceptronFreeEnergy.poissonRandomMeasureLaw_map line 20
  3. def OAI.SphericalPerceptronFreeEnergy.stableLogIntensity line 35
  4. instance OAI.SphericalPerceptronFreeEnergy.stableLogIntensity_sigmaFinite line 38
  5. lemma OAI.SphericalPerceptronFreeEnergy.stableLogDensity_translate line 42
  6. lemma OAI.SphericalPerceptronFreeEnergy.stableLogIntensity_lintegral_translate line 51
  7. lemma OAI.SphericalPerceptronFreeEnergy.stableLogIntensity_translate line 74
  8. def OAI.SphericalPerceptronFreeEnergy.logMarkShift line 82
  9. lemma OAI.SphericalPerceptronFreeEnergy.logMarkShift_measurable line 85
  10. lemma OAI.SphericalPerceptronFreeEnergy.stableLogIntensity_mark_shift line 89
  11. lemma OAI.SphericalPerceptronFreeEnergy.stablePoisson_mark_shift line 107
  12. lemma OAI.SphericalPerceptronFreeEnergy.poissonMeasure_atom_succ line 117
  13. lemma OAI.SphericalPerceptronFreeEnergy.poissonMeasure_mean line 131
  14. lemma OAI.SphericalPerceptronFreeEnergy.finitePointMeasure_lintegral line 144
  15. lemma OAI.SphericalPerceptronFreeEnergy.finitePoissonLaw_campbell line 149
  16. lemma OAI.SphericalPerceptronFreeEnergy.countablePoissonLaw_campbell line 166
  17. lemma OAI.SphericalPerceptronFreeEnergy.poissonRandomMeasureLaw_campbell line 179
  18. lemma OAI.SphericalPerceptronFreeEnergy.ae_ne_top_of_laplace_tendsto line 185
  19. lemma OAI.SphericalPerceptronFreeEnergy.poissonRandomMeasureLaw_lintegral_ne_top line 224
  20. lemma OAI.SphericalPerceptronFreeEnergy.stableLogIntensity_min_exp_finite line 263
  21. lemma OAI.SphericalPerceptronFreeEnergy.stablePoisson_total_finite line 295
  22. lemma OAI.SphericalPerceptronFreeEnergy.stableLogIntensity_univ line 301
  23. lemma OAI.SphericalPerceptronFreeEnergy.poissonRandomMeasureLaw_lintegral_pos_of_infinite line 319
  24. lemma OAI.SphericalPerceptronFreeEnergy.stablePoisson_total_positive line 349
  25. lemma OAI.SphericalPerceptronFreeEnergy.standardGaussian_density_deriv line 355
  26. lemma OAI.SphericalPerceptronFreeEnergy.standardGaussian_density_mul_integrable line 366
  27. def OAI.SphericalPerceptronFreeEnergy.finiteMeasureCutKernel line 376
  28. instance OAI.SphericalPerceptronFreeEnergy.finiteMeasureCutKernel_finite line 381
  29. lemma OAI.SphericalPerceptronFreeEnergy.aemeasurable_measure_lintegral_of_finite line 389
  30. lemma OAI.SphericalPerceptronFreeEnergy.finitePoissonLaw_ae_finite line 409