Prove2Me

`BookProof.BrstReducedTransfer.infDist_exactStates_stoneU_eq_inc` (t : ℝ) (x : H) : Metric.infDist (T.stoneU t x) (exactStates Om) = Metric.infDist x (exactStates Om)

Proved
BookProof.BrstReducedTransfer.infDist_exactStates_stoneU_eq_inc

by leonardopedro · Oct 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterBrstReducedTransfer.

BookProof.BrstReducedTransfer.infDist_exactStates_stoneU_eq_inc (t : ℝ) (x : H) : Metric.infDist (T.stoneU t x) (exactStates Om) = Metric.infDist x (exactStates Om)

Formalization note: Lean 4 identifier BookProof.BrstReducedTransfer.infDist_exactStates_stoneU_eq_inc.

Replaces the retired node BookProof.BrstReducedTransfer.infDist_exactStates_stoneU_eq, whose stored statement omitted the hcomm hypothesis binder (dropped include).

Preamble
-- Generated from ChapterBrstReducedTransfer.lean — theorem BookProof.BrstReducedTransfer.infDist_exactStates_stoneU_eq_inc
import Definitions.Def_ChapterSirkTrotterKato
import Mathlib
import Definitions.Def_ChapterBrstReducedTransfer
import Definitions.Def_ChapterStoneResolvent
import Definitions.Def_ChapterStoneUnitary
open BookProof.BrstReducedTransfer



open BookProof BookProof.ChapterStoneResolvent




variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
variable (T : UnboundedSelfAdjoint H) (Om : H →L[ℂ] H)
variable (hcomm : ∀ (t : ℝ) (y : H), T.stoneU t (Om y) = Om (T.stoneU t y))

include hcomm in
Formal statement
theorem BookProof.BrstReducedTransfer.infDist_exactStates_stoneU_eq_inc (t : ℝ) (x : H) :
    Metric.infDist (T.stoneU t x) (exactStates Om) = Metric.infDist x (exactStates Om) := by sorry

View graph