OAI/Probability/Perceptron/Variational/ProductMarkLaw.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.normalizedMeasure_prod line 15
  2. lemma OAI.SphericalPerceptronFreeEnergy.exponentialMarkTilt_prod_add line 24
  3. lemma OAI.SphericalPerceptronFreeEnergy.fractional_log_moment_prod_add line 44
  4. def OAI.SphericalPerceptronFreeEnergy.productMarkLaw line 54
  5. theorem OAI.SphericalPerceptronFreeEnergy.finiteCascadeLogRecursion_add_product line 58
  6. lemma OAI.SphericalPerceptronFreeEnergy.real_quadratic_complete_square line 83
  7. lemma OAI.SphericalPerceptronFreeEnergy.real_quadratic_integrable line 91
  8. lemma OAI.SphericalPerceptronFreeEnergy.real_quadratic_integral line 96
  9. lemma OAI.SphericalPerceptronFreeEnergy.standardGaussian_quadratic_density line 102
  10. lemma OAI.SphericalPerceptronFreeEnergy.standardGaussian_quadratic_integrable line 110
  11. lemma OAI.SphericalPerceptronFreeEnergy.standardGaussian_quadratic_integral line 124
  12. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_quadratic_fractional_integrable line 137
  13. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_quadratic_fractional_log line 149
  14. def OAI.SphericalPerceptronFreeEnergy.gaussianShiftStep line 170
  15. lemma OAI.SphericalPerceptronFreeEnergy.gaussianShiftStep_measurable line 173
  16. def OAI.SphericalPerceptronFreeEnergy.standardGaussianMark line 177
  17. def OAI.SphericalPerceptronFreeEnergy.quadraticCascadePrecision line 179
  18. def OAI.SphericalPerceptronFreeEnergy.quadraticCascadeOffset line 183
  19. lemma OAI.SphericalPerceptronFreeEnergy.quadraticCascadePrecision_tail_pos line 189
  20. theorem OAI.SphericalPerceptronFreeEnergy.finiteCascade_quadratic_recursion line 196
  21. theorem OAI.SphericalPerceptronFreeEnergy.canonical_cascade_quadratic_log line 227
  22. lemma OAI.SphericalPerceptronFreeEnergy.canonical_scalar_integrable line 239
  23. lemma OAI.SphericalPerceptronFreeEnergy.canonical_scalar_integral line 246
  24. lemma OAI.SphericalPerceptronFreeEnergy.canonical_scalar_log line 254
  25. lemma OAI.SphericalPerceptronFreeEnergy.quadraticCascadePrecision_le line 261
  26. lemma OAI.SphericalPerceptronFreeEnergy.quadraticCascadePrecision_hasDerivAt line 271
  27. def OAI.SphericalPerceptronFreeEnergy.quadraticCascadeReciprocalSlope line 277
  28. lemma OAI.SphericalPerceptronFreeEnergy.quadraticCascadeOffset_hasDerivAt line 283
  29. def OAI.SphericalPerceptronFreeEnergy.canonicalGaussianFreeValue line 295
  30. lemma OAI.SphericalPerceptronFreeEnergy.canonicalGaussianFreeValue_hasDerivAt line 298
  31. def OAI.SphericalPerceptronFreeEnergy.cascadeLogFluctuationConstant line 314
  32. lemma OAI.SphericalPerceptronFreeEnergy.cascadeLogFluctuationConstant_nonneg line 317
  33. lemma OAI.SphericalPerceptronFreeEnergy.decoratedCascade_log_second_moment_bound line 321
  34. lemma OAI.SphericalPerceptronFreeEnergy.decoratedCascade_log_deviation_le line 378
  35. lemma OAI.SphericalPerceptronFreeEnergy.finiteCascade_terminal_log_deviation_le line 400