OAI/Probability/Perceptron/Variational/PointedShape.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SphericalPerceptronFreeEnergy.cascadeShapeFocus_castline 11 - lemma
OAI.SphericalPerceptronFreeEnergy.cascadeShapeReplicasOfFn_focusline 18 - theorem
OAI.SphericalPerceptronFreeEnergy.finite_leaf_tuple_pointed_shapeline 31 - lemma
OAI.SphericalPerceptronFreeEnergy.ennreal_tsum_pi_focusline 121 - lemma
OAI.SphericalPerceptronFreeEnergy.root_partition_sum_focusedline 132