OAI/Probability/Perceptron/Variational/CouplingKernel.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SphericalPerceptronFreeEnergy.SourceBaseData line 13
  2. def OAI.SphericalPerceptronFreeEnergy.sourceBaseDataLaw line 15
  3. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 19) line 19
  4. def OAI.SphericalPerceptronFreeEnergy.sourceDisorderReassoc line 23
  5. lemma OAI.SphericalPerceptronFreeEnergy.sourceDisorderReassoc_preserving line 26
  6. def OAI.SphericalPerceptronFreeEnergy.indexedLeafKernel line 35
  7. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 38) line 38
  8. def OAI.SphericalPerceptronFreeEnergy.sourceSpinLeafKernel line 40
  9. lemma OAI.SphericalPerceptronFreeEnergy.sourceSpinLeafKernel_apply line 45
  10. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 50) line 50
  11. def OAI.SphericalPerceptronFreeEnergy.sourceBaseEnergy line 56
  12. lemma OAI.SphericalPerceptronFreeEnergy.sourceBaseEnergy_measurable line 60
  13. lemma OAI.SphericalPerceptronFreeEnergy.sourceBaseData_regular line 71
  14. def OAI.SphericalPerceptronFreeEnergy.sourceKernelPressure line 81
  15. lemma OAI.SphericalPerceptronFreeEnergy.sourceKernelPressure_eq line 87
  16. lemma OAI.SphericalPerceptronFreeEnergy.sourceKernelPressure_ae line 95
  17. lemma OAI.SphericalPerceptronFreeEnergy.sourceKernelPressure_memLp line 104
  18. lemma OAI.SphericalPerceptronFreeEnergy.sourceKernelPressure_variance line 113
  19. lemma OAI.SphericalPerceptronFreeEnergy.measurable_disorder_state_lift line 125
  20. def OAI.SphericalPerceptronFreeEnergy.sourceCouplingHamiltonian line 130
  21. def OAI.SphericalPerceptronFreeEnergy.sourceCouplingEnergy line 134
  22. lemma OAI.SphericalPerceptronFreeEnergy.sourceCouplingBase_measurable line 141
  23. lemma OAI.SphericalPerceptronFreeEnergy.sourceCouplingField_measurable line 146
  24. lemma OAI.SphericalPerceptronFreeEnergy.sourceCouplingHamiltonian_measurable line 155
  25. lemma OAI.SphericalPerceptronFreeEnergy.sourceCouplingEnergy_measurable line 160
  26. lemma OAI.SphericalPerceptronFreeEnergy.sourceKernelPressure_shift line 167
  27. lemma OAI.SphericalPerceptronFreeEnergy.sourceCoupling_all_exp_ae line 178
  28. lemma OAI.SphericalPerceptronFreeEnergy.sourceCouplingHamiltonian_section line 194
  29. lemma OAI.SphericalPerceptronFreeEnergy.sourceCouplingEnergy_section line 199
  30. lemma OAI.SphericalPerceptronFreeEnergy.sourceCoupling_regular_ae line 204