OAI/Probability/Perceptron/Cavity/BulkAnnealedTangent.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.bulkReplicaMean_add_dominated line 12
  2. lemma OAI.SphericalPerceptronFreeEnergy.bulkTangentDirection_bounded line 39
  3. def OAI.SphericalPerceptronFreeEnergy.bulkTangentPerturbation line 45
  4. lemma OAI.SphericalPerceptronFreeEnergy.bulkTangentPerturbation_measurable line 49
  5. lemma OAI.SphericalPerceptronFreeEnergy.bulkTangentPerturbation_bound line 53
  6. lemma OAI.SphericalPerceptronFreeEnergy.bulkMarkNorm_integrable line 59
  7. lemma OAI.SphericalPerceptronFreeEnergy.bulkTangentPerturbation_integrable line 63
  8. lemma OAI.SphericalPerceptronFreeEnergy.bulk_tangent_annealed_perturbation_bound line 71
  9. lemma OAI.SphericalPerceptronFreeEnergy.continuous_real_compact_bound line 91
  10. def OAI.SphericalPerceptronFreeEnergy.tangentDerivTest line 96
  11. lemma OAI.SphericalPerceptronFreeEnergy.tangentDerivTest_continuous line 99
  12. lemma OAI.SphericalPerceptronFreeEnergy.bulk_tangent_row_ibp_any line 105
  13. lemma OAI.SphericalPerceptronFreeEnergy.bulk_tangent_annealed line 113