OAI/Probability/IsingPerceptron/MapWithDensityEquiv.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Map With Density Equiv.

  1. lemma OAI.IsingPerceptron.map_withDensity_equiv line 14
  2. def OAI.IsingPerceptron.powerIntensityDensity line 30
  3. def OAI.IsingPerceptron.powerIntensity line 33
  4. lemma OAI.IsingPerceptron.measurable_powerIntensityDensity line 35
  5. lemma OAI.IsingPerceptron.powerIntensityDensity_scale line 42
  6. theorem OAI.IsingPerceptron.map_powerIntensity_mul line 65
  7. instance OAI.IsingPerceptron.powerIntensity_sigmaFinite line 84
  8. theorem OAI.IsingPerceptron.map_marked_powerIntensity line 88
  9. lemma OAI.IsingPerceptron.poissonLaw_congr line 114
  10. theorem OAI.IsingPerceptron.poissonLaw_marked_power line 119
  11. lemma OAI.IsingPerceptron.integrable_power_min line 131
  12. def OAI.IsingPerceptron.stableLaplaceCost line 167
  13. def OAI.IsingPerceptron.stableLaplaceConstant line 169
  14. lemma OAI.IsingPerceptron.measurable_stableLaplaceCost line 172
  15. lemma OAI.IsingPerceptron.stableLaplaceCost_nonneg line 176
  16. lemma OAI.IsingPerceptron.stableLaplaceCost_le_min line 180
  17. lemma OAI.IsingPerceptron.integrable_stableLaplaceCost line 185
  18. lemma OAI.IsingPerceptron.stableLaplaceConstant_lt_top line 192
  19. lemma OAI.IsingPerceptron.stableLaplaceConstant_pos line 197
  20. lemma OAI.IsingPerceptron.integrable_negExp line 219
  21. lemma OAI.IsingPerceptron.measure_zero_of_integral_tests line 228
  22. theorem OAI.IsingPerceptron.stable_laplace_finite_positive line 244
  23. def OAI.IsingPerceptron.poissonTotal line 294
  24. lemma OAI.IsingPerceptron.measurable_poissonTotal line 296
  25. lemma OAI.IsingPerceptron.stableLaplaceCost_scale line 299
  26. lemma OAI.IsingPerceptron.powerIntensity_laplace_scale line 307
  27. theorem OAI.IsingPerceptron.poissonTotal_laplace line 315
  28. theorem OAI.IsingPerceptron.poissonTotal_finite_positive line 323
  29. lemma OAI.IsingPerceptron.integrable_exp_neg_mul line 336
  30. lemma OAI.IsingPerceptron.measureReal_mul_le_integral line 345
  31. lemma OAI.IsingPerceptron.stable_laplace_upper_tail line 356
  32. lemma OAI.IsingPerceptron.stable_laplace_inverse_tail line 391
  33. lemma OAI.IsingPerceptron.integrable_rpow_of_power_tail line 416
  34. lemma OAI.IsingPerceptron.integrable_rpow_of_exp_tail line 464
  35. lemma OAI.IsingPerceptron.log_sq_le_powers line 491
  36. theorem OAI.IsingPerceptron.integrable_log_sq_of_moments line 509
  37. lemma OAI.IsingPerceptron.stable_positive_moment line 520
  38. lemma OAI.IsingPerceptron.stable_negative_moment line 530
  39. lemma OAI.IsingPerceptron.negExp_eq_exp_toReal line 540
  40. lemma OAI.IsingPerceptron.poissonTotal_real_laplace line 543
  41. lemma OAI.IsingPerceptron.poissonTotal_real_pos line 560
  42. lemma OAI.IsingPerceptron.poissonTotal_positive_moment line 565
  43. lemma OAI.IsingPerceptron.poissonTotal_negative_moment line 573
  44. theorem OAI.IsingPerceptron.poissonTotal_log_square line 580