def definition def or abbrev

`prob`

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

formal statement (Lean)

  25noncomputable def prob₁ (m : TwoOutcomeMeasurement) : ℝ :=

proof body

Definition body.

  26  Real.exp (-m.C₁) / (Real.exp (-m.C₁) + Real.exp (-m.C₂))
  27
  28/-- Probability of outcome 2 -/
  29noncomputable def prob₂ (m : TwoOutcomeMeasurement) : ℝ :=
  30  Real.exp (-m.C₂) / (Real.exp (-m.C₁) + Real.exp (-m.C₂))
  31
  32/-- Probabilities are non-negative -/