On this page
Sign and Gaussian patterns of the Ising perceptron: the theorem
Imports 5 library modules and 21 external
- GaussianAnalysis.gaussian.measurable_matrix
- GaussianAnalysis.gaussian.gauss
- GaussianApplications.PerceptronSignDefinitions
- GaussianApplications.PerceptronSignStatement
- GaussianApplications.Perceptron.Pressure
External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, mathcomp.analysis.derive, mathcomp.analysis.exp, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.measurable_realfun, mathcomp.analysis.probability_theory.probability, mathcomp.algebra.arithmetic_tactic
Target T6 of phase 12. perceptron_sign_theorem proves perceptron_sign_statement of PerceptronSignStatement.v from perceptron_sign_compare of Perceptron/Pressure.v, a Rocq formalization of the credited argument of the first paragraph of the proof of Theorem ext:sign of 'The free energy of the Ising random perceptron' (family 222 of the OpenAI math collection, revision 1581d4cbd, sections/extensions.tex). The collection has no Lean version of it.
The constant is C = 1 + (|B3| + 6 |B1| |B2| + 6 |B1|^3) / 2: it is positive for all bounds, and when bounded_C3 f B0 B1 B2 B3 holds the bounds are nonnegative, so C is at least the constant (B3 + 6 B1 B2 + 6 B1^3) / 2 of perceptron_sign_compare. The continuity of f''' in bounded_C3 is not used.
Main results
| Results | Statement |
|---|---|
Proves perceptron_sign_statement (T6) with C = 1 + (|B3| + 6 |B1| |B2| + 6 |B1|^3) / 2, from perceptron_sign_compare of Perceptron/. The continuity of f''' required by bounded_C3 is not used. Axioms: three of boolp. |
Declarations1 exported
Proves perceptron_sign_statement (T6) with C = 1 + (|B3| + 6 |B1| |B2| + 6 |B1|^3) / 2, from perceptron_sign_compare of Perceptron/. The continuity of f''' required by bounded_C3 is not used. Axioms: three of boolp.
Statement as written in the source
Theorem perceptron_sign_theorem : perceptron_sign_statement.