(V : F →L[ℂ] E) (X : E →L[ℂ] E) (hVV : V.adjoint.comp V = ContinuousLinearMap.id ℂ F) (hinv : ∀ x : F, ∃ y : F, X (V x) = V y) (n : ℕ) (v : E) (hv : V (V.adjoint v) = v) : (X ^ n)...

-- Generated from ChapterH4.lean — theorem BookProof.ChapterH4.compress_transfer
import Mathlib
import Definitions.Def_ChapterH4
open BookProof.ChapterH4









open scoped BigOperators


noncomputable section





variable {E F : Type*}
  [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]
  [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]

theorem BookProof.ChapterH4.compress_transfer (V : F →L[ℂ] E) (X : E →L[ℂ] E)
    (hVV : V.adjoint.comp V = ContinuousLinearMap.id ℂ F)
    (hinv : ∀ x : F, ∃ y : F, X (V x) = V y) (n : ℕ)
    (v : E) (hv : V (V.adjoint v) = v) :
    (X ^ n) v = V ((compress V X ^ n) (V.adjoint v)) := by sorry