On this page

GaussianAnalysisprobabilitylog_partition

Derivatives of a log-partition function

GaussianAnalysis.probability.log_partitionlibrary/probability/log_partition.v215 lines8 lemmas and theorems, 1 definitionsource

Imports 0 library modules and 18 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.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, mathcomp.analysis.derive, mathcomp.analysis.realfun, mathcomp.analysis.exp, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic

Imported by 1

GaussianApplications.Perceptron.Pressure

For a nonempty finite type X, weights w x > 0 and functions h x of a real parameter t, the log-partition function t |-> ln (\sum_x w x exp (h x t)) has derivative the Gibbs mean of h' (is_derive_log_partition), and the derivative of the Gibbs mean of q is the mean of h' q + q' minus the product of the means of q and h' (is_derive_gibbs_mean). So, if the h x have three derivatives with |h'| <= b1, |h''| <= b2 and |h'''| <= b3, the log-partition function has three derivatives, and the third one is at most b3 + 6 b1 b2 + 6 b1^3 in absolute value (log_partition_derive3).

Part of target T6 of phase 12: 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 manuscript bounds this third derivative by bounded Gibbs moments and cumulants of f', f'' and f'''. Here the third derivative is m3 - 3 m1 m2 + 2 m1^3 for the Gibbs means m1, m2 and m3 of h', h'^2 + h'' and h'^3 + 3 h' h'' + h''', and each term is bounded separately: no cancellation is used.

gibbs_mean w H q the mean of q under the probability on X with weights proportional to w x exp (H x)

Main results

Results	Statement
gibbs_meangibbs_mean_leis_derive_gibbs_meanis_derive_log_partitionlog_partition_derive3	For a nonempty finite type `X`, weights `w x > 0` and functions `h x` of a real parameter `t`: the derivative of the log-partition function `ln (sum_x w x exp (h x t))` is the Gibbs mean of `h'`, and the derivative of the Gibbs mean of `q` is the mean of `h' q + q'` minus the product of the means of `q` and `h'`. So if the `h x` have three derivatives with `\|h'\| <= b1`, `\|h''\| <= b2` and `\|h'''\| <= b3`, the log-partition function has three derivatives and the third is at most `b3 + 6 b1 b2 + 6 b1^3` in absolute value. A Gibbs mean of `q` is at most the bound of `q` in absolute value (`gibbs_mean_le`).

Declarations9 exported

sectionis_derive_fsum

Context {R : realType} {X : finType}.

lemma is_derive_fsum source, line 49

forall {R : realType} {X : finType} [F F' : X -> R -> R] [t : R],
(forall x : X, is_derive t 1 (F x) (F' x t)) ->
is_derive t 1
  (fun t0 : R =>
   \sum_x F x t0)
  (\sum_x F' x t)

The derivative of a finite sum of functions.

Statement as written in the source

Lemma is_derive_fsum (F F' : X -> R -> R) (t : R) :
  (forall x, is_derive t 1 (F x) (F' x t)) ->
  is_derive t 1 (fun t => \sum_x F x t) (\sum_x F' x t).

Used by 3 declarations in 2 files

this file: is_derive_gibbs_sum, is_derive_gibbs_mass
GaussianApplications.Perceptron.Pressure: perceptron_pressure_derive3

sectiongibbs_mean

Context {R : realType} {X : finType}.

definition gibbs_mean main result source, line 70

Type

forall {R : realType} {X : finType}, (X -> R) -> (X -> R) -> (X -> R) -> R

Definition

Definition gibbs_mean (w H q : X -> R) : R :=
  (\sum_x w x * expR (H x) * q x) / \sum_x w x * expR (H x).

The mean of q under the probability on X with weights w x exp (H x).

Main result, as the README states it

For a nonempty finite type X, weights w x > 0 and functions h x of a real parameter t: the derivative of the log-partition function ln (sum_x w x exp (h x t)) is the Gibbs mean of h', and the derivative of the Gibbs mean of q is the mean of h' q + q' minus the product of the means of q and h'. So if the h x have three derivatives with |h'| <= b1, |h''| <= b2 and |h'''| <= b3, the log-partition function has three derivatives and the third is at most b3 + 6 b1 b2 + 6 b1^3 in absolute value. A Gibbs mean of q is at most the bound of q in absolute value (gibbs_mean_le).

Used by 4 declarations in 1 file

this file: gibbs_mean_le, is_derive_gibbs_mean, is_derive_log_partition, log_partition_derive3

lemma gibbs_mass_gt0 source, line 73

forall {R : realType} {X : finType} [w : X -> R] (H : X -> R),
(forall x : X, 0 < w x) -> (0 < #|X|)%N -> 0 < \sum_x w x * expR (H x)

Statement as written in the source

Lemma gibbs_mass_gt0 (w H : X -> R) : (forall x, 0 < w x) ->
  (0 < #|X|)%N -> 0 < \sum_x w x * expR (H x).

Used by 3 declarations in 1 file

this file: gibbs_mean_le, is_derive_gibbs_mean, is_derive_log_partition

lemma gibbs_mean_le main result source, line 84

forall {R : realType} {X : finType} [w : X -> R] (H : X -> R) [q : X -> R] [b : R],
(forall x : X, 0 < w x) ->
(0 < #|X|)%N -> (forall x : X, `|q x| <= b) -> `|gibbs_mean w H q| <= b

Main result

Stated in the README together with gibbs_mean.

Statement as written in the source

Lemma gibbs_mean_le (w H q : X -> R) (b : R) : (forall x, 0 < w x) ->
  (0 < #|X|)%N -> (forall x, `|q x| <= b) -> `|gibbs_mean w H q| <= b.

Used by 1 declaration in 1 file

this file: log_partition_derive3

sectionlog_partition

Context {R : realType} {X : finType}.
Variables (w : X -> R) (h h1 : X -> R -> R).
Hypothesis w0 : forall x, 0 < w x.
Hypothesis X0 : (0 < #|X|)%N.
Hypothesis dh : forall x (t : R), is_derive t 1 (h x) (h1 x t).
Local Notation mean q t := (gibbs_mean w (h^~ t) (q^~ t)).

lemma is_derive_gibbs_sum source, line 106

forall {R : realType} {X : finType} (w : X -> R) [h h1 : X -> R -> R],
(forall (x : X) (t : R), is_derive t 1 (h x) (h1 x t)) ->
forall [q q' : X -> R -> R] [t : R],
(forall x : X, is_derive t 1 (q x) (q' x t)) ->
is_derive t 1
  (fun t0 : R =>
   \sum_x w x * expR (h x t0) * q x t0)
  (\sum_x w x * expR (h x t) * (h1 x t * q x t + q' x t))

Statement as written in the source

Lemma is_derive_gibbs_sum (q q' : X -> R -> R) (t : R) :
  (forall x, is_derive t 1 (q x) (q' x t)) ->
  is_derive t 1 (fun t => \sum_x w x * expR (h x t) * q x t)
    (\sum_x w x * expR (h x t) * (h1 x t * q x t + q' x t)).

Used by 1 declaration in 1 file

this file: is_derive_gibbs_mean

lemma is_derive_gibbs_mass source, line 120

forall {R : realType} {X : finType} (w : X -> R) [h h1 : X -> R -> R],
(forall (x : X) (t : R), is_derive t 1 (h x) (h1 x t)) ->
forall t : R,
is_derive t 1
  (fun t0 : R =>
   \sum_x w x * expR (h x t0))
  (\sum_x w x * expR (h x t) * h1 x t)

Statement as written in the source

Lemma is_derive_gibbs_mass (t : R) :
  is_derive t 1 (fun t => \sum_x w x * expR (h x t))
    (\sum_x w x * expR (h x t) * h1 x t).

Used by 2 declarations in 1 file

this file: is_derive_gibbs_mean, is_derive_log_partition

lemma is_derive_gibbs_mean main result source, line 132

forall {R : realType} {X : finType} [w : X -> R] [h h1 : X -> R -> R],
(forall x : X, 0 < w x) ->
(0 < #|X|)%N ->
(forall (x : X) (t : R), is_derive t 1 (h x) (h1 x t)) ->
forall [q q' : X -> R -> R] [t : R],
(forall x : X, is_derive t 1 (q x) (q' x t)) ->
is_derive t 1
  (fun t0 : R =>
   gibbs_mean w (h^~ t0) (q^~ t0))
  (gibbs_mean w (h^~ t) ((fun (x0 : X) (t0 : R) => h1 x0 t0 * q x0 t0 + q' x0 t0)^~ t) -
   gibbs_mean w (h^~ t) (q^~ t) * gibbs_mean w (h^~ t) (h1^~ t))

The derivative of a Gibbs mean: mean (h1 q + q') - mean q * mean h1.

Main result

Stated in the README together with gibbs_mean.

Statement as written in the source

Lemma is_derive_gibbs_mean (q q' : X -> R -> R) (t : R) :
  (forall x, is_derive t 1 (q x) (q' x t)) ->
  is_derive t 1 (fun t => mean q t)
    (mean (fun x t => h1 x t * q x t + q' x t) t - mean q t * mean h1 t).

Used by 1 declaration in 1 file

this file: log_partition_derive3

lemma is_derive_log_partition main result source, line 146

forall {R : realType} {X : finType} [w : X -> R] [h h1 : X -> R -> R],
(forall x : X, 0 < w x) ->
(0 < #|X|)%N ->
(forall (x : X) (t : R), is_derive t 1 (h x) (h1 x t)) ->
forall t : R,
is_derive t 1
  (fun t0 : R =>
   ln (\sum_x w x * expR (h x t0)))
  (gibbs_mean w (h^~ t) (h1^~ t))

The derivative of the log-partition function is the mean of h1.

Main result

Stated in the README together with gibbs_mean.

Statement as written in the source

Lemma is_derive_log_partition (t : R) :
  is_derive t 1 (fun t => ln (\sum_x w x * expR (h x t))) (mean h1 t).

Used by 1 declaration in 1 file

this file: log_partition_derive3

theorem log_partition_derive3 main result source, line 157

forall {R : realType} {X : finType} [w : X -> R] [h h1 : X -> R -> R],
(forall x : X, 0 < w x) ->
(0 < #|X|)%N ->
(forall (x : X) (t : R), is_derive t 1 (h x) (h1 x t)) ->
forall [h2 h3 : X -> R -> R],
(forall (x : X) (t : R), is_derive t 1 (h1 x) (h2 x t)) ->
(forall (x : X) (t : R), is_derive t 1 (h2 x) (h3 x t)) ->
exists L1 L2 L3 : R -> R,
  [/\ forall t : R,
      is_derive t 1
        (fun t0 : R =>
         ln (\sum_x w x * expR (h x t0)))
        (L1 t),
      forall t : R, is_derive t 1 L1 (L2 t), forall t : R, is_derive t 1 L2 (L3 t)
    & forall t b1 b2 b3 : R,
      (forall x : X, `|h1 x t| <= b1) ->
      (forall x : X, `|h2 x t| <= b2) ->
      (forall x : X, `|h3 x t| <= b3) -> `|L3 t| <= b3 + 6 * b1 * b2 + 6 * b1 ^+ 3]

Three derivatives of the log-partition function, the third bounded by b3 + 6 b1 b2 + 6 b1^3 when |h1| <= b1, |h2| <= b2 and |h3| <= b3.

Main result

Stated in the README together with gibbs_mean.

Statement as written in the source

Theorem log_partition_derive3 (h2 h3 : X -> R -> R) :
  (forall x (t : R), is_derive t 1 (h1 x) (h2 x t)) ->
  (forall x (t : R), is_derive t 1 (h2 x) (h3 x t)) ->
  exists L1 L2 L3 : R -> R,
  [/\ forall t : R,
        is_derive t 1 (fun t => ln (\sum_x w x * expR (h x t))) (L1 t),
      forall t : R, is_derive t 1 L1 (L2 t),
      forall t : R, is_derive t 1 L2 (L3 t) &
      forall t b1 b2 b3 : R, (forall x, `|h1 x t| <= b1) ->
        (forall x, `|h2 x t| <= b2) -> (forall x, `|h3 x t| <= b3) ->
        `|L3 t| <= b3 + 6 * b1 * b2 + 6 * b1 ^+ 3].

Used by 1 declaration in 1 file

GaussianApplications.Perceptron.Pressure: perceptron_pressure_derive3

Generated from commit 9046883 (tag phase12) of the ellipsoid fitting repository. Signatures are printed by Rocq 9.1.1; links in the source statements come from the compiled .glob files. The source links open the files on GitHub at this commit, in the now-public repository.