On this page
Sign and Gaussian patterns of the Ising perceptron: the definitions
Imports 2 library modules and 20 external
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
Target T6 of phase 12 (AGENTS.md, section Phase 12; the plan notes/phase12-plan.md, section 3). The definitions of the statement of PerceptronSignStatement.v, from 'The free energy of the Ising random perceptron' (family 222 of the OpenAI math collection, revision 1581d4cbd, sections/model.tex, equation def:pressure, and sections/extensions.tex, Theorem ext:sign). The collection has no Lean version of it. R is any realType.
- spin_col x is the column of the spins of x in {-1, 1}^N, x of {ffun 'I_N -> bool}.
- perceptron_pressure f G = (1/N) ln (2^(-N) sum_x exp (sum_mu f ((G x)_mu / sqrt N))), for patterns G of 'M[R]_(M, N), with rows g^1, ..., g^M, and a potential f : R -> R: the normalized pressure p_N(f) of the manuscript, with the uniform probability on the cube and b_mu(x) = <g^mu, x> / sqrt N, at M patterns.
- gauss_pressure M N f is its expectation under Gaussian patterns: G = vec_mx g, with g of law gauss (M * N), so that the M N entries of G are independent standard normal. sign_pressure M N f is its expectation under sign patterns: the average over the 2^(M N) matrices of entries in {-1, 1}, so that the entries are independent uniform signs.
- bounded_C3 f B0 B1 B2 B3: f has derivatives f', f'' and f''' everywhere, f''' is continuous (f is of class C^3), and |f| <= B0, |f'| <= B1, |f''| <= B2, |f'''| <= B3 on R.
Declarations5 exported
Variable R : realType. Implicit Types M N : nat.
forall (R : realType) [N : nat], {ffun 'I_N -> bool} -> 'cV_N
Definition spin_col N (x : {ffun 'I_N -> bool}) : 'cV[R]_N := \col_i (if x i then 1 else -1).
Used by 3 declarations in 2 files
- this file: perceptron_pressure
- GaussianApplications.Perceptron.Pressure: pressure_energy, perceptron_pressure_derive3
forall [R : realType] [M N : nat], (R -> R) -> 'M_(M, N) -> RDefinition perceptron_pressure M N (f : R -> R) (G : 'M[R]_(M, N)) : R := N%:R^-1 * ln ((2 ^+ N)^-1 * \sum_(x : {ffun 'I_N -> bool}) expR (\sum_(mu < M) f ((G *m spin_col x) mu 0 / Num.sqrt N%:R))).
Used by 9 declarations in 3 files
- this file: gauss_pressure, sign_pressure
- GaussianApplications.PerceptronSignStatement: perceptron_sign_statement
- GaussianApplications.Perceptron.Pressure: perceptron_pressureE, perceptron_pressure_le, measurable_perceptron_pressure, perceptron_pressure_derive3, sign_pressureE, perceptron_sign_compare
forall [R : realType], nat -> nat -> (R -> R) -> RDefinition gauss_pressure M N (f : R -> R) : R := \int[gauss (M * N)]_g perceptron_pressure f (vec_mx g).
Used by 2 declarations in 2 files
- GaussianApplications.PerceptronSignStatement: perceptron_sign_statement
- GaussianApplications.Perceptron.Pressure: perceptron_sign_compare
forall [R : realType], nat -> nat -> (R -> R) -> RDefinition sign_pressure M N (f : R -> R) : R := (2 ^+ (M * N))^-1 * \sum_(s : {ffun 'I_M * 'I_N -> bool}) perceptron_pressure f (\matrix_(mu, i) (if s (mu, i) then 1 else -1)).
Used by 3 declarations in 2 files
- GaussianApplications.PerceptronSignStatement: perceptron_sign_statement
- GaussianApplications.Perceptron.Pressure: sign_pressureE, perceptron_sign_compare
forall [R : realType], (R -> R) -> R -> R -> R -> R -> Prop
Definition bounded_C3 (f : R -> R) (B0 B1 B2 B3 : R) : Prop := exists f1 f2 f3 : R -> R, [/\ forall x : R, is_derive x 1 f (f1 x), forall x : R, is_derive x 1 f1 (f2 x), forall x : R, is_derive x 1 f2 (f3 x), continuous f3 & forall x : R, [/\ `|f x| <= B0, `|f1 x| <= B1, `|f2 x| <= B2 & `|f3 x| <= B3]].
Used by 1 declaration in 1 file
- GaussianApplications.PerceptronSignStatement: perceptron_sign_statement