Require Import VectorStates.

Definition probability_of_outcome {n} (ϕ ψ : Vector n) : R :=
  Cmod (inner_product ϕ ψ) ^2.

Definition prob_partial_meas {m n} (ϕ : Vector (2^m)) (ψ : Vector (2^(m + n))) :=
  big_sum (fun y ⇒ probability_of_outcome (ϕ ⊗ basis_vector (2^n) y) ψ) (2^n).

Lemma probability_of_outcome_comm : ∀ {d} (ϕ ψ : Vector d),
  probability_of_outcome ϕ ψ = probability_of_outcome ψ ϕ.

Lemma probability_of_outcome_is_norm : ∀ {d} (ϕ ψ : Vector d),
  probability_of_outcome ϕ ψ = ((norm (ϕ† × ψ)) ^ 2)%R.

Lemma rewrite_I_as_sum : ∀ m n,
  (m ≤ n)%nat →
  I m = big_sum (fun i ⇒ (basis_vector n i) × (basis_vector n i)†) m.

Lemma prob_partial_meas_alt :
  ∀ {m n} (ϕ : Vector (2^m)) (ψ : Vector (2^(m + n))),
  @prob_partial_meas m n ϕ ψ = ((norm ((ϕ ⊗ I (2 ^ n))† × ψ)) ^ 2)%R.

Lemma partial_meas_tensor :
  ∀ {m n} (ϕ : Vector (2^m)) (ψ1 : Vector (2^m)) (ψ2 : Vector (2^n)),
  Pure_State_Vector ψ2 →
  @prob_partial_meas m n ϕ (ψ1 ⊗ ψ2) = probability_of_outcome ϕ ψ1.