OAI/Probability/Perceptron/Variational/HeatLogBCF.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.heatLog_continuous line 14
  2. def OAI.SphericalPerceptronFreeEnergy.heatLogBCF line 21
  3. lemma OAI.SphericalPerceptronFreeEnergy.heatLogBCF_coe line 27
  4. lemma OAI.SphericalPerceptronFreeEnergy.exp_heatLog line 30
  5. lemma OAI.SphericalPerceptronFreeEnergy.heatLog_zero line 36
  6. lemma OAI.SphericalPerceptronFreeEnergy.heatLog_semigroup line 41
  7. structure OAI.SphericalPerceptronFreeEnergy.Jet3 line 53
  8. lemma OAI.SphericalPerceptronFreeEnergy.Jet3.deriv_eq line 62
  9. lemma OAI.SphericalPerceptronFreeEnergy.Jet3.deriv2_eq line 63
  10. lemma OAI.SphericalPerceptronFreeEnergy.Jet3.deriv3_eq line 66
  11. lemma OAI.SphericalPerceptronFreeEnergy.Jet3.contDiff line 70
  12. def OAI.SphericalPerceptronFreeEnergy.Jet3.gaussianAverage line 81
  13. lemma OAI.SphericalPerceptronFreeEnergy.Jet3.gaussianAverage_norms line 90
  14. def OAI.SphericalPerceptronFreeEnergy.Jet3.exp line 98
  15. lemma OAI.SphericalPerceptronFreeEnergy.inv_bcf_bound line 118
  16. def OAI.SphericalPerceptronFreeEnergy.invBCF line 123
  17. lemma OAI.SphericalPerceptronFreeEnergy.invBCF_apply line 130
  18. lemma OAI.SphericalPerceptronFreeEnergy.invBCF_norm_le line 133
  19. lemma OAI.SphericalPerceptronFreeEnergy.invBCF_hasDerivAt line 138
  20. def OAI.SphericalPerceptronFreeEnergy.Jet3.heatLogPos line 144
  21. def OAI.SphericalPerceptronFreeEnergy.Jet3.heatLog line 178
  22. lemma OAI.SphericalPerceptronFreeEnergy.Jet3.heatLog_f line 181
  23. lemma OAI.SphericalPerceptronFreeEnergy.gaussianAverage_jet_error line 187
  24. lemma OAI.SphericalPerceptronFreeEnergy.log_linear_error_le line 198
  25. lemma OAI.SphericalPerceptronFreeEnergy.gaussianAverage_ge_const line 215
  26. lemma OAI.SphericalPerceptronFreeEnergy.log_gaussian_generator_error line 220
  27. lemma OAI.SphericalPerceptronFreeEnergy.expBCF_norm_le line 284
  28. lemma OAI.SphericalPerceptronFreeEnergy.Jet3.exp_norms line 289
  29. lemma OAI.SphericalPerceptronFreeEnergy.Jet3.heatLog_uniform_bounds line 331
  30. lemma OAI.SphericalPerceptronFreeEnergy.heatLog_generator_uniform line 389