OAI/Probability/SphericalField/Cascade/Coordinates.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptron.canonicalCoordinateStep_measurable line 18
  2. def OAI.SphericalPerceptron.canonicalCoordinatePotential line 25
  3. lemma OAI.SphericalPerceptron.canonicalCoordinatePotential_measurable line 28
  4. lemma OAI.SphericalPerceptron.canonical_coordinate_spin_log line 31
  5. def OAI.SphericalPerceptron.canonicalCoordinateLog line 45
  6. lemma OAI.SphericalPerceptron.canonical_coordinate_recursion line 50
  7. theorem OAI.SphericalPerceptron.canonical_coordinate_log_mean line 66
  8. lemma OAI.SphericalPerceptron.canonical_coordinate_log_deviation_le line 79
  9. lemma OAI.SphericalPerceptron.gaussian_square_memLp_two line 94
  10. lemma OAI.SphericalPerceptron.gaussian_square_mean line 103
  11. lemma OAI.SphericalPerceptron.gaussian_square_sum_memLp_two line 108
  12. lemma OAI.SphericalPerceptron.gaussian_square_sum_mean line 112
  13. lemma OAI.SphericalPerceptron.gaussian_square_sum_variance line 125
  14. lemma OAI.SphericalPerceptron.gaussian_square_average_deviation_le line 133
  15. lemma OAI.SphericalPerceptron.decoratedTerminalTotal_measurable line 151
  16. lemma OAI.SphericalPerceptron.canonicalCoordinateLog_measurable line 163
  17. lemma OAI.SphericalPerceptron.product_deviation_le line 170
  18. theorem OAI.SphericalPerceptron.canonical_coordinate_joint_deviation_le line 195