OAI/Probability/Perceptron/Variational/CountableMarkedDiagonal.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.truncatedFreshMarkedKernel line 12
  2. lemma OAI.SphericalPerceptronFreeEnergy.countableFreshMarkedKernel line 35
  3. def OAI.SphericalPerceptronFreeEnergy.gaussianMixedTest line 49
  4. lemma OAI.SphericalPerceptronFreeEnergy.gaussianMixedTest_apply line 52
  5. lemma OAI.SphericalPerceptronFreeEnergy.freshMixedKernel_diagonal_noise line 56
  6. lemma OAI.SphericalPerceptronFreeEnergy.countableFreshMixed_diagonal line 101
  7. def OAI.SphericalPerceptronFreeEnergy.labelMarkedBlockKernel line 116
  8. lemma OAI.SphericalPerceptronFreeEnergy.labelProfile_mixed_kernel line 129
  9. lemma OAI.SphericalPerceptronFreeEnergy.labelProfileField_product_measurable line 148
  10. def OAI.SphericalPerceptronFreeEnergy.labelMixedValue line 154
  11. lemma OAI.SphericalPerceptronFreeEnergy.measurableReplicaProduct line 158
  12. lemma OAI.SphericalPerceptronFreeEnergy.labelMixedValue_measurable line 166
  13. lemma OAI.SphericalPerceptronFreeEnergy.labelMixedValue_bound line 171
  14. lemma OAI.SphericalPerceptronFreeEnergy.labelTwoMixed_measurable line 179
  15. lemma OAI.SphericalPerceptronFreeEnergy.labelProfile_twoMixed_fubini line 191