OAI/Probability/Perceptron/Brownian/GaussianField.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_replica_integrationByParts line 16
  2. lemma OAI.SphericalPerceptronFreeEnergy.tilt_law_apply line 38
  3. lemma OAI.SphericalPerceptronFreeEnergy.tilt_law_pi line 49
  4. lemma OAI.SphericalPerceptronFreeEnergy.tilt_mean_twice line 70
  5. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_pi_coordinate_integrationByParts line 87
  6. lemma OAI.SphericalPerceptronFreeEnergy.measurable_tiltMean line 125
  7. def OAI.SphericalPerceptronFreeEnergy.gaussianField line 132
  8. lemma OAI.SphericalPerceptronFreeEnergy.gaussianField_measurable line 135
  9. lemma OAI.SphericalPerceptronFreeEnergy.gaussianField_bound line 142
  10. lemma OAI.SphericalPerceptronFreeEnergy.gaussianField_insertNth line 153
  11. lemma OAI.SphericalPerceptronFreeEnergy.tilt_mean_mulObservable line 162
  12. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_field_coordinate_ibp line 169
  13. lemma OAI.SphericalPerceptronFreeEnergy.ennreal_rpow_sum_le line 241
  14. lemma OAI.SphericalPerceptronFreeEnergy.ennreal_rpow_tsum_le line 250
  15. lemma OAI.SphericalPerceptronFreeEnergy.finitePoissonLaw_rpow_lintegral_le line 258
  16. lemma OAI.SphericalPerceptronFreeEnergy.countablePoissonLaw_rpow_lintegral_le line 274
  17. lemma OAI.SphericalPerceptronFreeEnergy.poissonRandomMeasureLaw_rpow_lintegral_le line 289
  18. lemma OAI.SphericalPerceptronFreeEnergy.ennreal_rpow_le_one_add line 295
  19. lemma OAI.SphericalPerceptronFreeEnergy.poissonRandomMeasureLaw_fractional_moment line 302
  20. lemma OAI.SphericalPerceptronFreeEnergy.stableLogIntensity_of_integrable line 319
  21. lemma OAI.SphericalPerceptronFreeEnergy.stableLogIntensity_small_moment line 333
  22. lemma OAI.SphericalPerceptronFreeEnergy.stableLogIntensity_large_moment line 353
  23. lemma OAI.SphericalPerceptronFreeEnergy.stablePoissonTotal_fractional_integrable line 373
  24. lemma OAI.SphericalPerceptronFreeEnergy.tilt_replica_integral line 407