structure
definition
def or abbrev
BornRule
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Definition body.
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 -/