OAI/Probability/Perceptron/Cavity/CavityDisintegration.lean
14 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SphericalPerceptronFreeEnergy.stdGaussian_radial_preservingline 12 - def
OAI.SphericalPerceptronFreeEnergy.cavityBlockNormalizeline 21 - lemma
OAI.SphericalPerceptronFreeEnergy.cavityBlockNormalize_measurableline 25 - lemma
OAI.SphericalPerceptronFreeEnergy.gaussianBlockSplit_normalizeline 29 - lemma
OAI.SphericalPerceptronFreeEnergy.sphereBlock_gaussian_lawline 35 - def
OAI.SphericalPerceptronFreeEnergy.cavityRadialBlockline 53 - lemma
OAI.SphericalPerceptronFreeEnergy.cavityRadialBlock_measurableline 57 - lemma
OAI.SphericalPerceptronFreeEnergy.cavityRadialBlock_eqline 61 - theorem
OAI.SphericalPerceptronFreeEnergy.sphereBlock_radial_lawline 67 - lemma
OAI.SphericalPerceptronFreeEnergy.countableGaussian_eval_preservingline 78 - lemma
OAI.SphericalPerceptronFreeEnergy.countableGaussian_square_strongLawline 82 - def
OAI.SphericalPerceptronFreeEnergy.cavityCoupledScaleline 101 - lemma
OAI.SphericalPerceptronFreeEnergy.cavityCoupledScale_measurableline 104 - lemma
OAI.SphericalPerceptronFreeEnergy.cavityCoupledScale_tendstoline 109