pith. machine review for the scientific record. sign in
structure definition def or abbrev

ProbDist

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)

  44structure ProbDist (ι : Type*) [Fintype ι] where
  45  prob : ι → ℝ
  46  prob_pos : ∀ i, 0 < prob i
  47  prob_sum : ∑ i, prob i = 1
  48
  49theorem ProbDist.prob_nonneg (q : ProbDist ι) (i : ι) : 0 ≤ q.prob i :=

proof body

Definition body.

  50  le_of_lt (q.prob_pos i)
  51
  52/-- The variational free energy F[q ; E, β]. -/

used by (24)

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

depends on (12)

Lean names referenced from this declaration's body.