OAI/Probability/Perceptron/Variational/HeatTilt.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.canonicalBandRadiusWeight_mass line 21
  2. lemma OAI.SphericalPerceptronFreeEnergy.canonicalField_band_bounds line 26
  3. lemma OAI.SphericalPerceptronFreeEnergy.canonicalWeighted_mass_le line 57
  4. lemma OAI.SphericalPerceptronFreeEnergy.canonicalWeighted_upper_tail line 82
  5. lemma OAI.SphericalPerceptronFreeEnergy.canonicalWeighted_lower_tail line 94
  6. def OAI.SphericalPerceptronFreeEnergy.heatTilt line 106
  7. lemma OAI.SphericalPerceptronFreeEnergy.heatTilt_zero line 109
  8. lemma OAI.SphericalPerceptronFreeEnergy.gaussianAverage_affine line 113
  9. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_exp_affine_deriv line 120
  10. lemma OAI.SphericalPerceptronFreeEnergy.heatLog_directional_deriv line 154
  11. lemma OAI.SphericalPerceptronFreeEnergy.gaussianAverage_add line 170
  12. lemma OAI.SphericalPerceptronFreeEnergy.gaussianAverage_smul line 174
  13. lemma OAI.SphericalPerceptronFreeEnergy.heatTilt_add line 178
  14. lemma OAI.SphericalPerceptronFreeEnergy.heatTilt_smul line 185
  15. lemma OAI.SphericalPerceptronFreeEnergy.heatTilt_const line 192
  16. lemma OAI.SphericalPerceptronFreeEnergy.heatTilt_nonneg line 199
  17. lemma OAI.SphericalPerceptronFreeEnergy.heatTilt_mono line 204
  18. lemma OAI.SphericalPerceptronFreeEnergy.heatTilt_abs_le line 211
  19. lemma OAI.SphericalPerceptronFreeEnergy.heatTilt_sq line 222
  20. lemma OAI.SphericalPerceptronFreeEnergy.Jet3.heatLog_d1 line 238
  21. lemma OAI.SphericalPerceptronFreeEnergy.Jet3.heatLog_d1_sq_le line 253
  22. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_exp_affine_mul_deriv line 258
  23. lemma OAI.SphericalPerceptronFreeEnergy.heatTilt_directional_deriv line 290
  24. lemma OAI.SphericalPerceptronFreeEnergy.heatTilt_directional_bound line 301
  25. lemma OAI.SphericalPerceptronFreeEnergy.heatTilt_affine_sub_bound line 319
  26. lemma OAI.SphericalPerceptronFreeEnergy.heatLog_terminal_quadratic_error line 328
  27. lemma OAI.SphericalPerceptronFreeEnergy.heatTilt_continuous line 348
  28. def OAI.SphericalPerceptronFreeEnergy.heatTiltBCF line 352
  29. lemma OAI.SphericalPerceptronFreeEnergy.heatTiltBCF_apply line 358
  30. lemma OAI.SphericalPerceptronFreeEnergy.heatTiltBCF_norm_le line 361
  31. def OAI.SphericalPerceptronFreeEnergy.heatTiltCLM line 364
  32. lemma OAI.SphericalPerceptronFreeEnergy.heatLogBCF_terminal_quadratic_error line 373
  33. lemma OAI.SphericalPerceptronFreeEnergy.heatLogBCF_hasFDerivAt line 377
  34. def OAI.SphericalPerceptronFreeEnergy.shiftBCF line 393
  35. lemma OAI.SphericalPerceptronFreeEnergy.shiftBCF_apply line 396
  36. lemma OAI.SphericalPerceptronFreeEnergy.shiftBCF_norm_le line 398
  37. lemma OAI.SphericalPerceptronFreeEnergy.shiftBCF_lipschitz line 401
  38. lemma OAI.SphericalPerceptronFreeEnergy.shiftBCF_Jet3_hasDerivAt line 415