OAI/Probability/SphericalField/Gaussian/Quadratic.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptron.stablePoisson_descendant_transform_marked line 17
  2. lemma OAI.SphericalPerceptron.normalizedMeasure_prod line 32
  3. lemma OAI.SphericalPerceptron.exponentialMarkTilt_prod_add line 41
  4. lemma OAI.SphericalPerceptron.fractional_log_moment_prod_add line 61
  5. def OAI.SphericalPerceptron.productMarkLaw line 71
  6. theorem OAI.SphericalPerceptron.finiteCascadeLogRecursion_add_product line 75
  7. lemma OAI.SphericalPerceptron.real_quadratic_complete_square line 100
  8. lemma OAI.SphericalPerceptron.real_quadratic_integrable line 108
  9. lemma OAI.SphericalPerceptron.real_quadratic_integral line 113
  10. lemma OAI.SphericalPerceptron.standardGaussian_quadratic_density line 119
  11. lemma OAI.SphericalPerceptron.standardGaussian_quadratic_integrable line 127