(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 : ℕ) : (X ^ n).comp V = V.comp ((compress V X) ^ n)

-- Generated from ChapterH4.lean — theorem BookProof.ChapterH4.compress_pow
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_pow (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 : ℕ) :
    (X ^ n).comp V = V.comp ((compress V X) ^ n) := by sorry