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

RecognitionSystem

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 RecognitionSystem where
  45  TR : ℝ
  46  TR_pos : 0 < TR
  47
  48/-- Thermodynamic beta (inverse temperature) for a recognition system. -/
  49noncomputable def RecognitionSystem.beta (sys : RecognitionSystem) : ℝ := 1 / sys.TR

proof body

Definition body.

  50
  51/-- Beta is positive. -/
  52theorem RecognitionSystem.beta_pos (sys : RecognitionSystem) : 0 < sys.beta := by
  53  unfold RecognitionSystem.beta
  54  exact div_pos one_pos sys.TR_pos
  55
  56/-- Beta * TR = 1. -/
  57theorem RecognitionSystem.beta_mul_TR (sys : RecognitionSystem) : sys.beta * sys.TR = 1 := by
  58  unfold RecognitionSystem.beta
  59  field_simp [sys.TR_pos.ne']
  60
  61/-! ## Gibbs Weights and Partition Functions -/
  62
  63/-- The Gibbs weight (Boltzmann factor) of a state with ratio x.
  64    This is the unnormalized probability: exp(-J(x)/TR). -/

used by (40)

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

… and 10 more

depends on (27)

Lean names referenced from this declaration's body.