OAI/Computability/QuantumFactoring/ProductStates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.productState line 19

   Source documentation

   Independent, not necessarily identically distributed, retained registers.

   noncomputable def productState {ι : Type*} [Fintype ι] {α : ι → Type*}
       (ψ : ∀ i, α i → ℂ) (x : ∀ i, α i) : ℂ := ∏ i, ψ i (x i)

2. lemma OAI.ExactQuantumFactoring.productState_normalized line 22
3. lemma OAI.ExactQuantumFactoring.productState_all_mass line 30
4. lemma OAI.ExactQuantumFactoring.productState_constant_mass line 46