projectState_embedState

formal source

 557    rfl
 558
 559/-- Projection recovers the original state after zero-padding. -/
 560theorem projectState_embedState {d N : ℕ} (h : d ≤ Fintype.card (CoupledCoreIndex N))
 561    (v : Fin d → ℂ) :
 562    projectState h (embedState h v) = v := by
 563  ext i
 564  unfold projectState embedState
 565  simp [coupledCoreEquivFin]
 566
 567/-- Zero-padding is injective. -/
 568theorem embedState_injective {d N : ℕ} (h : d ≤ Fintype.card (CoupledCoreIndex N)) :
 569    Function.Injective (embedState h) := by
 570  intro v w hEq
 571  have hproj := congrArg (projectState h) hEq
 572  simpa [projectState_embedState] using hproj
 573
 574/-- Lift a finite-dimensional linear operator to the coupled-core carrier by
 575zero-padding, acting, and projecting back. -/
 576def liftOperator {d N : ℕ} (h : d ≤ Fintype.card (CoupledCoreIndex N))
 577    (T : (Fin d → ℂ) →ₗ[ℂ] (Fin d → ℂ)) :
 578    CoupledCoreSpace N →ₗ[ℂ] CoupledCoreSpace N :=
 579  (embedState h).comp (T.comp (projectState h))
 580
 581/-- The lifted operator acts exactly like the original operator on the embedded
 582subspace. -/
 583theorem liftOperator_intertwines {d N : ℕ} (h : d ≤ Fintype.card (CoupledCoreIndex N))
 584    (T : (Fin d → ℂ) →ₗ[ℂ] (Fin d → ℂ)) (v : Fin d → ℂ) :
 585    liftOperator h T (embedState h v) = embedState h (T v) := by
 586  unfold liftOperator
 587  simp [projectState_embedState]
 588
 589/-- The obvious capacity bound: `d ≤ 4^d`. -/
 590theorem self_le_four_pow_self : ∀ d : ℕ, d ≤ 4 ^ d