OAI/Probability/Perceptron/Variational/LabelSingleRestoredValue.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.sourceLabelSingleIntegrand line 11
  2. lemma OAI.SphericalPerceptronFreeEnergy.sourceLabelSingleIntegrand_integrable line 17
  3. lemma OAI.SphericalPerceptronFreeEnergy.sourceLabelSingleIntegrand_value line 27
  4. def OAI.SphericalPerceptronFreeEnergy.singleRestorationBound line 67
  5. lemma OAI.SphericalPerceptronFreeEnergy.singleRestorationBound_nonneg line 70
  6. lemma OAI.SphericalPerceptronFreeEnergy.sourceLabelRestorationNumerator_single_bound line 73
  7. lemma OAI.SphericalPerceptronFreeEnergy.sourceLabelRestorationRatio_single_value line 83
  8. lemma OAI.SphericalPerceptronFreeEnergy.sourceLabelSingle_witness line 94
  9. def OAI.SphericalPerceptronFreeEnergy.scalarRestorationSingleMoment line 130
  10. lemma OAI.SphericalPerceptronFreeEnergy.restorationBlockTest_one line 135
  11. lemma OAI.SphericalPerceptronFreeEnergy.jointRestorationBlockTest_one line 141
  12. lemma OAI.SphericalPerceptronFreeEnergy.scalarRestorationSingleMoment_compact line 147
  13. lemma OAI.SphericalPerceptronFreeEnergy.scalarRestorationSingleMoment_label line 157
  14. lemma OAI.SphericalPerceptronFreeEnergy.scalarRestorationSingleMoment_diagonalMap line 168