def
definition
prob
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Measurement.BornRule on GitHub at line 25.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
22 C₂_nonneg : 0 ≤ C₂
23
24/-- Probability of outcome 1 -/
25noncomputable def prob₁ (m : TwoOutcomeMeasurement) : ℝ :=
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 -/
33lemma prob₁_nonneg (m : TwoOutcomeMeasurement) : 0 ≤ prob₁ m := by
34 unfold prob₁
35 apply div_nonneg
36 · exact (Real.exp_pos _).le
37 · exact (add_pos (Real.exp_pos _) (Real.exp_pos _)).le
38
39lemma prob₂_nonneg (m : TwoOutcomeMeasurement) : 0 ≤ prob₂ m := by
40 unfold prob₂
41 apply div_nonneg
42 · exact (Real.exp_pos _).le
43 · exact (add_pos (Real.exp_pos _) (Real.exp_pos _)).le
44
45/-- Probabilities sum to 1 (normalization) -/
46theorem probabilities_normalized (m : TwoOutcomeMeasurement) :
47 prob₁ m + prob₂ m = 1 := by
48 unfold prob₁ prob₂
49 have hdenom : Real.exp (-m.C₁) + Real.exp (-m.C₂) ≠ 0 :=
50 (add_pos (Real.exp_pos _) (Real.exp_pos _)).ne'
51 set denom : ℝ := Real.exp (-m.C₁) + Real.exp (-m.C₂)
52 have hadd :
53 Real.exp (-m.C₁) / denom + Real.exp (-m.C₂) / denom = (Real.exp (-m.C₁) + Real.exp (-m.C₂)) / denom := by
54 simpa [denom] using (add_div (Real.exp (-m.C₁)) (Real.exp (-m.C₂)) denom).symm
55 -- Finish.