embedState_injective

formal source

 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
 591  | 0 => by norm_num
 592  | d + 1 =>
 593      let m := 4 ^ d
 594      have hm : d ≤ m := self_le_four_pow_self d
 595      have hm_pos : 1 ≤ m := by
 596        dsimp [m]
 597        exact Nat.succ_le_of_lt (pow_pos (by norm_num) _)
 598      have hstep : d + 1 ≤ m + m := by