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

ObservableRatioModel

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)

  29structure ObservableRatioModel (α : Type) where
  30  ratio : α → ℝ
  31  ratio_pos : ∀ s, 0 < ratio s
  32  log_charge : α → ℝ
  33  log_charge_eq : ∀ s, log_charge s = Real.log (ratio s)
  34
  35/-- A sector label is a free parameter if it can take any real value. -/

used by (4)

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

depends on (9)

Lean names referenced from this declaration's body.