BornRule

formal source

 153    P[γ] = W[γ] / Σ_γ' W[γ']
 154
 155    This is not postulated—it emerges from the cost structure. -/
 156structure BornRule where
 157  /-- The paths being considered -/
 158  paths : List (List Config)
 159  /-- Non-empty path set -/
 160  nonempty : paths ≠ []
 161  /-- Total weight (partition function) -/
 162  Z : ℝ := paths.foldl (fun acc γ => acc + PathWeight γ) 0
 163  /-- Probability of a path -/
 164  prob (γ : List Config) : ℝ := if γ ∈ paths then PathWeight γ / Z else 0
 165
 166/-- Sum of (f x / c) over a list equals (sum of f x) / c. -/
 167lemma List.sum_map_div' {α : Type*} (l : List α) (f : α → ℝ) (c : ℝ) (hc : c ≠ 0) :
 168    (l.map (fun x => f x / c)).sum = (l.map f).sum / c := by
 169  induction l with
 170  | nil => simp
 171  | cons head tail ih =>
 172    simp only [List.map_cons, List.sum_cons, ih]
 173    field_simp
 174
 175/-- Helper: foldl addition equals List.sum for a mapped list -/
 176lemma foldl_add_eq_sum {α : Type*} (l : List α) (f : α → ℝ) :
 177    l.foldl (fun acc x => acc + f x) 0 = (l.map f).sum := by
 178  have h_gen : ∀ (init : ℝ), l.foldl (fun acc x => acc + f x) init = init + (l.map f).sum := by
 179    induction l with
 180    | nil => intro init; simp
 181    | cons head tail ih =>
 182      intro init
 183      simp only [List.foldl_cons, List.map_cons, List.sum_cons]
 184      rw [ih (init + f head)]
 185      ring
 186  simpa using h_gen 0