def
definition
embedState
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.CoupledRecognitionCores on GitHub at line 529.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
back -
coupledCoreEquivFin -
CoupledCoreIndex -
CoupledCoreSpace -
of -
CoupledCoreIndex -
CoupledCoreSpace -
of -
of -
of
used by
formal source
526 Fintype.equivFin (CoupledCoreIndex N)
527
528/-- Zero-pad a finite-dimensional state into a coupled-core carrier. -/
529def embedState {d N : ℕ} (_h : d ≤ Fintype.card (CoupledCoreIndex N)) :
530 (Fin d → ℂ) →ₗ[ℂ] CoupledCoreSpace N where
531 toFun := fun v s =>
532 let i := coupledCoreEquivFin N s
533 if hi : i.val < d then v ⟨i.val, hi⟩ else 0
534 map_add' := by
535 intro v w
536 ext s
537 dsimp [coupledCoreEquivFin]
538 split_ifs <;> simp
539 map_smul' := by
540 intro z v
541 ext s
542 dsimp [coupledCoreEquivFin]
543 split_ifs <;> simp
544
545/-- Restrict a coupled-core state back to the first `d` coordinates of the
546enumerated basis. -/
547def projectState {d N : ℕ} (h : d ≤ Fintype.card (CoupledCoreIndex N)) :
548 CoupledCoreSpace N →ₗ[ℂ] (Fin d → ℂ) where
549 toFun := fun ψ i => ψ ((coupledCoreEquivFin N).symm (Fin.castLE h i))
550 map_add' := by
551 intro ψ χ
552 ext i
553 rfl
554 map_smul' := by
555 intro z ψ
556 ext i
557 rfl
558
559/-- Projection recovers the original state after zero-padding. -/