OAI/Probability/Perceptron/Variational/ShellBridge.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.canonicalWeighted_compl_band_le line 11
  2. lemma OAI.SphericalPerceptronFreeEnergy.exp_log_quotient_mul line 30
  3. def OAI.SphericalPerceptronFreeEnergy.canonicalCoordinateBandTotalE line 37
  4. lemma OAI.SphericalPerceptronFreeEnergy.canonicalCoordinateBandTotalE_le line 43
  5. lemma OAI.SphericalPerceptronFreeEnergy.canonicalCoordinate_half_band line 52
  6. theorem OAI.SphericalPerceptronFreeEnergy.canonicalCoordinate_bad_half_band_tendsto_zero line 114
  7. lemma OAI.SphericalPerceptronFreeEnergy.canonicalCoordinate_shell_log_upper line 161
  8. lemma OAI.SphericalPerceptronFreeEnergy.canonicalCoordinate_shell_log_lower line 190
  9. lemma OAI.SphericalPerceptronFreeEnergy.convex_nonneg_radius_transfer line 223
  10. lemma OAI.SphericalPerceptronFreeEnergy.sqrt_radius_band line 251
  11. lemma OAI.SphericalPerceptronFreeEnergy.coordinateAngularLog_unit_radius_bounds line 271
  12. lemma OAI.SphericalPerceptronFreeEnergy.canonicalCoordinate_unitSphere_upper line 298
  13. lemma OAI.SphericalPerceptronFreeEnergy.canonicalCoordinate_unitSphere_lower line 312