OAI/Probability/Perceptron/Variational/LevelTrialApprox.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.trialLevelQuantile line 11
  2. lemma OAI.SphericalPerceptronFreeEnergy.trialLevelQuantile_mono line 14
  3. lemma OAI.SphericalPerceptronFreeEnergy.trialLevelQuantile_le line 22
  4. lemma OAI.SphericalPerceptronFreeEnergy.trialLevelQuantile_lt line 25
  5. lemma OAI.SphericalPerceptronFreeEnergy.uniform_threshold_sum line 30
  6. def OAI.SphericalPerceptronFreeEnergy.levelStepTrial line 52
  7. lemma OAI.SphericalPerceptronFreeEnergy.le_levelStepTrial line 56
  8. lemma OAI.SphericalPerceptronFreeEnergy.levelStepTrial_ae line 66
  9. lemma OAI.SphericalPerceptronFreeEnergy.levelStepTrial_L1 line 81
  10. lemma OAI.SphericalPerceptronFreeEnergy.trialLevelQuantile_terminal line 89
  11. theorem OAI.SphericalPerceptronFreeEnergy.exists_uniform_step_trial_approx line 96
  12. theorem OAI.SphericalPerceptronFreeEnergy.expectedPressure_upper_trial line 124
  13. theorem OAI.SphericalPerceptronFreeEnergy.expectedPressure_upper_variational line 155