OAI/Probability/SphericalField/Entropy/StepIntegral.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptron.timeTail_atom_integral line 13
  2. lemma OAI.SphericalPerceptron.tailIntegral_weightedStepTrial line 26
  3. def OAI.SphericalPerceptron.weightedStepTail line 36
  4. lemma OAI.SphericalPerceptron.weightedStepTail_continuous line 39
  5. lemma OAI.SphericalPerceptron.weightedStepTail_lower line 44
  6. lemma OAI.SphericalPerceptron.weightedStepTail_upper line 53
  7. lemma OAI.SphericalPerceptron.weightedStepTail_of_le line 61
  8. lemma OAI.SphericalPerceptron.weightedStepTail_pos line 67
  9. lemma OAI.SphericalPerceptron.weightedStepTail_inv_continuousOn line 73
  10. lemma OAI.SphericalPerceptron.integral_one_sub_inv line 80
  11. theorem OAI.SphericalPerceptron.entropy_weightedStepTrial line 86
  12. lemma OAI.SphericalPerceptron.weightedStepTail_affine line 146
  13. lemma OAI.SphericalPerceptron.weightedStepTail_below_min line 165
  14. lemma OAI.SphericalPerceptron.affine_pos_on line 172
  15. lemma OAI.SphericalPerceptron.integral_positive_affine_inv line 177
  16. lemma OAI.SphericalPerceptron.integral_positive_affine_inv_sq line 198
  17. lemma OAI.SphericalPerceptron.integral_eq_stepLogRatios line 227
  18. lemma OAI.SphericalPerceptron.weightedStep_integral_inv line 252
  19. theorem OAI.SphericalPerceptron.entropy_weightedStepTrial_finite_formula line 291
  20. def OAI.SphericalPerceptron.weightedStepA line 312
  21. lemma OAI.SphericalPerceptron.weightedStepA_root line 315
  22. lemma OAI.SphericalPerceptron.weightedStepA_increment line 328
  23. lemma OAI.SphericalPerceptron.weightedStep_truncated_entropy_nonneg line 362
  24. lemma OAI.SphericalPerceptron.entropy_weightedStepTrial_toReal line 377
  25. lemma OAI.SphericalPerceptron.entropy_weightedStepTrial_toReal_finite_formula line 385
  26. lemma OAI.SphericalPerceptron.stepCumulative_pos line 404
  27. lemma OAI.SphericalPerceptron.stepCumulative_lt_one line 411
  28. lemma OAI.SphericalPerceptron.stepCumulative_strictMono line 424