On this page
The pressure of the Ising perceptron
Imports 6 library modules and 25 external
- GaussianAnalysis.gaussian.measurable_matrix
- GaussianAnalysis.gaussian.gauss
- GaussianAnalysis.probability.lindeberg
- GaussianAnalysis.probability.log_partition
- GaussianAnalysis.probability.rademacher_lindeberg
- GaussianApplications.PerceptronSignDefinitions
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.realfun, mathcomp.analysis.exp, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.numfun, mathcomp.analysis.measurable_realfun, mathcomp.analysis.probability_theory.probability, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic
Imported by 1
Part of target T6 of phase 12 (AGENTS.md, section Phase 12), the comparison of the expected pressure of the Ising perceptron under sign and Gaussian patterns. 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.
Take patterns G in 'M[R]_(M, N) with N >= 1, and a potential f with three derivatives such that |f| <= B0, |f'| <= B1, |f''| <= B2 and |f'''| <= B3. The normalized pressure p_N(G, f) of PerceptronSignDefinitions.v is (1/N) ln (2^(-N) sum_x exp (E_G(x))), with the energy E_G(x) = sum_mu f ((G x)_mu / sqrt N) (perceptron_pressureE). It is at most M B0 in absolute value (perceptron_pressure_le) and measurable in the entries of G (measurable_perceptron_pressure). As in the manuscript, the entry G_(mu, i) enters only (G x)_mu, with the factor x_i / sqrt N. So the pressure has three derivatives in each entry, and the third is at most (B3 + 6 B1 B2 + 6 B1^3) / (N^2 sqrt N) in absolute value (perceptron_pressure_derive3, from log_partition_derive3 of library/probability/log_partition.v). The coordinate replacement of library/probability/rademacher_lindeberg.v over the M N entries then gives perceptron_sign_compare: g |-> p_N(vec_mx g, f) is integrable against gauss (M * N), and
|E_sign p_N - E_Gauss p_N| <= (B3 + 6 B1 B2 + 6 B1^3) / 2 M N^(-3/2).
The average over the sign patterns indexed by 'I_M * 'I_N is the average over the rows of signs indexed by 'I_(M * N) (sign_pressureE).
The manuscript takes f in C_c^infinity and states the error O_f(N^(-1/2)) when M is of order N. Here the constant is explicit, depends only on B1, B2 and B3, and holds for every M.
pressure_ | sum_mu f ((G x)_mu / sqrt N), the energy of the spins x for the patterns G |
Main results
| Results | Statement |
|---|---|
For N >= 1 and f with three derivatives such that |f| <= B0, |f'| <= B1, |f''| <= B2 and |f'''| <= B3: the pressure p_N(G, f) is at most M B0 in absolute value and measurable in the entries of G; along each entry of G it has three derivatives, the third at most (B3 + 6 B1 B2 + 6 B1^3) / (N^2 sqrt N) in absolute value (from log_partition_derive3); and g |-> p_N(vec_mx g, f) is integrable against gauss (M * N) with |E_sign p_N - E_Gauss p_N| <= (B3 + 6 B1 B2 + 6 B1^3) / 2 M N^(-3/2) (from rademacher_gauss_lindeberg over the M N entries). |
Declarations7 exported
Context {R : realType}. Variables (M N : nat) (f f1 f2 f3 : R -> R) (B0 B1 B2 B3 : R). Hypothesis N0 : (0 < N)%N. Hypothesis df : forall x : R, is_derive x 1 f (f1 x). Hypothesis df1 : forall x : R, is_derive x 1 f1 (f2 x). Hypothesis df2 : forall x : R, is_derive x 1 f2 (f3 x). Hypothesis fB0 : forall x, `|f x| <= B0. Hypothesis fB1 : forall x, `|f1 x| <= B1. Hypothesis fB2 : forall x, `|f2 x| <= B2. Hypothesis fB3 : forall x, `|f3 x| <= B3. Local Notation sN := (Num.sqrt N%:R : R).
forall {R : realType} [M N : nat], (R -> R) -> 'M_(M, N) -> {ffun 'I_N -> bool} -> R
Definition pressure_energy (G : 'M[R]_(M, N)) (x : {ffun 'I_N -> bool}) := \sum_(mu < M) f ((G *m spin_col R x) mu 0 / sN).
The energy of the spins x for the patterns G.
Used by 3 declarations in 1 file
forall {R : realType} [M N : nat] (f : R -> R) (G : 'M_(M, N)), perceptron_pressure f G = N%:R^-1 * ln (\sum_x 2 ^- N * expR (pressure_energy f G x))
Statement as written in the source
Lemma perceptron_pressureE (G : 'M[R]_(M, N)) : perceptron_pressure f G = N%:R^-1 * ln (\sum_x (2 ^+ N)^-1 * expR (pressure_energy G x)).
Used by 2 declarations in 1 file
- this file: perceptron_pressure_le, perceptron_pressure_derive3
forall {R : realType} [M N : nat] [f : R -> R] [B0 : R], (0 < N)%N -> (forall x : R, `|f x| <= B0) -> forall G : 'M_(M, N), `|perceptron_pressure f G| <= M%:R * B0
For N >= 1 and f with three derivatives such that |f| <= B0, |f'| <= B1, |f''| <= B2 and |f'''| <= B3: the pressure p_N(G, f) is at most M B0 in absolute value and measurable in the entries of G; along each entry of G it has three derivatives, the third at most (B3 + 6 B1 B2 + 6 B1^3) / (N^2 sqrt N) in absolute value (from log_partition_derive3); and g |-> p_N(vec_mx g, f) is integrable against gauss (M * N) with |E_sign p_N - E_Gauss p_N| <= (B3 + 6 B1 B2 + 6 B1^3) / 2 M N^(-3/2) (from rademacher_gauss_lindeberg over the M N entries).
Statement as written in the source
Lemma perceptron_pressure_le (G : 'M[R]_(M, N)) : `|perceptron_pressure f G| <= M%:R * B0.
Used by 1 declaration in 1 file
- this file: perceptron_sign_compare
forall {R : realType} [M N : nat] [f f1 : R -> R], (forall x : R, is_derive x 1 f (f1 x)) -> measurable_fun [set: 'rV_(M * N)] (fun g : 'rV_(M * N) => perceptron_pressure f (vec_mx g))
Stated in the README together with perceptron_pressure_le.
Statement as written in the source
Lemma measurable_perceptron_pressure : measurable_fun [set: 'rV[R]_(M * N)] (fun g => perceptron_pressure f (vec_mx g)).
Used by 1 declaration in 1 file
- this file: perceptron_sign_compare
forall {R : realType} [M N : nat] [f f1 f2 f3 : R -> R] [B1 B2 B3 : R], (0 < N)%N -> (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)) -> (forall x : R, `|f1 x| <= B1) -> (forall x : R, `|f2 x| <= B2) -> (forall x : R, `|f3 x| <= B3) -> forall (j : 'I_(M * N)) (g : 'rV_(M * N)), exists F1 F2 F3 : R -> R, [/\ forall t : R, is_derive t 1 (fun t0 : R => perceptron_pressure f (vec_mx (t0 *: delta_mx 0 j + g))) (F1 t), forall t : R, is_derive t 1 F1 (F2 t), forall t : R, is_derive t 1 F2 (F3 t) & forall t : R, `|F3 t| <= (B3 + 6 * B1 * B2 + 6 * B1 ^+ 3) / (N%:R ^+ 2 * (Num.ExtraDef.sqrtr N%:R : R))]
The pressure along one pattern entry has three derivatives, the third at most (B3 + 6 B1 B2 + 6 B1^3) / (N^2 sqrt N) in absolute value.
Stated in the README together with perceptron_pressure_le.
Statement as written in the source
Lemma perceptron_pressure_derive3 (j : 'I_(M * N)) (g : 'rV[R]_(M * N)) : exists F1 F2 F3 : R -> R, [/\ forall t : R, is_derive t 1 (fun t => perceptron_pressure f (vec_mx (t *: delta_mx 0 j + g))) (F1 t), forall t : R, is_derive t 1 F1 (F2 t), forall t : R, is_derive t 1 F2 (F3 t) & forall t, `|F3 t| <= (B3 + 6 * B1 * B2 + 6 * B1 ^+ 3) / (N%:R ^+ 2 * sN)].
Used by 1 declaration in 1 file
- this file: perceptron_sign_compare
forall {R : realType} (M N : nat) (f : R -> R), sign_pressure M N f = 2 ^- (M * N) * \sum_s perceptron_pressure f (vec_mx (sign_row s))
The average over the sign patterns, indexed as rows of 'I_(M * N).
Stated in the README together with perceptron_pressure_le.
Statement as written in the source
Lemma sign_pressureE : sign_pressure M N f = (2 ^+ (M * N))^-1 * \sum_(s : {ffun 'I_(M * N) -> bool}) perceptron_pressure f (vec_mx (sign_row s)).
Used by 1 declaration in 1 file
- this file: perceptron_sign_compare
forall {R : realType} (M : nat) [N : nat] [f f1 f2 f3 : R -> R] [B0 B1 B2 B3 : R], (0 < N)%N -> (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)) -> (forall x : R, `|f x| <= B0) -> (forall x : R, `|f1 x| <= B1) -> (forall x : R, `|f2 x| <= B2) -> (forall x : R, `|f3 x| <= B3) -> (gauss (M * N)).-integrable [set: 'rV_(M * N)] (EFin \o (fun g : 'rV_(M * N) => perceptron_pressure f (vec_mx g))) /\ `|sign_pressure M N f - gauss_pressure M N f| <= (B3 + 6 * B1 * B2 + 6 * B1 ^+ 3) / 2 * M%:R * N%:R `^ (- (3 / 2))
Stated in the README together with perceptron_pressure_le.
Statement as written in the source
Theorem perceptron_sign_compare : (gauss (M * N)).-integrable setT (EFin \o (fun g : 'rV[R]_(M * N) => perceptron_pressure f (vec_mx g))) /\ `|sign_pressure M N f - gauss_pressure M N f| <= (B3 + 6 * B1 * B2 + 6 * B1 ^+ 3) / 2 * M%:R * N%:R `^ (- (3 / 2)).
Used by 1 declaration in 1 file
- GaussianApplications.PerceptronSignTheorem: perceptron_sign_theorem