pith. machine review for the scientific record. sign in
theorem proved tactic proof

filter_map_weight_sum

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)

 129theorem filter_map_weight_sum : ∀ {n : ℕ} (ψ : QuantumState n),
 130    (((Finset.univ.filter (fun i => ψ.amplitudes i ≠ 0)).toList.map
 131      (fun i => (⟨i, ψ.amplitudes i, ‖ψ.amplitudes i‖^2, rfl⟩ : LedgerBranch n))).map
 132    LedgerBranch.weight).sum = 1 := by

proof body

Tactic-mode proof.

 133  intro n ψ
 134  rw [List.map_map]
 135  have hcomp : (LedgerBranch.weight ∘ fun i => (⟨i, ψ.amplitudes i, ‖ψ.amplitudes i‖^2, rfl⟩ : LedgerBranch n))
 136             = (fun i => ‖ψ.amplitudes i‖^2) := by ext i; rfl
 137  rw [hcomp, list_map_sum_eq_finset_sum, sum_filter_eq_sum_all]
 138  exact ψ.normalized
 139
 140/-- Convert a quantum state to an uncommitted ledger. -/

used by (1)

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

depends on (11)

Lean names referenced from this declaration's body.