OAI/Probability/Perceptron/Variational/StepEntropy.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.weightedStepTrial line 11
  2. lemma OAI.SphericalPerceptronFreeEnergy.timeTail_atom_integral line 38
  3. lemma OAI.SphericalPerceptronFreeEnergy.tailIntegral_weightedStepTrial line 51
  4. def OAI.SphericalPerceptronFreeEnergy.weightedStepTail line 61
  5. lemma OAI.SphericalPerceptronFreeEnergy.weightedStepTail_continuous line 64
  6. lemma OAI.SphericalPerceptronFreeEnergy.weightedStepTail_lower line 69
  7. lemma OAI.SphericalPerceptronFreeEnergy.weightedStepTail_upper line 78
  8. lemma OAI.SphericalPerceptronFreeEnergy.weightedStepTail_of_le line 86
  9. lemma OAI.SphericalPerceptronFreeEnergy.weightedStepTail_pos line 92
  10. lemma OAI.SphericalPerceptronFreeEnergy.weightedStepTail_inv_continuousOn line 98
  11. lemma OAI.SphericalPerceptronFreeEnergy.integral_one_sub_inv line 105
  12. theorem OAI.SphericalPerceptronFreeEnergy.entropy_weightedStepTrial line 111
  13. def OAI.SphericalPerceptronFreeEnergy.stepCumulative line 171
  14. lemma OAI.SphericalPerceptronFreeEnergy.weightedStepTail_affine line 174
  15. lemma OAI.SphericalPerceptronFreeEnergy.weightedStepTail_below_min line 193
  16. lemma OAI.SphericalPerceptronFreeEnergy.affine_pos_on line 200
  17. lemma OAI.SphericalPerceptronFreeEnergy.integral_positive_affine_inv line 205
  18. lemma OAI.SphericalPerceptronFreeEnergy.integral_positive_affine_inv_sq line 226
  19. lemma OAI.SphericalPerceptronFreeEnergy.integral_eq_stepLogRatios line 255
  20. lemma OAI.SphericalPerceptronFreeEnergy.weightedStep_integral_inv line 280
  21. theorem OAI.SphericalPerceptronFreeEnergy.entropy_weightedStepTrial_finite_formula line 319
  22. def OAI.SphericalPerceptronFreeEnergy.weightedStepA line 340
  23. lemma OAI.SphericalPerceptronFreeEnergy.weightedStepA_root line 343
  24. lemma OAI.SphericalPerceptronFreeEnergy.weightedStepA_increment line 356
  25. lemma OAI.SphericalPerceptronFreeEnergy.weightedStep_truncated_entropy_nonneg line 390
  26. lemma OAI.SphericalPerceptronFreeEnergy.entropy_weightedStepTrial_toReal line 405
  27. lemma OAI.SphericalPerceptronFreeEnergy.entropy_weightedStepTrial_toReal_finite_formula line 413
  28. lemma OAI.SphericalPerceptronFreeEnergy.stepCumulative_pos line 432
  29. lemma OAI.SphericalPerceptronFreeEnergy.stepCumulative_lt_one line 439
  30. lemma OAI.SphericalPerceptronFreeEnergy.stepCumulative_strictMono line 452