LF2: auxiliary effect constructions

Category: 3-Local (LF2 Effect-algebra helpers).

Shared infrastructure for building concrete (possibly non-projective) effects, used by the Empirical POVM examples (trine, USD, …):

• scaledRankOneEffect — c|φ⟩⟨φ| as an Effect for 0 ≤ c ≤ 1 and unit φ (the c = 1 case is rankOneEffect); PSD via Mathlib's Matrix.PosSemidef.smul, le_one via the convex decomposition (1-c)P + (1-P);
• trace_outer_mul_eq_inner — Tr(|ψ⟩⟨ψ| · M) = ⟨ψ, M ψ⟩, the trace-form / expectation bridge;
• scaledRankOne_quadratic — ⟨ψ, (c|φ⟩⟨φ|) ψ⟩ = c‖⟨ψ,φ⟩‖², the quadratic form (the per-outcome Born weight of a scaled rank-1 effect).

noncomputable def CSD.LF2.scaledRankOneEffect {N : ℕ} (c : ℝ) (hc0 : 0 ≤ c) (hc1 : c ≤ 1) (φ : EuclideanSpace ℂ (Fin N)) (hφ : ‖φ‖ = 1) : Effect N

c|φ⟩⟨φ| as an Effect, for 0 ≤ c ≤ 1 and a unit vector φ. The c = 1 case is rankOneEffect.

Equations

• CSD.LF2.scaledRankOneEffect c hc0 hc1 φ hφ = { M := ↑c • CSD.LF2.outerProduct φ, isHermitian := ⋯, nonneg := ⋯, le_one := ⋯ }

@[simp]

theorem CSD.LF2.scaledRankOneEffect_M {N : ℕ} (c : ℝ) (hc0 : 0 ≤ c) (hc1 : c ≤ 1) (φ : EuclideanSpace ℂ (Fin N)) (hφ : ‖φ‖ = 1) : (scaledRankOneEffect c hc0 hc1 φ hφ).M = ↑c • outerProduct φ

theorem CSD.LF2.trace_outer_mul_eq_inner {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (M : Matrix (Fin N) (Fin N) ℂ) : (outerProduct ψ * M).trace = inner ℂ ψ ((Matrix.toEuclideanLin M) ψ)

Tr(|ψ⟩⟨ψ| · M) = ⟨ψ, M ψ⟩ — the trace-form / expectation bridge (the paper's §5.14 trace-inner core identity; LF3's copy was retired under BACKLOG #146 (D)).

theorem CSD.LF2.scaledRankOne_quadratic {N : ℕ} (c : ℝ) (φ ψ : EuclideanSpace ℂ (Fin N)) (hφ : ‖φ‖ = 1) (hψ : ‖ψ‖ = 1) : RCLike.re (inner ℂ ψ ((Matrix.toEuclideanLin (↑c • outerProduct φ)) ψ)) = c * ‖inner ℂ ψ φ‖ ^ 2

Quadratic form of a scaled rank-1 effect: ⟨ψ, (c|φ⟩⟨φ|) ψ⟩ = c‖⟨ψ,φ⟩‖². The per-outcome Born weight of a scaled rank-1 effect on a unit preparation.