`BookProof.ChapterG.expectation_gauge_invariant` {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (U : V →L[ℂ] V) (hU : U ∈ unitary (V →L[ℂ] V)) (A : V

Proved

BookProof.ChapterG.expectation_gauge_invariant

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterG.

BookProof.ChapterG.expectation_gauge_invariant {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (U : V →L[ℂ] V) (hU : U ∈ unitary (V →L[ℂ] V)) (A : V →L[ℂ] V) (hA : A * U = U * A) (Ψ : V) : ⟪U Ψ, A (U Ψ)⟫_ℂ = ⟪Ψ, A Ψ⟫_ℂ

Formalization note: Lean 4 identifier BookProof.ChapterG.expectation_gauge_invariant.

Preamble

-- Generated from ChapterG.lean — theorem BookProof.ChapterG.expectation_gauge_invariant
import Mathlib
import Definitions.Def_ChapterG
open BookProof.ChapterG


open scoped ComplexConjugate InnerProductSpace Matrix

Formal statement

theorem BookProof.ChapterG.expectation_gauge_invariant {V : Type*} [NormedAddCommGroup V]
    [InnerProductSpace ℂ V] [CompleteSpace V]
    (U : V →L[ℂ] V) (hU : U ∈ unitary (V →L[ℂ] V))
    (A : V →L[ℂ] V) (hA : A * U = U * A) (Ψ : V) :
    ⟪U Ψ, A (U Ψ)⟫_ℂ = ⟪Ψ, A Ψ⟫_ℂ := by sorry

View graph