(a : A) (N h : ℂ) (j m : ℂ) (Xj Xm : A) (hjl : (algebraMap ℂ A (N - h * j) - a) * Xj = 1) (hjr : Xj * (algebraMap ℂ A (N - h * j) - a) = 1) (hml : (algebraMap ℂ A (N - h * m) - a) * Xm...
ProvedBookProof.ChapterH1.resolvent_shift_reprtimepiece
Lean 4 theorem BookProof.ChapterH1.resolvent_shift_repr (module BookProof.ChapterH1), source chapter BookProof/ChapterChapterH1.lean.
Preamble
-- Generated from ChapterH1.lean — theorem BookProof.ChapterH1.resolvent_shift_repr
import Mathlib
import Definitions.Def_ChapterH1
open BookProof.ChapterH1
open scoped BigOperators
open intervalIntegral
noncomputable section
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
variable {A : Type*} [Ring A] [Algebra ℂ A]Formal statement
theorem BookProof.ChapterH1.resolvent_shift_repr (a : A) (N h : ℂ) (j m : ℂ) (Xj Xm : A)
(hjl : (algebraMap ℂ A (N - h * j) - a) * Xj = 1)
(hjr : Xj * (algebraMap ℂ A (N - h * j) - a) = 1)
(hml : (algebraMap ℂ A (N - h * m) - a) * Xm = 1)
(hmr : Xm * (algebraMap ℂ A (N - h * m) - a) = 1)
[Invertible (1 + (h * (m - j)) • Xm)] :
Xj = ⅟(1 + (h * (m - j)) • Xm) * Xm := by sorrySource