`projectState`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.CoupledRecognitionCores
domain: Foundation
line: 547 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.CoupledRecognitionCores on GitHub at line 547.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 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. -/
 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 → ℂ)) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.