The Lean 4 theorem `krylov_rayleigh_transfer` in the `ChapterH6` chapter of the timepiece formalization

-- Generated from ChapterH6.lean — theorem BookProof.ChapterH6.krylov_rayleigh_transfer
import Mathlib
import Definitions.Def_ChapterH6
import Definitions.Def_ChapterH4
open BookProof.ChapterH4
open BookProof.ChapterH6

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


noncomputable section

open Filter Topology

theorem BookProof.ChapterH6.krylov_rayleigh_transfer (V : F →L[ℂ] E) (X : E →L[ℂ] E) (y : F) :
    inner ℂ y (compress V X y) = inner ℂ (V y) (X (V y)) := by sorry