pith. machine review for the scientific record. sign in
lemma proved term proof

gibbsPD_p

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 116@[simp] lemma gibbsPD_p (sys : RecognitionSystem) (X : Ω → ℝ) :
 117    (gibbsPD sys X).p = gibbs_measure sys X := rfl

proof body

Term-mode proof.

 118
 119/-! ## §2. J-descent operators on probability distributions -/
 120
 121/-- A **J-descent operator** on probability distributions over `Ω` with
 122    equilibrium `peq` is a step `step : Distrib Ω → Distrib Ω` such that
 123
 124    1. `step peq = peq`  (the equilibrium is a fixed point), and
 125    2. for every distribution `q`,
 126       `D_KL(step q ‖ peq) ≤ D_KL(q ‖ peq)`  (KL non-expansiveness).
 127
 128    Inside RS, the recognition operator R̂ projected onto the distribution
 129    layer is a J-descent operator with `peq = gibbsPD sys X`.  More generally,
 130    any deterministic Markov kernel that has `peq` as its stationary distribution
 131    satisfies these properties via the data-processing inequality. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (24)

Lean names referenced from this declaration's body.