OAI/Probability/Perceptron/Variational/EnrichedUniformBounds.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.diagonalMark_norm_le line 11
  2. lemma OAI.SphericalPerceptronFreeEnergy.enrichedRootMap_norm_le line 24
  3. lemma OAI.SphericalPerceptronFreeEnergy.perturbationScale_le_one line 39
  4. lemma OAI.SphericalPerceptronFreeEnergy.perturbationWeight_eq line 42
  5. lemma OAI.SphericalPerceptronFreeEnergy.half_power_sum_le_one line 45
  6. lemma OAI.SphericalPerceptronFreeEnergy.perturbationAmplitude_square_le line 51
  7. lemma OAI.SphericalPerceptronFreeEnergy.enrichedFeatureBound_sq_le line 72
  8. lemma OAI.SphericalPerceptronFreeEnergy.finite_profile_telescope line 85
  9. def OAI.SphericalPerceptronFreeEnergy.profileGaussianRoot line 92
  10. def OAI.SphericalPerceptronFreeEnergy.profileGaussianStep line 95
  11. lemma OAI.SphericalPerceptronFreeEnergy.profileGaussian_coefficient line 99
  12. lemma OAI.SphericalPerceptronFreeEnergy.profileGaussian_coefficient_squares line 111
  13. lemma OAI.SphericalPerceptronFreeEnergy.enrichedCoordinateLevel_nonneg line 122
  14. lemma OAI.SphericalPerceptronFreeEnergy.enrichedCoordinateLevel_monotone line 129
  15. lemma OAI.SphericalPerceptronFreeEnergy.enrichedCoordinateLevel_le line 139
  16. lemma OAI.SphericalPerceptronFreeEnergy.enrichedIncrementMap_profile line 152
  17. def OAI.SphericalPerceptronFreeEnergy.sourceGaussianRow line 164
  18. lemma OAI.SphericalPerceptronFreeEnergy.sourceGaussianRow_measurable line 170
  19. lemma OAI.SphericalPerceptronFreeEnergy.sourceGaussianRow_square_bound line 174
  20. lemma OAI.SphericalPerceptronFreeEnergy.sourceGaussianRow_identity line 189